Мы можем писать индуктивные типы в терминах типа фиксированной точки:
Fix : (* -> *) -> *
In : (f : * -> *) -> f (Fix f) -> Fix f
NatF r = () + r
Nat = Fix NatF
Z = In NatF (InL ())
S n = In NatF (InR n)
Но этого типа исправления недостаточно для индексированных типов данных, и нам нужна индексированная фиксированная точка:
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
Используя IFix, мы можем получить Fix обратно, установив тип индекса на unit.
Какие типы данных мы не можем записать, используя IFix, есть ли более общая фиксированная точка, чем IFix?