PiSigma: ¿por qué 'desplegar' une una variable?

Estoy tratando de entender el artículo ΠΣ: Tipos dependientes sin el azúcar mediante la implementación de un intérprete y un corrector de tipo para el idioma. Al hacerlo, he visto que la unfold t as x -> usintaxis para definiciones recursivas (la sintaxis se define en la Sección 2.1) vincula una variable, pero no veo por qué es necesaria. Ninguno de los ejemplos en el documento realmente usa el enlace variable; todos usan una forma abreviada unfold t(significado unfold t as x -> x).

Yo no veo que el tipo de regla de verificación para ello (de la sección 5) utiliza la variable vinculante, pero no entiendo las implicaciones de esto. Por lo que puedo decir unfold t as x -> ues completamente equivalente a let x = unfold t in u.

¿Alguien puede proporcionar un ejemplo de cuándo el enlace variable es útil o necesario? ¿Hay algún término que verifique el tipo con la forma larga unfoldpero no con la forma corta y let?

No creo que haya ninguna razón mágica / necesaria. En mi opinión, está escrito de esa manera para que sea más obvio que unfoldes una regla de eliminación analítica / de verificación; al igual que por qué splitse escribe de la manera en que se escribe, en lugar de escribirse como primera y segunda proyección, y por qué casese escribe de la manera en que se escribe, uneitheren lugar de escribirse como en Haskell.

Con respecto al bit "analítico", observe cómo las otras reglas de eliminación son sintéticas / inferidas (beta) o bidireccionales (explosión)