8
$\begingroup$

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?

Improve this question
$\endgroup$
  • $\begingroup$ I'd quote the type checking rule, but my knowledge LaTeX is too limited. Would some kind editor do that for me? Thanks! $\endgroup$ – Steve Trout Feb 12 '16 at 3:29
1
$\begingroup$

I don't think there's any magic/necessary reason. IMO, it's written that way to make it more straightforwardly obvious that unfold is an analytic/checking elimination rule; just like why split is written the way it is rather than being written as first and second projections, and why case is written the way it is rather than being written like uneither in Haskell.

Re the "analytic" bit, note how the other elimination rules are either synthetic/inferring (beta) or bidirectional (bang)

Improve this answer
$\endgroup$
  • $\begingroup$ Ah, I see the distinction there. That's a possible reason why !x isn't written force x as y -> y. Whether or not there's a deeper reason, this answer satisfies my curiosity. Thanks! $\endgroup$ – Steve Trout Feb 17 '16 at 16:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.