ふつうの純粋な型レベルプログラミング in Haskell
とりあえず 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 c | a b -> c
まずは簡単な base case のほうから.
instance Add Z a a
上の add Z a = a に対応しているのがわると思う.
次にもうちょっと複雑なほうを.
instance Add a b c => Add (S a) b (S c)
これはちょっと対応関係が見にくいかもしれないけど,感覚としては Add (S a) b にマッチしたら,Add a b の結果を c に入れて (S c) を返すかんじ.
このように,関数適用のようなものは instance context に書くことで実現できる.
試しに
add :: Add a b c => a -> b -> c add = undefined zero = undefined :: Z one = undefined :: S Z two = add one one three = add one two
と書いて型をみてみると,
*Main> :t one one :: S Z *Main> :t two two :: S (S Z) *Main> :t three three :: S (S (S Z))
と,たしかに足し算ができている.
次はかけ算.複数の関数適用が必要な場合も同様にできる.
値レベルでは
mul Z b = b mul (S a) b = add (mul a b) b
型レベルでは
class Mul a b c | a b -> c instance Mul Z b Z instance (Mul a b c', Add c' b c) => Mul (S a) b c mul :: Mul a b c => a -> b -> c mul = undefined
今度は述語を定義してみる.新たな型として
data T data F
を導入する.もちろん感覚としては T が真で F が偽.
例えば < をまず値レベルで定義してみると
Z < Z = F Z < (S a) = T (S a) < Z = F (S a) < (S b) = a < b
これを型レベルに書き直すと
class Le a b c | a b -> c instance Le Z Z F instance Le Z (S a) T instance Le (S a) Z F instance Le a b c => Le (S a) (S b) c le :: Le a b c => a -> b -> c le = undefined
ここらへんで一度本当にできているかたしかめてみる.
*Main> :t le one three le one three :: T *Main> :t le three two le three two :: F
この述語を使って条件分岐のようなものをしてみる.
例として余りを求める rem' を定義する.*1
値レベルでは
rem' x y = if x < y then x else rem' (x-y) y
型レベルでは
class Rem x y r | x y -> r instance (Le x y b, Rem' b x y r) => Rem x y r class Rem' b x y r | b x y -> r instance Rem' T x y x instance (Add y x' x, Rem x' y r) => Rem' F x y r rem' :: Rem x y r => x -> y -> r rem' = undefined
このように,条件分岐は新たに型クラスを定義して,そこでマッチさせるような形で実現する.
ここで Add を使っているのが不思議かもしれないが,例えば x = S (S (S Z)), y = S (S Z) のときは,fundeps によって Add x x' y で x' = (S Z) に unify できるので,これで引き算が可能になる.
*Main> :t rem' three two rem' three two :: S Z *Main> :t rem' three one rem' three one :: Z *Main> :t rem' (add two two) two rem' (add two two) two :: Z
最後に型レベルを値レベルにするときに便利な関数を紹介.
class Nat a where nat :: Num b => a -> b instance Nat Z where nat _ = 0 instance Nat a => Nat (S a) where nat _ = 1 + nat (undefined :: a)
これを使うと,
*Main> nat (mul two three) 6
のように,普通の数字にすることができる.
*1:rem は Prelude に既に定義されているので,rem' としている