『Ghosts of Departed Proofs』
2018/7
Ghosts of Departed Proofsという技法についての論文
論文中に登場する「GDP」はこれのことを指す
この論文に用いられているコード
ただし、論文内で型しか示されてないものは、コード内も型しかない
大まかな流れ
Abstract
前提条件のある関数を「Ghosts of Departed Proofs (GDP)」を用いて定義する
前提条件を満たしていることを幽霊型を用いて表す
型で表現できるので、実行時オーバーヘッドはない
特に、依存型や線形型などの強力な型システムを使わずに設計する
1 Introduction
目標は、ライブラリ作者として、人間工学的に、安全なAPIを設計すること
GDPの特徴
Properties and proofs are represented in code.
Proofs carried by phantom type parameters.
Library-controlled APIs to create proofs.
Combinators for maipulating ghost proofs.
2 Case Study 1: Sorted Lists
2つのsort済みリストをmergeする関数を、GDPで設計する
ここで、GDPに使ういくつかの便利関数(
name , the )や型 Named を導入する3 Case Study 2: Sharing State Threads
Section 3とSection 4は、あまり望ましくない例として書かれている
型安全だが、ちょっと不便
GDPを使ってSTモナドを拡張する例
STモナドで扱う
s を2つにして、型でアクセス制限を行う4 Case Study 3: Key-value Lookups
GDPを使って、Mapをlookupする時に、keyが存在することを型で保証する
5 Case Study 4: Arbitrary Invariants
Section 2, 3, 4で示したものを統括して扱う仕組みを考える
「型に付けた型レベルの名前」と「それに付与する証明」を分離できるようにする
型 ~~ 名前 ::: 証明 という型を書く6 Related Work
7 Summary
>#WIP
Section 2までは嬉しさは理解できる
Sortの例は良いと思う
Section 5のheadの定義はどこまで実用的なのか不明
読みメモ
Abstract
前提条件のある関数をどう定義するか？
head のように部分関数を定義するか Maybe などで失敗しうることを返り値で示すか「Ghosts of Departed Proofs」という概念についての説明をする
検証済みであることを幽霊型で表す
型で済むので実行時のオーバーヘッドがない
1 Introduction
強力な型システムを使わずとも普通のHaskellの型システムで恩恵を受けられる
目標は、ライブラリ作者として、ergonimic(人間工学的)に、安全なAPIを設計すること
ここでの「安全な」とは実行時エラーを起こさないこと
ergonimicとは、利用者に過度の負担をかけないこと
GDPの利用のケーススタディ
APIの間違った使用はコンパイルエラー
いくつかのアプローチ
gdpEndpts のコードの解説はSection 5にあるGhosts of Departed Proofsの特徴
Properties and proofs are represented in code.
Proofs carried by phantom type parameters.
ここでのcarryはprops drilingみたいな意味合いで言っている
関数を連鎖していく時に、その証明済みの型で定義することで、安全な値が複数の関数を通っていくイメージ
幽霊型を使うことで、ランタイムのオーバーヘッドがない
Library-controlled APIs to create proofs.
ライブラリの作者は、そのAPIの動作に関する公理を導入できる唯一の存在者であるべき
具体例を見ないと微妙に何を言っているかわからない #??
型を公開せずに、関数のみを公開するみたいな話か？
Combinators for maipulating ghost proofs.
2 Case Study 1: Sorted Lists
name はsmart constructorrank-2 typeで存在型のエミュレート #??
2.4でちょっと解説されていた
rank2を使うことで、利用者に任意のnameを付けさせずに、nameを与えることができる
コンパイラがexistな名前をつける感じになる
nameは名前を付けた値を直接返すのではなく、「あなたがその名前のついた値で何をしたかったのか言ってください、そうすればあなたのためにそれをします」とユーザーに言う。
どういうこっちゃ
例
hsmodule Sorted (Named, SortedBy, sortBy, mergeBy) where
import The
import Named
import Data.Coerce
import qualified Data.List as L
import qualified Data.List.Utils as U
newtype SortedBy comp a = SortedBy a -- compでsort済みであることを表す
instance The (SortedBy comp a) a
sortBy :: ((a -> a -> Ordering) ~~ comp) -- 名前付きcomparator. compoと名付けられたcompartorと読める
-> [a]
-> SortedBy comp [a] -- このcompでsortされたことを表す
sortBy comp xs = coerce (L.sortBy (the comp) xs)
mergeBy :: ((a -> a -> Ordering) ~~ comp)
-> SortedBy comp [a]
-> SortedBy comp [a]
-> SortedBy comp [a]
mergeBy comp xs ys =
coerce (U.mergeBy (the comp) (the xs) (the ys)) mergeBy 3つの引数からnameを取り除いて普通にmergeByしたあとに、
coerceと型宣言によって、
SortedBy comp [a] に戻してから返しているランタイムから見れば、普通のmergeBy'を実行しているのと何も変わらない
sortByが一種のsmart constructorのような役割を担っている
使用する
HsgdpMain :: IO ()
gdpMain = do
let xs = [1..5]
ys = reverse [1..5]
name (comparing Down) $ \gt -> do -- gt::(a->a->Ordering)~name
let xs' = sortBy gt xs
ys' = sortBy gt ys
print (the (mergeBy gt xs' ys')) name によって、 gt にスコープの決められたnameが付与されている gt が、名前付きの compring Down になっている比較対象として、通常のmergeBy'を使った場合
hsmain :: IO ()
main = do
let xs = [1..5]
ys = reverse [1..5]
gt = comparing Down
print (mergeBy' gt xs ys) -- [5,4,3,2,1,2,3,4,5,1]使用感は同じである
main の方は、 ys がsortされていないので、結果は間違ったものになるもちろんコンパイルエラーは出ないのでそれに気付け無い！！！
ソートの方法が間違っている例
hsng = do
name compare $ \up ->
name (comparing Down) $ \down ->
let list1 = sortBy up [1,2,3:: Int]
list2 = sortBy down [1,2,3]
in
the (mergeBy up list1 list2) -- type error!これどうなん？
hs-- comp指定してないから、miniumの結果5になって違うじゃん
miss :: IO ()
miss = do
let xs = reverse [1..5]
name (comparing Down) $ \gt -> do
let xs' = sortBy gt xs
print (minimum_O1 xs')
minimum_O1:: SortedBy comp [a]-> Maybe a
minimum_O1 xs = case the xs of
[] -> Nothing
(x:_) -> Just xいや、これも仕様的には正しいと言えるのか。
Downに対するミニマムだから
何かしらのsortがされている保証を満たしているので
3 Case Study 2: Sharing State Threads
Section 3とSection 4は、あまり望ましくない例として書かれている
GDPを使ってSTモナドを拡張する
この論文内では、曖昧さ回避のため(
ST ではなく) St とする2つの共有メモリ
(s,s') を操作するAPIを設計しているLeft側では両方のメモリ内を操作できるが、Rightでは片方しか操作できないように型で制限している
hsdata Region = Region
type St s a = State (Region ~~ s) a
runSt :: (forall s. St s a) -> a
runSt action = name Region (evalState action)
newRef :: a -> St s (STRef s a)
newRef = undefined
readRef :: STRef s a -> St s a
readRef = undefined
writeRef :: STRef s a -> a -> St s ()
writeRef = undefined
runSt2 :: (forall s s'. St (s, s') a) -> a
runSt2 action = undefined
liftL :: St s a -> St (s,s') a
liftL = undefined
liftR :: St s' a -> St (s,s') a
liftR = undefined
share :: STRef s a -> St s (STRef (s,s') a)
share = undefined
use :: STRef (s,s') a -> STRef s a
use = undefined
symm :: STRef (s,s') a -> STRef (s',s) a
symm = undefined
stSharing :: Bool
stSharing = runSt2 $ do
(secret, ref) <- liftL $ do
unshared <- newRef 42
shared <- share =<< newRef 17
return (unshared, shared)
liftR $ do
let mine = use (symm ref)
x <- readRef mine
writeRef mine (x + 1)
liftL $ do
check <- readRef secret
return (check == 42)4 Case Study 3: Key-value Lookups
Section 3とSection 4は、あまり望ましくない例として書かれている
Mapをlookupする時に、keyが存在することを型で保証したい
hs-- type Diagraph v = Map v [v]
type Digraph vs v = JMap vs v [Key vs v]hsnewtype JMap ks k v = JMap (Map k v) deriving Functor
newtype Key ks k = Key k
instance The (JMap ks k v) (Map k v)
instance The (Key ks k) k
member :: k -> JMap ks k v -> Maybe (Key ks k)
member = undefined
lookup:: Key ks k -> JMap ks k v -> v
lookup = undefined
reinsert:: Key ks k -> v -> JMap ks k v -> JMap ks k v
reinsert = undefined
withMap:: Map k v -> (forall ks. JMap ks k v -> t) -> t
withMap _ _ = undefined ks はkey set Key ks k ks というkey setに k が存在することを示す型 JMap ks k v ks というkey setを持つ Map k v withMap name と似た役割ksをMapにアタッチする
member keyがksに存在するかどうか判定
lookup 安全なlookup
特定のkは、一つのMapの中にのみ属すことも保証する
5 Case Study 4: Arbitrary Invariants
これまで2種類の方法を示した
name 自体をを使うもの runST2 や withMap のようなlibraryが用意したrank 2の関数を使うものSection 3とSection 4は、あまり望ましくない例として書かれている
「型に付けた型レベルの名前」と「それに付与する証明」を分離できるようにする
a ~~ n ::: p と表記する a は、元々の型 n という型レベルの名前を持つ p は証明で、この条件を満たすことを表すことを表現するこれを使うことで、任意の条件を幽霊型として符号化できる
hsgdpHead :: ([a] ~~ xs ::: IsCons xs) -> a
gdpHead xs = head (the xs)引数
[a] は、 IsCons xs を満たすものである xs という名前が付いているため、これを型の定義内で使い回せる(上記のコードでは使いまわしてはいない)
更にこの例だと、元の
Prelude.head の定義をそのまま使い回せる NonEmpty a と [a] で同じ関数の再定義が不要になっているでもこれ、結局パターンマッチ出てるし、そんなに嬉しいか？
ここに
Proof p という証明を用意すると、 a ::: p で、 a に証明を適用できるlibraryの提供者はLiquidHaskellやhs-to-coqを使って、型の正当性を確認すればいい
エンドユーザーは知る必要はない
普通に使える
Defn が出てきた辺りからよくわからんくなってきたなreflectionとの組み合わせ
この辺から、応用すぎて何を言っているのか理解できない
6 Related Work
7 Summary
headに関してGhosts of Departed Proofsを使う嬉しさは何なのか