実体のある型レベル自然数をHaskellで実装してみた

GHC では型システムが急速に進化していて、ついに型レベル自然数 (type-level natural number) も組み込まれました。

この型レベル自然数は、0, 1, 2, ... というリテラルによって型レベル自然数を得られ、足し算・掛け算・冪乗・引き算・比較が可能です。考えられる使い道としては、配列の要素外アクセスを制限したり、バージョン管理をしたりといったことを、コンパイル時に静的に行うことでしょう。

しかしこの型レベル自然数の類 (kind) は Nat であり、真の型（proper type, 実際に値を持つ類 * の型）ではありません。これはもったいない気がします。型に属する値が何種類あるか、という観点から、ヴォイド型 Void は 0、ユニット型 () は 1、ブール型 Bool は 2、直和 Either a b は足し算 a + b、直積 (a, b) は掛け算 a * b、関数 b -> a は冪乗 a ^ b と対応していますから、有限の種類の値しか持たない型を型レベル自然数として使えれば嬉しいと思いました。

GHC 7.8.3 を搭載した新しいバージョンの Haskell Platform が出たこともあり、久しぶりに Haskell を触っているうちにそんなことを思って、「実体のある型レベル自然数」を実装しました。実体のある型レベル自然数というアイデア自体ほかで見たことが無いので、この実装は完全にオリジナルのものだと思います（似たことを考えている人がいたら教えてください）。

速度の面でどうしても限界があることもあり、実用性があるかどうかは分かりませんが、この実装のテクニックを応用することで便利な道具がいろいろ作れる気がするので、「実体のある型レベル自然数」の実装を、詳しく紹介していくことにします。

まず、「純粋な自然数型」を定義します。

data Zero
data Succ a = Zero | Succ a
class Pure a
instance Pure Zero
instance Pure a => Pure (Succ a)

型 Zero はデータコンストラクタを持たないので、ヴォイド型と同様、値の種類は0種類であると見なせます（いわゆるボトムは値に含めないことにします）。型 Succ a は Either () a と同型（isomorphic, 相互に変換可能）ですから、a よりも1種類だけ値が多いことになります。

ここでは、型と値がそれぞれペアノ数 (Peano number) として定義されています。例えば 3 に対応するのは Succ (Succ (Succ Zero)) であり、この型の値は Zero, Succ Zero, Succ (Succ Zero)（それぞれ 0, 1, 2 に対応している）の3種類です。

組み込みの型レベル自然数と「純粋な自然数型」との間の変換と、純粋な自然数型からの関数と対応する要素数のリストとの間の変換をここで定義しておきます。

class Pure a where
    type ToNat a :: Nat
    puretolist :: (a -> b) -> [b]
    listtopure :: [b] -> (a -> b)
instance Pure Zero where
    type ToNat Zero = 0
    puretolist f = []
    listtopure [] !_ = undefined
instance Pure a => Pure (Succ a) where
    type ToNat (Succ a) = ToNat a + 1
    puretolist f = f Zero : puretolist (f . Succ)
    listtopure (x : _) Zero = x
    listtopure (_ : xs) (Succ n) = listtopure xs n

type family ToPure (a :: Nat) where
    ToPure 0 = Zero
    ToPure n = Succ $ ToPure $ n-1

ここでは、クラスに関連付けられた型族や閉じた型族などを使っています。

さて、これで純粋な自然数型については十分な演算が得られました。次は、純粋な自然数型を直和・直積・関数として組み合わせて得られる型を、対応する（値の種類の等しい）純粋な自然数型と相互に変換が出来るようにします。まずは型クラスを定義します。

class Pure (Goal a) => Conv a where
    type Goal (a :: *) :: *
    fw :: a -> Goal a
    bw :: Goal a -> a

Goal a が対応する純粋な自然数型を表し、fw, bw は（forward と backward の）変換関数を表します。この型クラスがあれば、リストとの間の変換も簡単にできます。

tolist :: Conv a => (a -> b) -> [b]
tolist f = puretolist (f . bw)
fromlist :: Conv a => [b] -> (a -> b)
fromlist xs = listtopure xs . fw

では、これから Conv のインスタンスを再帰的に定義していきます。まずは自明なインスタンスから。

