メルクリウス

メルクリウス (Mercurius) はローマ神話のデイ・コンセンテス (Dei Consentes) の一人であり、商人や旅人の守護神である[1]。英語読みでマーキュリー (Mercury) とも表記される。

ギリシア神話の神々の伝令使ヘルメースと同化し、雄弁家、盗賊、商人、職人の庇護者とされた。ヘルメースと融合する前の元来の職能や性格は明瞭でないが、その名は merces （商品、財貨）に関係があるとも言われる商業の神である[2]。ニュンペーのラールンダとの間にラールたち（ラレース）をもうけた。

メルクリウスの神殿は紀元前496年にアウェンティヌス丘の上に建てられたとされるが、これはローマの聖所ポメリウムの外にあったため、元からローマにいた神ではなく、外部から来た神と考えられている。

ローマ暦では、水曜日をメルクリウスの日 Diēs Mercuriī （ディエース・メルクリイー）としている。

カール・グスタフ・ユングは「メルクリウス」について次のように述べる。

「メルクリウスは（錬金術でいうところの、即ち、無意識の）作業（オプス）の始めに位置し、終りに位置する。

メルクリウスは原初の両性具有存在ヘルマプロディートスであり、一旦は二つに分れて古典的な兄－妹の対の形を取るが、最後に「結合」において再び一つに結びつき、「新しい光」、即ち、「賢者の石」という形態をとって光り輝く。

メルクリウスは金属であるが同時に液体でもあり（「メルクリウス＝水星」を象徴する金属は水銀）、物質でもあるが同時に霊でもあり、冷たいが同時に火と燃え、毒であるが同時に妙薬でもあり、『諸対立を一つに結びつける対立物の合一の象徴なのである。』」

「メルクリウス」の変容性と多様性は錬金術の根本表象であり、即ち、「メルクリウス」は我々の無意識、心的世界の一つの表象といえる。

「ライオンとユニコーン」は共に、錬金術における「メルクリウス」の象徴であるとされる。他に、「鳩、鹿、鷲、龍」なども「メルクリウス」の同義語とされる。

有界量化とは、大雑把にいうと、部分型付けの型を有界量化子として設定しておき、型適用することで多相的に使えるようにすることだった気がします。型の範囲を制限するので境界を示すパラメータがあるので、境界があるから有界なのかな。

% 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')]]).

パラメータの型には全称量化子の∀のかわりにallと書いたりしてます。
全称型は型適用をすることで通常の型にできるので普通に使えるようになります。

t ::=                     % 型
      top                 % 最大の型
    | tx                  % 変数
    | (t -> t)            % 関数の型
    | (all(tx :: t) => t) % 全称型
    .
m ::=                     % 項
      x                   % 変数
    | (fn(x : t) -> m)    % ラムダ抽象
    | m $ m               % 関数適用
    | (fn(tx <: t) => m)  % 型抽象
    | m![t]               % 型適用
    .
v ::=                     % 値:
      (fn(x : t) -> m)    % ラムダ抽象
    | (fn(tx <: t) => m)  % 型抽象
    .

pure な fsub は System F で部分型付けがあるシステムなのですな。

TAPL26,28 有界量化有界量化のメタ理論

図26-1.有界量化（カーネルF<:）

→ ∀ <: Top System F(図23-1)と単調型付け(図15-1)に基づく

構文

t ::=      項：
  x        変数
  λx:T.t   ラムダ抽象
  t t      関数適用
  λX<:T.t  型抽象
  t [T]    型適用
v ::=      値：
  λx:T.t   ラムダ抽象値
  λX<:T.t  型抽象値
T ::=      型：
  X        型変数
  Top      最大の型
  T->T     関数の型
  ∀X<:T.T  全称型
Γ::=       文脈：
  ∅       からの文脈
  Γ,x:T    項変数の束縛
  Γ,X<:T   型変数の束縛

評価 t ==> t’

t1 ==> t1’
-------------------------------- (E-App1)
t1 t2 ==> t1’ t2

t2 ==> t2’
-------------------------------- (E-App2)
v1 t2 ==> v1 t2’

t1 ==> t1’
-------------------------------- (E-TApp)
t1 [T2] ==> t1’ [T2]

(λX<:T11.t12)[T2] ==> [X->T2]t12 (E-TAppTAbs)
(λ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)

X <: T∈Γ
--------------------------------- (S-TVar)
Γ ⊢ X <: T

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

Γ,X<:U1 ⊢ S2 <: T2
--------------------------------- (S-All)
Γ ⊢ ∀X<:U1.S2 <: ∀X<:U1.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

Γ,X<:T1 ⊢ t2 : T2
-------------------------------------- (T-TAbs)
Γ ⊢ λX<:T1.t2 : ∀X.T2

Γ ⊢ t1 : ∀X<:T11.T12   Γ ⊢ T2 <: T11
-------------------------------------- (T-TApp)
Γ ⊢ t1[T2] : [X -> T2] T12

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

図28-1.F<:の型露出アルゴリズム

→ ∀ <: Top

露出 Γ ↦ T ⇑ T’

X <: T ∈ Γ   Γ ↦ T ⇑ T’
--------------------------- (XA-Promote)
Γ ↦ X ⇑ T’

Tは型変数でない
--------------------------- (XA-Other)
Γ ↦ T ⇑ T

図28-2.F<:のアルゴリズム的型付け

