線形型つきドメイン特化言語 (DSL) を Haskell上に実装する

線形λ計算というのは、「変数をちょうど一度だけ使わなければならない」という線形型をもったλ計算だ。これを Haskell で実装してみた。「ファイルが開かれたら必ず閉じる」という制約のような、線形型 (linear type) が必要な DSL の実装の参考になるかもしれない。
線形λ計算の実装は、既に Olegさんがやっている。それは変数参照をde Bruijn indexを使って書くようになっている。
一方、この実装は、よりHaskellに近い記法で書けるようになっている。

使用例

λ抽象の前に lam, 関数適用の前に app, 変数参照の前に var が必要である以外は Haskell と同じ記法で書ける。

Linear Lambda Calculus の頭文字をとって LLC モナドという名前にしてある。

LLCモナドの型は LLC t ii jj a となっていて、

t

型のタグ。他のLLCと混ざらないようにするため

ii, jj

LLCモナドの事前条件と事後条件。 線形性をエンコードするために使っている.

a

モナドが持っている値。

という役割を果たしている。

また a :-> b は線形な(?) 関数で、引数が一度しか使われないことを表している。

他に、どうしても出てくる変な型クラスが2つある。

HList ii n

型レベルリストiiの長さがn.

Consume ii jj

線形性をエンコードするために使っている。

こんな感じになる。