instance Conv Zero where
    type Goal Zero = Zero
    fw = id
    bw = id
instance Pure a => Conv (Succ a) where
    type Goal (Succ a) = Succ a
    fw = id
    bw = id

さて、いよいよ直和・直積・関数を扱っていきます。見易さのために、型演算子を導入しておきます。

type a +! b = Either a b
type a *! b = (a,b)
type a ^! b = b -> a
infixl 6 +!
infixl 7 *!
infixr 8 ^!

では、直和についてのインスタンスを作ります。

instance (Conv (o a b), Conv (Goal (o a b) +! c)) =>
                        Conv ((o :: * -> * -> *) a b +! c) where
    type Goal (o a b +! c) = Goal (Goal (o a b) +! c)
    fw (Left x) = fw (Left (fw x) :: Goal (o a b) +! c)
    fw (Right y) = fw (Right y :: Goal (o a b) +! c)
    bw n = case bw n of
        Left x -> Left (bw x)
        Right y -> Right y
instance (Pure a, Conv (o b c), Conv (Succ a +! Goal (o b c))) =>
                        Conv (Succ a +! (o :: * -> * -> *) b c) where
    type Goal (Succ a +! o b c) = Goal (Succ a +! Goal (o b c))
    fw (Left x) = fw (Left x :: Succ a +! Goal (o b c))
    fw (Right y) = fw (Right (fw y) :: Succ a +! Goal (o b c))
    bw n = case bw n of
        Left x -> Left x
        Right y -> Right (bw y)
instance (Pure a, Pure b, Conv (a +! Succ (Succ b))) =>
                        Conv (Succ a +! Succ b) where
    type Goal (Succ a +! Succ b) = Goal (a +! Succ (Succ b))
    fw (Left Zero) = fw (Right Zero :: a +! Succ (Succ b))
    fw (Left (Succ x)) = fw (Left x :: a +! Succ (Succ b))
    fw (Right y) = fw (Right (Succ y) :: a +! Succ (Succ b))
    bw n = case bw n of
        Left x -> Left (Succ x)
        Right Zero -> Left Zero
        Right (Succ y) -> Right y
instance Pure a => Conv (Zero +! a) where
    type Goal (Zero +! a) = a
    fw (Left !_) = undefined
    fw (Right x) = x
    bw x = Right x
instance Pure a => Conv (Succ a +! Zero) where
    type Goal (Succ a +! Zero) = Succ a
    fw (Left x) = x
    fw (Right !_) = undefined
    bw x = Left x

重複インスタンスや非整合インスタンスを避けるために少し苦労しています。「純粋な自然数型」と「純粋な自然数型で無い型」の場合分けを、文脈（context, (...) => の部分）によって行うとなぜか怒られるので、直和・直積・関数がすべて2引数の型コンストラクタであることを利用して、型の形の上から場合分けをしています。GHC の型検査器がもう少し賢くなったらもっと素直に書けるようになるだろうと思いますが、なぜそのための機能が今のところ実装されていないのかは知りません。

fw と bw の実装がパッと見だと不思議に見えるかもしれませんが、型を考えると分かってくると思います。fw と bw が互いに逆の変換になっていることを確かめてみてください（Zero 型についての扱いはあまり神経質にならなくていいと思います）。なお、型推論を助けるために、字句的スコープを持つ型変数を利用していることに注意してください。

次は、直積についてのインスタンスを作ります。直和のほうが分かれば難しくはないはずです。

instance (Conv (o a b), Conv (Goal (o a b) *! c)) =>
                        Conv ((o :: * -> * -> *) a b *! c) where
    type Goal (o a b *! c) = Goal (Goal (o a b) *! c)
    fw (x, y) = fw (fw x, y)
    bw n = let (x, y) = bw n in (bw x, y)
instance (Pure a, Conv (o b c), Conv (Succ a *! Goal (o b c))) =>
                        Conv (Succ a *! (o :: * -> * -> *) b c) where
    type Goal (Succ a *! o b c) = Goal (Succ a *! Goal (o b c))
    fw (x, y) = fw (x, fw y)
    bw n = let (x, y) = bw n in (x, bw y)
