クロノス

クロノス（古希: Κρόνος, Kronos）は、ギリシア神話の大地および農耕の神である。山よりも巨大な巨神族ティーターンの長であり、ウーラノスの次に全宇宙を統べた二番目の神々の王でもある。万物を切り裂くアダマスの鎌を武器とする。ゼウスの父親としてもよく知られており、ティーターン神族を率いてオリュンポスの神々と全宇宙を揺るがす大戦争を行った。

Symbol Snake, grain, sickle, scythe

Planet Saturn

Parents Uranus and Gaia

部分型付けは OOP の継承のような親子関係を持つ型システムをレコードについて主に実装し考察します。名前によらない親子関係は構造的部分型といいます。単純な部分型付けの型付け規則はアルゴリズミックではなく、左再帰を含むので Prolog で実行すると無限ループしてしまいます。OCaml のような関数型言語で実装しても同様無限ループします。そこで左再帰の除去を行ったアルゴリズミックな構文主導の規則に書き換えることで、若干複雑な規則になりますが規則をそのまま書き下して動かせるようになります。

Prolog の例としてよく挙げられる親子関係の推論をより発展させた子孫関係を調べる述語を考えてみましょう。

アルゴリズミックではない規則の例:

isono.pl

親(tarao,sazae).
親(sazae,namihe).

子孫(A,A).
子孫(A,B):- 親(A,B).
子孫(A,B):- 子孫(A,C),子孫(C,B).

:- 子孫(tarao,namihe).
:- halt.

このプログラムは推移的な規則があり、左再帰が含まれているので停止しません。これはうまく左再帰を削除して、以下のようにアルゴリズム的にアルゴリズミックに書き換えることでうまく動作するようになります。

アルゴリズミックな規則の例:

isono2.pl

親(tarao,sazae).
親(sazae,namihe).

子孫(A,A).
子孫(A,B):- 親(A,B).
子孫(A,B):- 親(A,C),子孫(C,B).

:- 子孫(tarao,namihe).
:- halt.

オブジェクト指向の言語のように記号を使って書き換えてみましょう:

isono3.pl

:- op(920, xfx, [<:]).
class(tarao <: sazae).
class(sazae <: namihe).
A <: A.
A <: B :- class(A <: B).
A <: B :- class(A <: C),C <: B.
:- tarao <: namihe.
:- halt.

このような規則を Norminal な型システムの部分型付け関係といいます。

TAPL の部分型付けのお話は Strucutual な型システムのお話です。
名前を使わず構造的な親子関係でも左再帰の問題があり停止しないので難しい。
そこで名前的な型システムの親子関係と同様にアルゴリズム的に書き換える必要があります。
的な的なーｗ

TAPL15,16 部分型付け

図15-1.部分型付けを持つ単純型付きラムダ計算(λ<:)

→<: Top λ→(図9-1)に基づく

構文

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

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

T ::=       型：
  Top       最大の型
  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)

部分型付け S <: T

S <: S               (S-Refl)

S <: U　　U <: T
-------------------- (S-Trans)
S <: T

S <: Top             (S-Top)

T1 <: S1　　S2 <: T2
-------------------- (S-Arrow)
S1 -> S2 <: T1 -> T2

型付け Γ ⊢ 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

Γ ⊢ t : S　　S <: T
------------------------------------ (T-Sub)
Γ ⊢ t : T

この規則、推移則があり左再帰があるので Prolog で動かすと無限ループに陥る。
分かりやすいけれども、アルゴリズム的ではない規則が含まれています。

図15-3.レコードと部分型付け

→{} <: λ<:(図15-1)と単調なレコードの規則(図15-2)の拡張

新い構文形式

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

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

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

新しい部分型付け規則 S <: T

{li:Ti i∈1..n+k} <: {li:Ti i∈1..n}   (S-RcdWidth)

各iに対して Si <: Ti
------------------------------------- (S-RcdDepth)
{li:Si i∈1..n} <: {li:Ti i∈1..n}


