型レベル計算で、zipWith をやりたい。 ちなみに zipWith :: (a -> b -> c) -> [a] -> [b] -> [c] で、まあそういう関数だ。しかし まともに使える関数を作るには、陽に型を指定せずとも型が推論されてくれないと困る。そこで zipWithに渡す関数の種類を、引…

型レベルの数値と、引き算Sub, 型レベルのconsリスト、リストの長さを求める型クラスLengthと関数length_tを定義する。 data S n data Z class Sub n n' n'' | n n' -> n'' instance Sub n Z n instance Sub n n' n'' => Sub (S n) (S n') n'' class Length …