instance (Pure a, Pure b, Conv (Succ b +! a *! Succ b)) =>
                        Conv (Succ a *! Succ b) where
    type Goal (Succ a *! Succ b) = Goal (Succ b +! a *! Succ b)
    fw (Zero, y) = fw (Left y :: Succ b +! a *! Succ b)
    fw (Succ x, y) = fw (Right (x, y) :: Succ b +! a *! Succ b)
    bw n = case bw n of
        Left y -> (Zero, y)
        Right (x, y) -> (Succ x, y)
instance Pure a => Conv (Zero *! a) where
    type Goal (Zero *! a) = Zero
    fw (!_, _) = undefined
    bw !_ = undefined
instance Pure a => Conv (Succ a *! Zero) where
    type Goal (Succ a *! Zero) = Zero
    fw (_, !_) = undefined
    bw !_ = undefined

最後に関数についてのインスタンスを作ります。関数をデータとして操作するのが慣れていないと分かりづらいかもしれませんが、これも型を考えれば分かるはずです。

instance (Conv (o a b), Conv (Goal (o a b) ^! c)) =>
                        Conv ((o :: * -> * -> *) a b ^! c) where
    type Goal (o a b ^! c) = Goal (Goal (o a b) ^! c)
    fw f = fw (fw . f)
    bw n = bw . bw n
instance (Pure a, Conv (o b c), Conv (Succ a ^! Goal (o b c))) =>
                        Conv (Succ a ^! (o :: * -> * -> *) b c) where
    type Goal (Succ a ^! o b c) = Goal (Succ a ^! Goal (o b c))
    fw f = fw (f . bw)
    bw n = bw n . fw
instance (Pure a, Pure b, Conv (Succ a *! Succ a ^! b)) =>
                        Conv (Succ a ^! Succ b) where
    type Goal (Succ a ^! Succ b) = Goal (Succ a *! Succ a ^! b)
    fw f = fw (f Zero, f . Succ)
    bw n = let (x, f) = bw n in \m -> case m of Zero -> x; Succ l -> f l
instance Pure a => Conv (Zero ^! Succ a) where
    type Goal (Zero ^! Succ a) = Zero
    fw f = seq (f Zero) undefined
    bw !_ = undefined
instance Pure a => Conv (Succ a ^! Zero) where
    type Goal (Succ a ^! Zero) = Succ Zero
    fw f = Zero
    bw Zero = const Zero
instance Conv (Zero ^! Zero) where
    type Goal (Zero ^! Zero) = Succ Zero
    fw f = Zero
    bw Zero = id

大体同じパターンなのですが、0 の 0 乗が 1 になっていることに注意してください。集合論でも、空集合から空集合への写像はただ一つ（集合として見ると、空集合に対応する関数）であるので、そこから理解するのが分かりやすい気がします。まあ、圏論では恒等射は全ての対象にあるから、と言えば納得する人もいるかもしれません。

＊　＊　＊　＊　＊

お疲れ様でした。これが「実体のある型レベル自然数」の実装の全てです。ですがもう少し続けて、実体のある型レベル自然数を使ってちょっとだけ遊んで見ましょう。

まずは、計算が出来ているかどうか確かめてみましょう。便利な型シノニムを定義しておきます。

type (a :: k -> l) $ (b :: k) = a b
infixr 0 $
type I = Succ Zero
type II = Succ (Succ Zero)

GHCi でソースコードをロードして、計算をチェックします。

> :kind! ToNat $ Goal $ (I +! II) ^! (I +! II *! II)
ToNat $ Goal $ (I +! II) ^! (I +! II *! II) :: GHC.TypeLits.Nat
= 243

きちんと正しい結果が出て来ましたね！GHCi の応答も思いのほか速いはずです。

次に、ある型がちょうどフィボナッチ数個あることを表す型を作ります。Conv b という文脈を付けるために、GADT を使っています。

type Fib t = Fib' (Succ Zero) (Succ Zero) t
data Fib' a b t where
    DoneFib :: Conv b => (b -> t) -> Fib' a b t
    MoreFib :: Fib' b (a +! b) t -> Fib' a b t

これをリストに変換する関数は今や本当に簡単に作れます。

