# Recursive type encoding on System F (and other pure type systems)

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?

• 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 – paulotorrens Jan 15 '17 at 8:42