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:
をこっそり使って
に変形すると、これはInductive family of types - PS。
参考文献
*1:natural transformation