I'm trying to understand the paper ΠΣ: Dependent Types without the Sugar by implementing an interpreter and type checker for the language. In doing so, I've seen that the unfold t as x -> u
syntax for recursive definitions (syntax is defined in Section 2.1) binds a variable, but I don't see why that's needed. None of the examples in the paper actually use the variable binding -- they all use a shorthand form unfold t
(meaning unfold t as x -> x
).
I do see that the type checking rule for it (from section 5) uses the variable binding, but I don't understand the implications of this. As far as I can tell unfold t as x -> u
is entirely equivalent to let x = unfold t in u
.
Can someone provide an example of when the variable binding is helpful or necessary? Is there some term that type-checks with the long form of unfold
but not with the short form and let
?