ゼウス

ゼウス（古希: ΖΕΥΣ, Ζεύς, Zeus）は、ギリシア神話の主神たる全知全能の存在[1]。全宇宙や天候を支配する天空神で、人類と神々双方の秩序を守護・支配する神々の王である。全宇宙を破壊できるほど強力な雷を武器とし、多神教の中にあっても唯一神的な性格を帯びるほどに絶対的で強大な力を持つ[2]。

「光輝」と呼ばれる天界の輝きを纏った鎧に山羊革の胸当てをつけ、聖獣は鷲、聖木はオーク。主要な神殿は、オークの木のささやきによって神託を下したエーペイロスの聖地ドードーナ、および4年ごとに彼の栄誉を祝福してオリンピック大祭が開かれたオリュンピアにあった。この他にも、「恐怖」という甲冑をギガントマキアーにおいて着用している。

今日はいよいよ型システムを見ていきます。

図8-1.ブール値のための型付け規則

B(型付き) B(図3-1)の拡張

新しい構文形式

T ::= …  型：
　Bool    ブール値型

新しい型付け規則 t : T

true : Bool                          (T-True)

false : Bool                         (T-False)

t1 : Bool　t2 : T　t3 : T
----------------------------------- (T-If)
if t1 then t2 else t3 : T

対応する実装は tyarith.pl です。 arith.pl の bool部分の型付け規則を以上のように書けます。
評価規則と同様に型付け規則は構文検査を行う述語が型を返すように拡張した Prolog の述語として実装できます。

:- op(910, fx, [/-]).
/- true : bool.
/- false : bool.
/- if(M1, M2, M3) : T2 :- /- M1 : bool, /- M2 : T2, /- M3 : T2.

SWI-Prolog の : はモジュール用にすでに使われているので /- 演算子を前置演算子として定義し '/-'/1 述語が : 演算子で分離された式と型を受け取ることで実装しました。/- 演算子はこれ以降 ⊢ 演算子の代わりとして用います。

図8-2.数(NB)のための型付け規則

B N(型付き) NB(図3-2)と図8-1の拡張

新しい構文形式

T ::= … 型：
  Nat    自然数型

新しい型付け規則 t : T

0 : Nat                              (T-Zero)

t1 : Nat
------------------------------------ (T-Succ)
succ t1 : Nat

t1 : Nat
------------------------------------ (T-Pred)
pred t1 : Nat

t1 : Nat
------------------------------------ (T-IsZero)
iszero t1 : Bool

対応する実装は tyarith.pl です。

/- 0 : nat.
/- succ(M1) : nat      :- /- M1 : nat.
/- pred(M1) : nat      :- /- M1 : nat.
/- iszero(M1) : bool   :- /- M1 : nat.

Prolog で書くと以上のようになります。

図9-1.純粋単純型付きラムダ計算(λ→)

→(型付き) λ(図5-3)に基づく

構文

t ::=       項：
　x         変数
　λx:T.t   ラムダ抽象
　t t       関数適用

v ::=       値：
　λx:T.t   ラムダ抽象値

T ::=       型：
　T->T      関数の型

Γ ::=      文脈：
　∅         空の文脈
　Γ,x:T    項変数の束縛

評価 t ==> t'

t1 ==> t1'
————————————————————— (E-App1)
t1 t2 ==> t1' t2

t2 ==> t2'
————————————————————— (E-App2)
v1 t2 ==> v1 t2'

(λx:T11.t12) v2 ==> [x->v2]t12            (E-AppAbs)

型付け Γ ⊢ t : T

x : T ∈ Γ
————————————————————— (T-Var)
Γ ⊢ x : T

Γ,x:T1 ⊢ t2 : T2
————————————————————— (T-Abs)
Γ ⊢ λx:T1.t2 : T1 -> T2

Γ ⊢ t1 : T11 -> T12　　Γ ⊢ t2 : T11
————————————————————— (T-App)
Γ ⊢ t1 t2 : T12

対応する、実装は simplebool.pl であり、untyped.pl に単純型システムを追加したものとなります。

11章拡張

フルバージョンの fulluntyped.pl に単純型システムを追加すると fullsimple.pl になります。

図11-1.非解釈基本型

→A λ→(図9-1)の拡張

新しい構文形式

T ::= … 型：
  A      基本型

図11-2.Unit型

→Unit λ→(図9-1)の拡張

新しい構文形式

t ::=       項：
  unit      定数unit

v ::=       値：
  unit      定数unit

T ::= …    型：
  Unit      Unit型

新しい型付け規則 Γ ⊢ t : T

Γ ⊢ unit : Unit                    (T-Unit)


新しい派生形式

t1;t2   def=    (λx:Unit.t2) t1
                ただし x ∉ FV(t2)

図11-3.型指定

→as λ→(図9-1)の拡張

新しい構文形式

t ::= …      項：
  t as T      型指定

新しい評価規則 t ==> t’

v1 as T ==> v1                             (E-Ascribe)

t1 ==> t1’
————————————————————— (E-Ascribe1)
t1 as T ==> t1’ as T


新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t1 : T
————————————————————— (T-Ascribe)
Γ ⊢ t1 as T : T

図11-4.let束縛

→let λ→(図9-1)の拡張

新しい構文形式

t ::= …            項：
  let x=t in t      let束縛


新しい評価規則 t ==> t’

let x=v1 in t2 ==> [x->v1] t2        (E-LetV)

t1 ==> t1’
—————————————————— (E-Let)
let x=t1 in t2 ==> let x=t1’ in t2


