Codificación de tipo recursivo en el Sistema F (y otros sistemas de tipo puro)

Estoy estudiando sistemas de tipos puros, particularmente el cálculo de construcciones, y tratando de usar una codificación para tipos recursivos, lo que, según Philip Wadler, es posible . Como ejemplo, estoy usando la biblioteca Morte Haskell para codificar los números de Scott tal como los da Cardelli .

Un resumen de la codificación es como tal: dado un tipo recursivo (positivo) ...

... podemos codificarlo como un tipo en el Sistema F como ...

... o, usando la notación de sistemas de tipo puro (con un explícito $F$) ...

...ya que $F$ es un constructor de tipos ($*$ es el tipo de tipos).

Para codificar tales, necesitamos declarar tres funciones, $fold$, $in$ y $out$, según Wadler, y utilizado por Cardelli en la codificación de los números de Scott.

doblar: Todo X. (FX -> X) -> T -> X

doblar = \ X. \ k: FX -> X. \ t: T. t X k

en: FT -> T

in = \ s: F T. \ X. \ k: FX -> X. k (F (doblar X k) s).

(Dónde $T$ es $Lfix\ X. F\ X$.)

Es trivial escribir el $fold$funcionar como se indica. Pero al intentar escribir el$in$función, no parece mecanografiar. La expresion$(fold\ X\ k)$ tiene tipo $T\rightarrow X$y $(F\ (fold\ X\ k)\ s)$ debe ser de tipo $F\ X$. Entonces inferimos que$F$ debe ser de tipo $(T\rightarrow X)\rightarrow F\ T\rightarrow F\ X$(se parece a fmap) Esto no comprueba, porque Fes un constructor de tipos (de tipo$*\rightarrow*$)

Esto no parece un error tipográfico ... ¿me estoy perdiendo algo?

Existe una convención en la teoría de categorías en la que se usa el mismo símbolo para un constructor de tipos y la función de mapa sobre ese constructor de tipos. Por lo tanto, si f: X -> Y entonces F f: FX -> F Y.