General Recursion

[onepunchtech]

What would it look like to add on general recursion? What would typing letrec look like (I'm assuming it would be letrec)? Are there specific designs you already had in mind?

Adding general recursion was mentioned as a possible future update here https://github.com/AndrasKovacs/elaboration-zoo/issues/7#issuecomment-546970285

[atennapel]

Here is a gist from Andras: https://gist.github.com/AndrasKovacs/6b1270d9edb702641f42fd6440f0f750 I think this typing rule should work:

Ctx, rec : (a : A) -> B[a], a : A |- t : B[a]
----------------------------
Ctx |- fix rec a. t : (a : A) -> B[a]

I think you can then implement letrec as sugar over let and fix, but you'll have to figure out a way to make the type annotation in there.

letrec rec a = t1; t2 ~ let rec = (fix rec a. t1); t2

---

If you want to have datatypes with induction then a pretty minimal setup is (I'm assuming consistency is not important):

• Add unit and boolean types
• Add sigma types
• Add a fixpoint type, such as:

  Fix : (U -> U) -> U
  con : {F : U -> U} -> F (Fix F) -> Fix F
  elimFix : {F : U -> U} (P : Fix F -> U) (alg : (rec : (z : Fix F) -> P z) (y : F (Fix F)) -> P (con {F} y)) (x : Fix F) -> P x

  with computation rule:

  elimFix {F} P alg (Con {F} x) ~> alg (\z. elimFix {F} P alg z) x

If you want indexed datatypes you have to add a native identity type and "upgrade" the fixpoint to:

Fix : {I : U} -> ((I -> U) -> I -> U) -> I -> U

You can even get indexed inductive-recursive types, with the following fixpoint:

Fix : {I : U} {R : I -> U}
  (F : (S : I -> U) -> ({i : I} -> S i -> R i) -> I -> U) -> ({S : I -> U} -> (T : {i : I} -> S i -> R i) -> {-i : I} -> F S T i -> R i) ->
  I -> U

If you want efficiency and/or consistency, things become more complicated...

[onepunchtech]

Can you explain what the B[a] notation means?

[atennapel]

It's a type where the a variable may appear. I probably should've just written only B.

[atennapel]

Another way is to add fix with typing rule:

A : Type
B : A -> Type
f : (x : A) -> Either A (B x)
x : A
--------------------------------------------------------
fix {A} {B} f x : B x

With computation rule:

fix f x ~> either (\a. fix f a) (\b. b) (f x)

For some Either type, for example if you have sigma and booleans:

Either : Type -> Type -> Type = \A B. (tag : Bool) ** if tag then A else B
Left : {A B} -> A -> Either A B = \x. (True, x)
Right : {A B} -> B -> Either A B = \x. (False, x)
either : {A B R} -> (A -> R) -> (B -> R) -> Either A B -> R = \f g x. elimBool (\tag. (if tag then A else B) -> R) f g (fst x) (snd x)