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

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

CC BY-SA 3.0
2016-02-17T16:31:12.450Z
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!
Steve Trout
CC BY-SA 3.0
2016-02-14T21:51:04.713Z
2016-02-14T21:51:04.713Z
wren romano
<p>I'm trying to understand the paper <a href="https://www.andres-loeh.de/PiSigma/PiSigma.pdf">ΠΣ: Dependent Types without the Sugar</a> by implementing an interpreter and type checker for the language. In doing so, I've seen that the <code>unfold t as x -&gt; u</code> 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 <code>unfold t</code> (meaning <code>unfold t as x -&gt; x</code>).</p>

<p>I <em>do</em> 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 <code>unfold t as x -&gt; u</code> is entirely equivalent to <code>let x = unfold t in u</code>.</p>

<p>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 <code>unfold</code> but not with the short form and <code>let</code>?</p>

CC BY-SA 3.0
2016-02-12T03:29:21.407Z
I'd quote the type checking rule, but my knowledge LaTeX is too limited. Would some kind editor do that for me? Thanks!
Steve Trout
<type-theory><dependent-type>
PiSigma: why does 'unfold' bind a variable?
Steve Trout
# PiSigma: why does 'unfold' bind a variable?

(Asked by: username_0 on 2016-02-12)

I'm trying to understand the paper [ΠΣ: Dependent Types without the Sugar](https://www.andres-loeh.de/PiSigma/PiSigma.pdf) 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`?

**Tags:** type-theory, dependent-type
> **Comments:**
> **username_0**: I'd quote the type checking rule, but my knowledge LaTeX is too limited. Would some kind editor do that for me? Thanks!  

---

## 1 answers

### Answer by username_1 on 2016-02-14. Score: 1 | Accepted answer

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)

> **Comments:**
> **username_0**: 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!  

---

