全体ミーティング 2010/05/19 渡邊 裕貴.

Presentation on theme: "全体ミーティング 2010/05/19 渡邊 裕貴."— Presentation transcript:

1 全体ミーティング 2010/05/19 渡邊 裕貴

2 今日の内容 Haskell の型システムの拡張について それを利用して実装された type-preserving compiler について
Generalized algebraic data types (GADT) Type families それを利用して実装された type-preserving compiler について “A type-preserving compiler in Haskell.” L.J. Guillemette and S. Monnier. ICFP 2008.

3 Haskell の ADT (普通のバリアント)
リストの例 List 型のコンストラクタとして Nil と Cons を定義 data List a = Nil | Cons a (List a) ちなみに OCaml では type 'a list = Nil | Cons of 'a * 'a list

4 Haskell の ADT (普通のバリアント)
コンストラクタを リストを返す関数と見なすと data List a where Nil :: List a Cons :: a -> List a -> List a ここは型変数 a でなければいけない ここを拡張したい

5 Generalized algebraic data types (GADT)
コンストラクタの戻り値の型パラメータを指定できる GHC よる拡張 式を表すデータ型の例 data Term a where IntLiteral :: Int -> Term Int Add :: Term Int -> Term Int -> Term Int Eq :: Term Int -> Term Int -> Term Bool IfThenElse :: Term Bool -> Term a -> Term a -> Term a First-class phantom types または guarded recursive data types ともいう

6 GADT (続き) 式を評価する関数の例 eval :: Term a -> a eval (IntLiteral v) = v eval (Add a b) = eval a + eval b eval (Eq a b) = eval a == eval b eval (IfThenElse c t f) = if eval c then eval t else eval f パターンマッチング時に型が正しく refine される ので、この関数は well-typed である 個々のマッチングパターンにおいて、型パラメータが適切に推論される

7 GADT (続き) 実用例 バージョン管理システム darcs で パッチの等価性を型で定式化して扱うのに 使われているらしい……
data Pair a b where Pair :: a -> b -> Pair a b SymmetricPair :: a -> a -> Pair a a foo :: Pair a b -> b foo (Pair x y) = y foo (SymmetricPair x y) = x p. 14 より引用、一部改変

8 Type families 型から型への関数のようなもの 型で自然数の加算を表現する例 GHC による拡張
data Zero data Succ a type family Add a b type instance Add Zero a = a type instance Add (Succ a) b = Succ (Add a b) あくまでも型なので、コンパイル時に計算される コンストラクタのない型 Coq でやるなら、Zero と Succ を Prop として inductive に定義する必要がある。

9 Bounded vectors 要素数を型で表すリスト data Vec e len where Nil :: Vec e Zero
Cons :: e -> Vec e len -> Vec e (Succ len) vappend :: Vec e n -> Vec e m -> Vec e (Add n m) vappend Nil ys = ys vappend (Cons x xs) ys = Cons x (vappend xs ys) vec1 :: Vec Char (Succ (Succ Zero)) vec1 = vappend (Cons '1' Nil) (Cons '2' Nil)

10 Generic map キーの型に応じてデータ構造を変えるマップ data family GMap k v
data instance GMap Int v = GMapInt [(Int, v)] -- GMapInt :: [(Int, v)] -> GMap Int v data instance GMap () v = GMapUnit (Maybe v) -- GMapUnit :: Maybe v -> GMap () v data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v) -- GMapEither :: GMap a v -> GMap b v -> GMap (Either a b) v

11 A type-preserving compiler in Haskell
Haskell で書かれた type-preserving compiler Haskell の型システムを用いて type preserving を証明 その中で GADT や type families を使っている 入力言語: System F (型多相なラムダ計算) 出力言語: ??? アセンブリを吐くところまではできていないらしい

12 レジスタ割当、機械語生成、最適化は future work
コンパイルの流れ CPS 変換 De Bruijn index 化 クロージャ変換 Hoisting 今日はアルゴリズムの話はなし レジスタ割当、機械語生成、最適化は future work

13 対象言語の内部表現 Higher-order abstract syntax (HOAS) De Bruijn indices
いずれの形式も 対象言語で well-typed でない式は Haskell の式としても well-typed でない コンパイルの過程の最初の方では HOAS を用い、途中から de Bruijn に移行

