To Home
Last modified: Thu Dec 28 23:58:06 JST 2006
First-Class Structures for Standard ML
先に Non-Dependent Types for Standard ML Modules を読むことを勧めます
目次
メモ

概要

Moduleを値として扱えるように。この手の論文は多い。
型づけは決定可能。

肝


pack s as S
open e as X
とsignatureのマッチング

Type Syntax

Core types (u)

u ::= t
| u -> u'
| int
| sp.t

Signature Bodies (B)

B ::= type t = u; B //transparent (manifest)
| type t; B //abstract (opaque)
| val x : u; B
| structure X : S; B //Nest
| εB
Signature Expressions (S)
S ::= sig B end
| T // signature identifier

signatureに名前を付けられる (module type S = sig .. end)

Term (structure)

Structure Bodies
b ::= type t = u; b //transparent (manifest only)
| val x : u; b
| structure X = s; b //Nest
| functor F (X:S) = s; b
| signature T = S; b
| εb

Structure Expression

s ::= sp
| struct b end
| F(s)
| s :> S // opaque constraint (s : S)

Semantic Objects

α ∈ Var
M, N, P, Q ∈ VarSet
u ∈ Type (::= α | u -> u' | int)
φ ∈ Real (= Var -> Type) // 型変数への代入
S ∈ Str (= TypeId -> Type, ValId -> Type, StrId -> Str)
L ∈ Sig (::= ΛP.S) // semantic signatures ※
X ∈ ExStr (::= ∃P.S) // existential structures
F ∈ Fun (::= ∀P.S -> X) // semantic functors
C ∈ Context (型, signature, 変数, structure, functorの名前をlookup)

ΛP.S
  Pは抽象型の集合
  Sはstructure
  型は type t |> α や type t |> int のように書く。

Enrichment Relation

S enriches S' (Sの方がS'より豊か 高い機能(?) 多くのフィールド!)
1. D(S) ⊇ D(S')
2. S'に含まれるt,xはS, S'で等しい
3. S'内のstructureについても再帰的にenrichである

subtypingは?? α ≧ int (型、変数に対して)

Functor Instantiation

∀P.S -> X instantiates to a functor instance S' -> X' (∀P.S -> X > S' -> X')
代入(Realization) D(φ) = P なるφがあってφ(S) = S' かつ φ(X) = X'

φ(∀P.S -> X) = φ(S) -> φ(X) ... S' -> X'
代入は全ての変数に。イメージ↓
(struct type 'a t type b' t end)[int/'a]
... (struct type 'a t type b' t end)[int/'a, b''/b']
(struct type int t type b'' t end)
代入[int/'a]は'b,'c (!≡ 'a) については適当な名前の付け替えでよい

Signature Matching

semantic structure S matches a signature ΛP.S'
D(φ) = P, S ≧ φ(S') (enriches)

Denotation Judgements

プログラムテキストからSemantic Signaturesへの変換。 e.g.) structure X : S; B |> ΛP∪Q.X : S,S' structure ...
性質
structureの同じレベル内で名前の重複がない。
abstractな型に型変数が対応づけられている。この型変数は新たに導入し、ΛP.Sの Pの部分にその型変数が入る。

type t = u の所の u の評価をいつ行うか?

Classification Judgements (Typing Judgements)

Package Types

差分

Core types
+ <S>

Core Expressions
+ pack s as S
| open e as X : S in e' pack s as S : <X>

packするときにsignatureをつけておく。
  何を提供するか?
openするときにas Xという名前をつけて使う。signatureもつける。
  何を使用するか?

例)
Fig 8 

structure Sieve
  struct
    type state = <Stream>; //package type
    val start =
      pack TwoOnwards as Stream; // TwoOnwards :> Stream
    val next =
      λs:state.open s as S:Stream in pack Next(S) as Stream;
    val value =
      λs:state.open s as S:Stream in S.value S.start
  end;
next, value は Sieve.state -> Sieve.state !?
Core内でfunctor適用を書ける。 (nextのbody)
package typeがCoreとModuleをつなぐ

ちょっと考えてみる
  Core -> Module へのアクセス
    package typeをCore typeとして扱える
    package typeのついたものを関数の引数としてとることができる。
  Module -> Core
    functor適用 -> 関数適用に持っていく (nthstateはpackage typeの値を返す)
    再帰が書ける!! 

val nthstate =
  fix λnthstate:int->Sieve.state.
      λn:int. ifzero n
          then Sieve.start
          else Sieve.next (nthstate (pred n))

val nthprime = λn:int.Sieve.value (nthstate n)

推論規則

Signature Expressions (S)

Denotation Semantics

sp : path (::= X | sp.X)
素材
first_module_rule.tex
  推論規則の検索といきたかったところだが。
typing.tex
  OnTwowardsの右辺の型付けの木

例と共に

Stream はsignature STREAMとでも書こうか 
module type STREAM =
  sig
    type : state; //なにか状態をもつ
    val start: state;
    val value: state -> int //とりだし
  end
2以上の整数のSTREAMを定義 TwoOnwards
TwoOnwards に Streamのtailを返すfunctor Next を適用する。
Nextを再帰的に適用して素数表を生成。N番以降の素数をもつSTREAMを作る。

登場人物整理
STREAM, STATE .. signature
TwoOnwards .. structure 2以上の整数列を実装したもの
Next, Value .. STATEを引数にとるfunctor
  STREAM -> STREAM
relation.vcg
stream.vcg

Streamをsemantic signatureにもっていったあとのイメージ(Not / OK)
  opaque.vcg

メモ

structure NAME = struct ... end
structure NAME = PATH etc..
structureで名前付け

V(O) ... O中の自由変数
functorのsignatureがない。functorは適用されてナンボらしい。
内部のfunctorにしかアクセスできない?? 外部モジュールのfunctorを使用するのは無理????
# module type A = sig module A : functor (Arg : sig type t end) -> sig type t = Arg.t end end;;
module type A =
  sig module A : functor (Arg : sig type t end) -> sig type t = Arg.t end end
一意に決まる??
  type?
  semantic objects?
Xはstructureの名前を表すメタ変数
existential structure の束縛変数はfunctorに絡む。内部で発生した型変数 を外は受け継ぐ。
  functor instantiationに絡む。
  opaque constraintに絡む。( OnTwowards :> Stream )
Fig4の言わんとしていること。
  Module レベルで State, Start, Next, Valueを定義している。
  Nextは 

  sig 
    type state
    (* val filter : state -> state *)
    val start  : state
    val next   : state -> state
    val value  : state -> int
  end
なものを返す。あれ? ModuleレベルとCoreレベルでおんなじようなものを定義 してないですか?ってこと。

Enrich Relationは

どこまでできる?
functorの適用を再帰的にできる (Moduleをパックして値化→functor適用のループを Coreで)
moduleに名前をいちいちつけなくてよい???
等価性判定とかは述べてない。eqtypeとか良くわかってないんですけど。 等価性判定ができるものじゃないらしい。 
- - val a = [ structure struct val a = 1 end as sig val a : int end];;
! Toplevel input:
! val a = [ structure struct val a = 1 end as sig val a : int end];;
!         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
! Compliance Warning: 
! The phrase is an instance of the Moscow ML extension:
!   <atexp> ::= [structure <modexp> as <sigexp>]
! which is not supported by the Definition of Standard ML.
> val a = [structure ...] : [{val a : int}]
- - a;;
> val it = [structure ...] : [{val a : int}]
- - val b = [ structure struct val a = 1 end as sig val a : int end];;
! Toplevel input:
! val b = [ structure struct val a = 1 end as sig val a : int end];;
!         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
! Compliance Warning: 
! The phrase is an instance of the Moscow ML extension:
!   <atexp> ::= [structure <modexp> as <sigexp>]
! which is not supported by the Definition of Standard ML.
> val b = [structure ...] : [{val a : int}]
- - a;;
> val it = [structure ...] : [{val a : int}]
- - a = b;;
! Toplevel input:
! a = b;;
! ^
! Type clash: expression of type
!   [{val a : int}]
! cannot have equality type ''a
package型の等価性は述べられている。
principal typeをもち
型が決定可能である

観察日記風
  contextの中に∃は入らない。∃をとって入れる。
  contextから探してstructureをとってきたとき(pathの評価時)は∃φを付ける。
  signatureのΛはcontextの中でも存在する。なにが抽象型 かを記録している。
  ( OnTwowards :> Stream ) の局面に注目
structure & signature
constraintはopaqueなもの(":>")のみ。(transparentなconstraint ":" は扱わない。Ocaml風)
SMLの二つの適用はsignatureの表現を共有するため!?
SMLではletは局所変数の名前づけで、fun,valはglobalな名前づけ!?

First-Class ... の pack s as S の型づけ 規則の前提は 3行めまで SとS' が入れ替わっている。

stratificationがなくなっているとは?
Leroy .. stratified
functorはpathに対してのみ適用可能
Harper and Lillibridge .. amalgamation (not stratified)

static semantic objectはDefinition of Standard MLで使用されている。(がad hocであるらしい)
2つの流儀
文法的に表現可能なもの(つまりtype phrase)で表しきる方法
dependent typeを持ち込む
semantic objectを用いる方法
これをprogrammerが覚えるのか?
証明に影響しないか?

OOとの違い。


モジュールシステムは
シンプル。
  継承はない
  => 階層構造をつくらなくてよい (signature matching)
類似
  アクセス制限が可能
  recordのsubtyping rule (enrich relation)

言語拡張必要か?を観察

レコードで structureを真似できないか?

レコードとは!?

  1. 静的に決まる名前(ラベル)から値を連想する
  2. (あらかじめどのようなフィールドがあるかを宣言する) ← かならずしもそうではないようで..
> val it = {f = "hoge", g = "moge", h = "ge"} :
  {f : string, g : string, h : string}

- type record = { f : string };
type record = {f:string}
- type record2 = { f: string, g : int };
type record2 = {f:string, g:int}
- fun get_f x = (#f x);
stdIn:28.1-28.21 Error: unresolved flex record
   (can't tell what fields there are besides #f)
- fun get_f (x:record) = (#f x);
val get_f = fn : record -> string
- fun get_ff (x:record2) = (#f x);
val get_ff = fn : record2 -> string
共通するフィールド名をもつレコードがあって良い。ここでは record1,record2。ただ、 レコードを受け取る関数は多相関数にならない!? (ほんとかなぁ fという名をもつレコード 全体を表す型の表現があったと思ったけれど)
参考
  SML#
  大堀先生の "A Polymorphic Record Calculus and Its Compilation" をもとに SMLを多相レコード型で拡張している。と思うが、makeできなかった....。

挑戦してみる 

(* いちいち作るものの型宣言 *)
(* signatureに対応          *)
type new_struct = 
     { divisor : state -> int, 
       filter  : state -> state,
       (** state = .. typeはかけない **)
       start   : state -> state,
       next    : state -> state,
       value   : state -> int }

val sift s =
    { divisor = s.value s.start,
      filter = let rec sub state = 
		   if  divides  divisor  ((#value s) state)
		   then  (sub  (#next s state))
		   else  state in sub end,
      start = filter (* of self *) }
  1. レコードは作るまえにフィールド名とその型の宣言をする。一方で、structureは あらかじめその型(signature)を宣言する必要はなく、デフォルトのsignatureがつく。
  2. フィールド同士に依存関係をもつことができない!? (this,self pointer...?)
  3. 型宣言は書けない
大体 recordの評価方法ってどんなんじゃ!?

依存性をもてないのイメージ 

> type depend = {data : string, print_data : unit -> unit}
- #print_data { data = "takashi"; print_data = fn () => print data } ();;
! Toplevel input:
! #print_data { data = "takashi"; print_data = fn () => print data } ();;
!                               ^
! Syntax error.
ここで、 print_data に束縛できる値は unit -> unit 型である関数全体である。この print_data に束縛される関数がたまたま"近隣住人になった" dataの値をしるわけがない。 (closureに他のフィールドである data が入らない。)

todo

型のcompatibility
  Λと∃で束縛される変数の意味。
  変数重複を許していない(避けている!?)箇所
前例との比較

existential structureについて考えてみる

コンテキストにstructureが入る場合にこの∃による束縛は無くなる
入れる場合
参照する場合
c.f.) letで型多相、型環境内のtype scheme

mosmlでみてみる 
structure Nest = struct
  structure Child = 
    struct type t = int end :> sig type t end;
end;
> New type names: t
  structure Nest : {structure Child : {type t = t}}
- structure Hoge = struct type t = int end :> sig type t end;
> New type names: t/1
  structure Hoge : {type t = t/1}
新しい型名が導入されたとか言う。globalに管理しているから∃でなくてもよいって ことかな?

おまけ

signatureに書けるもの (というかstructureの中で書けるからsignatureで書ける) Ocaml
  signature定義を要素として書ける
  functorのsignature 
# module A = struct
  module type S = sig type t end
  module F = functor(X:S) -> struct type u = T of X.t end
  end;;
    module A :
  sig
    module type S = sig type t end
    module F : functor (X : S) -> sig type u = T of X.t end
  end
# module RA = (A: sig module type S end);; (* えっ!? *)
module RA : sig module type S end

SML(- mosml)
signatureはTop-levelでのみ書ける
functorもTop-levelでのみ
だからsignatureにはsignature定義やfunctorのsignatureといったものはない。

Moscow ML
structure内にsignatureの定義を書けるが structureのsignatureには残らない
structure内にfunctor定義を書けてsignatureに残る(外からアクセス可能) 
- structure A = struct
signature S = sig type t end
functor F (X:S) = struct datatype t = T of X.t end
signature S = sig type t end
end;;
! Toplevel input:
! signature S = sig type t end
! ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
! Compliance Warning: 
! The phrase is an instance of the Moscow ML extension:
!   <strdec> ::= signature <sigbind>
! which is not supported by the Definition of Standard ML.
! Toplevel input:
! functor F (X:S) = struct datatype t = T of X.t end
! ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
! Compliance Warning: 
! The phrase is an instance of the Moscow ML extension:
!   <strdec> ::= functor <funbind>
! which is not supported by the Definition of Standard ML.
! Toplevel input:
! signature S = sig type t end
! ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
! Compliance Warning: 
! The phrase is an instance of the Moscow ML extension:
!   <strdec> ::= signature <sigbind>
! which is not supported by the Definition of Standard ML.
> structure A :
  {functor F :
     !t.
      {type t = t}->
          ?t/1.{datatype t = (t/1,{con T : t -> t/1}), con T : t -> t/1}}

Includemod.check_modtype_equiv

型をunifyするのに型Aと型Bとの等価性判定をしなければならない。等価性判定をどうするかが もっとも重要であるが、従来のmodule typeの比較と同様に行えばよい。

non-dependent typeとfirst-class structure

1.値(structure)が動的に切り替わるのに型がそれに依存してしまっては静的に型つけできない!?
semantic objectについての議論はP59(Chapter 2)

歴史

SOL
Quest
DL
XML

translucent sum (opaque型とmanifest型の指定が可能)

参考文献

Claudio V. Russo, First-Class Structures for Standard ML
The 1999 International Conference on Function Programming (ICFP)

Mark Shields and Simon Peyton Jones. First-class Modules for Haskell
In the Ninth International Conference on Foundations of Object-Oriented Languages (FOOL 9), Portland, Oregon

Moscow ML

mosmlでコンパイルしよう

作者: 増山隆
To Home