RedPRL
An idea for abstract function interfaces
Functions out of inductive types are defined by eliminators, but this has unfortunate effects: if we unfold the function, then we get the whole brutal eliminator expression, and it is not at all easy to put this :genie: back in the bottle. In the past I have considered techniques where we have special forms to declare a top-level function, Agda-style --- local functions are still easily accommodated in that setting --- but I have another idea that might be worth considering.
We could decouple the function's interface from its substantiation. The idea is that the interface of an addition function would be as follows:
interface add : nat -> nat -> nat where
| add ze n ----> n
| add (su m) n ----> su (add m n)
Now, this function does not yet exist! In particular, we cannot call add. It has to be implemented first. We implement it using the eliminator:
implementation add :=
elim [
| zero => n => n
| suc {_ => ih} => n => suc {ih n}
]
The elaborator checks that add satisfies the interface up to judgmental equality. If that succeeds, we now have an new variable add in scope that does not unfold to anything, but the rewrite rules from the interface have been registered to it! First-order unification, with some tweaks to allow systems to bubble out, is enough to implement the evaluator for such functions.
One day one could try adding tactics that find an implementaiton satisfying those equations --- this is essentially what pattern compilation does, and is worked out by McBride and friends (implemented in Lean nowadays too). It's quite tricky though, so it would be nice to have a middle ground for now.
Subtleties
We must restrict attention to linear patterns.
How to deal with an interface like | omega n ------> omega n? I do not like the idea of trying to have some low ch'i termination checker on the interfaces, since the purpose of the implementation is to provide a termination proof!
My simple answer is that it is unnecessary to register the rewrites until after the termination proof is
substantiated. Checking that the rewrites are modeled by the implementation does not require registering them, so omega n ---> omega n does not pose a problem.
Aside:
This approach reminds me of the āmodularā account of datatypes in ML. Lots is different, but there is a similarity in that the interface is clean and usable, but the implementation is god-awful (pattern compiled). The nice thing here is the remark at the end that verifying the implementation ensures termination of the abstract rewriting, and thus certifies it. A similar issueābut with no similar solutionācomes up when considering āsingleton types,ā as well as singleton kinds, to express cross-module inlining. You may specify that x=e, but what if e is not terminating (or, worse, raises an exception, or calls your mother). One idea is the āvalue restrictionā, which amounts to a special technique in Jonās sense, but then you still have the problem that functions are partial, and can unleash effects. I still have the hope that in the grand scheme of things a ārealā PL (with effects) would come equipped with a logic for proving properties of itāthis would be the only way to address the vexed issue of benign effects, it seems to me.
(c) Robert Harper All Rights Reserved.
On Aug 24, 2020, at 20:11, Jonathan Sterling [email protected] wrote:
Functions out of inductive types are defined by eliminators, but this has unfortunate effects: if we unfold the function, then we get the whole brutal eliminator expression, and it is not at all easy to put this š§ back in the bottle. In the past I have considered techniques where we have special forms to declare a top-level function, Agda-style --- local functions are still easily accommodated in that setting --- but I have another idea that might be worth considering.
We could decouple the function's interface from its substantiation. The idea is that the interface of an addition function would be as follows:
interface add : nat -> nat -> nat where | add ze ze ----> ze | add (su m) ze ----> su m | add (su m) (su n) ---> su (add m n) Now, this function does not yet exist! In particular, we cannot call add. It has to be implemented first. We implement it using the eliminator:
implementation add := elim [ | zero => n => n | suc {_ => ih} => n => suc {ih n} ] The elaborator checks that add satisfies the interface up to judgmental equality. If that succeeds, we now have an new variable add in scope that does not unfold to anything, but the rewrite rules from the interface have been registered to it! First-order unification, with some tweaks to allow systems to bubble out, is enough to implement the evaluator for such functions.
One day one could try adding tactics that find an implementaiton satisfying those equations --- this is essentially what pattern compilation does, and is worked out by McBride and friends (implemented in Lean nowadays too). It's quite tricky though, so it would be nice to have a middle ground for now.
Subtleties
We must restrict attention to linear patterns.
How to deal with an interface like | omega n ------> omega n? I do not like the idea of trying to have some low ch'i termination checker on the interfaces, since the purpose of the implementation is to provide a termination proof!
My simple answer is that it is unnecessary to register the rewrites until after the termination proof is substantiated. Checking that the rewrites are modeled by the implementation does not require registering them, so omega n ---> omega n does not pose a problem.
ā You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/RedPRL/cooltt/issues/178, or unsubscribe https://github.com/notifications/unsubscribe-auth/AALWY5OKFILAH7RK6UGK2FTSCL6RTANCNFSM4QKBMEZQ.
@RobertHarper That's a nice connection with the datatype interfaces, indeed!