-- \a -> \b -> a b
t1 = lam (\a -> lam (\b -> app (var a) (var b)))
-- t1 :: (HList ss' n, Consume xs' xs') => LLC t xs' xs' ((a :-> b) :-> (a :-> b))

-- \a -> a+1
t2 = lam (\a -> app (inj1 (+1)) (var a))
-- t2 :: (HList xs' n, Consume xs' xs', Num a) => LLC t xs' xs' (a :-> a)

-- (\a -> a+1) 1
t3 = app t2 (inj0 1)
-- t3 :: (HList kk n, Consume kk kk, Num b) => LLC t kk kk b
--
-- *Main> (run t3 :: IO Int)
-- 2

-- 線形性の違反は GHCの型エラーとして報告される。
-- 例えば 次の例は 変数 b を使っていないので型エラーになる。
--
-- :t lam (\a -> lam (\b -> var a))
-- <interactive>:1:23:
--     Couldn't match type `F a0' with `U'
--     When using functional dependencies to combine
--       UpdateR (xs :> s) (S n) t (xs' :> s),
--         arising from the dependency `xs n t -> xs''
--         in the instance declaration at Linear.hs:83:10
--       UpdateR ((xs' :> F a_e) :> F a0) (S O) U ((xs' :> U) :> U),
--         arising from a use of `var' at <interactive>:1:23-25
--     In the expression: var a
--     In the first argument of `lam', namely `(\ b -> var a)'

-- 次の例は変数 b を2回使っているので型エラー
-- :t lam (\a -> lam (\b -> app (var a) (app (var a) (var b))))
-- <interactive>:1:41:
--     Couldn't match type `U' with `F (a0 :-> a1)'
--     In the first argument of `app', namely `(var a)'
--     In the second argument of `app', namely `(app (var a) (var b))'
--     In the expression: app (var a) (app (var a) (var b))

t4 = lam (\a -> app (io1 putStrLn) (var a))
-- t4 :: (HList xs' n, Consume xs' xs') => LLC t xs' xs' (String :-> ())

ソース

{-# LANGUAGE 
    MultiParamTypeClasses,FunctionalDependencies,FlexibleInstances,FlexibleContexts,
    UndecidableInstances,OverlappingInstances,NoMonomorphismRestriction,Rank2Types,
    TypeOperators,EmptyDataDecls,KindSignatures,TypeFamilies
    #-}

-- * 線形λ計算をHaskellに埋め込んでみた by @keigoi
--
-- 型付きのドメイン特化言語 (DSL) を Haskellに埋め込んでみる例。
-- 
-- プログラミングにおいて、「このファイルハンドルは必ず閉じる」などという制約を
-- 付与したくなることは多い。
-- このような制約は線形型 (linear type) で実現できるが、Haskellには線形型がないので、
-- 普通のphantom typeの方法ではそういうEDSL を Haskellの上に作ることはできない．
--
-- このコードでは、Oleg の Heterogeneous List のテクニックを使って、
-- 線形性をもつ型システムを Haskell 上に実現する方法を示す．
--
-- 埋め込まれるのは線形λ計算といって、全ての変数をちょうど1回だけ使わなければいけない型システムだ。
-- このコードは Oleg Kiselyov の http://okmij.org/ftp/tagless-final/course/LinearLC.hs 
-- を参考にしている．
-- これも線形型の埋め込みを達成している． その方法は de Bruijn indexに基づくもので、
-- 例えば @lam (lam (app (s z) z))@ は @(\x -> \y -> x y)@ のように書く．
--
-- このコードでは HList (http://okmij.org/ftp/Haskell/types.html#HList) を応用して、
-- もうちょっとプログラマーフレンドリーな形で書けるようになる．
-- たとえば, @(\x -> \y -> x y)@ は @lam (\x -> (\y -> app (var x) (var y))@ と書かれ、
-- これは Haskell の記法に近いのでうれしいはずである．
-- 
-- (ghc-7.0.3で確認したが、 悲しいことに ghc-6.8.2 さんはパニックになってしまう。)

-- | 型レベルの 0 
data O = O deriving Show
-- | 型レベル +1. @'S' n@ は @(n+1)@ を表す.
data S n = S n deriving Show

-- | 型レベル引き算。 HListの操作で、リストを後ろから数えるために使う。
class Sub a b c | a b -> c where
  sub :: a -> b -> c
-- 普通に引き算を定義するとこうなるが、そうすると GHCの型推論が途中で止まってしまい
-- @Sub n n m@ みたいなインスタンスが文脈に残ってしまう。 ここで n-n=0 なので m = O と推論されてほしいのに…。
{-
instance Sub n O n where
  sub n _ = n
instance Sub n m x => Sub (S n) (S m) x where
  sub ~(S n) ~(S m) = sub n m
-}
-- 仕方がないので n-n=0, (1+n) - n = 1, .. などと GHCに教えてあげることにする．
instance Sub n n O where sub _ _ = O
instance Sub (S n) n (S O) where sub _ _ = S O
instance Sub (S (S n)) n (S (S O)) where sub _ _ = S (S O)
instance Sub (S (S (S n))) n (S (S (S O))) where sub _ _ = S (S (S O))
-- and so on..


-- | 型レベル snoc (コンス @(:)@ の左右逆). @xs :> x@ は リスト @xs@ のしっぽに @x@ を加えたリストを表す．
data xs :> x = xs :> x
-- | 型レベル空リスト． (@[]@). 
data Nil = Nil


-- | 長さ @n@ の型レベルリスト. HList と違うのは cons でなく snoc を使っていること． 
--   これは見た目の問題であり別に cons でもかまわない．
class HList xs n | xs -> n where
  len :: xs -> n
instance HList xs n => HList (xs :> x) (S n) where
  len ~(xs :> x) = S (len xs)
instance HList Nil O where
  len _ = O


-- | リスト xs の n 番目の要素を s とする． ここで n 番目とは左から右に数えている
class Pickup xs n s | xs n -> s where
  pickup :: xs -> n -> s
instance (HList xs l, Sub l (S n) m, PickupR xs m s)
    => Pickup xs n s where
  pickup xs n = pickupR xs (sub (len xs) (S n))

-- | Pickupの逆順. リスト xs の n 番目の要素を s とする． ここで n 番目とは右から左に数えている
class PickupR xs n s | xs n -> s where
  pickupR :: xs -> n -> s
instance xs ~ (xs':>t) => PickupR xs O t where
  pickupR (_ :> t) _ = t
instance (PickupR xs' n t, xs ~ (xs':>s')) => PickupR xs (S n) t where
  pickupR (xs' :> _) (S n) = pickupR xs' n

-- | リスト xs の n 番目の要素を t に置き換えたものを xs' とする． ここで n 番目とは左から右に数えている
class Update xs n t xs' | xs n t -> xs' where
  update :: xs -> n -> t -> xs'
instance (HList xs l, Sub l (S n) m, UpdateR xs m t xs') 
 => Update xs n t xs' where
  update xs n t = updateR xs (sub (len xs) (S n)) t

-- | Updateの逆順．
class UpdateR xs n t xs' | xs n t -> xs' where
  updateR ::  xs -> n -> t -> xs'
instance UpdateR (xs:>s) O t (xs:>t) where
  updateR (xs:>_) _ t = xs :> t
instance UpdateR xs n t xs' => UpdateR (xs:>s) (S n) t (xs':>s) where
  updateR (xs:>s) (S n) t = updateR xs n t :> s


---- ここから線形型のはなし

-- | まだ使われていない変数
newtype F a = F a
-- | 使用済み
data U = U
-- | 線形な (引数が一度だけ使われる) 関数
newtype a :-> b = Arr { ext :: a -> IO b }


-- | An indexed monad. @ii@ と @jj@ は 計算の直前と直後の 各変数の状態を示している。
--   たとえば @LLC t (xs :> F Int) (xs :> U) a@ は リストの最後にある
--   Int型の変数がただ一度だけ使われることを示している．
--   t はrunが混ざらないようにするためのタグで、よくあることなので気にしない．
newtype LLC t ii jj a = LLC { run' :: ii -> IO (jj,a) }

-- | 自由変数を含まないLLCの項を実行する．
run :: forall a n jj. (forall t. LLC t Nil Nil a) -> IO a
run s = case s of LLC m -> m Nil >>= \(_,a) -> return a

-- | 変数の型。 たとえば lam (\x -> t) の x は Var n型をもつ．この n は型レベル自然数である．
-- 
--   線形ラムダ計算の変数は一度しか使ってはいけないので、
--   変数に直接その型を付けるのではなく、HListに型を格納しておいて、そこを指すインデックスに型を格納する．
--   その変数を一度使ったら HList が書き換えられ、二度と使えないようになる。
--   そのようにして、線形型の型付けを実現している．
newtype Var n = Var n

infixr 6 :->

-- | 元記事の型クラス `HiHo' ． 
--   ラムダ抽象において
class Consume ii jj where
  consume :: ii -> jj
instance Consume Nil Nil where
  consume _ = Nil
instance Consume ii jj => Consume (ii:>F a) (jj:>F a) where
  consume (ii:>i) = consume ii :> i
instance Consume ii jj => Consume (ii:>F a) (jj:>U) where
  consume (ii:>_) = consume ii :> U

-- | ラムダ抽象
lam :: (HList ii n, Consume ii jj) => (Var n -> LLC t (ii:>F a) (jj:>U) b) -> LLC t ii jj (a :-> b)
lam f = LLC (\ii -> return (consume ii, Arr $ \a -> run' (f (Var $ len ii)) (ii:>F a) >>= \(_,b) -> return b))
    
-- | 関数適用
app :: LLC t ii jj (a :-> b) -> LLC t jj kk a -> LLC t ii kk b
app f x = LLC (\ii -> run' f ii >>= (\(jj,Arr f') -> run' x jj >>= \(kk, x') -> f' x' >>= \b -> return (kk, b)))

-- | 変数の使用
var :: (Pickup ii n (F a), Update ii n U jj) => Var n -> LLC t ii jj a
var (Var n) = LLC (\ii -> return (update ii n U, case pickup ii n of F x -> x))

-- | 定数
inj0 :: x -> LLC t ii ii x
inj0 x = LLC (\ii -> return (ii, x))

-- | 関数定数
inj1 :: (x -> y) -> LLC t ii ii (x :-> y)
inj1 f = LLC (\ii -> return (ii, Arr $ \x -> return (f x)))

-- | 副作用が使える関数定数
io1 :: (x -> IO y) -> LLC t ii ii (x :-> y)
io1 f = LLC (\ii -> return (ii, Arr f))


-- * 例

-- \a -> \b -> a b
t1 = lam (\a -> lam (\b -> app (var a) (var b)))
-- t1 :: (HList ii' n, Consume ii' ii') => LLC t ii' ii' ((a :-> b) :-> (a :-> b))

-- \a -> a+1
t2 = lam (\a -> app (inj1 (+1)) (var a))
-- t2 :: (HList ii' n, Consume ii' ii', Num a) => LLC t ii' ii' (a :-> a)

-- (\a -> a+1) 1
t3 = app t2 (inj0 1)
-- t3 :: (HList kk n, Consume kk kk, Num b) => LLC t kk kk b
--
-- *Main> (run t3 :: IO Int)
-- 2


-- 線形性の違反は GHCの型エラーとして報告される。
-- 例えば 次の例は b を使っていないので型エラーになる。
--
-- :t lam (\a -> lam (\b -> var a))
-- <interactive>:1:23:
--     Couldn't match type `F a0' with `U'
--     When using functional dependencies to combine
--       UpdateR (ii :> s) (S n) t (ii' :> s),
--         arising from the dependency `ii n t -> ii''
--         in the instance declaration at Linear.hs:83:10
--       UpdateR ((ii' :> F a_e) :> F a0) (S O) U ((ii' :> U) :> U),
--         arising from a use of `var' at <interactive>:1:23-25
--     In the expression: var a
--     In the first argument of `lam', namely `(\ b -> var a)'

-- 次の例はbを2回使っているので型エラー
-- :t lam (\a -> lam (\b -> app (var a) (app (var a) (var b))))
-- <interactive>:1:41:
--     Couldn't match type `U' with `F (a0 :-> a1)'
--     In the first argument of `app', namely `(var a)'
--     In the second argument of `app', namely `(app (var a) (var b))'
--     In the expression: app (var a) (app (var a) (var b))



t4 = lam (\a -> app (io1 putStrLn) (var a))
-- t4 :: (HList ii' n, Consume ii' ii') => LLC t ii' ii' (String :-> ())

main = run (app t4 (inj0 "Hello, World!!"))