モナドなしで一意名生成

haskell

Haskellで形式言語を扱う場合、四則演算を許す数式程度なら代数的データ型が非常に良く抽象構文を表現できるが、名前の束縛が必要になるととたんに面倒なことになる。名前の衝突が厄介なので、各変数に一意の記号を付けたいのだが、たとえばData.UniqueはIOモナドだし、似た機構を自分で作るにしても大域状態を扱う必要がある。これは(\x -> x)のような閉じた式を表現するデータを作るのにも大域状態を参照しないといけないということで、非常に不便だ。

解決の方向はいくつか考えられるが、なんとかして一意な名前の生成を手軽にできないか考えてみる。単純にnewUniqueをunsafePerformIOでIOモナドの外から無理矢理呼ぶのは、参照透明性を無茶苦茶に破壊するので話にならない。そこで少し工夫する。

fresh :: (Unique -> a) -> a
fresh f = f $ unsafePerformIO newUnique

意図としては、得られたUniqueをfの中のみで使ってくれるのなら、unsafePerformIO newUniqueが毎回異なる値に評価されるという事実に気づかないで済むのではないかというものである。参照透明性が破れていることに気づかないなら、参照透明性は破れていないようなものだろう。

しかし生成されたUniqueがfから漏れない保証はない。実際、fresh idとすれば毎回異なるUniqueが得られる。fの戻り値を適当な型に固定すればこの問題は解消されるが、それでは一般には使いにくすぎる。

そこで、runSTからSTRefが漏れないように保証するために使われている技を真似てみる。引数を一つ持つ新しい型MyUniqueを定義し、fとしてはそのパラメタに関して全称量化されたもののみを認める。

newtype MyUnique s = MU Unique
  deriving (Eq, Ord)

fresh :: (forall s. MyUnique s -> a) -> a
fresh f = f $ MU $ unsafePerformIO newUnique

これで、freshから不用意にMyUniqueが漏れることはないはずだ。しかし、これでは出所の異なる二つのMyUniqueは、型が違うので比較することができない。本末転倒である。

MyUnique sのsが、一意な名前の有限集合を表すと思ってみる。MyUnique sの値はその集合のどれかの要素を表す。sがtの部分集合なら、MyUnique sの値はMyUnique tの値としても解釈できる。これはMyUnique s -> MyUnique tの関数が存在することを意味する。この関数をembedと名付け、クラスメソッドにする。

{-# LANGUAGE RankNTypes, MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables #-}
module MyUnique(MyUnique, Subset, embed, fresh, fresh1, EmptySet)  where

import Data.IORef
import System.IO.Unsafe

newtype MyUnique s = MU Integer
  deriving (Ord, Eq)

class Subset s t where
  _embed :: MyUnique s -> MyUnique t

instance Subset s (Wrapper s) where
  _embed (MU u) = MU u

data Wrapper s = Wrapper

embed :: (Subset s t) => MyUnique s -> MyUnique t
embed = _embed

data EmptySet = EmptySet

{-# NOINLINE uniqueSupply #-}
uniqueSupply :: IORef Integer
uniqueSupply = unsafePerformIO $ newIORef 0

fresh :: forall s a. (forall t. (Subset s t) => (MyUnique t -> Maybe (MyUnique s)) -> MyUnique t -> a) -> a
fresh f = unsafePerformIO $ do
  u <- atomicModifyIORef uniqueSupply $ \s -> (s+1, s)
  return $ f (\(MU k) -> if k == u then Nothing else Just (MU k)) (MU u :: MyUnique (Wrapper s))

fresh1 :: forall s a. MyUnique s -> (forall t. (Subset s t) => (MyUnique t -> Maybe (MyUnique s)) -> MyUnique t -> a) -> a
fresh1 _ = fresh

embedでなく_embedをクラスメソッドにしているのはモジュール外でインスタンスを作られないため。fresh1の最初の引数は型変数sの値を手軽に指定するためのダミーである。Wrapperは型検査器を納得させるためだけの存在。

これでひとまず動作するものができた。

import MyUnique

main =
  fresh1 (undefined :: MyUnique EmptySet) $ \_ u0 ->
  fresh1 u0 $ \_ u1 ->
  fresh1 u1 $ \_ u2 ->
  let
    x0 = embed (embed u0 `asTypeOf` u1)
    x1 = embed u1
    x2 = u2
  in print [x0 == x1, x0 == x2, x1 == x2, x2 == x2]

残る課題は、

  • これは本当に便利なのか？
  • 安全なのか？参照透明性は破られていないのか？
    • これはどうやって調べるんだろう。あるいは参照透明性が破られていないことの証明はどうするのか。そもそも参照透明性の定義って何だっけ。
  • fに渡しているMyUnique t -> Maybe (MyUnique s)という関数はembedの逆だが、これをSubsetのクラスメソッドにしたい。そのためには値を型でエンコードする必要がありそうだ。また依存型か！
  • fが渡された一意名を使うときは、内部で利用を完結させるか、存在型に包んで外に出すしかない。つまり利用法が制限されていて、Data.Uniqueのような一意名の無制限な利用はできない(IOでないので当然とも言える)。これで構文を扱うなら、名前を一時的にしか使わない手法、つまりHigher Order Abstract Syntaxとかlocally nameless(自由変数は名前で呼び、局所変数はDe Bruijn index)とかが合うように思える。いずれにせよ実証コードを書かないといけない。

とりあえずここまで。