1
$\begingroup$

We can write inductive types in terms of a fixpoint type:

Fix : (* -> *) -> *
In : (f : * -> *) -> f (Fix f) -> Fix f

NatF r = () + r
Nat = Fix NatF
Z = In NatF (InL ())
S n = In NatF (InR n)

But this fix type is not sufficient for indexed datatypes and we need an indexed fixpoint:

IFix : (I : *) -> ((I -> *) -> (I -> *)) -> I -> *
IIn : (I : *) -> (F : (I -> *) -> (I -> *)) -> (i : I) -> F (IFix I F) i -> IFix I F i

FinF r n = (n = Z) + ((m : Nat) ** r m ** (n = S m))
Fin = IFix Nat FinF

Using IFix we can get Fix back by setting the index type to unit.

What datatypes can we not write using IFix, is there a more general fixpoint than IFix?

$\endgroup$

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.