■ [Haskell] Type Familiesを使って型レベルで階乗を実装してみる

Type Familiesを使って型レベルで階乗を実装してみます。基本の考え方としては、dataで定義する型が型レベルの値で、type familyで定義する型属が型レベルの関数になります。

まずは、数の定義から。EmptyDataDecls拡張を使います。

{-# LANGUAGE TypeFamilies,
             EmptyDataDecls,
             UndecidableInstances,
             ScopedTypeVariables #-}

data Zero
data Succ a

後で楽なようにいくつかの数も定義しておきます。

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
type Six = Succ Five

まず、足し算を定義してみます。TypeFamilies拡張が必要です。

type family Add a b
type instance Add Zero a = a
type instance Add (Succ a) b = Succ (Add a b)

試してみるには、GHCiで以下のようにするのが良さそうです。

> :type (undefined :: Add One One) :: Two

答えが正しいと結果の型（ここではTwo）が表示されますが、以下のように正しくないとエラーになります。

> :type (undefined :: Add One One) :: Three
<interactive>:1:1:
    Couldn't match expected type `Succ Zero'
           against inferred type `Zero'
      Expected type: Three
      Inferred type: Add One One
    In the expression: (undefined :: Add One One) :: Three

これを元にかけ算を定義します。UndecidableInstances拡張が必要です。

type family Mul a b
type instance Mul Zero a = Zero
type instance Mul (Succ a) b = Add b (Mul a b)

> :type (undefined :: Mul Two Three) :: Six

これらを使って階乗を定義します。

type family Fac a
type instance Fac Zero = One
type instance Fac (Succ a) = Mul (Succ a) (Fac a)

> :type (undefined :: Fac Three) :: Six
> :type (undefined :: Fac Four) :: Mul Two (Mul Three Four)

このままだと結果を見るのが面倒なので、型で定義した数を実行時の数に変換するクラスを追加しておくと楽です。ScopedTypeVariables拡張が必要です。

class N a where
  n :: a -> Int

instance N Zero where
  n _ = 0

instance N a => N (Succ a) where
  n _ = 1 + n (undefined :: a)

これで、

> n (undefined :: Four)
4

となって確認が楽になります。ただし、コンテキストスタックのサイズを増やさないとすぐにオーバーフローします。

> :set -fcontext-stack=30
> n (undefined :: Fac Four)
24