Implement abstract exports

[Toxaris]

Maybe it would be nice to export some identifiers abstractly, that is, export their name and their type but not their value. Example usage:

module Natural;

Natural : * = Pi A : * . (A -> A) -> A -> A;
zero : Natural = lambda A succ zero . zero;
succ : Natural -> Natural = lambda n A succ zero . succ (n A succ zero);
loop : Natural -> Pi A : * . (A -> A) -> A -> A;
loop n = n;

export abstract Natural;
export abstract zero;
export abstract succ;
export loop;

The goal is that in modules that import the Natural module, the type Natural feels like a primitive type, zero and succ feel like introduction forms, and loop feels like an elimination form.

[Blaisorblade]

I'm not sure this example makes sense as-is. If you make only Natural abstract, things would work much better.

On the one hand, this seems (intentionally) similar to the Agda feature:

Maybe it would be nice to export some identifiers abstractly, that is, export their name and their type but not their value.

OTOH, you write that loop should be like an elimination form:

The goal is that in modules that import the Natural module, the type Natural feels like a primitive type, zero and succ feel like introduction forms, and loop feels like an elimination form.

For me, that requires sth. like loop zero f = lambda x . x and loop (succ n) f = f . loop n f. For a real elimination form they should hold definitionally outside the module.

But AFAIK in Agda, for abstract identifiers you essentially export a postulate which will never reduce outside of the module. Dan Licata writes that for abstract identifiers you know nothing outside of the signature, which is IMHO equivalent:

https://lists.chalmers.se/pipermail/agda/2012/004690.html

So, if you want to make zero and succ abstract, I think you need to define and export lemmas which state the equations I wrote as propositional equalities (however encoded, e.g. Leibniz): you'll only manage to define those lemmas while knowing zero and succ bodies. Then, the client would need to use those lemmas to rewrite any application of loop. In the above thread, they show a similar (but much simpler) example — where the lemma is just see-through:

   abstract

     T : Set -> Set
     T A = A

     see-through : ∀ {A} → T A ≡ A
     see-through = refl

   opaque : ∀ {A} → T A ≡ A
   opaque = see-through

[Blaisorblade]

@Toxaris later explained (verbally) that the idea is that identifiers from the same module can "reduce together" — or something like that. So, above, loop could see through the bodies of zero and succ.

What @Toxaris said made sense, but I forgot how it was going to be specified technically. In the above example, loop disappears right away if the semantics is specified using beta-reduction... it seems that looking up abstract ident. b from module A should behave differently depending on where we look it up – more specifically, we need to make the lookup depend on the dynamic context, in particular on the "currently executing procedure".

[Toxaris]

I don't know a technical specification, either. I was also thinking about keeping track of the "currently executing procedure" somehow. This needs more thinking, or maybe just doesn't make sense.

[Blaisorblade]

There's related work involving McBride — I keep posting it wherever it's relevant, so why not here as well? http://dl.acm.org/citation.cfm?id=2502411