メルクリウス (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
プログラムの全体を見る
:- 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
プログラムの全体を見る
:- 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
プログラムの全体を見る
:- 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.
メリクリウスってメリークリスマスっぽいひびきがあるなｗ