Polymorphic recursion in inductive type

Stream: new members

[Anton Lorenzen]

I want to represent de brujin indices as in slides 24-25 of https://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less
and https://www.researchgate.net/profile/Ross_Paterson4/publication/2612840_De_Bruijn_notation_as_a_nested_datatype/links/5703a08008aeade57a25a487/De-Bruijn-notation-as-a-nested-datatype.pdf
That is, I want to go from

inductive {u} Incr (v : Type u) : Type u
| zero : Incr
| succ : v -> Incr

inductive {u} Term : Type u -> Type (u + 1)
| var {v} : v -> Term v
| app {v} : Term v -> Term v -> Term v
| lam {v} : Term (Incr v) -> Term v

to

inductive {v} Exp : Type v -> Type (v + 1)
| var {a} : a -> Exp a
| app {a} : Exp a -> Exp a -> Exp a
| lam {a} : Exp (Incr (Exp a)) -> Exp a

The second one doesn't compile. Is there a way to reduce the universe in the recursive Exp?

[Johan Commelin]

@Anton Lorenzen I'm far from an expert, but do you not want to simply use nat in place of Incr?

[Johan Commelin]

If you are formalising a type theory, than I would expect that you don't need any universes at all.

[Anton Lorenzen]

@Johan Commelin I am not an expert either, but I think the idea is that you can succ a lambda expression for better performance/type safety

[Anton Lorenzen]

So no

[Anton Lorenzen]

I am formalising a type theory and don't need universes for that but I think I need levels for this technique to work?

[Anton Lorenzen]

In Haskell (with TermE as Exp)

data Incr v = Zero | Succ v
data Term v = Var v | App (Term v, Term v) | Lam (Term (Incr v))
data TermE a = VarE a
| AppE (Pair (TermE a))
| LamE (TermE (Incr (TermE a)))

[Johan Commelin]

Johan Commelin I am not an expert either, but I think the idea is that you can succ a lambda expression for better performance/type safety

I don't know what "succ a lambda expression" means. If you just mean de Bruijn indices, than I would expect to see nat.

[Johan Commelin]

What is the v in Incr v in Haskell?

[Johan Commelin]

Is it an arbitrary type?

[Johan Commelin]