新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t1 : T    Γ, x : T1 ⊢ t2 : T2
—————————————————— (T-Let)
Γ ⊢ let x=t1 in t2 : T2

図11-5.二つ組

→× λ→(図9-1)の拡張

新しい構文形式

t ::=         項：
  {t,t}       二つ組
  t.1         第一要素の射影
  t.2         第二要素の射影

v ::=         値：
  {v,v}       二つ組値

T ::= …      型：
  T1 × T2    直積型

新しい評価規則 t ==> t’
{v1,v2}.1 ==> v1                     (E-PairBeta1)

{v1,v2}.2 ==> v2                     (E-PairBeta2)

t1 ==> t1’
—————————————————— (E-Proj1)
t1.1 ==> t1’.1

t1 ==> t1’
—————————————————— (E-Proj2)
t1.2 ==> t1’.2

t1 ==> t1’
—————————————————— (E-Pair1)
{t1,t2} ==> {t1’,t2}

t2 ==> t2’
—————————————————— (E-Pair2)
{v1,t2} ==> {v1,t2’}


新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t1 : T1    Γ ⊢ t2 : T2
—————————————————— (T-Pair)
Γ ⊢ {t1,t2} : T1 × T2 

Γ ⊢ t1 : T11 × T12
—————————————————— (T-Proj1)
Γ ⊢ t1.1 : T11

Γ ⊢ t1 : T11 × T12
—————————————————— (T-Proj2)
Γ ⊢ t1.2 : T12

図11-6.組

→{} λ→(図9-1)の拡張

新しい構文形式

t ::= …       項：
  {ti i∈1..n} 組
  t.i          射影

v ::= …       値：
  {vi i∈1..n} 組の値

T ::= …       型：
  {Ti i∈1..n} 組の型

新しい評価規則 t ==> t'

{vi i∈1..n}.j ==> vj               (E-ProjTuple)

t1 ==> t1'
—————————————————— (E-Proj)
t1.i ==> t1'.i

