ふつうの純粋な型レベルプログラミング in Haskell - EAGLE 雑記とりあえず fundeps で自然数編．続きはあるんですか? まず，おまじないとして {-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses, UndecidableInstances, FlexibleInstances, EmptyDataDecls, ScopedTypeVariables #-} あたりが要る． 自然数の表現方法．普通にペアノ数として扱う． data Z data S a 自然数上の演算として例えば足し算を書いてみる． 普通の値レベルでの足し算を書いてみると，パターンマッチを用いて add Z a = a add (S a) b = S (add a b) このようになる．これを型レベルに書き直していく． 型レベルにおける関数は fundeps を持つ型クラスとして表現できる． class Add a b