Your current Incr looks very much like option to me (that is, Haskell's Maybe)

[Anton Lorenzen]

The idea behind this technique is to avoid expressions like Lam (Var 2) (with an illegal index) by changing the type of variables in each recursive lambda constructor. So initially the variables have type v (for example String), inside one lambda they are Z | S String, inside two lambdas they are Z | S (Z | S string) and so on. (the paper explains that better than me). The problem is that this requires polymorphic recursion and I think I need to tell Lean in some way that this recursion is well-founded..

[Johan Commelin]

Aha, I think I understand. So why not reuse option?

[Anton Lorenzen]

Or, rather, my explanation is for the first formalization, which is slow on instantiation because of all the succ's. So the second formalization avoids this by adding Incr to the terms so that we can "succ an expression" as in saying "all of the indices in here should be succ'ed".

[Anton Lorenzen]

I guess I could reuse option, but I don't see how this would make the second one compile?

[Reid Barton]

As someone who has used this Term before, I'm totally bewildered by Exp. But anyways I don't think Lean supports this form.

[Reid Barton]

Coq doesn't accept it either, with a different kind of error message (Non strictly positive occurrence of "Exp"). I think you would probably get a positivity error in Lean as well, if you didn't get the universe error.

[Reid Barton]

Agda accepts it even though the documentation seems to indicate it shouldn't :shrug:

[Anton Lorenzen]

@Reid Barton Yes, you are right. I think I could rewrite it as a fixpoint though

data TermEF a t = VarE a
| AppE (Pair (TermE a t))
| LamE (TermE (Incr (t a)))
data TermE a = Fix (TermEF a)

The question is therefore if I can do "recursion on universes" and have Exp be in the universe of the number of lamdas it contains. And also, if that is actually a good idea (I guess not).

[Reid Barton]

But your TermEF depends on TermE, so you have not eliminated the recursion

[Reid Barton]

Did you want to replace that one by t also?

[Anton Lorenzen]

No, it doesn't, I am just being sloppy. I meant:

data TermEF a t = VarE a
| AppE (Pair (TermEF a t))
| LamE (TermEF (Incr (t a)) t)
type TermE a = Fix (TermEF a)

[Anton Lorenzen]

So, in Lean

inductive {v} Lift : Type v -> Type (v + 1)
| lift {a} : a -> Lift a

inductive {v} Exp (t : Type v -> Type (v + 1)) : Type (v + 1) -> Type (v + 2)
| var {a} : a -> Exp a
| app {a} : Exp a -> Exp a -> Exp a
| lam {a} : Exp (Incr (t a)) -> Exp (Lift a)

[Anton Lorenzen]

No, I don't think I mean that. I guess I am going to use the Term part from above

[Anton Lorenzen]

Thanks!

[Reid Barton]

The question is therefore if I can do "recursion on universes" and have Exp be in the universe of the number of lamdas it contains. And also, if that is actually a good idea (I guess not).

You definitely can't do any kind of quantification over universes other than prenex (i.e., at the outermost position). For example you can't prove a lemma by induction where you invoke the inductive hypothesis at a different universe, because that would compile to passing a term quantified over universes to the recursor.

[Reid Barton]

The universe level checks can be overly conservative, which might make techniques like this less useful. For example

inductive {u} Incr' : Type u → Type (u + 1)
| zero : Π (v : Type u), Incr' v
| succ : Π (v : Type u), v → Incr' v

is isomorphic to Incr, but it has to have result Type (u + 1) not Type u.

[Reid Barton]

Having Term live in Type (u + 1) will likely be a pain if you want to do any kind of monadic programming.

[Mario Carneiro]

@Anton Lorenzen Your rendering of Exp doesn't make much sense to me either. The recursive option type for encoding indices is not a problem, but I would expect the lam argument to have a different type, like so:

inductive {v} Exp : Type v -> Type (v + 1)
| var {a} : a -> Exp a
| app {a} : Exp a -> Exp a -> Exp a
| lam {a} : Exp (Incr a) -> Exp a

[Mario Carneiro]

You can eliminate the universe bumping in this definition by taking advantage of the fact that there are only a "small" (nat indexed) number of options you can tack on a type

def {u} Incr' (v : Type u) : ℕ → Type u
| 0 := punit
| (n+1) := v × Incr' n

inductive {u} Exp' (v : Type u) : ℕ -> Type u
| var {a} : Incr' v a -> Exp' a
| app {a} : Exp' a -> Exp' a -> Exp' a
| lam {a} : Exp' (a+1) -> Exp' a

def Exp (v) := Exp' v 0

[Jannis Limperg]

This technique looks like a more complicated version of the usual encoding of scope-safe terms:

inductive Term : ℕ → Type
| var {n} : fin n → Term n
| app {n} : Term n → Term n → Term n
| lam {n} : Term (n + 1) → Term n

Term n is a term in any context of length at least n (and variables are indexes into such a context).

[Anton Lorenzen]

Hey Jannis, nice to see you here :)

[Mario Carneiro]

@Jannis Limperg It is; I just wrote it that way because Anton seemed to want variables indexed on arbitrary types

[Mario Carneiro]

There isn't any real advantage to the version I posted first over the version you just wrote, and some significant disadvantages. Using types for indexing like this makes sense in haskell but in a dependent type theory there isn't much downside to just using nat

[Jannis Limperg]

Nice to see you too, Anton. Type theory remains a small field. ;)

@Mario Carneiro I thought so too, but wasn't sure that I hadn't missed some subtlety.