PS

GADTs

複雑なGADTsはYoneda lemmaを使ってInductive family of types - PSにもっていける、ということらしい。

data Z
data S n

data IntList n where
    Nil  :: IntList Z
    Cons :: Int -> IntList m -> IntList (S m)

Covariant Yoneda lemma:

  •  \operatorname{Nat}(\mathcal{Hask}(x, \unicode{x2013}), \mathtt{IntList}) \cong \mathtt{IntList}(x)

をこっそり使って

に変形すると、これはInductive family of types - PS

参考文献

*1:natural transformation