ふつうの純粋な型レベルプログラミング 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' としている