In this answer it is shown we can encode inductive types in System F-omega using the church encoding:

$Fix F = \forall T : \mathsf{Type} \,.\, (F T \to T) \to T$

for some type constructor $F$.

It is also known that this encoding does not admit constant-time destructors for those datatypes.

If we add positive-recursive types to System F-omega then we can use the Parigot encoding to get efficient datatypes (when sharing correctly they can also be space efficient).

Can we also generalize the Parigot encoding to be of a form similar to the F-algebra style of datatypes? My intuition says we'd have to modify the encoding to something like:

$Fix F = \forall T : \mathsf{Type} \,.\, (F (Fix F, T) \to T) \to T$

Only I am not sure this type will pass the positive-recursion check.

  • $\begingroup$ I think this may be impossible in System F-omega, because there needs to be a constraint on $F$ (Functor, but maybe something weaker will suffice), but System F does not have the power to encode that constraint I think. $\endgroup$
    – Labbekak
    Apr 22 '20 at 21:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.