前回はsimply-typedの拡張としてλμを実装したけれど、 今回はsimply-typedにrecursive typeを実装してみた。 recursive typeはいわゆる(G)ADT相当の機能だけど、型パラメータを持たないのでADTの真面目な実装に比べると楽だと思う。 recursive typeはType ->…

λμのtypecheckerを実装したので (ソースコードは参考文献[3]を参照) λμ[1]はλ→に継続(callCC)を入れたもの(CCC + Continuation monad)。 syntax的にはμ-abstractionとnaming(termに名前をつける)が追加される。 型なしの項を受け取って、それにうまく型をつ…

この記事のunification algorithmは間違っているので λμのTypeCheckerの実装 - Just $ A sandboxを参考にしてください λ→のtypingアルゴリズム. variableとabstractionは型が一意に決まるので, 問題はapplication. MN:aからM:?x -> aの?xをどうやって決定す…