A Program
これはプログラミング言語開発のための備忘録であって、ずっと工事中。
追伸
「狂信者のたわごと」を参照のこと。この最後のところはTypeのPolarityのことを言っていました。Positive Type, Negative Typeという二つの言い方があって、前者はその構成(construction rule)によって、後者は除去(elimination rule)によって定まっているという話。
【参考文献】
主旨
長年の未踏の夢であり、ずっと開発が断念し続けているプログラミング言語の名前は「A Program」であり、この言語はもとよりC言語、OpenCL(現在はCudaなどを標的に)、Verilog HDLそれぞれにトランスパイルできることが最低要件として開発が始まった。ここにSmalltalk, LISPのエッセンスを加え、強力な「先行計算」である型理論(すなわち定理証明)が入ることが「A Program」の目指すところである。
この文章はA Programのドキュメントとして作り始めた文法設計の「悩み集」をあけっぴろげに公開しているものです。コメントをいただけた場合は真摯に検討します。
A Programの文法
計算の規則(Computation Rule)
代入文は次の形をした文である。
identifier := expression;
代入文は専ら計算グラフを構成するために用いられる。
f : Float
c : Float
x := f - 32;
y := 5;
z := 9;
c := (f - x) * y / z;
あるいは中括弧を用いた記法によってスコープを分けても良い。
f : Float
c : Float
c := {
x := f - 32;
y := 5;
z := 9;
^(f - x) * y / z;
};
lower := 0;
upper := 300;
step := 20;
{
fahrenheit := lower;
} @ {
celcius := (fahrenheit - 32) * 5 / 9;
fahrenheit := fahrenheit + step;
};
自然数の定義の仕方(A way to define a natural number)
工事中：気づいたこととして、代数的データ構造は和&積構造となっているため、各構成子(constructor)に対する除去子(eliminator)を個別に代入しに行くことができる、ということが文法的に判明した。
Nat := @{
zero() : *;
succ(*) : *;
};
恒等関数の書き方をここで習得しておこう。
identity_of_nat := Nat@zero() Nat.zero();
identity_of_nat := Nat@succ(m : *) Nat.succ(m);
工事中
除去子を作る過程は、基本的にデータの構成子それぞれに対して場合分けして結果の値を構築する手順を踏む。この場合分けをそれぞれ異なる代入文で行うことはしばしば冗長になるため、「型」の後に@演算子を数珠繋ぎにして場合分けを記述することができる。
identity_of_nat := Nat
@zero() Nat.zero()
@succ(m : *) Nat.succ(m);
同じ恒等関数は次のラムダ式を使っても書くことができる。
identity_of_nat := \x : Nat -> x;
処理系はこのようなラムダ式を見ると、その引数の型に従って除去子を自動で組み立てる。この場合では\x : Nat(引数xの型はNatである)から、自ずからNatに関する除去子を構築するべきことが分かる。そして、Natに関する除去子はNat@zero()とNat@succ(m : *)に場合分けして処理を組み立てればいいのだから、それに従って恒等関数identity_of_natが作り上げられる。この意味で、ラムダ式はA Programにおける第一級の文法的存在ではなく、あくまで除去子を構築するための糖衣構文であることが分かる。
このようにして定義した関数identity_of_natには関数型が付与される。
identity_of_nat : Nat -> Nat;
これらの恒等関数の記法はA Programにおけるすべての関数定義の基本となるものであるから、いつでもプログラミングに迷ったときにはここに立ち戻ってくるのが良い。
#tradition identity
//add := Nat@zero() Nat.identity;
add := Nat@zero()
{
//adder := \x : Nat -> x;
adder := Nat@zero() Nat.zero();
adder := Nat@succ(m : *) Nat.succ(m);
^adder;
}
add := Nat@succ(n : *)
{
//adder := \x : Nat -> Nat.succ(*n x);
adder := Nat@zero() Nat.succ(*n Nat.zero());
adder := Nat@succ(m : *) Nat.succ(*n succ(m));
^adder;
};
zero := Nat.zero();
one := Nat.succ(zero);
two := Nat.succ(one);
three := Nat.succ(two);
sum := add two three;
ここでaddの型は次のように決定される。
add : Nat
@zero() -> Nat
@succ(*) ->
代数的データ型(Algebraic data type)
工事中：これは実質的にはinductive typeそのものであろう
Even, Odd {
zero : *Even;
succ(*Odd) : *Even;
succ(*Even) : *Odd;
};
ある型に対する自明な型(Trivial Type for a Given Type)
ある型Tが与えられた時、次の形をした型TTを「型Tに対する自明な型」という。
TT {
trivial(T) : *;
};
このような自明な型はありとあらゆる型を想起したときに、そのどれに対しても直ちに思いつくことができる。しかしながら、このような自明な型は、プログラムの構文としては本質的な意味を持たないような型の定義をしている。
これまで我々が使ってきたラムダ式は、実はこの自明な型TTに対する除去子を構成する構文である。実際に、恒等関数を任意の型Tに定義しようとするとき、我々はこの自明な型TTの除去子を使うことで次のようにその定義を記述できる。
identity := TT@trivial(t : T) t;
あるいは全く同様に
identity := TT@trivial(t : T) {
^t;
}
他でもないことではあるが、これらで定義した恒等関数を適用するためには要素t : Tに対して次のように適用する必要がある。
identity TT.trivial(t) // yields t
A Programでは、関数を定義するためには必ず型の除去子を通してでなければならない。したがって、ある型Tの恒等関数を型Tの除去子を用いて定義するには、必ず型Tの構成子の全てのパターンについて、引数となった値を再構築するような記述を行う必要がある。
一方で、型Tに対する自明な型TTは、明らかに型Tの要素の情報を全て持っている。それでいて、型TTの除去子を定義するのには、型Tの構成子に関するパターン類別を必要としない。この除去子において引数は計算によって本質的に小さな構成要素に分解されず、むしろ同等であるか、それより大きな構成単位からなる返り値を組み立てるために使われる。この意味で、自明な型TTの除去子は型Tの要素に対する構成的な除去子である。
元々の型Tと、その型に対する自明な型TTとの違いは除去子の特性の観点で次のようにいうこともできる。すなわち、元の型Tの除去子では、構成子をその構成要素に分解して処理を行う。この過程で構成子がより小さい単位に分解されるため、除去子を評価することで文字通り元の型Tの要素を消化して、更に小さい単位の計算へと還元されていく。一方で、その自明な型TTの除去子は構成単位を分解せずに処理を行うため、型Tの意味での計算を意味していない。工事中
自明な型について分かったところでA Programにおけるラムダ式の構文について正確な記述を行おう。ラムダ式は次の二つの特徴からなる除去子である。
- ラムダ式の返り値には、引数の型
Tに対する自明な型の除去子に現れる式の記述が書ける。
\t : T -> {
// ここにはTT@trivial(T)に記述できる全ての記述が入る
}
- ラムダ式の除去子が使われるときは、必ず引数が自明な型の構成子によって包まれた形で処理される。
(\t : T -> something) t
// (TT@trivial(t : T) something) TT.trivial(t)に同じ
ラムダ式は引数の型に対する自明な型の除去子の位置にくる全ての式表現を受け入れる。構成的な除去子を
これらのことから、ラムダ式はある型に対する構成的な除去子を作るとき、そのときにだけ専ら用いられるべき除去子である。
工事中そのため、恒等関数はラムダ式を用いて次のようにかけることになるのである。
identity := \t : T -> t;
高階代数的データ型(Higher algebraic data type)
工事中：Higher inductive typeの除去則をどうやって言語内に入れるかということ。
計算の規則(Computation Rule)
代入文は次の形をした文である。
identifier := expression;
代入文は専ら計算グラフを構成するために用いられる。
f : Float
c : Float
x := f - 32;
y := 5;
z := 9;
c := (f - x) * y / z;
あるいは中括弧を用いた記法によってスコープを分けても良い。
f : Float
c : Float
c := {
x := f - 32;
y := 5;
z := 9;
^(f - x) * y / z;
};
工事中：次のは採用しない文法だが、近しいものは使う
\convert(f : Float) {
c : Float;
c := (f - 32) * 5 / 9;
^c;
}
main := {
f, c : Float;
f := scan;
c := \convert(f);
^print(c);
}
教訓
計算は
a := b
b := a
式の問題(Expression problem)
工事中：あとでアルゴリズム+データ構造という章に分割して、そこで述べたい。なぜなら明らかにプログラム=アルゴリズム+データ構造と分解したときにおこる言語の記述性に関する問題であるから。
Whether a language can solve the Expression Problem is a salient indicator of its capacity for expression. One can think of cases as rows and functions as columns in a table. In a functional language, the rows are fixed (cases in a datatype declaration) but it is easy to add new columns (functions). In an object-oriented language, the columns are fixed (methods in a class declaration) but it is easy to add new rows (subclasses). We want to make it easy to add either rows or columns.
Philip Wadler, 1998
定数と定数関数(Constants and Constant functions)
「定数」と「定数関数」とに文法的な差異はどこにあるのだろうか。
ひとまず定数aの表現として
a
を採用しよう。その上で次の三つの定数、関数、定数関数の定義を見比べてみてほしい。
x := a
f() := a
f(x) := a
これらの定義において、一つ目の表現
x := a
は定数の定義である。ここで定義された名前xは定数であるから、引数を取らない。
二つ目の表現
f() := a
は関数の定義である。ここで定義された名前fは関数であるから*「引数を取ることが想定される」*が、その引数は0型である。すなわち、想定された引数は何もなく、引数を取らない関数である。
三つ目の表現は再び関数の定義である。
f(x) := a
この関数fは仮引数xを取るが、なんとその仮引数xは関数fの定義部には一度も現れることがない。この関数fは定数aを返すことになるのだからまぎれもなく定数関数である。
このようにして定義した三つの表現はいずれも計算結果として「定数aの示すところの値」を返すことが期待される。……だから、このようにして得た新しい表現を使うことで、明らかに我々は初めの定数aの表現として
a
a()
a(x)
が受け入れられることになる。これは本当だろうか？
工事中
教訓
プリミティブなデータがなく、あまねく全てが識別子で棲み分けられる我々のプログラムにおいては定数や定数関数もその裁きを受けねばならない。工事中
a(a(a))()
スコープと名前空間
名前は有限の資源である。ある文脈上で名前は二度と同じものを利用できないというのが通説である。例えば、「りんご」が同時に赤くて甘い果物を指し示すとしよう。それと同時にRonald Wayne、Stephen Wozniak、Steve Jobsの「Apple(りんご)社」を指し示すとしよう。我々はプログラミング言語という観点から、名前についてこの曖昧な指示用法を認めない。
通例で列挙を行う場合1)最初の項目、2)第二の項目、3)第三の項目と我々は必ず書くが、ここでは人名であり、Appleを創業した彼らに列挙に伴う伝統的な優先順位が入らないようにした。この目的で、名前はアルファベット順で示している。
型理論という先行計算
工事中：命題=型というドグマを受け入れると、基本的に型理論に現れる型「Nat」、「$x = y$(等式型)」、「$(A, B)$(和型)」、「$\Sigma_{a : A} B(a)$」などは全て論理式と見なせるわけで、それに対して一般にwitness : propという形の式は、定理の証明と見なすことができます。じゃあ例えば等式型$x = y$をコンパイル段階で証明してしまったとしたしたら、それはプログラミング言語処理系として何を意味しているのか？という話になるわけなのですが、明らかに定数最適化を行ったことに相当するわけで「先行計算」なわけです。また、プログラム全体の集合を楕円で図示したとして、その中でループが必ず停止する部分集合を少し小さい楕円で図示したとしましょう。すると、この大きな楕円から小さな楕円にプログラムを縮約しているという観点から言えば、型チェックというのはプログラムという数学的オブジェクトを計算して縮約していることに大まかに対応しています。計算とは縮約とか、あるいは項書き換えのことを言うわけですが、「停止するする計算」とか、「正規形(normal form)」というのはそういう大きな楕円の小さな部分にものを縮めていく計算の過程なわけで、型理論は大まかに言えば先行計算の枠組みの一部であると見ることができるというのが大まかな主張。
次のような数式の計算を考えてみよう。ここでNatは自然数の型である。
a : Nat
b : Nat
c := a + b
この記述はaの型がNat型であり、bの型が同様にNat型であるときに、それらの和であるところのa + bがcであると言っている。このときにcの型は何であろうか？
この問いに答えるため、より直観に訴える初等的な算術を行うことを考えてみよう。ここでは単純な3 + 4 = 7をこの表現の枠組みで記述してみたい。
a := 3
b := 4
c := a + b
この記述はaが数3であり、bが数4であるときに、それらの和であるところの3 + 4がcであると言っている。このときにcの値は何であろうか？もちろん、c := 7である。
では最初の問題に戻ってみよう。我々はa : Natであり、b : Natであるとき、c : ?を解いているのであった。ちょうど、a := 3であり、b := 4であるとき、c := ?を解いたように。
初等的な算術では直ちに答えがc = 7であると導けた理由は我々が加算に慣れ親しんでいて、1) 1つ目のオペランド(a)が数3であって、2) 2つ目のオペランド(b)が数4であるようなときの和が7であるという算術表を受け入れているからだ。型についても同じ算術表があればc : ?という型を推論する問題に答えることができる。すなわち、1) 1つ目のオペランドがNat型であって、2) 2つ目のオペランドがNat型であるようなときの和の型はNatであることを受け入れよう。つまり、型レベルの加算の算術表を受け入れるのである。
型システム
型とはA Programの処理系においてコンパイル時に精査されるプログラム中の項の値である。一般に、ある項aが型Aであることを次のように表す。
a : A;
これを項aは型Aであるとか、項aは型Aを持つと読む。あるいは項aが型Aであることを強いるという意味合いで、項aに型Aを与えるとも読む。このような文a : Aを型宣言の文という。
ある型Aと型Bがあるとき、それらを->演算子で繋げたもの(A - > B)も型である。したがって、このような型A -> Bを型宣言に用いることもできて、
f : A -> B;
は正しい文である。この場合、一般の型付けと同様に項fは型A -> Bを持つ。このような型A -> Bを関数型と呼ぶ。関数型において演算子->の左にある型(A)を引数型、演算子->の右にある型(B)を返値型と呼ぶ。
ある関数型A -> Bに対して、1) その関数型の要素f : A -> B(関数)と2) その関数型の引数型を持つ項a : A(引数)を考えよう。関数型A -> Bの項fは、項aがその引数型Aであるとき、f aという式を構成しうる。このような式を関数適用と呼ぶ。式f aは関数fを引数aに適用する、あるいは引数aは関数fに適用されると読む。
関数適用の式(f a)の型は、適用された関数(f)の返値型で推論される。
f a :: B;
これを型の推論といい、式f aは型Bであるとか、式f aは型Bを持つと読む。ここで型推論の読み方を型宣言の読み方と見比べてみてほしい。それらがそっくりであることに気づくだろう。実際にa : Aを「項aは型Aである」と読み、f a : Bを「式f aは型Bである」と読むのであるから、これらの違いは読むべき対象が項であるか式であるかの違いである。この違いを強調する目的で、型の推論f a :: Bは式f aは型Bと推論するとも読み、この読み方によって型の付与とは区別する。工事中：そして、型宣言が文であることとは異なり、型推論は判断である。
x :: \T1. {x :: T1} T1;
\x -> x :: \T1. T1 -> T1;
\x. {
x : A;
^x
} :: {} A -> A;
\x : A. x == \x. { x : A; ^x }
a :: <T1> {a :: T1} T1;
a : A;
a is an identifier
------------------
a :: <A> {a : A} A
b :: <A, B> {a : A} B
-------------------------
\a. b :: <A, B> {} A -> B
{} :: <> {}
---------------------
{a : A} :: <> {a : A}
{a : A} :: <> {a : A}
---------------------------
{a : A; ^a} :: <> {a : A} A
{} :: <> {}
---------------
{^@} :: <> {} @
{A : @; B : @; ^@} :: <> {A : @; B : @} @
-----------------------------------------
\A. \B. {A : @; B : @; ^@} :: <> {A : @; B : @} @ -> @ -> @
{A : @; ^@} :: <> {A : @} @
---------------------------
\A. {A : @; ^@} :: <> {} @ -> @
(\A. {A : @; ^@}) :: <> {} @ -> @, T :: <> {} @
-----------------------------------------------
(\A. {A : @; ^@}) T :: <T1, T2> {@ -> @ == T1 -> T2, T1 :< @} T2
----------------------------------------------------------------
(\A. {A : @; ^@}) T :: <T1, T2> {@ == T1; @ == T2, T1 :< @} T2
--------------------------------------------------------------
(\A. {A : @; ^@}) T :: <T2> {@ == T2, @ :< @} T2
------------------------------------------------
(\A. {A : @; ^@}) T :: <> {@ :< @} @
------------------------------------
(\A. {A : @; ^@}) T :: <> {} @
X :: <> {} @
-------------
@X :: <> {} X
List := \A. {A : @; ^@}; :: <> {} @ -> @
nil := @List A; :: List A
cons := \a. \lst. {a : A; lst : List A; ^@List A}; :: A -> List A -> List A
f :: <T1> {} T1, a :: <T2> {} T2
-----------------------------------------------------
f a :: <T1, T2, T3, T4> {T1 == T3 -> T4; T2 :< T3} T4
:: <A, B> {x : A; x : B}
---------------------------(&)
:: <A, B> {x : A & B}
:: <A, B> {x : B; A == B} A
---------------------------(==, term)
:: <A> {x : A} A
:: <A, B, C, D> {A -> B == C -> D}
----------------------------------(==, ->)
:: <A> {A == C; B == D}
:: <A, B> {A :< B} A
--------------------(:<)
:: <B> {} B
:: <A, B, X, Y> {X -> Y :< A -> B}
----------------------------------
:: <A, B, X, Y> {A :< X, Y :< B}
:: <A, B, C> {A :< B & C}
-----------------------------
:: <A, B, C> {A :< B; A :< C}
:: <A, B, C> {A :< B; B :< C}
-----------------------------
:: <A, B, C> {A :< C}
:: <A, B> {x : A; x : B} C
--------------------------(W)
:: <A, B> {x : A & B} C
TOP DOWN
x is an identifier
------------------
x :: <A> {x : A} A
----------------------
\x. x :: <A> {} A -> A
x is an identifier x is an identifier
------------------, ------------------
x :: <A> {x : A} A x :: <B> {x : B} B
---------------------------------------------------------
x x :: <A, B, C, D> {x : A; x : B; A == C -> D; B :< C} D
---------------------------------------------------------
x x :: <B, C, D> {x : C -> D; x : B; B :< C} D
----------------------------------------------
x x :: <B, C, D> {x : (C -> D) & B; B :< C} D
-------------------------------------------------
\x. x x :: <B, C, D> {B :< C} ((C -> D) & B) -> D
-------------------------------------------------
\x. x x :: <C, D> {} ((C -> D) & C) -> D
\x. x x :: <C, D> {} ((C -> D) & C) -> D, \x. x :: <A> {} A -> A
----------------------------------------------------------------
(\x. x x) (\x. x) :: <A, C, D, E, F> {
((C -> D) & C) -> D == E -> F;
A -> A :< E
} F
--------------------------------------
(\x. x x) (\x. x) :: <A, C, D, E, F> {
(C -> D) & C == E;
D == F;
A -> A :< E
} F
--------------------------------------
(\x. x x) (\x. x) :: <A, C, D, E> {
(C -> D) & C == E;
A -> A :< E
} D
-----------------------------------
(\x. x x) (\x. x) :: <A, C, D> {
A -> A :< (C -> D) & C
} D
--------------------------------
(\x. x x) (\x. x) :: <A, C, D> {
A -> A :< C -> D;
A -> A :< C
} D
--------------------------------(or 1)
(\x. x x) (\x. x) :: <A, C, D> {
C :< A;
A :< D;
A -> A :< C
} D
--------------------------------
(\x. x x) (\x. x) :: <A, C, D> {
A :< D;
A -> A :< A
} D
--------------------------------(or 2)
(\x. x x) (\x. x) :: <A, C, D> {
A -> A :< C -> D;
A -> A == C
} D
--------------------------------
(\x. x x) (\x. x) :: <A, D> {
A -> A :< (A -> A) -> D
} D
-----------------------------
(\x. x x) (\x. x) :: <A, D> {
A -> A :< A;
A :< D
} D
-----------------------------
(\x. x x) (\x. x) :: <A, D> {
A -> A :< D
} D
-----------------------------
(\x. x x) (\x. x) :: <A> {} A -> A
we calculate
A & B :< T
for most: A :< T or B :< T
A :< B & C
for most: A :< B and A :< C
X :< A -> B
for most: X == A -> B
A -> B :< X
for most: NG
X -> Y :< A -> B
for most: A :< X, Y :< B
a : A, a :: <T> {a : T} T
-------------------------
a :: <> {} A
A is an identifier
------------------
A : @
a is an identifier, A : @
-------------------------
a : A
A : @, B : @
------------
A -> B : @
a : A
------
a :: A
f :: A -> B, a :: A
-------------------(#)
f a :: B
x : A, exp :: A
---------------(#)
x := exp
x := a
------
x == a
a == b, b == c
--------------
a == c
a : A;
f : A -> B;
g : B -> C;
c : C;
c := g (f a);
f : A -> B a : A
-------------, -------
f :: T1 -> T0 a :: T1
g : B -> C f :: T1 -> T0, a :: T1
------------, ----------------------
g :: T0 -> C f a :: T0
g :: T0 -> C, f a :: T0
-----------------------
g (f a) :: C
c : C, g (f a) :: C
-------------------(#)
c := g (f a)
t :: <T> {t :: T}, T
<> {}
f :: T1
<T1> {f :: T1}, f :: T1
<> {}
a :: T2
<T2> {a :: T2}, a :: T2
<T1, T2> {f :: T1, a :: T2}
T1 == T3 -> T4
T2 :< T3
<T2, T3, T4> {f :: T3 -> T4, a :: T2}
T2 :< T3
, f a :: T4
<> {}
x :: T1
<T1> {x :: T1}, x :: T1
<T1> {x :: T1}
\x
<T1> {}
, \x -> x :: T1 -> T1
<> {}
x :: T1
<T1> {x :: T1}, x :: T1
<> {}
x :: T2
<T2> {x :: T2}, x :: T2
<T1, T2> {x :: T1 & T2}
T1 == T3 -> T4
T2 :< T3
<T2, T3, T4> {x :: (T3 -> T4) & T2}
T2 :< T3
, x x :: T4
<T2, T3, T4> {x :: (T3 -> T4) & T2}
T2 :< T3
\x
<T2, T3, T4> {}
T2 :< T3
, \x -> x x :: (T3 -> T4) & T2 -> T4
=>
<T3, T4> {}
, \x -> x x :: (T3 -> T4) & T3 -> T4
<T1> {}
, \x -> x :: T1 -> T1
<T3, T4> {}
, \x -> x x :: (T3 -> T4) & T3 -> T4
<T1, T3, T4, T5, T6> {}
(T3 -> T4) & T3 -> T4 == T5 -> T6
T1 -> T1 :< T5
<T1, T3, T4, T5, T6> {}
(T3 -> T4) & T3 == T5
T4 == T6
T1 -> T1 :< T5
<T1, T3, T4, T5, T6> {}
(T3 -> T4) & T3 == T5
T4 == T6
T1 -> T1 :< T5
Case) T3 -> T4 :< T1 -> T1
for max: T3 == T4
T1 -> T1 :< T3 NOP
Case T3 :< T1 -> T1
for max: T3 == (T1 -> T1)
(T1 -> T1) -> T4 :< (T1 -> T1)
for max: T1 -> T1 == T4
<T1, T5, T6> {}
((T1 -> T1) -> T1 -> T1) & (T1 -> T1) == T5
T1 -> T1 == T6
T1 -> T1 :< T5
, (\x -> x x) (\x -> x) :: T6
<T1> {}
, (\x -> x x) (\x -> x) :: T1 -> T1
<T1> {x :: T1}, x :: T1
<...> {..., x :: T1}, y :: T2
<...> {...}, \x -> y :: T1 -> T2
<...> {...}, f :: T1
<...> {...}, a :: T2
<...> {...},
T1 == T3 -> T4
T2 :< T4
for an existing
something == T
otherthing :< T
we calculate
A & B :< T
for most: A :< T or B :< T
X :< A -> B
for most: X == A -> B
A -> B:< X
for most: NG
X -> Y :< A -> B
for most: X == A, Y == B
<T2, T3, T4> {f :: T3 -> T4, a :: T2}
T2 :< T3
, f a :: T4
<T2, T3, T4> {f :: T3 -> T4, a :: T2}
T2 :< T3
\f
<T2, T3, T4> {a :: T2}
T2 :< T3
, \f -> f a :: (T3 -> T4) -> T4
(\x -> x x) (\x -> x x)
<T1, T2> {}
, \x -> x x :: (T1 -> T2) & T1 -> T2
<T1, T2, T3, T4, T5, T6> {}
(T1 -> T2) & T1 -> T2 == T5 -> T6
(T3 -> T4) & T3 -> T4 :< T5
<T1, T2, T3, T4, T5, T6> {}
(T1 -> T2) & T1 == T5
T2 -> T6
(T3 -> T4) & T3 -> T4 :< T5
一般の条件T1 :< T2に対する処理
<T1, T2> {} x :: T1
T1 :< T2
=>
<T2> {} x :: T2
Sl :< T1, T2 :< S2
------------------------
(T1 -> T2) :< (S1 -> S2)
x :< A, x :< B
--------------
x :
f :: A -> B, a : A
------------------
S & T :< S
S & T :< T
#Arg, #Env + {x : S}, y :: T
-----------------------------
#Arg, #Env, \x -> y :: S -> T
#Arg, #Env, f :: S & T -> U, x :: S, x :: T
-------------------------------------------
#Arg, #Env, f x :: U
#Arg + {T}, #Env, x :: S
-----------------------------
#Arg + {U}, #Env, x :: S[T\U]
{a :: A}, A
a
{x :: T1}, T1
{x :: T2}, T2
<T1, T2> {x :: T1, x :: T2}
T1 = T3 -> T4
T2 <= T3
, T4
<T2, T3, T4> {x :: T3 -> T4, x :: T2}
T2 <= T3
, T4
<T3, T4> {x :: T3 & (T3 -> T4)}, T4
x x
x :: T3 -> T4
x :: T3
<T3, T4> {}, (T3 & (T3 -> T4)) -> T4
\x. x x
<T> {x :: T}, T
x
<T> {}, T -> T
\x. x
<T3, T4> {}, (T3 & (T3 -> T4)) -> T4
and
<T> {}, T -> T
then
(\x. x x) :: <T3, T4> {}, (T3 & (T3 -> T4)) -> T4
T3 == T -> T
T4 == T -> T
-------------------------------------------------
(\x. x x) :: <> {}, ((T -> T) & ((T -> T) -> (T -> T)) - > (T -> T)
and
(\x x) :: <T> {}, T -> T
T == T
------------------------
(\x x) :: <> {}, T -> T
,
(\x x) :: <T> {}, T -> T
T == T -> T
------------------------
(\x x) :: <> {}, (T -> T) -> (T -> T)
then
(\x. x x) (\x x) :: {} (T -> T)
finally, generallize
(\x. x x) (\x x) :: <T> {} (T -> T)
<F> {f :: F}, F
<A> {a :: A}, A
<F, A> {f :: F, a :: A}
F == T0 -> T1
A <= T0
, T1
<A, T0, T1> {f :: T0 -> T1, a :: A}
A <= T0
, T1
<T0, T1> {f :: T0 -> T1, a :: T0}, T1
f a
<T0, T1> {a :: T0}, (T0 -> T1) -> T1
\f. f a
a : A;
f : A -> B;
b : B;
b := f a;
f : A -> B a : A
----------- ------
f :: A -> B, a :: A
-------------------
b : B, f a :: B
----------------------------(#)
b := f a
a : A;
f : A -> A;
a := f a;
f : A -> A a : A
----------- ------
f :: A -> A, a :: A
-------------------
a : A, f a :: A
----------------------------(#)
a := f a
identifier : expression; // 型宣言文
expression :: expression; // 型推論
identifier := expression; // 代入文
expression == expression; // 計算
我々はある要素aに型Aを与えるときに演算子:を使ってa : Aと表記する。一方で、ある式expがある型Eであることを推論するときに演算子::を使ってexp :: Eと表記する。
型の付与a : Aと、型の推論exp :: Eの違いは代入文において明らかになる。次の代入文は型の等しさA == Eが与えられたとき、そのときに限り正しい文である。
a := exp; // a : A, exp :: EかつA == Eのときに限る
このことを踏まえると、関数適用の式f aを識別子bに代入する文b := f aが正しい文であるためには、何を確認する必要があるだろうか？もちろん、1)識別子bに関する型宣言b : Bと2)式f aに対する型推論f a :: Bである。明らかに型推論は済んでいるから、代入文b := f aに先行して型宣言をすれば、代入は正しく行われる。
b : B;
b := f a;
A -> (B -> C)
型には正の型と負の型の二つが存在する。
関数型ではないあらゆる型は、いくつかの値から構築される。
関数呼び出しと引数
関数を呼び出す場合の引数の与え方はプログラミング言語によって異なるが、あまねく言語を見渡してみると2つに大別される。
- 位置引数：関数呼び出しするときに位置によってどの引数へ値を受け渡すかを決定する。
- 名前付き引数：関数宣言に記述された仮引数を指定することでどの実引数に値を受け渡すか決定する。
位置引数はとても古典的な引数の受け渡し型である。関数名の後にその引数を順番に記述することで、その順序を以てしてどの値がどの引数に対応するかを明示する。
int add(int a, int b) {
return a + b;
}
int main()
{
int result;
result = add(5, 3);
}
名前付き引数は位置引数に比べると工事中
def add(a, b):
return a + b
result = add(a=5, b=3)
一方で位置引数しか持ち合せないような言語においても、名前と値を対応させるような何らかのデータ構造、例えばC言語のstructureやjavascriptのobject、を使えば、関数の内外で引数を名前として指し示しながら授受することができる。工事中
function add(options) {
return options.a + options.b;
}
result = add({ a: 5, b: 3 });
単純化されたいくつかのプログラミングにおいては、位置引数と名前付き引数が共に合一する。ラムダ計算がその好例で、ラムダ抽象はちょうど1つの引数だけを持ってそれを名前に束縛し、関数適用はまさしく一つの引数の適用を主旨としている。
工事中
module adder (
input [7:0] a, b,
output [7:0] sum
);
assign sum = a + b;
endmodule
module main;
wire [7:0] result;
adder add (
.a(5),
.b(3),
.sum(result)
);
endmodule
Verilog HDLにおいては全く同じことをモジュールの引数への代入によって表せる。
module adder (
input [7:0] a, b,
output [7:0] sum
);
assign sum = a + b;
endmodule
module main;
wire [7:0] result;
adder add;
add.a(5);
add.b(3);
add.sum(result);
endmodule
初めの気づきとして、位置引数にしても名前付き引数にしても、引数の授受は代入操作にとても似ている。我々は関数を呼び出すとき、その一回一回の関数呼び出しフェーズに対して、固有の代入操作を行っていると見れる。このことは回路合成において関数というよりもモジュールという計算実態への配線操作として引数受け渡しが登場する計算パラダイムを見ることで明らかである。この意味で、代入操作の構文と関数への引数の受け渡しは同じ構文としていい。
更に構造体やオブジェクト、さらには連想配列といったデータ構造を仲介することで、名前付き引数と同じ使用感で位置引数によって引数の名前を指定できることを見た。すなわち、関数の引数リストと構造体といったデータ構造のオブジェクトは等価である。
ラムダ計算においても1つの引数に対して名前を割り当てなければならなかったように、反対に位置引数においても、仮引数に名前を設けないことにはそれを関数の実態で利用して計算実行することはできない。
工事中
これらの考察から我々のプログラムにおいては関数の引数と構造体を全く同じものに扱う必要が出てきた。二つのアプローチが取れる。
- 構造体的アプローチ：関数は必ず1つの構造体のみを引数に取らなければならない(制約である)。構造体はデータ構造として関数それとは分離される。
- 関数引数的アプローチ：構造体は必ずそれが適応される関数と共にしか現れず、関数によって型の中に内包される。一方で、構造体はデータそれ単体で存在しえない(制約である)。
我々が取るのは他でもなく関数引数的アプローチである。このアプローチをとることで、最終的にオブジェクト指向を内包することに繋がる。すなわち、関数引数的アプローチをとることで、想定された処理を伴わない代入の羅列が登場することが無いようになるのである。
教訓
我々はもはや構造体を、それを処理する実態から切り離さない。すなわち、構造体を関数引数の座から引き下ろさない。次の構文は我々のプログラムには採用しない文法である。
person := { name : String; age := 20; };
工事中：要するに関数引数的アプローチこそが代数的データ構造そのものなわけ。だって、zero(), succ(Nat) : Natという代数的データ構造(積・和型のデータ構造)があったとして、これ明らかにElimination Ruleで消すとき「無引数の関数」と「1引数Natのみを取る関数」を取るわけではないですか。言いたいことはつまりですね、関数というものを徹底的に言語から除去したいということなんですよ。その代わりに、代数的データ構造の除去則においてのみ、言語構造に関数を登場させたいわけ。(言い換えると、いわゆるアルゴリズム=関数をformationするには必ず型を通して行いたいわけです)そうするとですね、つまり代数的データ構造の除去則にしか関数=「アルゴリズム」が出てこないことになるので、自ずからオブジェクト指向的に、データと処理が分離不能な関係になる、と見込んでいるわけです。
何も決まっていないこと
相互再帰Even, Oddとかをどうするのか。
Nat型のサブタイプとして記述するのか、なんなのか。
依存型ァァアアア！！！お前マジで当初の解決策通りの方策がとれねえじゃねえか！！！
実装を参考にすべきプログラミング言語
- Lean4
思うんだけど、Higher Inductive Typeを導入してホモトピー型理論を導入するってことはだよ、基本的にはシステムに内在した強力な定理証明を持つプログラミング言語を開発することに他ならなくて、その定理証明には「型理論は先行計算」のパラダイムに即したコンパイラ最適化が走るという、それが僕の現在の理解だよ。