Encodage de type récursif sur le système F (et d'autres systèmes de type pur)

J'étudie les systèmes de types purs, en particulier le calcul des constructions, et j'essaie d'utiliser un codage pour les types récursifs, ce qui, selon Philip Wadler, est possible . À titre d'exemple, j'utilise la bibliothèque Morte Haskell pour coder les chiffres Scott comme donnés par Cardelli .

Un résumé de l'encodage est en tant que tel: étant donné un type récursif (positif) ...

... nous pouvons le coder comme un type sur le système F comme ...

... ou, en utilisant la notation des systèmes de type pur (avec une explicite $F$) ...

...depuis $F$ est un constructeur de type ($*$ est le type de types).

Afin de coder de tels codes, nous devons déclarer trois fonctions, $fold$, $in$ et $out$, selon Wadler, et utilisé par Cardelli pour l'encodage des chiffres Scott.

plier: Tous X. (FX -> X) -> T -> X

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

dans: FT -> T

dans = \ s: F T. \ X. \ k: FX -> X. k (F (pli X k) s).

(Où $T$ est $Lfix\ X. F\ X$.)

Il est trivial d'écrire le $fold$fonctionner comme indiqué. Mais en essayant d'écrire le$in$fonction, il ne semble pas typecheck. L'expression$(fold\ X\ k)$ a un type $T\rightarrow X$, et $(F\ (fold\ X\ k)\ s)$ devrait être de type $F\ X$. Ensuite, nous déduisons que$F$ devrait être de type $(T\rightarrow X)\rightarrow F\ T\rightarrow F\ X$(ressemble à un fmap). Cela ne vérifie pas le type, car il Fs'agit d'un constructeur de type (de type$*\rightarrow*$).

Cela ne ressemble pas à une faute de frappe ... manque-t-il quelque chose?

Il existe une convention dans la théorie des catégories selon laquelle le même symbole est utilisé pour un constructeur de type et la fonction map sur ce constructeur de type. Par conséquent, si f: X -> Y alors F f: FX -> F Y.