mbps https://blog.hatena.ne.jp/mbps/ PS https://mbps.hatenablog.com/ 圏論 F-algebra Haskell 複雑な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: をこっそり使って *1 に変形すると、これはInductive family of types - PS。 参考文献 Haskell for all: GADTs *1:natural transformati… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmbps.hatenablog.com%2Fentry%2F2014%2F10%2F03%2F010000" title="GADTs - PS" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> http://chart.apis.google.com/chart?cht=tx&chl=%20%5Cmathrm%7BNat%7D%28%5Cmathcal%7BHask%7D%28x%2C%20%5Cunicode%7Bx2013%7D%29%2C%20%5Cmathtt%7BIntList%7D%29%20%5Ccong%20%5Cmathtt%7BIntList%7D%28x%29%20 Hatena Blog https://hatena.blog 2014-10-03 01:00:00 rich https://mbps.hatenablog.com/entry/2014/10/03/010000 1.0 100%