Standard MLのModule言語におけるDependent typeって

型のSyntax

t ::= ...
      sp.t

式(term)のSyntax sp ::= ...
つまり、型のSynataxとして書けるものがtermに依存してしまっている。型は termとは分離して考えたいので困りもの。(spの部分が決まらないと、つまりどんな strucutureが定義されているかが分からないとsp.tが正しい型の表現なのか どうかが分からない。)
要するにパスによる表現を止めて新たな型の導入は全て型変数に置き換えた。
そして「defaultのsignatureを割り当てる」ではなく、「signatureの Semantic Objectを割り当てる。」にした。
c.f. Leroy, A modular module systems では型の互換性の情報を保つために pathのstrengthingを行なっていた。

疑問

でも、Non-Dependent typeとFirst-Class structureってどんな関係があるの!?

generativityってそもそも何?

実行時型エラーに陥るのような危険な型の識別(identification)を防ぐ...らしい。

特徴

Topレベルでないネストしたfunctorが書ける?

4. Static Semantics

反例1

structure X = 
  struct datatype t = int with x, y end
structure Y =
  struct structure X = struct end
         datatype u = int -> int with x', y'
  end;
val z = (Y.y' (X.x 1)) 2

このzは型付けが失敗しなければならない。しかし、状態を持たないやりかたで型付けして、 抽象型にαから順に優先して型変数を割り振るとすると...。

1. X.tに型変数α割り当て
2. Y内でXが定義されているので外のXは中からは隠される。
     この時に、X.tにαを割り当てたことも忘れてしまうとまずい
3. X.tにαを割り当てたことをわすれてY.uにもαを割り当ててしまう。

ちゃんと一意に降っていかないといけない。このような抽象型に対する型変数の 割当の一貫性を保たなければならない局面は (structureで)

• 抽象データ型の宣言 (datatype type with x,x')
• functor適用 F(x)
• signatureのopaque適用 s :> S

である。型変数の割り当てには大域的な状態が必要!?

思い出したこと

C++のdependent name

メモ

applicative functor

structure A = F((struct type t = int end));;

まずはfunctor適用の引数に struct .. end が直接書ける。
generative functor ... 適用毎に型がことなる (distinct)
applicative functor ... 互換になりうる。
mosml/examples/modules/collect.sml に例がある
  IncList.add 2 DecList.empty;; (* OK *)
  IncSet.add 2 DecSet.empty;; (* Wrong *)

datatype type with x, x' のイメージ
x'として case x v of x' v => v を想像すれば良いのだろうか?

- functor F (X : sig type t end) = struct datatype u = T of X.t end;
> functor F :
  !t.{type t = t}->?u.{datatype u = (u,{con T : t -> u}), con T : t -> u}
- structure A = F(struct type t = int end);;
> New type names: u
  structure A : {datatype u = (u,{con T : int -> u}), con T : int -> u}
- - structure B = F(struct type t = int end);;
> New type names: u/1
  structure B : {datatype u = (u/1,{con T : int -> u/1}), con T : int -> u/1}
- - A.T 1;;
> val it = ?{T} 1 : u
- - B.T 1;;
> val it = ?{T} 1 : u/1
- - case A.T 1 of A.T x => x;;
> val it = 1 : int
- - case A.T 1 of B.T x => x;; (* 互換性のない deconstructor で値を取り出す *)
! Toplevel input:
! case A.T 1 of B.T x => x;;
!      ^^^^^
! Type clash: expression of type
!   u
! cannot have type
!   u/1

applicative functorの例

- functor FA X : sig type t end = struct datatype u = T of X.t end;
! Toplevel input:
! functor FA X : sig type t end = struct datatype u = T of X.t end;
!         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
! Compliance Warning: 
! The phrase is an instance of the Moscow ML extension:
!   <modexp> ::= functor <modid> : <sigexp> => <modexp>
! which is not supported by the Definition of Standard ML.
> New type names: u/7
  functor FA :
  !t.
   {type t = t}->
       {datatype u = ((u/7 t),{con T : t -> (u/7 t)}), con T : t -> (u/7 t)}
- functor FG(X : sig type t end) = struct datatype u = T of X.t end;
> functor FG :
  !t.
   {type t = t}->?u/8.{datatype u = (u/8,{con T : t -> u/8}), con T : t -> u/8}
- structure A = FA(struct type t = int end);
> structure A :
  {datatype u = ((u/7 int),{con T : int -> (u/7 int)}),
   con T : int -> (u/7 int)}
- structure B = FA(struct type t = int end);
> structure B :
  {datatype u = ((u/7 int),{con T : int -> (u/7 int)}),
   con T : int -> (u/7 int)}
- case A.T 1 of B.T v => v; (* A.u型とB.u型がcompatible *)
> val it = 1 : int

but....

- structure C = FA(struct type t = string end);
> structure C :
  {datatype u = ((u/7 string),{con T : string -> (u/7 string)}),
   con T : string -> (u/7 string)}
- case A.T 1 of C.T v => v;;
! Toplevel input:
! case A.T 1 of C.T v => v;;
!      ^^^^^
! Type clash: expression of type
!   (u/7 int)
! cannot have type
!   (u/7 string)

そりゃ、ちゃんと防がないとね。で、普通のSMLはgenerative。互換性のない新たな型を 生成する。

観察

mosml

- functor FG ( X : sig type t end) = struct datatype u = T of X.t end;;
> functor FG :
  !t.{type t = t}->?u.{datatype u = (u,{con T : t -> u}), con T : t -> u}
- - structure A = struct type t = int end;
> structure A : {type t = int}
- structure B = FG(A);
> New type names: u
  structure B : {datatype u = (u,{con T : int -> u}), con T : int -> u}

Ocaml

# module FG = functor (X : sig type t end ) -> struct type u = T of X.t end;;
module FG : functor (X : sig type t end) -> sig type u = T of X.t end
# module A = struct type t =  int end;; (* そもそも引数として与える前に名前づけ *)
module A : sig type t = int end
# module B = FG(A);;
module B : sig type u = FG(A).u = T of A.t end

SML/NJ

- functor FG ( X : sig type t end) = struct datatype u = T of X.t end;;
functor FG : <sig>
- structure A = struct type t = int end;;
structure A : sig type t = int end
- structure B = FG(A);;
structure B : sig datatype u = T of X.t end

mosmlでのBのデフォルトの signature を見ると A は現れない。これが dependent type。
抽象型のsemantics objectとして型変数を用意。全ての抽象型は 型変数に対応づける。
type t = u;
  u と同じものをtに割り当て。abbreviation
datatype t = ... (抽象データ型定義)
  新たな型変数を用意(そのための∃限量子)??

参考文献

Claudio V. Russo, Non-Dependent Types for Standard ML Modules
ICFS, 1999
  これを読んでから First-Class Structures for Standard ML を読んだ方がよい。
Xavier Leroy, A modular module system