14 Let (Add (Num 1) (Num 2)) (λx. Add x (Num 3))
コードの表し方 (1) Higher-order abstract syntax (HOAS) 対象言語での変数束縛を Haskell 内での束縛に直す data Exp t where Add :: Exp Int -> Exp Int -> Exp Int Let :: Exp t1 -> (Exp t1 -> Exp t2) -> Exp t2 … Haskell の型システムの性質をほとんどそのまま対象言語の型システムに適用できる。 型検査と CPS 変換を HOAS で行う。 let x = in x + 3 ↓ Let (Add (Num 1) (Num 2)) (λx. Add x (Num 3)) 例は による

15 コードの表し方 (2) De Bruijn indices 変数をインデックスで表す
インデックスは、自身から見ていくつ外側の λ を 指しているかを表す λz. (λy. y (λx. x)) (λx. z x) ↓ クロージャ変換、hoisting を de Bruijn で行う。 図は による

16 コードの表し方 (2) De Bruijn indices 形式の Haskell での表現 data Exp ts t where
Num :: Int -> Exp ts Int Add :: Exp ts Int -> Exp ts Int -> Exp ts Int App :: Exp ts (t1 -> t2) -> Exp ts t1 -> Exp ts t2 Var :: Index ts t -> Exp ts t Let :: Exp ts s -> Exp (s, ts) t -> Exp ts t … data Index ts t where Izero :: Index (t, ts) t Isucc :: Index ts t -> Index (s, ts) t ts は型環境を表す クロージャ変換、hoisting を de Bruijn で行う。

17 Let (Add (Num 1) (Num 2)) (Add (Var Izero) (Num 3))
コードの表し方 (2) De Bruijn indices の Haskell での表現の例 let x = in x + 3 ↓ Let (Add (Num 1) (Num 2)) (Add (Var Izero) (Num 3)) Add (Num 1) (Num 2) :: Exp ts Int Izero :: Index (Int, ts) Int Var Izero :: Exp (Int, ts) Int Add (Var Izero) (Num 3) :: Exp (Int, ts) Int Let (Add …) (Add …) :: Exp ts Int

18 All (All ((Var (S Z), Var Z) -> (Var Z, Var (S Z))))
型の表し方 対象言語の型も de Bruijn indices で表される ∀α. ∀β. (α, β) → (β, α) ↓ All (All ((Var (S Z), Var Z) -> (Var Z, Var (S Z)))) 型変数の置換などは type families を用いて定義される GHC では本当の型から型への関数は使えないので 対象言語の型を HOAS で表すことはできない

19 型の表し方 CPS 変換における型の変換 Type families で以下のように定義される type family Ktype t
type instance Ktype (t1 -> t2) = Cont Z (Ktype t1, Cont Z (Ktype t2)) type instance Ktype (All t) = Cont (S Z) (Cont Z (Ktype t)) type instance Ktype (Var i) = Var i … ⋮

20 Type preservation CPS 変換の type preservation
変換前のコードが well-typed ならば 変換後のコードも well-typed である 変換を行う Haskell 関数の型がそれを保証 cps :: Exp t -> (ValK (Ktype t) -> ExpK) -> ExpK

21 表現形式の選択 CPS 変換 クロージャ変換 / hoisting HOAS を用いる De Bruijn indices を用いる
でも複雑で混乱する 第三の選択肢: 普通に変数を 変数を表す整数や文字列で表す。-> uniqueness/freshness を保証するのが難しい

22 References 7.4. Extensions to data types and type synonyms
In The Glorious Glasgow Haskell Compilation System User's Guide, Version Generalized algebraic datatype In HaskellWiki “First-Class Phantom Types” J. Cheney and R. Hinze Technical Report CUCIS TR , Cornell University, 2003.

23 References 7.7. Type families Type families
In The Glorious Glasgow Haskell Compilation System User's Guide, Version Type families In HaskellWiki “Associated Types with Class” M. Chakravarty, G. Keller, S. Peyton-Jones, and S. Marlow In Proc. of The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.p. 1—13, ACM Press, 2005.

24 References “Type Associated Type Synonyms”.
M. Chakravarty, G. Keller, S. Peyton-Jones, and S. Marlow In Proc. of The 10th ACM SIGPLAN International Conference on Functional Programming, p.p. 241—253, ACM Press, 2005. “Type Checking with Open Type Functions” T. Schrijvers, S. Jones, M. Chakravarty, and M. Sulzmann In Proc. of The 13th ACM SIGPLAN International Conference on Functional Programming, p.p. 51—62, ACM Press, 2008. “A Type-Preserving Compiler in Haskell.” L.J. Guillemette and S. Monnier. In Proc. of the 13th ACM SIGPLAN International Conference on Functional Programming, p.p. 75—86, ACM Press, 2008.