tj ==> tj'
—————————————————— (E-Tuple)
{vi i∈1..j-1, tj, tk k∈j+1..n}
==> {vi i∈1..j-1, tj', tk k∈j+1..n}

新しい型付け規則 Γ ⊢ t : T

各iに対して Γ ⊢ ti : Ti
—————————————————— (T-Tuple)
Γ ⊢ {ti i∈1..n} : {Ti i∈1..n} 

Γ ⊢ t1 : {Ti i∈1..n} 
—————————————————— (T-Proj)
Γ ⊢ t1.j : Tj

図11-7.レコード

→{} λ→(図9-1)の拡張

新しい構文形式

t ::= …          項：
  {li=ti i∈1..n} レコード
  t.l             射影

v ::= …      値：
  {li=vi i∈1..n} レコードの値

T ::= …      型：
  {li:Ti i∈1..n} レコードの型

新しい評価規則 t ==> t’

{li=vi i∈1..n}.lj ==> vj            (E-ProjRcd)

t1 ==> t1'
—————————————————— (E-Proj)
t1.l ==> t1'.l

tj ==> tj'
—————————————————— (E-Rcd)
{li=vi i∈1..j-1, lj=tj, lk=tk k∈j+1..n}
==> {li=vi i∈1..j-1, lj=tj', lk=tk k∈j+1..n}


新しい型付け規則 Γ ⊢ t : T

各iに対して Γ ⊢ ti : Ti
—————————————————— (T-Rcd)
Γ ⊢ {li=ti i∈1..n} : {li:Ti i∈1..n} 

Γ ⊢ t1 : {li:Ti i∈1..n} 
—————————————————— (T-Proj)
Γ ⊢ t1.lj : Tj

図11-8.(型無し)レコードパターン

→{} let p(型無し) 図11-7と図11-4の拡張

新しい構文形式

p ::= x           変数パターン：

t ::= …          項：
  let p=t in t    パターン束縛


パターンマッチの規則

match(x, v) = [x->v]                 (M-Var)

各iに対して match(pi,vi) = σi
—————————————————— (M-Rcd)
match({li=pi i∈1..n} : {li=vi i∈1..n})
    = σ1 ∘ … ∘ σn

新しい評価規則 t ==> t’

let p=v1 in t2 ==> match(p, v1) t2   (E-LetV)

t1 ==> t1'
—————————————————— (E-Let)
let p=t1 in t2 ==> let p=t1’ in t2

図11-9.和

→+ λ→(図9-1)の拡張

新しい構文形式

t ::= …                        項：
  inl t                         タグ付け（左）
  inr t                         タグ付け（右）
  case t of inl x=>t | inr x=>t 場合分け

v ::= …                        値：
  inl v                         タグ付けの値（左）
  inr v                         タグ付けの値（右）

T ::= …                        型：
  T+T                           和型

新しい評価規則 t ==> t’

case (inl v0)
of inl x1 => t1 | inr x2 => t2
    ==> [x1 -> v0] t1             (E-CaseInl)

case (inr v0)
of inl x1 => t1 | inr x2 => t2
    ==> [x2 -> v0] t2             (E-CaseInr)

t0 ==> t0'
—————————————————— (E-Case)
case t0 of inl x1=>t1 | inr x2=>t2
==> case t0’ of inl x1=>t1 | inr x2=>t2

t1 ==> t1'
—————————————————— (E-Inl)
inl t1 ==> inl t1’

t1 ==> t1'
—————————————————— (E-Inr)
inr t1 ==> inr t1’


新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t1 : T1
—————————————————— (T-Inl)
Γ ⊢ inl t1 : T1 + T2

Γ ⊢ t1 : T2
—————————————————— (T-Inr)
Γ ⊢ inr t1 : T1 + T2

Γ ⊢ t0 : T1 + T2
Γ,x1:T1 ⊢ t1:T    Γ,x2:T2 ⊢ t2:T    
————————————————————— (T-Case)
Γ ⊢ case t0 of inl x1=>t1 | inr x2=>t2:T

図11-10.和（一意型付け）

→+ λ→(図9-1)の拡張

新しい構文形式

t ::= …                        項：
  inr v as T                    タグ付けの値（右）

新しい評価規則 t ==> t’

case (inl v0 as T0)
of inl x1 => t1 | inr x2 => t2
    ==> [x1 -> v0] t1             (E-CaseInl)

case (inr v0 as T0)
of inl x1 => t1 | inr x2 => t2
    ==> [x2 -> v0] t2             (E-CaseInr)

t1 ==> t1'
—————————————————— (E-Inl)
inl t1 as T2 ==> inl t1’ as T2

t1 ==> t1'
—————————————————— (E-Inr)
inr t1 as T2 ==> inr t1’ as T2

新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t1 : T1
—————————————————— (T-Inl)
Γ ⊢ inl t1 as T1 + T2 : T1 + T2

Γ ⊢ t1 : T2
—————————————————— (T-Inr)
Γ ⊢ inr t1 as T1 + T2 : T1 + T2

図11-11.バリアント

→<> λ→(図9-1)の拡張

新しい構文形式

t::= …                            項：
  <li:Ti i∈1..n>                  バリアント型

新しい評価規則 t ==> t’

case(<lj=vj as T) of <li=xi>=>Ti i∈1..n
    ==> [xj -> vj]tj         (E-CaseVariant)

t0 ==> t0’
——————————————————— (E-Case)
case t0 of <li=xi> => ti i ∈1..n
==> case t0’ of <li=xi> => ti i∈1..n

ti ==> ti’
——————————————————(E-Variant)
<li=ti> as T ==> <li=ti’> as T

新しい型付け規則 Γ ⊢ t : T

Γ ⊢ tj:Tj
—————————————————— (T-Variant)
Γ ⊢ <lj=tj> as <li:Ti i∈1..n> : <li:Ti i∈1..n>

Γ ⊢ t0:<li:Ti i∈1..n>
各iに対してΓ,xi:Ti ⊢ ti : T
—————————————————— (T-Case)
Γ ⊢ case t0 of <li:xi> => ti i∈1..n : T

図11-12.一般的再帰

→fix λ→(図9-1)の拡張

新しい構文形式

t::= …     項:
  fix t     tの不動点

新しい評価規則 t ==> t’

fix(λx:T1 . t2)
==> [x -> (fix (λx:T1 . t2))] t2 (E-FixBeta)


t1 ==> t1’
————————(E-Fix)
fix t1 ==> fix t1’

新しい型付け規則 Γ ⊢ t : T

Γ ⊢ t1 :T1 -> T1
—————————— (T-Fix)
Γ ⊢ fix t1 :T1

新しい派生形式

letrec x:T1 = t1 in t2
def= let x = fix(λx:T1.t1) in t2

図11-13.リスト

→B List λ→(図9-1)のブール値(図8-1)を用いた拡張

新しい構文形式
t::=…項:
  nil[T] 空のリスト
  cons[T] t t リスト構築子(constructor)
  isnil[T] t リストが空かどうかの検査
  head[T] t リスト先頭の要素(head)
  tail[T] t リストの残りの部分(tail)
v::= … 値:
  nil[T] 空のリスト
  cons[T] v v リスト構築子
T::= … 型:
  List T リストの型


新しい型付け規則
Γ ⊢ nil[T1] : List T1 (T-Nil)

Γ ⊢ t1 : T1    Γ ⊢ t2 : List T1
——————————————————(T-Cons)
Γ ⊢ cons[T1]t1 t2 : List T1

Γ ⊢ t1:T11
——————————————————(T-IsNil)
Γ ⊢ isnil[T11]t1 : Bool

Γ ⊢ t1 : List T11
———————————————(T-Head)
Γ ⊢ t1 : head[T11]t1 : T11

Γ ⊢ t1 : List T11
———————————————(T-Tail)
Γ ⊢ t1 : tail[T11]t1 : List T11


新しい評価規則

t1 ==> t1’
——————————————— (E-Cons1)
cons[T] t1 t2 ==> cons[T] t1’ t2

t2 ==> t2’
——————————————— (E-Cons2)
cons[T] v1 t2 ==> cons[T] v1 t2’

isnil[S](nil[T])==>true               (E-IsNilNil)

isnil[S](cons[T] v1 v2) ==> false (E-IsNilCons)

t1 ==> t1’
——————————————— (E-IsNil)
isnil[T] t1 ==> isnil[T] t1’

head[S](cons[T] v1 v2) ==> v1 (E-HeadCons)

t1 ==> t1’
——————————————— (E-Head)
head[T]t1 ==> head[T]t1’

tail[S](cons[T] v1 v2) ==> v2    (E-TailCons)

t1==>t1’
——————————————— (E-Tail)
tail[T]t1 ==> tail[T]t1’

実装

rtg.pl

構文をマクロで展開するようにしたライブラリを以下に示します:

プログラムの全体を見る

rtg.pl

% RTG : Regular Tree Grammer validator generator

:- module(rtg, [
  op(1200, xfx, [::=]),
  call2/2
]).

list2tpl([A],A).
list2tpl([A|B],(A,B_)) :- list2tpl(B,B_).

addm(A,M,L) :- atom(A), L =.. [A|M].
addm(A,M,L) :- A=..B,append(B,M,R), L =.. R.

split(A,L,[B,R|L]) :- var(A),addm(call2,[A,B],R).
split(A,L,[B,R|L]) :- syntax(A),addm(A,[B],R).
split(A,L,[A|L]) :- atom(A),!.
split(A,L,[B|Ps1_]) :-
  A =.. [A_|Ps],!,
  foldl([P,(L1,L2),(R,[C|L2])]>> (split(P,L1,[C|R]),!),
    Ps,(L,[]),(Ps1,Ps_)
  ),!,
  reverse(Ps1,Ps1_),!, reverse(Ps_,Ps__),!,
  B =.. [A_|Ps__].
  
split2(M,A,C) :- split(A,[],[N|B]),list2tpl([M=N|B],C).

user:term_expansion(syntax(A),ignore) :- assert(syntax(A)).
user:term_expansion(A::=B,A_ :- syntax(A_,M,B)) :- assert(syntax(A)), addm(A,[M],A_).

syntax_expansion(M,(B|Bs),((B_,!);Bs_)) :- split2(M,B,B_), syntax_expansion(M,Bs,Bs_).
syntax_expansion(M,B,B_) :- split2(M,B,B_).

user:goal_expansion(syntax(_,M,A),B_) :- syntax_expansion(M,A,B_)/*,writeln(A_:-B_)*/.

call2([],[]) :- !.
call2([F|Fs],[M|Ms]) :- !,call2(F,M),call2(Fs,Ms).
call2(X,M) :- atom(X),syntax(X),call(X,M).
call2(F,M) :- F=..[O|Fs],M=..[O|Ms], call2(Fs,Ms).

syntax(atom).
:- user:discontiguous(syntax/1).
:- user:discontiguous(ignore/0).

このライブラリを用いると、構文が述語として展開されて使えるようになります。

tyarith.pl

プログラムの全体を見る

tyarith.pl

:- op(920, xfx, [==>, ==>>]).
:- op(910, fx, [/-]).
:- style_check(- singleton). 

% ------------------------   SYNTAX  ------------------------

:- use_module(rtg).

t ::=             % 型:
      bool        % ブール値型
    | nat         % 自然数型
    .
m ::=             % 項:
      true        % 真
    | false       % 偽
    | if(m, m, m) % 条件式
    | 0           % ゼロ
    | succ(m)     % 後者値
    | pred(m)     % 前者値
    | iszero(m)   % ゼロ判定
    .
n ::=             % 数値:
      0           % ゼロ
    | succ(n)     % 後者値
    .
v ::=             % 値:
      true        % 真
    | false       % 偽
    | n           % 数値
    . 

% ------------------------   EVALUATION  ------------------------

if(true, M2, _) ==> M2.
if(false, _, M3) ==> M3.
if(M1, M2, M3) ==> if(M1_, M2, M3) :- M1 ==> M1_.
succ(M1) ==> succ(M1_)             :- M1 ==> M1_.
pred(0) ==> 0.
pred(succ(N1)) ==> N1              :- n(N1).
pred(M1) ==> pred(M1_)             :- M1 ==> M1_.
iszero(0) ==> true.
iszero(succ(N1)) ==> false         :- n(N1).
iszero(M1) ==> iszero(M1_)         :- M1 ==> M1_.

M ==>> M_                          :- M ==> M1, M1 ==>> M_.
M ==>> M. 

% ------------------------   TYPING  ------------------------

/- true : bool.
/- false : bool.
/- if(M1, M2, M3) : T2 :- /- M1 : bool, /- M2 : T2, /- M3 : T2.
/- 0 : nat.
/- succ(M1) : nat      :- /- M1 : nat.
/- pred(M1) : nat      :- /- M1 : nat.
/- iszero(M1) : bool   :- /- M1 : nat. 

% ------------------------   MAIN  ------------------------

run(M, Γ, Γ) :- !, m(M), !, /- M : T, !, M ==>> M_, !, writeln(M_ : T).
run(Ls)      :- foldl(run, Ls, [], _). 

% ------------------------   TEST  ------------------------

% true;
:- run([true]). 
% if false then true else false;
:- run([if(false, true, false)]). 
% 0;
:- run([0]). 
% succ (pred 0);
:- run([succ(pred(0))]). 
% iszero (pred (succ (succ 0)));
:- run([iszero(pred(succ(succ(0))))]). 
% iszero (pred (pred (succ (succ 0))));
:- run([iszero(pred(pred(succ(succ(0)))))]). 
% iszero 0;
:- run([iszero(0)]).

:- halt.

simplebool.pl

プログラムの全体を見る

simplebool.pl

:- discontiguous((/-)/2).
:- op(1050, xfy, [=>]).
:- op(920, xfx, [==>, ==>>, <:]).
:- op(910, xfx, [/-]).
:- op(500, yfx, [$, !, subst, subst2]).
:- style_check(- singleton). 

% ------------------------   SYNTAX  ------------------------

:- use_module(rtg).

w ::= bool | true | false. % キーワード:
syntax(x). x(X) :- \+ w(X), atom(X), sub_atom(X, 0, 1, _, P), (char_type(P, lower) ; P = '_'). % 識別子:
syntax(tx). tx(TX) :- atom(TX), sub_atom(TX, 0, 1, _, P), char_type(P, upper). % 型変数:

t ::=                  % 型:
      bool             % ブール値型
    | nat              % 自然数型
    | tx               % 型変数
    | (t -> t)         % 関数の型
    .
m ::=                  % 項:
      true             % 真
    | false            % 偽
    | if(m, m, m)      % 条件式
    | 0                % ゼロ
    | succ(m)          % 後者値
    | pred(m)          % 前者値
    | iszero(m)        % ゼロ判定
    | x                % 変数
    | (fn(x : t) -> m) % ラムダ抽象
    | m $ m            % 関数適用
    .
v ::=                  % 値:
      true             % 真
    | false            % 偽
    | (fn(x : t) -> m) % ラムダ抽象
    . 

% ------------------------   SUBSTITUTION  ------------------------

true![(J -> M)] subst true.
false![(J -> M)] subst false.
if(M1, M2, M3)![(J -> M)] subst if(M1_, M2_, M3_)       :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_, M3![(J -> M)] subst M3_.
J![(J -> M)] subst M                                    :- x(J).
X![(J -> M)] subst X                                    :- x(X).
(fn(X : T1) -> M2)![(J -> M)] subst (fn(X : T1) -> M2_) :- M2![X, (J -> M)] subst2 M2_.
M1 $ M2![(J -> M)] subst (M1_ $ M2_)                    :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
A![(J -> M)] subst B                                    :- writeln(error : A![(J -> M)] subst B), fail.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                               :- S![(J -> M)] subst M_.

gett(Γ, X, T) :- member(X : T, Γ). 

% ------------------------   EVALUATION  ------------------------

Γ /- (fn(X : T11) -> M12) $ V2 ==> R    :- v(V2), M12![(X -> V2)] subst R.
Γ /- V1 $ M2 ==> V1 $ M2_               :- v(V1), Γ /- M2 ==> M2_.
Γ /- M1 $ M2 ==> M1_ $ M2               :- Γ /- M1 ==> M1_.
Γ /- if(true, M2, _) ==> M2.
Γ /- if(false, _, M3) ==> M3.
Γ /- if(M1, M2, M3) ==> if(M1_, M2, M3) :- Γ /- M1 ==> M1_.
Γ /- M ==>> M_                          :- Γ /- M ==> M1, Γ /- M1 ==>> M_.
Γ /- M ==>> M. 

% ------------------------   TYPING  ------------------------

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T2              :- Γ /- M1 : bool, Γ /- M2 : T2, Γ /- M3 : T2.
Γ /- X : T                            :- x(X), gett(Γ, X, T).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_) :- [X : T1 | Γ] /- M2 : T2_.
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : (T11 -> T12), Γ /- M2 : T11. 

% ------------------------   MAIN  ------------------------

run(X : T, Γ, [X : T | Γ]) :- x(X), t(T), !, writeln(X : T).
run(M, Γ, Γ)               :- !, m(M), !, Γ /- M : T, !, Γ /- M ==>> M_, !, writeln(M_ : T).
run(Ls)                    :- foldl(run, Ls, [], _). 

% ------------------------   TEST  ------------------------

% lambda x:Bool. x;
:- run([(fn(x : bool) -> x)]). 
% lambda x:Bool.lambda x:Bool. x;
:- run([(fn(x : bool) -> fn(x : bool) -> x)]). 
%  (lambda x:Bool->Bool. if x false then true else false) 
%    (lambda x:Bool. if x then false else true); 
:- run([(fn(x : (bool -> bool)) -> if(x $ false, true, false)) $
           (fn(x : bool) -> if(x, false, true))]).
:- run([ 
  % a:Bool;
  a : bool,  
  % a;
  a,
  % (lambda x:Bool. x) a;
  (fn(x : bool) -> x) $ a,
  % (lambda x:Bool. (lambda x:Bool. x) x) a;
  (fn(x : bool) -> (fn(x : bool) -> x) $ x) $ a
]).
% (lambda x:Bool. x) true;
:- run([(fn(x : bool) -> x) $ true]). 
% (lambda x:Bool. (lambda x:Bool. x) x) true;
:- run([(fn(x : bool) -> (fn(x : bool) -> x) $ x) $ true]).

:- halt.

fullsimple.pl

プログラムの全体を見る

fullsimple.pl

:- discontiguous((/-)/2).
:- op(1100, xfy, [in]).
:- op(920, xfx, [==>, ==>>]).
:- op(910, xfx, [/-]).
:- op(600, xfy, [::, as]).
:- op(500, yfx, [$, !, tsubst, tsubst2, subst, subst2]).
:- op(400, yfx, [#]).
:- style_check(- singleton). 

% ------------------------   SYNTAX  ------------------------

:- use_module(rtg).
w ::= bool | nat | unit | float | string | true | false | 0.  % キーワード:
syntax(x). x(X) :- \+ w(X), atom(X), (sub_atom(X, 0, 1, _, P), char_type(P, lower) ; P = '_'). % 識別子:
syntax(tx). tx(TX) :- atom(TX), sub_atom(TX, 0, 1, _, P), char_type(P, upper). % 型変数:
syntax(floatl). floatl(F) :- float(F).     % 浮動小数点数
syntax(stringl). stringl(F) :- string(F).  % 文字列
syntax(l). l(L) :- atom(L) ; integer(L).   % ラベル
list(A) ::= [] | [A | list(A)].            % リスト

t ::=                           % 型:
      bool                      % ブール値型
    | nat                       % 自然数型
    | unit                      % Unit型
    | float                     % 浮動小数点数型
    | string                    % 文字列型
    | tx                        % 型変数
    | (t -> t)                  % 関数の型
    | {list(l : t)}             % レコードの型
    | [list(x : t)]             % バリアント型
    .
m ::=                           % 項:
      true                      % 真
    | false                     % 偽
    | if(m, m, m)               % 条件式
    | 0                         % ゼロ
    | succ(m)                   % 後者値
    | pred(m)                   % 前者値
    | iszero(m)                 % ゼロ判定
    | unit                      % 定数unit
    | floatl                    % 浮動小数点数値
    | m * m                     % 浮動小数点乗算
    | stringl                   % 文字列定数
    | x                         % 変数
    | (fn(x : t) -> m)          % ラムダ抽象
    | m $ m                     % 関数適用
    | (let(x) = m in m)         % let束縛
    | fix(m)                    % mの不動点
    | inert(t) | m as t         % 型指定
    | {list(l = m)}             % レコード
    | m # l                     % 射影
    | case(m, list([x,x]=m))    % 場合分け
    | [x, m] as t               % タグ付け
    .
n ::=                           % 数値:
      0                         % ゼロ
    | succ(n)                   % 後者値
    .
v ::=                           % 値:
      true                      % 真
    | false                     % 偽
    | n                         % 数値
    | unit                      % 定数unit
    | floatl                    % 浮動小数点数値
    | stringl                   % 文字列定数
    | (fn(x : t) -> m)          % ラムダ抽象
    | {list(l = v)}             % レコード
    | tag(x, v) as t            % タグ付け
    . 

% ------------------------   SUBSTITUTION  ------------------------

maplist2(_, [], []).
maplist2(F, [X | Xs], [Y | Ys]) :- call(F, X, Y), maplist2(F, Xs, Ys).

bool![(J -> S)] tsubst bool.
nat![(J -> S)] tsubst nat.
unit![(J -> S)] tsubst unit.
float![(J -> S)] tsubst float.
string![(J -> S)] tsubst string.
J![(J -> S)] tsubst S                     :- tx(J).
X![(J -> S)] tsubst X                     :- tx(X).
(T1 -> T2)![(J -> S)] tsubst (T1_ -> T2_) :- T1![(J -> S)] tsubst T1_, T2![(J -> S)] tsubst T2_.
{Mf}![(J -> S)] tsubst {Mf_}              :- maplist([L : T, L : T_] >> (T![(J -> S)] tsubst T_), Mf, Mf_).
[Mf]![(J -> S)] tsubst [Mf_]              :- maplist([L : T, L : T_] >> (T![(J -> S)] tsubst T_), Mf, Mf_).
T![(J -> S)] tsubst T_                    :- writeln(error : T![(J -> S)] tsubst T_), halt.
T![X, (X -> S)] tsubst2 T.
T![X, (J -> S)] tsubst2 T_                :- T![(J -> S)] tsubst T_.

true![(J -> M)] subst true.
false![(J -> M)] subst false.
if(M1, M2, M3)![(J -> M)] subst if(M1_, M2_, M3_)          :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_, M3![(J -> M)] subst M3_.
0![(J -> M)] subst 0.
succ(M1)![(J -> M)] subst succ(M1_)                        :- M1![(J -> M)] subst M1_.
pred(M1)![(J -> M)] subst pred(M1_)                        :- M1![(J -> M)] subst M1_.
iszero(M1)![(J -> M)] subst iszero(M1_)                    :- M1![(J -> M)] subst M1_.
unit![(J -> M)] subst unit.
F1![(J -> M)] subst F1                                     :- float(F1).
M1 * M2![(J -> M)] subst M1_ * M2_                         :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
X![(J -> M)] subst X                                       :- string(X).
J![(J -> M)] subst M                                       :- x(J).
X![(J -> M)] subst X                                       :- x(X).
(fn(X : T1) -> M2)![(J -> M)] subst (fn(X : T1) -> M2_)    :- M2![X, (J -> M)] subst2 M2_.
M1 $ M2![(J -> M)] subst (M1_ $ M2_)                       :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
(let(X) = M1 in M2)![(J -> M)] subst (let(X) = M1_ in M2_) :- M1![(J -> M)] subst M1_, M2![X, (J -> M)] subst2 M2_.
fix(M1)![(J -> M)] subst fix(M1_)                          :- M1![(J -> M)] subst M1_.
inert(T1)![(J -> M)] subst inert(T1).
{Mf}![(J -> M)] subst {Mf_}                                :- maplist([L = Mi, L = Mi_] >> (Mi![(J -> M)] subst Mi_), Mf, Mf_).
M1 # L![(J -> M)] subst M1_ # L                            :- M1![(J -> M)] subst M1_.
([L, M1] as T1)![(J -> M)] subst ([L, M1_] as T1)          :- M1![(J -> M)] subst M1_.
(M1 as T1)![(J -> M)] subst (M1_ as T1)                    :- M1![(J -> M)] subst M1_.
case(M1, Cases)![(J -> M)] subst case(M1_, Cases_)         :- M1![(J -> M)] subst M1_, maplist([[L,X] = M2, [L,X] = M2_] >> (M2![(J -> M)] subst M2_), Cases, Cases_).
S![(J -> M)] subst _                                       :- writeln(error : subst(J, M, S)), fail.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                                  :- S![(J -> M)] subst M_.

gett(Γ, X, T) :- member(X : T, Γ).
gett(Γ, X, T) :- member(X - _ : T, Γ). 

% ------------------------   EVALUATION  ------------------------

e([L = M | Mf], M, [L = M_ | Mf], M_)  :- \+ v(M).
e([L = M | Mf], M1, [L = M | Mf_], M_) :- v(M), e(Mf, M1, Mf_, M_). 

Γ /- if(true, M2, _) ==> M2.
Γ /- if(false, _, M3) ==> M3.
Γ /- if(M1, M2, M3) ==> if(M1_, M2, M3)           :- Γ /- M1 ==> M1_.
Γ /- succ(M1) ==> succ(M1_)                       :- Γ /- M1 ==> M1_.
Γ /- pred(0) ==> 0.
Γ /- pred(succ(N1)) ==> N1                        :- n(N1).
Γ /- pred(M1) ==> pred(M1_)                       :- Γ /- M1 ==> M1_.
Γ /- iszero(0) ==> true.
Γ /- iszero(succ(N1)) ==> false                   :- n(N1).
Γ /- iszero(M1) ==> iszero(M1_)                   :- Γ /- M1 ==> M1_.
Γ /- F1 * F2 ==> F3                               :- float(F1), float(F2), F3 is F1 * F2.
Γ /- V1 * M2 ==> V1 * M2_                         :- v(V1), Γ /- M2 ==> M2_.
Γ /- M1 * M2 ==> M1_ * M2                         :- Γ /- M1 ==> M1_.
Γ /- X ==> M                                      :- x(X), member(X - M : _, Γ).
Γ /- (fn(X : _) -> M12) $ V2 ==> R                :- v(V2), M12![(X -> V2)] subst R.
Γ /- V1 $ M2 ==> V1 $ M2_                         :- v(V1), Γ /- M2 ==> M2_.
Γ /- M1 $ M2 ==> M1_ $ M2                         :- Γ /- M1 ==> M1_.
Γ /- (let(X) = V1 in M2) ==> M2_                  :- v(V1), M2![(X -> V1)] subst M2_.
Γ /- (let(X) = M1 in M2) ==> (let(X) = M1_ in M2) :- Γ /- M1 ==> M1_.
Γ /- fix((fn(X : T) -> M12)) ==> M12_             :- M12![(X -> fix((fn(X : T) -> M12)))] subst M12_.
Γ /- fix(M1) ==> fix(M1_)                         :- Γ /- M1 ==> M1_.
Γ /- {Mf} ==> {Mf_}                               :- e(Mf, M, Mf_, M_), Γ /- M ==> M_.
Γ /- {Mf} # L ==> M                               :- member(L = M, Mf).
Γ /- M1 # L ==> M1_ # L                           :- Γ /- M1 ==> M1_.
Γ /- [L, M1] as T ==> [L, M1_] as T               :- Γ /- M1 ==> M1_.
Γ /- V1 as _ ==> V1                               :- v(V1).
Γ /- M1 as T ==> M1_ as T                         :- Γ /- M1 ==> M1_.
Γ /- case([L, V11] as _, Bs) ==> M_               :- v(V11), member([L,X] = M, Bs), M![(X -> V11)] subst M_.
Γ /- case(M1, Bs) ==> case(M1_, Bs)               :- Γ /- M1 ==> M1_.
Γ /- M ==>> M_                                    :- Γ /- M ==> M1, Γ /- M1 ==>> M_.
Γ /- M ==>> M.

gettabb(Γ, X, T)   :- member(X = T, Γ).
compute(Γ, X, T)   :- tx(X), gettabb(Γ, X, T).
simplify(Γ, T, T_) :- compute(Γ, T, T1), simplify(Γ, T1, T_).
simplify(Γ, T, T).

Γ /- S = T                    :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ /- S_ == T_.
Γ /- bool == bool.
Γ /- nat == nat.
Γ /- unit == unit.
Γ /- float == float.
Γ /- string == string.
Γ /- X == T                   :- tx(X), gettabb(Γ, X, S), Γ /- S = T.
Γ /- S == X                   :- tx(X), gettabb(Γ, X, T), Γ /- S = T.
Γ /- X == X                   :- tx(X).
Γ /- (S1 -> S2) == (T1 -> T2) :- Γ /- S1 = T1, Γ /- S2 = T2.
Γ /- {Sf} == {Tf}             :- length(Sf, Len), length(Tf, Len),
                                 maplist([L : T] >> (member(L : S, Sf), Γ /- S = T), Tf).
Γ /- [Sf] == [Tf]             :- length(Sf, Len), length(Tf, Len),
                                 maplist2([L : S, L : T] >> (Γ /- S = T), Sf, Tf). 

% ------------------------   TYPING  ------------------------

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T2              :- Γ /- M1 : T1, Γ /- T1 = bool,
                                            Γ /- M2 : T2, Γ /- M3 : T3, Γ /- T2 = T3.
Γ /- 0 : nat.
Γ /- succ(M1) : nat                   :- Γ /- M1 : T1, Γ /- T1 = nat, !.
Γ /- pred(M1) : nat                   :- Γ /- M1 : T1, Γ /- T1 = nat, !.
Γ /- iszero(M1) : bool                :- Γ /- M1 : T1, Γ /- T1 = nat, !.
Γ /- unit : unit.
Γ /- F1 : float                       :- float(F1).
Γ /- M1 * M2 : float                  :- Γ /- M1 : T1, Γ /- T1 = float, Γ /- M2 : T2, Γ /- T2 = float.
Γ /- X : string                       :- string(X).
Γ /- X : T                            :- x(X), gett(Γ, X, T).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_) :- [X : T1 | Γ] /- M2 : T2_.
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)), Γ /- M2 : T2, Γ /- T11 = T2.
Γ /- (let(X) = M1 in M2) : T          :- Γ /- M1 : T1, [X : T1 | Γ] /- M2 : T.
Γ /- fix(M1) : T12                    :- Γ /- M1 : T1, simplify(Γ, T1, (T11 -> T12)), Γ /- T12 = T11.
Γ /- inert(T) : T.
Γ /- {Mf} : {Tf}                      :- maplist([L = M, L : T] >> (Γ /- M : T), Mf, Tf).
Γ /- M1 # L : T                       :- Γ /- M1 : T1, simplify(Γ, T1, {Tf}), member(L : T, Tf).
Γ /- ([Li, Mi] as T) : T              :- simplify(Γ, T, [Tf]), member(Li : Te, Tf), Γ /- Mi : T_, Γ /- T_ = Te.
Γ /- (M1 as T) : T                    :- Γ /- M1 : T1, Γ /- T1 = T.
Γ /- case(M, Cases) : T1              :- Γ /- M : T, simplify(Γ, T, [Tf]),
                                            maplist([[L,_] = _] >> member(L : _, Tf), Cases),
                                            maplist([[Li,Xi] = Mi, Ti_] >> (
                                              member(Li : Ti, Tf),
                                              [Xi : Ti | Γ] /- Mi : Ti_
                                            ), Cases, [T1 | RestT]),
                                            maplist([Tt] >> (Γ /- Tt = T1), RestT).