→ ∀ <: Top λ<: (図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

Γ,X<:T1 ↦ t2 : T2

図28-3.カーネルF<:のアルゴリズム的部分型付け

→ ∀ <: Top λ<: (図16-2)の拡張

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

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

Γ |-> X <: X                       (SA-Refl-TVar)

X <: U ∈ Γ   Γ |-> U <: T
--------------------------------- (SA-Trans-TVar)
Γ |-> X <: T

Γ |-> T1 <: S1　　Γ |-> S2 <: T2
-------------------------------------- (SA-Arrow)
Γ |-> S1 -> S2 <: T1 -> T2

Γ,X<:U1 |-> S2 <: T2
---------------------------------------- (SA-All)
Γ |-> ∀X<:U1.S2 <: ∀X<:U1.T2

図28-4.フルF<:のアルゴリズム的部分型付け

→ ∀ <: Top フル図28-1の拡張

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

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

Γ |-> X <: X                       (SA-Refl-TVar)

X <: U ∈ Γ   Γ |-> U <: T
--------------------------------- (SA-Trans-TVar)
Γ |-> X <: T

Γ |-> T1 <: S1　　Γ |-> S2 <: T2
-------------------------------------- (SA-Arrow)
Γ |-> S1 -> S2 <: T1 -> T2

Γ |-> T1 <: S1   Γ,X<:T1 |-> S2 <: T2
---------------------------------------- (SA-All)
Γ |-> ∀X<:S1.S2 <: ∀X<:T1.T2

図28-5.カーネルF<:の結びと交わりを求めるアルゴリズム

→ ∀ <: Top

Γ ⊢ S ∨ T =
    T            Γ ⊢ S <: Tの場合
    S            Γ ⊢ T <: Sの場合
    J            S = X
                 X<:U ∈ Γ
                 Γ ⊢ U ∨ T = Jの場合
    J            T = X
                 X<:U ∈ Γ
                 Γ ⊢ S ∨ U = Jの場合
    M1->J2       S = S1->S2
                 T = T1->T2
                 Γ ⊢ S1 ∨ T1 = M1
                 Γ ⊢ S2 ∨ T2 = J2の場合
    ∀X<:U1.J2   S = ∀X<:U1.S2
                 T = ∀X<:U1.T2
                 Γ,X<:U1 ⊢ S2 ∨ T2 = J2
                    の場合
    Top          それ以外の場合

Γ ⊢ S ∧ T =
    S            Γ ⊢ S <: Tの場合
    T            Γ ⊢ T <: Sの場合
    J1->M2       S = S1->S2
                 T = T1->T2
                 Γ ⊢ S1 ∨ T1 = J1
                 Γ ⊢ S2 ∧ T2 = M2の場合
    ∀X<:U1.M2   S = ∀X<:U1.S2
                 T = ∀X<:U1.T2
                 Γ,X<:U1 ⊢ S2 ∧ T2 = M2
                    の場合
    fail         それ以外の場合

実装

purefsub 有界量化 λ+top+<:(28章)
fullfsub フルF<: 有界量化 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+top+<:+all+some(26,28章)
fullfsubref フルF<: 有界量化+参照 bool+nat+unit+float+string+λ+let+letrec+fix+inert+as+record+case of+try error+ref+top+bot+<:+source+sink+all (27章)

purefsub.pl

プログラムの全体を見る

purefsub.pl

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

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

:- use_module(rtg).

w ::= top. % キーワード:
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 ::=                     % 型
      top                 % 最大の型
    | tx                  % 変数
    | (t -> t)            % 関数の型
    | (all(tx :: t) => t) % 全称型
    .
m ::=                     % 項
      x                   % 変数
    | (fn(x : t) -> m)    % ラムダ抽象
    | m $ m               % 関数適用
    | (fn(tx <: t) => m)  % 型抽象
    | m![t]               % 型適用
    .
v ::=                     % 値:
      (fn(x : t) -> m)    % ラムダ抽象
    | (fn(tx <: t) => m)  % 型抽象
    . 

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

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_.
(all(TX :: T1) => T2)![(J -> S)] tsubst (all(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_.

J![(J -> M)] subst M                                        :- x(J).
X![(J -> M)] subst X                                        :- x(X).
(fn(X1 : T1) -> M2)![(J -> M)] subst (fn(X1 : T1) -> M2_)   :- M2![X1, (J -> M)] subst2 M2_.
M1 $ M2![(J -> M)] subst (M1_ $ M2_)                        :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
(fn(TX <: T1) => M2)![(J -> M)] subst (fn(TX <: T1) => M2_) :- M2![(J -> M)] subst M2_.
M1![T2]![(J -> M)] subst (M1_![T2])                         :- M1![(J -> M)] subst M1_.
A![(J -> M)] subst B                                        :- writeln(error : A![(J -> M)] subst B), fail.
T![X, (X -> M)] subst2 T.
T![X, (J -> M)] subst2 T_                                   :- T![(J -> M)] subst T_.

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_.
(fn(TX <: T1) => M2)![(J -> S)] tmsubst (fn(TX <: T1_) => M2_) :- T1![(J -> S)] tsubst 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_.

% ------------------------   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_.
Γ /- (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, Γ).

Γ /- T1 <: T1.
Γ /- _  <: top.
Γ /- (S1 -> S2) <: (T1 -> T2)                      :- Γ /- T1 <: S1, Γ /- S2 <: T2.
Γ /- X <: T                                        :- tx(X), promote(Γ, X, S), Γ /- S <: T.
Γ /- (all(TX :: S1) => S2) <: (all(_ :: T1) => T2) :- Γ /- S1 <: T1, Γ /- T1 <: S1,
                                                         [TX <: T1 | Γ] /- S2 <: T2. 

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

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

Γ /- X : T                                        :- x(X), !, member(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.
Γ /- (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]).
showSub(X, T) :- format('~w <: ~w\n', [X, T]).

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

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

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

% 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. 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 X<:Top->Top. lambda x:X. x x;
:- run([(fn('X' <: (top -> top)) => fn(x : 'X') -> x $ x)]).
:- run([x : top, x]).
:- run(['T' <: (top -> top), x : 'T']).

:- halt.

fullfsub.pl

プログラムの全体を見る

fullfsub.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.

fullfsubref.pl

プログラムの全体を見る

fullfsubref.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 | bot | true | false | error. % キーワード:
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(integer).                           % 整数
syntax(l). l(L) :- atom(L) ; integer(L).   % ラベル
list(A) ::= [] | [A | list(A)].            % リスト

t ::=                           % 型:
      bool                      % ブール値型
    | nat                       % 自然数型
    | unit                      % Unit型
    | float                     % 浮動小数点数型
    | string                    % 文字列型
    | top                       % 最大の型
    | bot                       % 最小の型
    | tx                        % 型変数
    | (t -> t)                  % 関数の型
    | {list(l : t)}             % レコードの型
    | [list(x : t)]             % バリアント型
    | ref(t)                    % 参照セルの型
    | source(t)
    | sink(t)
    | (all(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                     % 射影
    | case(m, list(x = (x, m))) % 場合分け
    | tag(x, m) as t            % タグ付け
    | loc(integer)              % ストアでの位置
    | ref(m)                    % 参照の生成
    | '!'(m)                    % 参照先の値の取り出し
    | m := m                    % 破壊的代入
    | error                     % 実行時エラー
    | try(m, 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)}             % レコード
    | tag(x, v) as t            % タグ付け
    | loc(integer)              % ストアでの位置
    | (fn(tx <: t) => m)        % 型抽象
    .

% ------------------------   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.
top![(J -> S)] tsubst top.
bot![(J -> S)] tsubst bot.
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_).
ref(T1)![(J -> S)] tsubst ref(T1_)                              :- T1![(J -> S)] tsubst T1_.
source(T1)![(J -> S)] tsubst source(T1_)                        :- T1![(J -> S)] tsubst T1_.
sink(T1)![(J -> S)] tsubst sink(T1_)                            :- T1![(J -> S)] tsubst T1_.
(all(TX :: T1) => T2)![(J -> S)] tsubst (all(TX :: T1_) => T2_) :- T1![TX, (J -> S)] tsubst2 T1_, T2![TX, (J -> S)] tsubst2 T2_.
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).
(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_.
(tag(L, M1) as T1)![(J -> M)] subst (tag(L, 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_).
ref(M1)![(J -> M)] subst ref(M1_)                           :- M1![(J -> M)] subst M1_.
'!'(M1)![(J -> M)] subst '!'(M1_)                           :- M1![(J -> M)] subst M1_.
(M1 := M2)![(J -> M)] subst (M1_ := M2_)                    :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
loc(L)![(J -> M)] subst loc(L).
try(M1, M2)![(J -> M)] subst try(M1_, M2_)                  :- M1![(J -> M)] subst M1_, M2![(J -> M)] subst M2_.
error![(J -> M)] subst error.
(fn(TX <: T1) => M2)![(J -> M)] subst (fn(TX <: T1) => 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 -> S)] tmsubst unit.
F1![(J -> S)] tmsubst F1                                       :- float(F1).
M1 * M2![(J -> S)] tmsubst M1_ * M2_                           :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
X![(J -> S)] 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 -> S)] tmsubst fix(M1_)                            :- M1![(J -> S)] tmsubst M1_.
inert(T1)![(J -> S)] tmsubst inert(T1).
(M1 as T1)![(J -> S)] tmsubst (M1_ as T1_)                     :- M1![(J -> S)] tmsubst M1_, T1![(J -> S)] tsubst T1_.
{Mf}![(J -> S)] tmsubst {Mf_}                                  :- maplist([L = Mi, L = Mi_] >> (Mi![(J -> S)] tmsubst Mi_), Mf, Mf_).
M1 # L![(J -> S)] tmsubst M1_ # L                              :- M1![(J -> S)] tmsubst M1_.
(tag(L, M1) as T1)![(J -> S)] tmsubst (tag(L, M1_) as T1_)     :- M1![(J -> S)] tmsubst M1_, T1![(J -> S)] tsubst T1_.
case(M1, Cases)![(J -> S)] tmsubst case(M1_, Cases_)           :- M1![(J -> S)] tmsubst M1_,
                                                                  maplist([L = (X, M2), L = (X, M2_)] >> (M2![(J -> S)] subst M2_), Cases, Cases_).
ref(M1)![(J -> S)] tmsubst ref(M1_)                            :- M1![(J -> S)] tmsubst M1_.
'!'(M1)![(J -> S)] tmsubst '!'(M1_)                            :- M1![(J -> S)] tmsubst M1_.
(M1 := M2)![(J -> S)] tmsubst (M1_ := M2_)                     :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
loc(L)![(J -> S)] tmsubst loc(L).
try(M1, M2)![(J -> S)] tmsubst try(M1_, M2_)                   :- M1![(J -> S)] tmsubst M1_, M2![(J -> S)] tmsubst M2_.
error![(J -> S)] tmsubst error.
(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  ------------------------

extendstore(St, V1, Len, St_)            :- length(St, Len), append(St, [V1], St_).
lookuploc(St, L, R)                      :- nth0(L, St, R).
updatestore([_ | St], 0, V1, [V1 | St]).
updatestore([V | St], N1, V1, [V | St_]) :- N is N1 - 1, updatestore(St, N, V1, St_).

eval_context(if(M1, M2, M3), ME, if(MH, M2, M3), H)           :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(succ(M1), ME, succ(MH), H)                       :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(pred(M1), ME, pred(MH), H)                       :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(iszero(M1), ME, iszero(MH), H)                   :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(M1 * M2, ME, MH * M2, H)                         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(V1 * M2, ME, V1 * MH, H)                         :- \+ v(M2), eval_context(M1, ME, MH, H).
eval_context(M1 $ M2, ME, MH $ M2, H)                         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(V1 $ M2, ME, V1 $ MH, H)                         :- \+ v(M2), eval_context(M2, ME, MH, H).
eval_context((let(X) = M1 in M2), ME, (let(X) = MH in M2), H) :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(fix(M1), ME, fix(MH), H)                         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(M1 as T, ME, MH as T, H)                         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(M1 # L, ME, MH # L, H)                           :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(tag(L, M1) as T, ME, tag(L, MH) as T, H)         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(case(M1, Branches), ME, case(MH, Branches), H)   :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(ref(M1), ME, ref(MH), H)                         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context('!'(M1), ME, '!'(MH), H)                         :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(M1 := M2, ME, MH := M2, H)                       :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context(V1 := M2, ME, V1 := MH, H)                       :- \+ v(M2), eval_context(M2, ME, MH, H).
eval_context(M1![T], ME, MH![T], H)                           :- \+ v(M1), eval_context(M1, ME, MH, H).
eval_context({Mf}, ME, {MH}, H)                               :- \+ v({Mf}), e(Mf, ME, MH, H).
eval_context(try(M1, M2), M1, try(H, M2), H).
eval_context(M1, M1, H, H)                                    :- \+ v(M1).

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

Γ/St /- if(true, M2, M3) ==> M2/St.
Γ/St /- if(false, M2, M3) ==> M3/St.
Γ/St /- pred(0) ==> 0/St.
Γ/St /- pred(succ(NV1)) ==> NV1/St           :- n(NV1).
Γ/St /- iszero(0) ==> true/St.
Γ/St /- iszero(succ(NV1)) ==> false/St       :- n(NV1).
Γ/St /- F1 * F2 ==> F3/St                    :- float(F1), float(F2), F3 is F1 * F2.
Γ/St /- X ==> M/St                           :- x(X), member(X:_=M, Γ).
Γ/St /- (fn(X : _) -> M12) $ V2 ==> R/St     :- v(V2), M12![(X -> V2)] subst R.
Γ/St /- (let(X) = V1 in M2) ==> M2_/St       :- v(V1), M2![(X -> V1)] subst M2_.
Γ/St /- fix((fn(X : T11) -> M12)) ==> M/St   :- M12![(X -> fix((fn(X : T11) -> M12)))] subst M.
Γ/St /- V1 as _ ==> V1/St                    :- v(V1).
Γ/St /- {Mf} # L ==> M/St                    :- v({Mf}), member(L = M, Mf).
Γ/St /- case(tag(L, V11) as _, Bs) ==> M_/St :- v(V11), member(L = (X, M), Bs), M![(X -> V11)] subst M_.
Γ/St /- ref(V1) ==> loc(L)/St_               :- v(V1), extendstore(St, V1, L, St_).
Γ/St /- '!'(loc(L)) ==> V1/St                :- lookuploc(St, L, V1).
Γ/St /- (loc(L) := V2) ==> unit/St_          :- v(V2), updatestore(St, L, V2, St_).
Γ/St /- (fn(X) => M11)![T2] ==> M11_/St      :- M11![(X -> T2)] tmsubst M11_.
Γ/St /- try(error, M2) ==> M2/St.
Γ/St /- try(V1, M2) ==> V1/St                :- v(V1).
Γ/St /- try(M1, M2) ==> try(M1_, M2)/St_     :- Γ/St /- M1 ==> M1_/St_.
Γ/St /- error ==> _/_                        :- !, fail.
Γ/St /- M ==> error/St                       :- eval_context(M, error, _, _), !.
Γ/St /- M ==> M_/St_                         :- eval_context(M, ME, M_, H), M \= ME, Γ/St /- ME ==> H/St_.

Γ/St /- M ==>> M_/St_ :- Γ/St /- M ==> M1/St1, !, Γ/St1 /- M1 ==>> M_/St_, !.
Γ/St /- M ==>> M/St.

% ------------------------   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.
Γ /- bot == bot.
Γ /- 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).
Γ /- ref(S) == ref(T)         :- Γ /- S = T.
Γ /- source(S) == source(T)   :- Γ /- S = T.
Γ /- sink(S) == sink(T)       :- Γ /- S = T.
Γ /- (all(TX :: S1) => S2) == (all(_ :: T1) => T2)
                              :- Γ /- S1 = T1, [TX-name|Γ] /- S2 = T2.

Γ /- S <: T                   :- Γ /- S = T.
Γ /- S <: T                   :- simplify(Γ, S, S_), simplify(Γ, T, T_), Γ \- S_ <: T_.
Γ \- _ <: top.
Γ \- bot <: _.
Γ \- X <: T                   :- tx(X), promote(Γ, X, S), Γ /- S <: T.
Γ \- (S1 -> S2) <: (T1 -> T2) :- Γ /- T1 <: S1, Γ /- S2 <: T2.
Γ \- {SF} <: {TF}             :- maplist([L : T] >> (member(L : S, SF), Γ /- S <: T), TF).
Γ \- [SF] <: [TF]             :- maplist([L : S] >> (member(L : T, TF), Γ /- S <: T), SF).
Γ \- ref(S) <: ref(T)         :- Γ /- S <: T, Γ /- T <: S.
Γ \- ref(S) <: source(T)      :- Γ /- S <: T.
Γ \- source(S) <: source(T)   :- Γ /- S <: T.
Γ \- ref(S) <: sink(T)        :- Γ /- T <: S.
Γ \- sink(S) <: sink(T)       :- Γ /- T <: S.
Γ \- (all(TX :: S1) => S2) <: (all(_ :: 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_.
Γ \- ref(S) /\ ref(T) : ref(S)             :- Γ /- S <: T, Γ /- T <: S.
Γ \- ref(S) /\ ref(T) : source(T_)         :- /* Warning: this is incomplete... */ Γ /- S /\ T : T_.
Γ \- source(S) /\ source(T) : source(T_)   :- Γ /- S /\ T : T_.
Γ \- ref(S) /\ source(T) : source(T_)      :- Γ /- S /\ T : T_.
Γ \- source(S) /\ ref(T) : source(T_)      :- Γ /- S /\ T : T_.
Γ \- sink(S) /\ sink(T) : sink(T_)         :- Γ /- S \/ T : T_.
Γ \- ref(S) /\ sink(T) : sink(T_)          :- Γ /- S \/ T : T_.
Γ \- sink(S) /\ ref(T) : sink(T_)          :- Γ /- S \/ T : 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_.
Γ \- ref(S) \/ ref(T) : ref(T)             :- Γ /- S <: T, Γ /- T <: S.
Γ \- ref(S) \/ ref(T) : source(T_)         :- Γ /- S \/ T : T_.
Γ \- source(S) \/ source(T) : source(T_)   :- Γ /- S \/ T : T_.
Γ \- ref(S) \/ source(T) : source(T_)      :- Γ /- S \/ T : T_.
Γ \- source(S) \/ ref(T) : source(T_)      :- Γ /- S \/ T : T_.
Γ \- sink(S) \/ sink(T) : sink(T_)         :- Γ /- S /\ T : T_.
Γ \- ref(S) \/ sink(T) : sink(T_)          :- Γ /- S /\ T : T_.
Γ \- sink(S) \/ ref(T) : sink(T_)          :- Γ /- S /\ T : T_.
Γ \- _ \/ _ : bot.

% ------------------------   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 : bot                                :- Γ /- M1 : T1, Γ /- M2 : T2, lcst(Γ, T1, bot).
Γ /- 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.
Γ /- fix(M1) : bot                                :- Γ /- M1 : T1, lcst(Γ, T1, bot).
Γ /- 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).
Γ /- M1 # L : bot                                 :- Γ /- M1 : T1, lcst(Γ, T1, bot).
Γ /- (tag(Li, Mi) as T) : T                       :- simplify(Γ, T, [Tf]), member(Li : Te, Tf), Γ /- Mi : T_, Γ /- T_ <: Te.
Γ /- case(M, Cases) : bot                         :- Γ /- M : T, lcst(Γ, T, bot),
                                                        maplist([L = _] >> member(L : _, Tf), Cases),
                                                        maplist([Li = (Xi, Mi)] >> (
                                                          member(Li : Ti, Tf),
                                                          [Xi:Ti|Γ] /- Mi : Ti_
                                                        ), Cases).
Γ /- case(M, Cases) : T_                          :- Γ /- M : T, lcst(Γ, T, [Tf]),
                                                        maplist([L = _] >> member(L : _, Tf), Cases),
                                                        maplist([Li = (Xi, Mi), Ti_] >> (
                                                          member(Li : Ti, Tf),
                                                          [Xi:Ti|Γ] /- Mi : Ti_
                                                        ), Cases, CaseTypes),
                                                        foldl([S, T1, U] >> (Γ /- S /\ T1 : U), CaseTypes, bot, T_).
Γ /- ref(M1) : ref(T1)                            :- Γ /- M1 : T1.
Γ /- '!'(M1) : T1                                 :- Γ /- M1 : T, lcst(Γ, T, ref(T1)).
Γ /- '!'(M1) : bot                                :- Γ /- M1 : T, lcst(Γ, T, bot).
Γ /- '!'(M1) : T1                                 :- Γ /- M1 : T, lcst(Γ, T, source(T1)).
Γ /- (M1 := M2) : unit                            :- Γ /- M1 : T, lcst(Γ, T, ref(T1)), Γ /- M2 : T2, Γ /- T2 <: T1.
Γ /- (M1 := M2) : bot                             :- Γ /- M1 : T, lcst(Γ, T, bot), Γ /- M2 : _.
Γ /- (M1 := M2) : unit                            :- Γ /- M1 : T, lcst(Γ, T, sink(T1)), Γ /- M2 : T2, Γ /- T2 <: T1.
Γ /- loc(l) : _                                   :- !, fail.
Γ /- try(M1, M2) : T                              :- Γ /- M1 : T1, Γ /- M2 : T2, Γ /- T1 /\ T2 : T.
Γ /- error : bot.
Γ /- (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_.

% ------------------------   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(type(X) = T, Γ/St, [X::T|Γ]/St)  :- tx(X), t(T), show(X :: *).
run(X <: T, Γ/St, [X<:T|Γ]/St)       :- tx(X), t(T), show(X <: T).
run(X : T, Γ/St, [X:T|Γ]/St)         :- x(X), t(T), show(X : T).
run(X : T = M, Γ/St, [X:T=M_|Γ]/St_) :- x(X), t(T), m(M), Γ /- M : T_, Γ /- T_ = T,
                                        Γ/St /- M ==>> M_/St_, !, show(X : T).
run(X = M, Γ/St, [X:T=M_|Γ]/St_)     :- x(X), m(M), Γ /- M : T,
                                        Γ/St /- M ==>> M_/St_, !, show(X : T).
run(M, Γ/St, Γ/St_)                  :- m(M), !, Γ /- M : T, !,
                                        Γ/St /- M ==>> M_/St_, !, writeln(M_ : T).

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

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

% lambda x:Bot. x;
:- run([(fn(x : bot) -> x)]).
% lambda x:Bot. x x;
:- run([(fn(x : bot) -> x $ x)]).
% lambda x:<a:Bool,b:Bool>. x;
:- run([(fn(x : [[a : bool, b : bool]]) -> x)]).
% 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))]).
% if error then true else false;
:- run([if(error, true, false)]).