fibtolist :: Fib t -> [t]
fibtolist = go
    where
        go :: Fib' a b t -> [t]
        go (DoneFib x) = tolist x
        go (MoreFib y) = go y

(a +! b) の部分を変えれば、フィボナッチ数列に限らずいろいろな数列が表現できます（もちろん引き算と割り算は使えませんが）。

＊　＊　＊　＊　＊

以上の実装をまとめておきます。

{-# LANGUAGE
    BangPatterns,
    ScopedTypeVariables,
    DataKinds, PolyKinds,
    GADTs, TypeOperators, TypeFamilies,
    MultiParamTypeClasses,
    FlexibleContexts, FlexibleInstances, UndecidableInstances #-}

module Main (module Main) where

import GHC.TypeLits

type (a :: k -> l) $ (b :: k) = a b
infixr 0 $

type a +! b = Either a b
type a *! b = (a,b)
type a ^! b = b -> a
infixl 6 +!
infixl 7 *!
infixr 8 ^!

data Zero
data Succ a = Zero | Succ a
type O = Zero
type I = Succ O
type II = Succ I
type III = Succ II
type IV = Succ III
type V = Succ IV
type VI = Succ V
type VII = Succ VI
type VIII = Succ VII
type IX = Succ VIII
type X = Succ IX

o = Zero
i = Succ Zero
ii = Succ i
iii = Succ ii
iv = Succ iii
v = Succ iv
vi = Succ v
vii = Succ vi
viii = Succ vii
ix = Succ viii
x = Succ ix



class Pure a where
    type ToNat a :: Nat
    puretolist :: (a -> b) -> [b]
    listtopure :: [b] -> (a -> b)
instance Pure Zero where
    type ToNat Zero = 0
    puretolist f = []
    listtopure [] !_ = undefined
instance Pure a => Pure (Succ a) where
    type ToNat (Succ a) = ToNat a + 1
    puretolist f = f Zero : puretolist (f . Succ)
    listtopure (x : _) Zero = x
    listtopure (_ : xs) (Succ n) = listtopure xs n

type family ToPure (a :: Nat) where
    ToPure 0 = Zero
    ToPure n = Succ $ ToPure $ n-1



class Pure (Goal a) => Conv a where
    type Goal (a :: *) :: *
    fw :: a -> Goal a
    bw :: Goal a -> a

tolist :: Conv a => (a -> b) -> [b]
tolist f = puretolist (f . bw)
fromlist :: Conv a => [b] -> (a -> b)
fromlist xs = listtopure xs . fw

instance Conv Zero where
    type Goal Zero = Zero
    fw = id
    bw = id
instance Pure a => Conv (Succ a) where
    type Goal (Succ a) = Succ a
    fw = id
    bw = id

instance (Conv (o a b), Conv (Goal (o a b) +! c)) =>
                        Conv ((o :: * -> * -> *) a b +! c) where
    type Goal (o a b +! c) = Goal (Goal (o a b) +! c)
    fw (Left x) = fw (Left (fw x) :: Goal (o a b) +! c)
    fw (Right y) = fw (Right y :: Goal (o a b) +! c)
    bw n = case bw n of
        Left x -> Left (bw x)
        Right y -> Right y
instance (Pure a, Conv (o b c), Conv (Succ a +! Goal (o b c))) =>
                        Conv (Succ a +! (o :: * -> * -> *) b c) where
    type Goal (Succ a +! o b c) = Goal (Succ a +! Goal (o b c))
    fw (Left x) = fw (Left x :: Succ a +! Goal (o b c))
    fw (Right y) = fw (Right (fw y) :: Succ a +! Goal (o b c))
    bw n = case bw n of
        Left x -> Left x
        Right y -> Right (bw y)
instance (Pure a, Pure b, Conv (a +! Succ (Succ b))) =>
                        Conv (Succ a +! Succ b) where
    type Goal (Succ a +! Succ b) = Goal (a +! Succ (Succ b))
    fw (Left Zero) = fw (Right Zero :: a +! Succ (Succ b))
    fw (Left (Succ x)) = fw (Left x :: a +! Succ (Succ b))
    fw (Right y) = fw (Right (Succ y) :: a +! Succ (Succ b))
    bw n = case bw n of
        Left x -> Left (Succ x)
        Right Zero -> Left Zero
        Right (Succ y) -> Right y
instance Pure a => Conv (Zero +! a) where
    type Goal (Zero +! a) = a
    fw (Left !_) = undefined
    fw (Right x) = x
    bw x = Right x
instance Pure a => Conv (Succ a +! Zero) where
    type Goal (Succ a +! Zero) = Succ a
    fw (Left x) = x
    fw (Right !_) = undefined
    bw x = Left x

instance (Conv (o a b), Conv (Goal (o a b) *! c)) =>
                        Conv ((o :: * -> * -> *) a b *! c) where
    type Goal (o a b *! c) = Goal (Goal (o a b) *! c)
    fw (x, y) = fw (fw x, y)
    bw n = let (x, y) = bw n in (bw x, y)
instance (Pure a, Conv (o b c), Conv (Succ a *! Goal (o b c))) =>
                        Conv (Succ a *! (o :: * -> * -> *) b c) where
    type Goal (Succ a *! o b c) = Goal (Succ a *! Goal (o b c))
    fw (x, y) = fw (x, fw y)
    bw n = let (x, y) = bw n in (x, bw y)
instance (Pure a, Pure b, Conv (Succ b +! a *! Succ b)) =>
                        Conv (Succ a *! Succ b) where
    type Goal (Succ a *! Succ b) = Goal (Succ b +! a *! Succ b)
    fw (Zero, y) = fw (Left y :: Succ b +! a *! Succ b)
    fw (Succ x, y) = fw (Right (x, y) :: Succ b +! a *! Succ b)
    bw n = case bw n of
        Left y -> (Zero, y)
        Right (x, y) -> (Succ x, y)
instance Pure a => Conv (Zero *! a) where
    type Goal (Zero *! a) = Zero
    fw (!_, _) = undefined
    bw !_ = undefined
instance Pure a => Conv (Succ a *! Zero) where
    type Goal (Succ a *! Zero) = Zero
    fw (_, !_) = undefined
    bw !_ = undefined

instance (Conv (o a b), Conv (Goal (o a b) ^! c)) =>
                        Conv ((o :: * -> * -> *) a b ^! c) where
    type Goal (o a b ^! c) = Goal (Goal (o a b) ^! c)
    fw f = fw (fw . f)
    bw n = bw . bw n
instance (Pure a, Conv (o b c), Conv (Succ a ^! Goal (o b c))) =>
                        Conv (Succ a ^! (o :: * -> * -> *) b c) where
    type Goal (Succ a ^! o b c) = Goal (Succ a ^! Goal (o b c))
    fw f = fw (f . bw)
    bw n = bw n . fw
instance (Pure a, Pure b, Conv (Succ a *! Succ a ^! b)) =>
                        Conv (Succ a ^! Succ b) where
    type Goal (Succ a ^! Succ b) = Goal (Succ a *! Succ a ^! b)
    fw f = fw (f Zero, f . Succ)
    bw n = let (x, f) = bw n in \m -> case m of Zero -> x; Succ l -> f l
instance Pure a => Conv (Zero ^! Succ a) where
    type Goal (Zero ^! Succ a) = Zero
    fw f = seq (f Zero) undefined
    bw !_ = undefined
instance Pure a => Conv (Succ a ^! Zero) where
    type Goal (Succ a ^! Zero) = Succ Zero
    fw f = Zero
    bw Zero = const Zero
instance Conv (Zero ^! Zero) where
    type Goal (Zero ^! Zero) = Succ Zero
    fw f = Zero
    bw Zero = id



type Fib t = Fib' (Succ Zero) (Succ Zero) t
data Fib' a b t where
    DoneFib :: Conv b => (b -> t) -> Fib' a b t
    MoreFib :: Fib' b (a +! b) t -> Fib' a b t

fibtolist :: Fib t -> [t]
fibtolist = go
    where
        go :: Fib' a b t -> [t]
        go (DoneFib x) = tolist x
        go (MoreFib y) = go y



main = print 0

「実体のある型レベル自然数」を使えば、いろいろと楽しいことが出来るはずです。もしもこの記事をきっかけにもっと素晴らしいものが生まれたならば、本当に嬉しいかぎりです。