Survey: First-Class Structures for Standard ML

Survey: First-Class
Structures for
Standard ML
米澤研究室修士1年増山隆
[email protected]
発表の概要
MLのModuleの概要
 拡張
 Moduleの型付け

 Semantic
Object
 Denotation Judgements
 Classification Judgements
MLのModuleの概要
MLのModule

Core言語
 アルゴリズムを記述する

Module言語
 Coreでかかれた定義をまとめる
 型を抽象化する
 structure
 signature
 functor
structure
型や変数の定義のリス
ト
Module言語における値
structure TwoOnwards =
struct
type state = int;
val start = 2;
val start2 = 100;
val next = fn i => succ i;
val value = fun i => i;
end
型を定義
値を定義
signature
structureのインターフェイス
Module言語における型(のようなもの)
signature Stream =
sig
type state;
型の指定
val start: state;
変数名とその型を指定
val next: state;
val value: state -> int;
end
signatureの役割

structureに
 型を抽象化
 structureの要素を隠蔽
structure Start = TwoOnwards :> State;
例) Startは
 抽象型state
(int で実装されていることは隠蔽)
 start, next, valueという変数
があるstructure (start2は隠蔽される)
functor
structureからstructureへの関数
functor Value (S: Stream) =
struct val value = S.value (S.start) end
不満な点1

Module言語には条件分岐がない
structure A =
if isDebug then
struct ... end
else
struct ... end
のようにできるとうれしい
不満な点2
Module言語ではループが書けない
例: Fig4のEratostenesの篩

 functorの適用回数が定数回になってしまう
Next(Next(Next(Start)))
functorの適用が実行時にできると、Module言語を
汎用の計算に用いることができる
拡張
拡張

Core言語を拡張する
 package
typesを導入
 pack, open 式を追加
pack

pack s as S
 structure
s を signature Sで制限してpackage化
する。
mosmlでは
[structure s as S]
open (unpack)

open s as X : S in e’
 e’の中で
X = s :> S としてstructure Xを使用でき
るようにする
mosmlでは
[let] structure X as S = s [in e’ end]
(structure XがCoreの式のスコープの中で宣言される)
packageの使用例
Sieve.nextのおかげでfunctor Nextを実行時に繰り返し適用できる
型付け
Semantic Objects
structure, functorに型としてSemantic
Objectを割り当てる
 SignatureをDenotation Judgementによって
Semantic Objectに変換する

∃P.S
 signature ΛP.S
 functor
∀P.( S -> ∃P.S )
 structure

signature matchingなどはこのSemantic
Objectレベルで行う
c.f. A Modular Module Systemではstructureにsignatureを付
けていた
Semantic Object (signature)
sig
type state
val start : state
val next : state -> state
val value : state -> int
end
Λ{α}.
( state |> α,
start : α,
next : α -> α,
value : α -> int )
Semantic Object (structure)
内部で導入された抽象型に
対する型変数
struct
type state = int;
val start = 2;
val next = fn x => x + 1;
val value = fn x => x
end
end :>
Stream
∃{β}.
( state |> β,
start : β,
next : β -> β,
value : β -> int )
Semantic Object (functor)
パラメター化された型
functor Next (S : Stream) =
struct
(* Streamにマッチする
structure *)
end
∀{γ}.
((state |>γ,
start :γ,
next : γ -> γ,
value : γ -> int) ->
∃φ.( state |>γ,
start :γ,
next : γ -> γ,
value : γ -> int))
RussoのModule言語設計
structure
functor
Classification
Judgements
∃P.S
signature
Denotation
Judgements
∀P.( S -> ∃P.S )
ΛP.S
semantic object
パス (p.t) が現れない(structureの値によらない型表現
→ non-dependent type)
型変数で依存性を表現
MLの文法では書き表せない
Harper,Lillibridge,Leroyの
Module言語設計
structure
functor
signature
型としてsignatureを使う
型の表現にパスが現れる
パスを使用して依存性を表現 (1st order dependent type)
MLの文法で表現可能
2つの方式の比較
structure A = struct type t = int end :>
sig type t end
structure B = struct type u = A.t end
Semantic
Object
A : ( t |> α)
B : ( u |> α)
Bを見終わった後の環境
Signature
A : sig type t end
B : sig type t = A.t end
Semantic Objectを型として使用する
利点
Principal typeをもつ
 package typesの等価性比較は決定可能

 Enrichment
を定義
Relation(subtyping)によって等価性
Denotation Judgements
Classification Judgements (1/3)
Classification Judgements (2/3)
Classification Judgements (3/3)
package typeのDenotation
Judgement
packのClassification Judgement
openのClassification Judgement
5行目: 返値の型にpackage eの中の抽象型が含まれない
まとめ

Coreに単純な拡張(pack, open)を加えること
でFirst-Class structureの機能を提供できた
 structureを実行時に差し替える
 一般の計算に使用できる

型システムには悪い影響を及ぼさない
 Semantic
Objectを使用して意味を定義
(Non-dependent type)
 型付けは決定可能
参考文献
First-Class Structures for Standard ML Claudio
Claudio V. Russo, ICFP 1999
 Non-Dependent Types for Standard ML Modules
Claudio V. Russo, PPDP 1999
 Types for Modules
Claudio V. Russo, 1998
 Moscow ML

http://www.dina.dk/~sestoft/mosml.html

Download Report