Γ /- M : _                            :- writeln(error : typeof(Γ, M)), fail. 

% ------------------------   MAIN  ------------------------

show(X - type)                  :- format('~w\n', [X]).
show(X - M : T)                 :- format('~w : ~w\n', [X, T]).
show(X = T)                     :- format('~w :: *\n', [X]).
show(X : T)                     :- format('~w : ~w\n', [X, T]).

run(type(X), Γ, [X - type | Γ])    :- tx(X), show(X - type).
run(type(X) = T, Γ, [X = T | Γ])   :- tx(X), t(T), show(X = T).
run(X : T, Γ, [X : T | Γ])         :- x(X), t(T), show(X : T).
run(X : T = M, Γ, [X - M : T | Γ]) :- x(X), t(T), m(M), Γ /- M : T_, Γ /- T_ = T, Γ /- M ==>> M_, show(X - M_ : T).
run(X = M, Γ, [X - M_ : T | Γ])    :- x(X), m(M), Γ /- M : T, Γ /- M ==>> M_, show(X - M_ : T).
run(M, Γ, Γ)                       :- !, m(M), !, Γ /- M : T, !, Γ /- M ==>> M_, !, writeln(M_ : T).
run(Ls)                            :- foldl(run, Ls, [], _). 

% ------------------------   TEST  ------------------------

