8
$\begingroup$

I am studying pure type systems, particularly the calculus of constructions, and trying to use an encoding for recursive types on it, which, according to Philip Wadler, is possible. As an example, I'm using the Morte Haskell library to encode Scott numerals as given by Cardelli.

A summary of the encoding is as such: given a (positive) recursive type...

$$\mu X.F\ X$$

...we may encode it as a type on System F as...

$$Lfix\ X.F\ X\ =\ \Lambda X.(F\ X\rightarrow X)\rightarrow X$$

...or, using pure type systems' notation (with an explicit $F$)...

$$Lfix\ =\ \Pi F: *\rightarrow*.\Pi X: *.(F\ X\rightarrow X)\rightarrow X$$

...since $F$ is a type constructor ($*$ is the type of types).

In order to encode such, we need to declare three functions, $fold$, $in$ and $out$, according to Wadler, and used by Cardelli on the encoding for Scott numerals.

fold : All X. (F X -> X) -> T -> X

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

in : F T -> T

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

(Where $T$ is $Lfix\ X. F\ X$.)

It's trivial to write the $fold$ function as given. But when trying to write the $in$ function, it doesn't seem to typecheck. The expression $(fold\ X\ k)$ has type $T\rightarrow X$, and $(F\ (fold\ X\ k)\ s)$ should be of type $F\ X$. Then we infer that $F$ should be of type $(T\rightarrow X)\rightarrow F\ T\rightarrow F\ X$ (looks like a fmap). This doesn't typecheck, because F is a type constructor (of type $*\rightarrow*$).

This doesn't look like a typo... am I missing something?

$\endgroup$
7
$\begingroup$

There is a convention in category theory that the same symbol is used for a type constructor and the map function over that type constructor. Hence, if f : X -> Y then F f : F X -> F Y.

$\endgroup$
  • $\begingroup$ So it is indeed a fmap! I got zero experience on category theory, but I actually found that about 10 minutes ago on "A note on Categorical Datatypes" (G. C. Wralth). I was now able to write the correct function, worked like a charm. Thank you very much, dr. Wadler! :D $\endgroup$ – paulotorrens Jan 15 '17 at 8:42

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.