幽霊型とrank-2 typesで型安全なスコープを作る
>#WIP
タイトルが雑なので直す
幽霊型とrank-2 typesを組み合わせたテクニック
スコープを作るのに使っている？
登場はSTモナドの方が先(90年代)
理解する分には前者のほうがわかりやすいのでは？
モナドがないのでノイズが小さい
『Ghosts of Departed Proofs』のSection 2で出てきた例
hsnewtype Named name a = Named a -- nameという幽霊型
type role Named nominal nominal
type a ~~ name = Named name a
name :: a -> (forall name. a ~~ name -> t) -> t
name x k = k (coerce x)
-- 使用する
gdpMain :: IO ()
gdpMain = do
let xs = [1..5]
ys = reverse [1..5]
name (comparing Down) $ \gt -> do
let xs' = sortBy gt xs
ys' = sortBy gt ys
print (the (mergeBy gt xs' ys'))使用する側を見ればわかりやすい
name でスコープを作っている comparison Down という関数に gt という名前を付けている gt という名前は、このスコープの中でのみ使用できる name 関数の定義rank-2 typeを使って、
name という幽霊型を生成している利用者に任意のnameを付けさせずに、nameを与えている
existなnameを指定している感じ
rank-2 typeを使わない場合、以下のような定義になる
hsany_name :: a -> (a ~~ name)
any_name = coerceしかし、これだと利用者が自在にnameを付けられるため、安全でなくなる
2.4節で解説されている
存在型のエミュレート
hsnewSTRef :: a -> ST s (STRef s a)
runST :: (forall s. ST s a) -> a
runST' :: ST s a -> a -- ダミー. この関数は存在しない. newSTRef で生成した参照をSTモナドのスコープの外に持ち出そうとした時hsrunST $ newSTRef 1 -- error
runST' $ newSTRef 1 -- okSTモナドの方は2つポイントがある
newSTRef で、 s が2つ使われている点>これは、ST の s を参照型 STRef にタグ付けすることで、STRef が ST の s に依存するという関係を作り出していたのです。ref
だからなんなんだ #??
runST で、rank-2 typeが使わている点参照をrunSTの外側に持ち出すことを禁止している
仮に、runSTがrank-1 typeな場合
hsv = runST' (newSTRef "abc") -- v :: STRef s String
foo = runST' (readSTRef v) -- foo :: String == "abc"
-- runST :: (forall s. ST s a) -> a
runST' :: ST s a -> a
runST' st = undefined参照
v を、STモナドの外に持ち出して、参照の使い回しができてしまっている参照はmutable変数のようなものなので、モナドの外部に持ち出すと純粋性が失われる
s が多相的なまま runST は、任意の
s に対して a の型が決まるならば、 ST s を外す、という動作をしている
>ST s aのsに具体的な型を指定してしまうとrunSTが使えなくなります。
>必ず破壊的な操作にはパラメータ s が多相的なまま残るようになっている．そして， runST はその多相的なまま残った s に対して， s によらずに a の型が決まるならば ST s を外せることにしている．そして， s によらずに a の型が決まる場合に，破壊的操作で生まれた配列のインスタンスやリファレンスが実行時にどのような実体を持っていようとも，結果が決定的になることを保証できるよう， API がうまく設計されている
こう書いたほうが「スコープ感」がわかりやすい？
hs-- ok
ok = runST $ do
n <- newSTRef 0
forM_ [1..10] $ \i -> do
modifySTRef n (+i)
readSTRef nhs-- error
ng = runST $ do -- runST $ newSTRef 0 と同じ
n <- newSTRef 0
return n参照は、1つの
runST に対してlocalでないといけないなぜ幽霊型が必要になるのか？
どこで
存在型との関係
型システム的に高度なことが凝縮されている
rank 2 type
幽霊型
直感的理解
関係ある？