%  lambda x:<a:Bool,b:Bool>. x;
:- run([(fn(x : [[a : bool, b : bool]]) -> x)]). 
% "hello";
:- run(["hello"]). 
% unit;
:- run([unit]). 
% lambda x:A. x;
:- run([(fn(x : 'A') -> x)]). 
% let x=true in x;
:- run([(let(x) = true in x)]). 
% timesfloat 2.0 3.14159;
:- run([2.0 * 3.14159]). 
% {x=true, y=false};
:- run([{[x = true, y = false]}]). 
% {x=true, y=false}.x;
:- run([{[x = true, y = false]} # x]). 
% {true, false};
:- run([{[1 = true, 2 = false]}]). 
% {true, false}.1;
:- run([{[1 = true, 2 = false]} # 1]). 
% lambda x:Bool. x;
:- run([(fn(x : bool) -> x)]). 
% (lambda x:Bool->Bool. if x false then true else false) 
%   (lambda x:Bool. if x then false else true); 
:- run([(fn(x : (bool -> bool)) -> if(x $ false, true, false)) $
           (fn(x : bool) -> if(x, false, true))]). 
% lambda x:Nat. succ x;
:- run([(fn(x : nat) -> succ(x))]). 
% (lambda x:Nat. succ (succ x)) (succ 0); 
:- run([(fn(x : nat) -> succ(succ(x))) $ succ(0)]). 
% T = Nat->Nat;
% lambda f:T. lambda x:Nat. f (f x);
:- run([type('T') = (nat -> nat),
        (fn(f : 'T') -> fn(x : nat) -> f $ (f $ x))]). 
% a = let x = succ 2 in succ x;
% a;
:- run([a = (let(x) = succ(succ(succ(0))) in succ(x)),
        a]). 
% <a=0> as <a:nat,b:bool>
:- run([[a, pred(succ(0))] as [[a : nat, b : bool]]]). 
% case <a=0> as <a:nat,b:bool> of
% <a=n> ==> isZero(n)
% | <b=b> ==> b;
:- run([case([a, pred(succ(0))] as [[a : nat, b : bool]],[
    [a,n] = iszero(n),
    [b,b] = b
])]).
:- halt.

まとめ

単純型付けの型システムは単一化をするだけです。
型付け規則として理解すれば、型システムは意外と簡単に作れるようになります。

Eagle
From Wikipedia, the free encyclopedia

This article is about the bird. For other uses, see Eagle (disambiguation).
"Eagles" redirects here. For other uses, see Eagles (disambiguation).

Eagle is the common name for many large birds of prey of the family Accipitridae. Eagles belong to several groups of genera, not all of which are closely related. Most of the 60 species of eagle are from Eurasia and Africa.[1] Outside this area, just 14 species can be found—2 in North America, 9 in Central and South America, and 3 in Australia.

図8-1.ブール値のための型付け規則

図8-2.数(NB)のための型付け規則

図9-1.純粋単純型付きラムダ計算(λ→)

11章 拡張

図11-1.非解釈基本型

図11-2.Unit型

図11-3.型指定

図11-4.let束縛

図11-5.二つ組

図11-6.組

図11-7.レコード

図11-8.(型無し)レコードパターン

図11-9.和

図11-10.和（一意型付け）

図11-11.バリアント

図11-12.一般的再帰

図11-13.リスト

実装

rtg.pl

tyarith.pl

simplebool.pl

fullsimple.pl

まとめ

11章拡張