{kj:Sj j∈1..n} は {li:Ti i∈1..n} の並べ替えである
------------------------------------- (S-RcdPerm)
{kj:Sj j∈1..n} <: {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

これはレコードに対する拡張です。

図15-4.Bottom型

→ <: Bot λ<:(図15-1)の拡張

新しい構文形式

T ::= …      型：
　Bot         最小の型

新しい部分型付け規則 S <: T

Bot <: T   (S-Bot)

これは最小の型を追加する規則です。

図15-5.バリアントと部分型付け

→ <> <: λ<:(図15-1)と単調なバリアントの規則(図11-11)の拡張

新しい構文形式

t ::= …              項：
　<l=t> (as はなし)   タグ付け

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

Γ ⊢ t1 : T1
—————————————— (T-Variant)
Γ ⊢ <l1=t1> : <l1:T1>

新しい部分型付け規則 S <: T

<li:Ti i∈1..n> <: <li:Ti i∈1..n+k>   (S-VariantWidth)

各iに対して Si <: Ti
——————————————————— (S-VariantDepth)
<li:Si i∈1..n> <: <li:Ti i∈1..n>


<kj:Sj j∈1..n> は <li:Ti i∈1..n> の並べ替えである
——————————————————— (S-VariantPerm)
<kj:Sj j∈1..n> <: <li:Ti i∈1..n>

バリアント型についての拡張ですね。

図16-1.レコードのある部分型関係(簡潔な版)

→ {} <: 図15-1と図15-3の拡張

S <: S               (S-Refl)

S <: U　　U <: T
—————————— (S-Trans)
S <: T

S <: Top             (S-Top)

T1 <: S1　　S2 <: T2
—————————— (S-Arrow)
S1 -> S2 <: T1 -> T2

{li i∈1..n} ⊆ {kj j∈1..m}
kj = li ならば Sj <: Ti
——————————————————— (S-Rcd)
{kj:Sj j∈1..m} <: {li:Ti i∈1..n}

これはレコードについての規則をより簡潔にした規則ですが、推移則が含まれており左再帰があるので停止しないアルゴリズミックではない構文主導ではない Prolog で停止しない規則です。<なげーよw

図16-2.アルゴリズム的部分型付け

→ {} <:

アルゴリズム的部分型付け |-> S <: T

|-> S <: Top                           (S-Top)

|-> T1 <: S1　　|-> S2 <: T2
——————————————————— (S-Arrow)
|-> S1 -> S2 <: T1 -> T2

{li i∈1..n} ⊆ {kj j∈1..m}
kj = li ならば |-> Sj <: Ti
——————————————————— (S-Rcd)
|-> {kj:Sj j∈1..m} <: {li:Ti i∈1..n}

構造的に内側に入り込んでいく形に書けば左再帰はなくなるのでアルゴリズム的であり Prolog で実行しても停止します。

図16-3.アルゴリズム的型付け

→ {} <:

アルゴリズム的型付け Γ ↦ t : T

x : T ∈ Γ
————————————————————— (TA-Var)
Γ ↦ x : T

Γ,x:T1 ↦ t2 : T2
————————————————————— (TA-Abs)
Γ ↦ λx:T1.t2 : T1 -> T2

Γ ↦ t1 : T1　　T1 = T11 -> T12
Γ ↦ t2 : T2　　↦ T2 <: T11
————————————————————— (TA-App)
Γ ↦ t1 t2 : T12

各iに対してΓ ↦ ti : Ti
————————————————————— (TA-Rcd)
Γ ↦ {l1=t1…ln=tn} : {l1:T1…ln:Tn}

Γ ↦ t1 : R1　　R1 = {l1:T1…ln:Tn}
————————————————————— (T-Proj)
Γ ↦ t1.li : Ti

停止する部分型付け関係を使っているので型システムも停止します。

図16-?.T-If,TA-If, SA-Bot,AppBot,ProjBot

型付け Γ ↦ t : T

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


Γ ⊢ t1 : T1   T1 = Bool
Γ ⊢ t2 : T2   Γ ⊢ t3 : T3   T2 ∨ T3=T
---------------------------------------- (TA-If)
Γ ⊢ if t1 then t2 else t3 : T

↦ Bot <: T (SA-Bot)

Γ ↦ t1 : T1　　T1 = Bot   Γ ↦ t2 : T2
---------------------------------------- (TA-AppBot)
Γ ↦ t1 t2 : Bot

Γ ↦ t1 : R1　　R1 = Bot
---------------------------------------- (TA-ProjBot)
Γ ↦ t1.li : Bot

これらも停止します。

19章 Fetherweight Java

OOP で Norminal な型システムを形式化した型システムが FJ です。
部分型付け関係が推移的であることに注目してみましょう。

図19-1.Featherweight Java (構文と部分型付け)

構文

CL ::=                     クラス宣言：
　class C extends C {[C f;] K [M] }

K ::=              コンストラクタ宣言：
　C([C f]) { super([f]); [this.f=f;] }

M ::=                    メソッド宣言：
　C m([C m]) { return t; }

t ::=                              項：
　x                                変数
　t.f                              フィールドアクセス
　t.m([t])                         メソッド呼び出し
　new C([t])                       オブジェクト生成
　(C) t                            キャスト

v ::=                              値：
　new C([v])                       オブジェクト生成

部分型付け規則 Γ ⊢ C <: D

C <: C

C <: D　　D <: E
———————————
C <: E

CT(C) = class C extends D {…}
————————————————
C <: D

図19-2.Fetherweight Java (補助的な定義)

フィールドの探索 fields(C)= [C f]

fields(Object) = •

CT(C) = class C extends D {[C f;] K [M]}
fields(D) = [D g]
—————————————————————
fields(C) = [D g],[C f]


メソッドの型の探索 mtype(m,C) = [C] -> C

CT(C) = class C extends D {[C f;] K [M]}
B m ([B x]) {return t;} ∈ [M]
—————————————————————
mtype(m,C) = [B] -> B

CT(C) = class C extends D {[C f;] K [M]}
mは[M]の中で定義されていない
—————————————————————
mtype(m,C) = mtype(m,D)


メソッドの本体の探索 mbody(m,C) = ([x],t)

CT(C) = class C extends D {[C f;] K [M]}
B m ([B x]) {return t;} ∈ [M]
—————————————————————
mbody(m, C) = ([x],t)

CT(C) = class C extends D{[C f;] K [M]}
m は [M] の中で定義されていない
—————————————————————
mbody(m,C)=mbody(m,D)


メソッドの正当なオーバーライド override(m, D, [C]->C0)

mtype(m,D) = [D]->D0 ならば、 [C] = [D] かつ C0 = D0
———————————————————————————
override(m, D, [C] -> C0)

図19-3.Fetherweight Java (評価)

評価 t ==> t’

fields(C) = [C f]
————————————————————— (E-ProjNew)
(new C([v])).fi ==> vi

mbody(m,C) = ([x], t0)
————————————————————— (E-InvkNew)
(new C([v])).m([u])
==> [[x]->[u],this->new C([v])]t0

C <: D
————————————————————— (E-CastNew)
(D)(new C([v])) ==> new C([v])

t0 ==> t0’
————————————————————— (E-Field)
t0.f ==> t0’.f

t0 ==> t0’
————————————————————— (E-Invk-Recv)
t0.m([t]) ==> t0’.m([t])

ti ==> ti’
————————————————————— (E-Invk-Arg)
v0.m([v],ti,[t]) ==> v0.m([v],ti’,[t])

ti ==> ti’
————————————————————— (E-New-Arg)
new C([v],ti,[t]) ==> new C([v],ti’,[t])

t0 ==> t0’
————————————————————— (E-Cast)
(C)t0 ==> (C)t0’

図19-4.Fetherweight Java (型付け)

項の型付け Γ ⊢ t : C

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

Γ ⊢ t0 : C0   fields(C0) = [C f]
—————————————————— (T-Field)
Γ ⊢ t0.fi : Ci

Γ ⊢ t0 : C0
mtype(m, C0) = [D] -> C
Γ ⊢ [t] : [C]      [C] <: [D]
—————————————————— (T-Invk)
Γ ⊢ t0.m([t] : C

fields(C) = [D f]
Γ ⊢ [t] : [C]      [C] <: [D]
—————————————————— (T-New)
Γ ⊢ new C([t]) : C

Γ ⊢ t0 : D     D <: C
—————————————————— (T-UCast)
Γ ⊢ (C)(t0) : C

Γ ⊢ t0 : D     C <: D    C =/= D
—————————————————— (T-DCast)
Γ ⊢ (C)(t0) : C

Γ ⊢ t0 : D     C /<: D    C /<: D
愚かさの警告
—————————————————— (T-SCast)
Γ ⊢ (C)(t0) : C

メソッドの型付け M OK in C

[x]:[C],this:C ⊢ t0:E0    E0 <: C0
CT(C) = class C extends D {…}
override(m,D,[C]->C0)
——————————————————
C0 m ([C x]) { return t0; } OK in C

クラスの型付け C OK

K=C([D g],[C f])
{super([g]); this.f = f; }
fields(D) = [D g]    [M] OK in C
————————————————
class C extends D {[C f;] K M} OK

定義19.5.3. FJの評価文脈

定義 19.5.3. FJの評価文脈の集合は以下のように定義される。

E ::= 評価文脈：
　[]               穴
　E.f              フィールド参照
　E.m([t])         メソッド呼び出し(レシーバ)
　E.m([v],E,[t])   メソッド呼び出し(引数)
　new C([v],E,[t]) オブジェクト生成(引数)
　(C)E             キャスト

実装

rcdsubbot 単純部分型付ラムダ計算レコードbot λ+top+bot+record+単純部分型 (15,16章)
fullsub フル単純部分型付きラムダ計算 botなし bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+単純部分型 (15章)
bot 単純部分型付きラムダ計算+bot λ+top+bot+単純部分型(16章)
joinexercise

rcdsubbot.pl

プログラムの全体を見る

rcdsubbot.pl

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

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

:- use_module(rtg).
w ::= top | bot.                          % キーワード:
syntax(x). x(X) :- \+ w(X), atom(X).      % 識別子:
syntax(l). l(L) :- atom(L) ; integer(L).  % ラベル
list(A) ::= [] | [A | list(A)].           % リスト

t ::=                  % 型:
      top              % 最大の型
    | bot              % 最小の型
    | (t -> t)         % 関数の型
    | {list(l : t)}    % レコードの型
    .
m ::=                  % 項:
      x                % 変数
    | (fn(x : t) -> m) % ラムダ抽象
    | m $ m            % 関数適用
    | {list(l = m)}    % レコード
    | m # l            % 射影
    .
v ::=                  % 値:
      (fn(x : t) -> m) % ラムダ抽象
    | {list(l = v)}    % レコード
    . 

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

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_.
{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_.
A![(X -> M)] subst B                                    :- writeln(error : A![(X -> M)] subst B), fail.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                               :- S![(J -> M)] subst M_.

% ------------------------   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_). 

Γ /- (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_.
Γ /- {Mf} ==> {Mf_}                  :- e(Mf, M, Mf_, M_), Γ /- M ==> M_.
Γ /- {Mf} # L ==> M                  :- member(L = M, Mf).
Γ /- M1 # L ==> M1_ # L              :- Γ /- M1 ==> M1_.
Γ /- M ==>> M_                       :- Γ /- M ==> M1, Γ /- M1 ==>> M_.
Γ /- M ==>> M. 

% ------------------------   SUBTYPING  ------------------------

T1  <: T1.
_   <: top.
bot <: _.
(S1 -> S2) <: (T1 -> T2) :- T1 <: S1, S2 <: T2.
{SF} <: {TF}             :- maplist([L : T] >> (member(L : S, SF), S <: T), TF). 

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

Γ /- X : T                            :- x(X), !, member(X : T, Γ).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_) :- [X : T1 | Γ] /- M2 : T2_, !.
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : (T11 -> T12), Γ /- M2 : T2, T2 <: T11.
Γ /- M1 $ M2 : bot                    :- Γ /- M1 : bot, Γ /- M2 : T2.
Γ /- {Mf} : {Tf}                      :- maplist([L = M, L : T] >> (Γ /- M : T), Mf, Tf).
Γ /- M1 # L : bot                     :- Γ /- M1 : bot.
Γ /- M1 # L : T                       :- Γ /- M1 : {Tf}, member(L : T, Tf).
Γ /- M : _                            :- writeln(error : typeof(Γ, M)), fail. 

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

show(X, T)              :- format('~w : ~w\n', [X, T]).
run(X : T, Γ, [X : T | Γ]) :- x(X), t(T), !, show(X, T).
run(M, Γ, Γ)               :- m(M), !, Γ /- M : T, !, Γ /- M ==>> M_, !, writeln(M_ : T).
run(Ls)                    :- foldl(run, Ls, [], _). 

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

:- run([(fn(x : top) -> x)]). 
:- run([(fn(x : top) -> x) $ (fn(x : top) -> x)]). 
:- run([(fn(x : (top -> top)) -> x) $ (fn(x : top) -> x)]). 
:- run([(fn(r : {[x : (top -> top)]}) -> r # x $ r # x)]). 
:- run([{[x = (fn(z : top) -> z), y = (fn(z : top) -> z)]}]). 
:- run([(fn(x : bot) -> x)]). 
:- run([(fn(x : bot) -> x $ x)]).
:- run([x : top, y : bot, {[1 = x, 2 = y]}]).

:- halt.

fullsub.pl

プログラムの全体を見る

fullsub.pl

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

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

:- use_module(rtg).

w ::= bool | nat | unit | float | string | top | 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                % 文字列型
    | top                   % 最大の型
    | tx                    % 型変数
    | (t -> t)              % 関数の型
    | {list(l : t)}         % レコードの型
    | (all(tx :: t) => t)   % 全称型
    | {some(tx :: t), 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                 % 射影
    | try(m, m)             % エラーの捕捉
    | {(t, m)} as t         % パッケージ化
    | (let(tx, x) = m in m) % アンパッケージ化
    | (fn(tx <: t) => m)    % 型抽象
    | m![t]                 % 型適用
    .
n ::=                       % 数値:
      0                     % ゼロ
    | succ(n)               % 後者値
    .
v ::=                       % 値:
      true                  % 真
    | false                 % 偽
    | n                     % 数値
    | unit                  % 定数unit
    | floatl                % 浮動小数点数値
    | stringl               % 文字列定数
    | (fn(x : t) -> m)      % ラムダ抽象
    | {list(l = v)}         % レコード
    | {(t, v)} as t         % パッケージ化
    | (fn(tx <: t) => m)    % 型抽象
    . 

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

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.
top![(J -> S)] tsubst top.
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_).
(all(TX :: T1) => T2)![(J -> S)] tsubst (all(TX :: T1_) => T2_) :- T1![TX, (J -> S)] tsubst2 T1_, T2![TX, (J -> S)] tsubst2 T2_.
{some(TX :: T1), T2}![(J -> S)] tsubst {some(TX :: T1_), T2_}   :- T1![TX, (J -> S)] tsubst2 T1_, T2![TX, (J -> S)] tsubst2 T2_.
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).
(M1 as T1)![(J -> M)] subst (M1_ as T1)                    :- M1![(J -> M)] subst M1_.
{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_.
({(T1, M2)} as T3)![(J -> M)] subst ({(T1, M2_)} as T3)    :- M2![(J -> M)] subst M2_.
(let(TX, X) = M1 in M2)![(J -> M)] subst (let(TX, X) = M1_ in M2_)
                                                           :- M1![X, (J -> M)] subst2 M1_, M2![X, (J -> M)] subst2 M2_.
(fn(TX <: T) => M2)![(J -> M)] subst (fn(TX <: T) => M2_)  :- M2![(J -> M)] subst M2_.
M1![T2]![(J -> M)] subst (M1_![T2])                        :- M1![(J -> M)] subst M1_.
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_.

true![(J -> S)] tmsubst true.
false![(J -> S)] tmsubst false.
if(M1, M2, M3)![(J -> S)] tmsubst if(M1_, M2_, M3_)            :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_,
                                                                  M3![(J -> S)] tmsubst M3_.
0![(J -> S)] tmsubst 0.
succ(M1)![(J -> S)] tmsubst succ(M1_)                          :- M1![(J -> S)] tmsubst M1_.
pred(M1)![(J -> S)] tmsubst pred(M1_)                          :- M1![(J -> S)] tmsubst M1_.
iszero(M1)![(J -> S)] tmsubst iszero(M1_)                      :- M1![(J -> S)] tmsubst M1_.
unit![(J -> M)] tmsubst unit.
F1![(J -> M)] tmsubst F1                                       :- float(F1).
M1 * M2![(J -> M)] tmsubst M1_ * M2_                           :- M1![(J -> M)] tmsubst M1_, M2![(J -> M)] tmsubst M2_.
X![(J -> M)] tmsubst X                                         :- string(X).
X![(J -> S)] tmsubst X                                         :- x(X).
(fn(X : T1) -> M2)![(J -> S)] tmsubst (fn(X : T1_) -> M2_)     :- T1![(J -> S)] tsubst T1_, M2![(J -> S)] tmsubst M2_.
M1 $ M2![(J -> S)] tmsubst (M1_ $ M2_)                         :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
(let(X) = M1 in M2)![(J -> S)] tmsubst (let(X) = M1_ in M2_)   :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
fix(M1)![(J -> M)] tmsubst fix(M1_)                            :- M1![(J -> M)] tmsubst M1_.
inert(T1)![(J -> M)] tmsubst inert(T1).
(M1 as T1)![(J -> S)] tmsubst (M1_ as T1_)                     :- M1![(J -> S)] tmsubst M1_, T1![(J -> S)] tsubst T1_.
{Mf}![(J -> M)] tmsubst {Mf_}                                  :- maplist([L = Mi, L = Mi_] >> (Mi![(J -> M)] tmsubst Mi_), Mf, Mf_).
M1 # L![(J -> M)] tmsubst M1_ # L                              :- M1![(J -> M)] tmsubst M1_.
({(T1, M2)} as T3)![(J -> M)] tmsubst ({(T1_, M2_)} as T3_)    :- T1![(J -> S)] tsubst T1_, M2![(J -> M)] tmsubst M2_,
                                                                  T3![(J -> S)] tsubst T3_.
(let(TX, X) = M1 in M2)![(J -> M)] tmsubst (let(TX, X) = M1_ in M2_)
                                                               :- M1![TX, (J -> M)] tmsubst2 M1_, M2![TX, (J -> M)] tmsubst2 M2_.
(fn(TX <: T1) => M2)![(J -> S)] tmsubst (fn(TX <: T1_) => M2_) :- T1![TX, (J -> S)] tsubst2 T1_, M2![TX, (J -> S)] tmsubst2 M2_.
M1![T2]![(J -> S)] tmsubst (M1_![T2_])                         :- M1![(J -> S)] tmsubst M1_, T2![(J -> S)] tsubst T2_.
T![X, (X -> S)] tmsubst2 T.
T![X, (J -> S)] tmsubst2 T_                                    :- T![(J -> S)] tmsubst T_.

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_.
Γ /- V1 as _ ==> V1                               :- v(V1).
Γ /- M1 as T ==> M1_ as T                         :- Γ /- M1 ==> M1_.
Γ /- {Mf} ==> {Mf_}                               :- e(Mf, M, Mf_, M_), Γ /- M ==> M_.
Γ /- {Mf} # L ==> M                               :- member(L = M, Mf).
Γ /- M1 # L ==> M1_ # L                           :- Γ /- M1 ==> M1_.
Γ /- {(T1, M2)} as T3 ==> {(T1, M2_)} as T3       :- Γ /- M2 ==> M2_.
Γ /- (let(_, X) = {(T11, V12)} as _ in M2) ==> M  :- v(V12), M2![(X -> V12)] subst M2_, M2_![(X -> T11)] tmsubst M.
Γ /- (let(TX, X) = M1 in M2) ==> (let(TX, X) = M1_ in M2)
                                                  :- Γ /- M1 ==> M1_.
Γ /- (fn(X <: _) => M11)![T2] ==> M11_            :- M11![(X -> T2)] tmsubst M11_.
Γ /- M1![T2] ==> M1_![T2]                         :- Γ /- M1 ==> M1_. 

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

% ------------------------   SUBTYPING  ------------------------

promote(Γ, X, T)   :- tx(X), member(X<:T, Γ).
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.
Γ /- top == top.
Γ /- 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).
Γ /- (all(TX :: S1) => S2) == (all(_ :: T1) => T2) :- Γ /- S1 = T1, [TX-name|Γ] /- S2 = T2.
Γ /- {some(TX :: S1), S2} == {some(_ :: T1), T2}   :- Γ /- S1 = T1, [TX-name|Γ] /- S2 = T2.

Γ /- S <: T                                        :- Γ /- S = T.
Γ /- S <: T                                        :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ <: T_.
Γ \- _ <: top.
Γ \- (S1 -> S2) <: (T1 -> T2)                      :- Γ /- T1 <: S1, Γ /- S2 <: T2.
Γ \- X <: T                                        :- tx(X), promote(Γ, X, S), Γ /- S <: T.
Γ \- {SF} <: {TF}                                  :- maplist([L : T] >> (member(L : S, SF), Γ /- S <: T), TF).
Γ \- (all(TX :: S1) => S2) <: (all(_ :: T1) => T2) :- Γ /- S1 <: T1, Γ /- T1 <: S1, [TX<:T1|Γ] /- S2 <: T2.
Γ \- {some(TX :: S1), S2} <: {some(_ :: T1), T2}   :- Γ /- S1 <: T1, Γ /- T1 <: S1, [TX<:T1|Γ] /- S2 <: T2.

Γ /- S /\ T : T                            :- Γ /- S <: T.
Γ /- S /\ T : S                            :- Γ /- T <: S.
Γ /- S /\ T : R                            :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ /\ T_ : R.
Γ \- {SF} /\ {TF} : {UF_}                  :- include([L : _] >> member(L : _, TF), SF, UF),
                                              maplist([L : S, L : T_] >> (member(L : T, TF), Γ /- S /\ T : T_), UF, UF_).
Γ \- (all(TX :: S1) => S2) /\ (all(_ :: T1) => T2) : (all(TX :: S1) => T2_)
                                           :- Γ /- S1 <: T1, Γ /- T1 <: S1, [TX<:T1|Γ] /- T1 /\ T2 : T2_.
Γ \- (all(TX :: S1) => S2) /\ (all(_ :: T1) => T2) : top.
Γ \- (S1 -> S2) /\ (T1 -> T2) : (S_ -> T_) :- Γ /- S1 \/ T1 : S_, Γ /- S2 /\ T2 : T_.
Γ \- _ /\ _ : top.

Γ /- S \/ T : S                            :- Γ /- S <: T.
Γ /- S \/ T : T                            :- Γ /- T <: S.
Γ /- S \/ T : R                            :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ \/ T_ : R.
Γ \- {SF} \/ {TF} : {UF_}                  :- maplist([L : S, L : T_] >> (member(L : T, TF), Γ /- S \/ T : T_ ; T_ = S), SF, SF_), include([L : _] >> (\+ member(L : _, SF)), TF, TF_), append(SF_, TF_, UF_).
Γ \- (all(TX :: S1) => S2) \/ (all(_ :: T1) => T2) : (all(TX :: S1) => T2_)
                                           :- Γ /- S1 <: T1, Γ /- T1 <: S1, [TX<:T1|Γ] /- T1 \/ T2 : T2_.
Γ \- (S1 -> S2) \/ (T1 -> T2) : (S_ -> T_) :- Γ /- S1 /\ T1 : S_, Γ /- S2 \/ T2 : T_. 

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

lcst(Γ, S, T)  :- simplify(Γ, S, S_), lcst2(Γ, S_, T).
lcst2(Γ, S, T) :- promote(Γ, S, S_), lcst(Γ, S_, T).
lcst2(Γ, T, T). 

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T                           :- Γ /- M1 : T1, Γ /- T1 <: bool,
                                                        Γ /- M2 : T2, Γ /- M3 : T3, Γ /- T2 /\ T3 : T.
Γ /- 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, lcst(Γ, T1, (T11 -> T12)), Γ /- M2 : T2, Γ /- T2 <: T11.
Γ /- (let(X) = M1 in M2) : T                      :- Γ /- M1 : T1, [X:T1|Γ] /- M2 : T.
Γ /- fix(M1) : T12                                :- Γ /- M1 : T1, lcst(Γ, T1, (T11 -> T12)), Γ /- T12 <: T11.
Γ /- inert(T) : T.
Γ /- (M1 as T) : T                                :- Γ /- M1 : T1, Γ /- T1 <: T.
Γ /- {Mf} : {Tf}                                  :- maplist([L = M, L : T] >> (Γ /- M : T), Mf, Tf), !.
Γ /- M1 # L : T                                   :- Γ /- M1 : T1, lcst(Γ, T1, {Tf}), member(L : T, Tf).
Γ /- ({(T1, M2)} as T) : T                        :- simplify(Γ, T, {some(Y :: TBound), T2}), Γ /- T1 <: TBound,
                                                        Γ /- M2 : S2, T2![(Y -> T1)] tsubst T2_, Γ /- S2 <: T2_.
Γ /- (let(TX, X) = M1 in M2) : T2                 :- Γ /- M1 : T1, lcst(Γ, T1, {some(_ :: TBound), T11}),
                                                        [X:T11, TX<:TBound|Γ] /- M2 : T2.
Γ /- (fn(TX <: T1) => M2) : (all(TX :: T1) => T2) :- [TX<:T1|Γ] /- M2 : T2, !.
Γ /- M1![T2] : T12_                               :- Γ /- M1 : T1, lcst(Γ, T1, (all(X :: T11) => T12)),
                                                        Γ /- T2 <: T11, T12![(X -> T2)] tsubst T12_.
Γ /- M : _                                        :- writeln(error : typeof(Γ, M)), fail. 

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

show(X : T)  :- format('~w : %w\n', [X, T]).
show(X <: T) :- format('~w <: %w\n', [X, T]).
show(X :: *) :- format('~w :: *\n', [X]).

run({(TX, X)} = M, Γ, [X:TBody=T12, TX<:TBound|Γ])
                                          :- tx(TX), x(X), m(M), Γ /- M : T, simplify(Γ, T, {some(_ :: TBound), TBody}),
                                             Γ /- M ==>> {(_, T12)} as _, format('~w\n~w : ~w\n', [TX, X, TBody]).
run({(TX, X)} = M, Γ, [X:TBody, TX<:TBound|Γ])
                                          :- tx(TX), x(X), m(M), Γ /- M : T, simplify(Γ, T, {some(_ :: TBound), TBody}),
                                             format('~w\n~w : ~w\n', [TX, X, TBody]).
run(type(X) = T, Γ, [X::T|Γ])   :- tx(X), t(T), show(X :: *).
run(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:T=M_|Γ])   :- x(X), t(T), m(M), Γ /- M : T_, Γ /- T_ = T,
                                   Γ /- M ==>> M_, show(X : T).
run(X = M, Γ, [X:T=M_|Γ])       :- x(X), m(M), Γ /- M : T, Γ /- M ==>> M_, show(X : T).
run(M, Γ, Γ)                    :- !, m(M), !, Γ /- M : T, !, Γ /- M ==>> M_, !, writeln(M_ : T).

run(Ls) :- foldl(run, Ls, [], _). 

% ------------------------   TEST  ------------------------
% lambda x:Top. x;
:- run([(fn(x : top) -> x)]). 
% (lambda x:Top. x) (lambda x:Top. x);
:- run([(fn(x : top) -> x) $ (fn(x : top) -> x)]). 
% (lambda x:Top->Top. x) (lambda x:Top. x);
:- run([(fn(x : (top -> top)) -> x) $ (fn(x : top) -> x)]). 
% (lambda r:{x:Top->Top}. r.x r.x) 
%   {x=lambda z:Top.z, y=lambda z:Top.z};
:- run([(fn(r : {[x : (top -> top)]}) -> r # x $ r # x) $ {[x = (fn(z : top) -> z), y = (fn(z : top) -> z)]}]). 
% "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)]). 
% {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]). 
% if true then {x=true,y=false,a=false} else {y=false,x={},b=false};
:- run([if(true, {[x = true, y = false, a = false]}, {[y = false, x = {[]}, b = false]})]). 
% timesfloat 2.0 3.14159;
:- run([2.0 * 3.14159]). 
% lambda X. lambda x:X. x;
:- run([(fn('X' <: top) => fn(x : 'X') -> x)]). 
% (lambda X. lambda x:X. x) [All X.X->X];
:- run([(fn('X' <: top) => fn(x : 'X') -> x)![(all('X' :: top) => 'X' -> 'X')]]). 
% lambda X<:Top->Top. lambda x:X. x x; 
:- run([(fn('X' <: (top -> top)) => fn(x : 'X') -> x $ x)]). 
% 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))]). 
% {*All Y.Y, lambda x:(All Y.Y). x} as {Some X,X->X};
:- run([{((all('Y' :: top) => 'Y'), (fn(x : (all('Y' :: top) => 'Y')) -> x))} as {some('X' :: top), ('X' -> 'X')}]). 

% {*Nat, {c=0, f=lambda x:Nat. succ x}} as {Some X, {c:X, f:X->Nat}};
:- run([{(nat, {[c = 0, f = (fn(x : nat) -> succ(x))]})} as {some('X' :: top), {[c : 'X', f : ('X' -> nat)]}}]). 
% let {X,ops} = {*Nat, {c=0, f=lambda x:Nat. succ x}} as {Some X, {c:X, f:X->Nat}}
% in (ops.f ops.c);
:- run([(let('X', ops) = {(nat, {[c = 0, f = (fn(x : nat) -> succ(x))]})} as {some('X' :: top), {[c : 'X', f : ('X' -> nat)]}}
         in ops # f $ ops # c)]).

:- halt.

bot.pl

プログラムの全体を見る

bot.pl

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

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

:- use_module(rtg).
w ::= top | bot.                     % キーワード:
syntax(x). x(X) :- \+ w(X), atom(X). % 識別子:

t ::=                                % 型:
    (t -> t)                         % 関数の型
    | top                            % 最大の型
    | bot                            % 最小の型
    .
m ::=                                % 項:
    x                                % 変数
    | (fn(x:t) -> m)                 % ラムダ抽象
    | m $ m                          % 関数適用
    .
v ::=                                % 値:
      fn(x:t) -> m                   % ラムダ抽象
    . 

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

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_.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                           :- S![(J -> M)] subst M_.

% ------------------------   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_.

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

% ------------------------   SUBTYPING  ------------------------

T1  <: T1.
_   <: top.
bot <: _.
(S1 -> S2) <: (T1 -> T2) :- T1 <: S1, S2 <: T2. 

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

Γ /- X:T                          :- x(X), !, member(X:T, Γ).
Γ /- (fn(X:T1) -> M2):(T1 -> T2_) :- [X:T1 | Γ] /- M2:T2_, !.
Γ /- M1 $ M2:T12                  :- Γ /- M1:(T11 -> T12), Γ /- M2:T2, T2 <: T11.
Γ /- M1 $ M2:bot                  :- Γ /- M1:bot, Γ /- M2:T2.
Γ /- M:_                          :- writeln(error:typeof(Γ, M)), fail. 

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

show(X, T)           :- format('~w:~w\n', [X, T]).
run(X:T, Γ, [X:T|Γ]) :- show(X, T).
run(M, Γ, Γ)         :- m(M), !, Γ /- M:T, !, M ==>* M_, !, writeln(M_:T).
run(Ls) :- foldl(run, Ls, [], _). 

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

:- run([(fn(x:top) -> x)]). 
:- run([(fn(x:top) -> x) $ (fn(x:top) -> x)]). 
:- run([(fn(x:(top -> top)) -> x) $ (fn(x:top) -> x)]). 
:- run([(fn(x:bot) -> x)]). 
:- run([(fn(x:bot) -> x $ x)]). 
:- run([y:(bot -> bot), x:bot, y $ x]).

:- halt.

joinexercise.pl

プログラムの全体を見る

joinexercise.pl

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

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

:- use_module(rtg).

w ::= bool | top | true | false.          % キーワード:
syntax(x). x(X) :- \+ w(X), atom(X).      % 識別子:
syntax(l). l(L) :- atom(L) ; integer(L).  % ラベル
list(A) ::= [] | [A | list(A)].           % リスト

t ::=                  % 型:
      bool             % ブール値型
    | top              % 最大の型
    | (t -> t)         % 関数の型
    | {list(l : t)}    % レコードの型
    .
m ::=                  % 項:
      true             % 真
    | false            % 偽
    | if(m, m, m)      % 条件式
    | x                % 型変数
    | (fn(x : t) -> m) % ラムダ抽象
    | m $ m            % 関数適用
    | {list(l = m)}    % レコード
    | m # l            % 射影
    .
v ::=                  % 値:
      true             % 真
    | false            % 偽
    | (fn(x : t) -> m) % ラムダ抽象
    | {list(l = v)}    % レコード
    .

% ------------------------   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_.
{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_.
S![J, (J -> M)] subst2 S.
S![X, (J -> M)] subst2 M_                               :- S![(J -> M)] subst M_.

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_.
Γ /- {Mf} ==> {Mf_}                     :- e(Mf, M, Mf_, M_), Γ /- M ==> M_.
Γ /- {Mf} # L ==> M                     :- member(L = M, Mf).
Γ /- M1 # L ==> M1_ # L                 :- Γ /- M1 ==> M1_.

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

% ------------------------   SUBTYPING  ------------------------

Γ /- T <: T.
Γ /- _ <: top.
Γ /- (S1 -> S2) <: (T1 -> T2) :- Γ /- T1 <: S1, Γ /- S2 <: T2.
Γ /- {SF} <: {TF}             :- maplist([L : T] >> (member(L : S, SF), Γ /- S <: T), TF).

Γ /- S /\ T : U :- halt.  % Write me
Γ /- S \/ T : U :- halt.  % Write me

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

Γ /- true : bool.
Γ /- false : bool.
Γ /- if(M1, M2, M3) : T               :- halt.
Γ /- X : T                            :- x(X), !, gett(Γ, X, T).
Γ /- (fn(X : T1) -> M2) : (T1 -> T2_) :- [X:T1|Γ] /- M2 : T2_.
Γ /- M1 $ M2 : T12                    :- Γ /- M1 : (T11 -> T12), Γ /- M2 : T2, Γ /- T2 <: T11.
Γ /- {Mf} : {Tf}                      :- maplist([L = M, L : T] >> (Γ /- M : T), Mf, Tf).
Γ /- M1 # L : T                       :- Γ /- M1 : {Tf}, member(L : T, Tf).

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

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

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

run(Ls) :- foldl(run, Ls, [], _).

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

% lambda x:Top. x;
:- run([(fn(x : top) -> x)]).
% (lambda x:Top. x) (lambda x:Top. x);
:- run([(fn(x : top) -> x) $ (fn(x : top) -> x)]).
% (lambda x:Top->Top. x) (lambda x:Top. x);
:- run([(fn(x : (top -> top)) -> x) $ (fn(x : top) -> x)]).
% (lambda r:{x:Top->Top}. r.x r.x)
%   {x=lambda z:Top.z, y=lambda z:Top.z};
:- run([(fn(r : {[x : (top -> top)]}) -> r # x $ r # x) $
           {[x = (fn(z : top) -> z), y = (fn(z : top) -> z)]}]).
% 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))]).
% {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]).
% if true then {x=true,y=false,a=false} else {y=false,x={},b=false};
:- run([if(true, {[x = true, y = false, a = false]}, {[y = false, x = {[]}, b = false]})]).

:- halt.

まとめ

部分型付けとは型と型の間の親子関係を表したものです。構造的部分型付けではフィールドが追加されたものかどうかを見ます。

宣言的な部分型付けの規則は左再帰を含むため、そのまま実装すると無限ループに陥ります。そのためアルゴリズム的ではありません。
アルゴリズム的な部分型付け規則は自動的に計算可能ですが多少規則は複雑になります。

Snake
From Wikipedia, the free encyclopedia

Snakes are elongated, legless, carnivorous reptiles of the suborder Serpentes.[2] Like all other squamates, snakes are ectothermic, amniote vertebrates covered in overlapping scales. Many species of snakes have skulls with several more joints than their lizard ancestors, enabling them to swallow prey much larger than their heads with their highly mobile jaws. To accommodate their narrow bodies, snakes' paired organs (such as kidneys) appear one in front of the other instead of side by side, and most have only one functional lung. Some species retain a pelvic girdle with a pair of vestigial claws on either side of the cloaca. Lizards have evolved elongate bodies without limbs or with greatly reduced limbs about twenty-five times independently via convergent evolution, leading to many lineages of legless lizards.[3] Legless lizards resemble snakes, but several common groups of legless lizards have eyelids and external ears, which snakes lack, although this rule is not universal (see Amphisbaenia, Dibamidae, and Pygopodidae).