% error true;
:- run([error $ true]).
% (lambda x:Bool. x) error;
:- run([(fn(x : bool) -> x) $ error]).
% 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))]).

/* Alternative object encodings */
:- run([
% CounterRep = {x: Ref Nat};
type('CounterRep') = {[x : ref(nat)]},
% SetCounter = {get:Unit->Nat, set:Nat->Unit, inc:Unit->Unit};
type('SetCounter') = {[
  get : (unit -> nat),
  set : (nat -> unit),
  inc : (unit -> unit)
  ]},
% setCounterClass =
%   lambda r:CounterRep.
%     lambda self: Unit->SetCounter.
%       lambda _:Unit.
%         { get = lambda _:Unit. !(r.x),
%           set = lambda i:Nat.  r.x:=i,
%           inc = lambda _:Unit. (self unit).set (succ((self unit).get unit))}
%         as SetCounter;
setCounterClass =
  (fn(r : 'CounterRep') ->
    fn(self : (unit -> 'SetCounter')) ->
      fn('_' : unit) ->
        {[get = (fn('_' : unit) -> '!'(r # x)),
          set = (fn(i : nat) -> r # x := i),
          inc = (fn('_' : unit) -> (self $ unit) # set $ succ((self $ unit) # get $ unit))
        ]} as 'SetCounter'),
% newSetCounter =
%   lambda _:Unit.
%     let r = {x=ref 1} in
%     fix (setCounterClass r) unit;
newSetCounter =
  (fn('_' : unit) ->
    (let(r) = {[x = ref(succ(0))]} in
    fix(setCounterClass $ r) $ unit)),
% c = newSetCounter unit;
c = newSetCounter $ unit, c # get $ unit,
% InstrCounter = { get:Unit->Nat,
%                  set:Nat->Unit,
%                  inc:Unit->Unit,
%                  accesses:Unit->Nat};
type('InstrCounter') = {[get : (unit -> nat),
                         set : (nat -> unit),
                         inc : (unit -> unit),
                         accesses : (unit -> nat)]},
% InstrCounterRep = {x: Ref Nat, a: Ref Nat};
type('InstrCounterRep') = {[x : ref(nat), a : ref(nat)]},
% instrCounterClass =
%   lambda r:InstrCounterRep.
%   lambda self: Unit->InstrCounter.
%   lambda _:Unit.
%   let super = setCounterClass r self unit in
%   { get = super.get,
%     set = lambda i:Nat. (r.a:=succ(!(r.a)); super.set i),
%     inc = super.inc,
%     accesses = lambda _:Unit. !(r.a)} as InstrCounter;
instrCounterClass =
  (fn(r : 'InstrCounterRep') ->
    fn(self : (unit -> 'InstrCounter')) ->
      fn('_' : unit) ->
        (let(super) = setCounterClass $ r $ self $ unit in
        {[get = super # get,
          set = (fn(i : nat) -> (let('_') = (r # a := succ('!'(r # a))) in super # set $ i)),
          inc = super # inc, accesses = (fn('_' : unit) -> '!'(r # a))
        ]} as 'InstrCounter')),

% newInstrCounter =
%   lambda _:Unit.
%     let r = {x=ref 1, a=ref 0} in
%     fix (instrCounterClass r) unit;
newInstrCounter =
  (fn('_' : unit) ->
    (let(r) = {[x = ref(succ(0)), a = ref(0)]} in
     fix(instrCounterClass $ r) $ unit)),
% ic = newInstrCounter unit;
ic = newInstrCounter $ unit,
ic # get $ unit,
ic # accesses $ unit,
ic # inc $ unit,
ic # get $ unit,
ic # accesses $ unit,

/* ------------ */

% instrCounterClass =
% lambda r:InstrCounterRep.
% lambda self: Unit->InstrCounter.
% lambda _:Unit.
% let super = setCounterClass r self unit in
% {get = lambda _:Unit. (r.a:=succ(!(r.a)); super.get unit),
% set = lambda i:Nat. (r.a:=succ(!(r.a)); super.set i),
% inc = super.inc,
% accesses = lambda _:Unit. !(r.a)} as InstrCounter;
instrCounterClass = (fn(r : 'InstrCounterRep') ->
  fn(self : (unit -> 'InstrCounter')) ->
    fn('_' : unit) -> (let(super) = setCounterClass $ r $ self $ unit in
      {[get = (fn('_' : unit) -> (fn('_' : unit) -> super # get $ unit) $ (r # a := succ('!'(r # a)))),
        set = (fn(i : nat) -> (fn('_' : unit) -> super # set $ i) $ (r # a := succ('!'(r # a)))),
        inc = super # inc,
        accesses = (fn('_' : unit) -> '!'(r # a))
      ]} as 'InstrCounter')),

% ResetInstrCounter = {get:Unit->Nat, set:Nat->Unit,
% inc:Unit->Unit, accesses:Unit->Nat,
% reset:Unit->Unit};
type('ResetInstrCounter') =
  {[get : (unit -> nat),
    set : (nat -> unit),
    inc : (unit -> unit),
    accesses : (unit -> nat),
    reset : (unit -> unit)]},

% resetInstrCounterClass =
% lambda r:InstrCounterRep.
% lambda self: Unit->ResetInstrCounter.
% lambda _:Unit.
% let super = instrCounterClass r self unit in
% {get = super.get,
% set = super.set,
% inc = super.inc,
% accesses = super.accesses,
% reset = lambda _:Unit. r.x:=0}
% as ResetInstrCounter;
resetInstrCounterClass =
  (fn(r : 'InstrCounterRep') ->
    fn(self : (unit -> 'ResetInstrCounter')) ->
      fn('_' : unit) ->
        (let(super) = instrCounterClass $ r $ self $ unit in
        {[get = super # get,
          set = super # set,
          inc = super # inc,
          accesses = super # accesses,
          reset = (fn('_' : unit) -> r # x := 0)
        ]} as 'ResetInstrCounter')),

% BackupInstrCounter = {get:Unit->Nat, set:Nat->Unit,
% inc:Unit->Unit, accesses:Unit->Nat,
% backup:Unit->Unit, reset:Unit->Unit};
type('BackupInstrCounter') =
  {[get : (unit -> nat),
    set : (nat -> unit),
    inc : (unit -> unit),
    accesses : (unit -> nat),
    backup : (unit -> unit),
    reset : (unit -> unit)]},

% BackupInstrCounterRep = {x: Ref Nat, a: Ref Nat, b: Ref Nat};
type('BackupInstrCounterRep') = {[x : ref(nat), a : ref(nat), b : ref(nat)]},

% backupInstrCounterClass =
% lambda r:BackupInstrCounterRep.
% lambda self: Unit->BackupInstrCounter.
% lambda _:Unit.
% let super = resetInstrCounterClass r self unit in
% {get = super.get,
% set = super.set,
% inc = super.inc,
% accesses = super.accesses,
% reset = lambda _:Unit. r.x:=!(r.b),
% backup = lambda _:Unit. r.b:=!(r.x)}
% as BackupInstrCounter;
backupInstrCounterClass =
  (fn(r : 'BackupInstrCounterRep') ->
    fn(self : (unit -> 'BackupInstrCounter')) ->
      fn('_' : unit) ->
        (let(super) = resetInstrCounterClass $ r $ self $ unit in
        {[get = super # get,
          set = super # set,
          inc = super # inc,
          accesses = super # accesses,
          reset = (fn('_' : unit) -> r # x := '!'(r # b)),
          backup = (fn('_' : unit) -> r # b := '!'(r # x))
        ]} as 'BackupInstrCounter')),

% newBackupInstrCounter =
% lambda _:Unit.
% let r = {x=ref 1, a=ref 0, b=ref 0} in
% fix (backupInstrCounterClass r) unit;
newBackupInstrCounter =
  (fn('_' : unit) ->
    (let(r) = {[x = ref(succ(0)), a = ref(0), b = ref(0)]} in
    fix(backupInstrCounterClass $ r) $ unit)),

% ic = newBackupInstrCounter unit;
ic = newBackupInstrCounter $ unit,
(fn('_' : unit) -> ic # get $ unit) $ (ic # inc $ unit),
(fn('_' : unit) -> ic # get $ unit) $ (ic # backup $ unit),
(fn('_' : unit) -> ic # get $ unit) $ (ic # inc $ unit),
(fn('_' : unit) -> ic # get $ unit) $ (ic # reset $ unit),
ic # accesses $ unit
]).

/* James Reily's alternative: */
:- run([
% Counter = {get:Unit->Nat, inc:Unit->Unit};
type('Counter') = {[get : (unit -> nat), inc : (unit -> unit)]},
% inc3 = lambda c:Counter. (c.inc unit; c.inc unit; c.inc unit);
inc3 = (fn(c : 'Counter') -> (fn('_' : unit) -> (fn('_' : unit) -> c # inc $ unit) $ (c # inc $ unit)) $ (c # inc $ unit)),

% SetCounter = {get:Unit->Nat, set:Nat->Unit, inc:Unit->Unit};
type('SetCounter') = {[get : (unit -> nat), set : (nat -> unit), inc : (unit -> unit)]},
% InstrCounter = {get:Unit->Nat, set:Nat->Unit, inc:Unit->Unit, accesses:Unit->Nat};
type('InstrCounter') = {[get : (unit -> nat), set : (nat -> unit), inc : (unit -> unit), accesses : (unit -> nat)]},
% CounterRep = {x: Ref Nat};
type('CounterRep') = {[x : ref(nat)]},
% InstrCounterRep = {x: Ref Nat, a: Ref Nat};
type('InstrCounterRep') = {[x : ref(nat), a : ref(nat)]},
% dummySetCounter =
% {get = lambda _:Unit. 0,
% set = lambda i:Nat.  unit,
% inc = lambda _:Unit. unit}
% as SetCounter;
dummySetCounter = {[
  get = (fn('_' : unit) -> 0),
  set = (fn(i : nat) -> unit),
  inc = (fn('_' : unit) -> unit)]}
  as 'SetCounter',
% dummyInstrCounter =
% {get = lambda _:Unit. 0,
% set = lambda i:Nat.  unit,
% inc = lambda _:Unit. unit,
% accesses = lambda _:Unit. 0}
% as InstrCounter;
dummyInstrCounter = {[
  get = (fn('_' : unit) -> 0),
  set = (fn(i : nat) -> unit),
  inc = (fn('_' : unit) -> unit),
  accesses = (fn('_' : unit) -> 0)]}
  as 'InstrCounter',

% setCounterClass =
% lambda r:CounterRep.
% lambda self: Source SetCounter.
% {get = lambda _:Unit. !(r.x),
% set = lambda i:Nat. r.x:=i,
% inc = lambda _:Unit. (!self).set (succ ((!self).get unit))}
% as SetCounter;
setCounterClass =
  (fn(r : 'CounterRep') ->
    fn(self : source('SetCounter')) ->
      {[get = (fn('_' : unit) -> '!'(r # x)),
        set = (fn(i : nat) -> r # x := i),
        inc = (fn('_' : unit) -> '!'(self) # set $ succ('!'(self) # get $ unit))
      ]} as 'SetCounter'),

% newSetCounter =
% lambda _:Unit. let r = {x=ref 1} in
% let cAux = ref dummySetCounter in
% (cAux :=
% (setCounterClass r cAux);
% !cAux);
newSetCounter =
  (fn('_' : unit) ->
    (let(r) = {[x = ref(succ(0))]} in let(cAux) = ref(dummySetCounter) in
    (fn('_' : unit) -> '!'(cAux)) $ (cAux := setCounterClass $ r $ cAux))),

% instrCounterClass =
% lambda r:InstrCounterRep.
% lambda self: Source InstrCounter.       /* NOT Ref */
% let super = setCounterClass r self in
% {get = super.get,
% set = lambda i:Nat. (r.a:=succ(!(r.a)); super.set i),
% inc = super.inc,
% accesses = lambda _:Unit. !(r.a)}
% as InstrCounter;
instrCounterClass =
  (fn(r : 'InstrCounterRep') ->
    fn(self : source('InstrCounter')) ->
      (let(super) = setCounterClass $ r $ self in
      {[get = super # get,
        set = (fn(i : nat) -> (fn('_' : unit) -> super # set $ i) $ (r # a := succ('!'(r # a)))),
        inc = super # inc,
        accesses = (fn('_' : unit) -> '!'(r # a))
      ]} as 'InstrCounter')),

% newInstrCounter =
% lambda _:Unit. let r = {x=ref 1, a=ref 0} in
% let cAux = ref dummyInstrCounter in
% (cAux :=
% (instrCounterClass r cAux);
% !cAux);
newInstrCounter =
  (fn('_' : unit) ->
    (let(r) = {[x = ref(succ(0)), a = ref(0)]} in
    let(cAux) = ref(dummyInstrCounter) in
    (fn('_' : unit) -> '!'(cAux)) $ (cAux := instrCounterClass $ r $ cAux))),

% c = newInstrCounter unit;
c = newInstrCounter $ unit,
(fn('_' : unit) -> c # get $ unit) $ (inc3 $ c),
(fn('_' : unit) -> c # get $ unit) $ (c # set $ succ(succ(succ(succ(succ(0)))))),
c # accesses $ unit
]).

% try error with true;
:- run([try(error, true)]).
% try if true then error else true with false;
:- run([try(if(true, error, true), false)]).

:- halt.

まとめ

f<: は System F に部分型付けを加えた(有界量化を含む)型システムです。

Hermaphroditus From Wikipedia, the free encyclopedia

In Greek mythology, Hermaphroditus or Hermaphroditos (/hərˌmæfrəˈdaɪtəs/ (About this soundlisten); Ancient Greek: Ἑρμαφρόδιτος) was the son of Aphrodite and Hermes. According to Ovid, he was born a remarkably handsome boy with whom the naiad Salmacis fell in love and prayed to be united forever. A god, in answer to her prayer, merged their two forms into one and transformed them into an androgynous form.[1] His name is compounded of his parents' names, Hermes and Aphrodite.[2] He was one of the Erotes.

Because Hermaphroditus was a son of Hermes, and consequently a great-grandson of Atlas, sometimes he is called Atlantiades (Greek: Ατλαντιάδης).[3] Hermaphroditus' father, Hermes, was also called Atlantiades because his mother, Maia was the daughter of Atlas.

Hermaphroditus' name is the basis for the word hermaphrodite.

メリクリウスってメリークリスマスっぽいひびきがあるなｗ