A Program

# A Program
これはプログラミング言語開発のための備忘録であって、ずっと**工事中**。

### 追伸
「[狂信者のたわごと](https://qiita.com/kyoshinsya/items/e5e45c7d39ffa55f27a2)」を参照のこと。この最後のところはTypeのPolarityのことを言っていました。Positive Type, Negative Typeという二つの言い方があって、前者はその構成(construction rule)によって、後者は除去(elimination rule)によって定まっているという話。
【参考文献】
- [Polarity in Type Theory](https://ncatlab.org/nlab/show/polarity+in+type+theory)

### 主旨
　長年の未踏の夢であり、ずっと開発が断念し続けているプログラミング言語の名前は「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におけるラムダ式の構文について正確な記述を行おう。ラムダ式は次の二つの特徴からなる除去子である。
1) ラムダ式の返り値には、引数の型`T`に対する自明な型の除去子に現れる式の記述が書ける。
```
\t : T -> {
    // ここにはTT@trivial(T)に記述できる全ての記述が入る
}
```
2) ラムダ式の除去子が使われるときは、必ず引数が自明な型の構成子によって包まれた形で処理される。
```
(\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);
}
```

###### 教訓
計算は
```:not a program
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つに大別される。

1) **位置引数**：関数呼び出しするときに位置によってどの引数へ値を受け渡すかを決定する。
2) **名前付き引数**：関数宣言に記述された仮引数を指定することでどの実引数に値を受け渡すか決定する。

位置引数はとても古典的な引数の受け渡し型である。関数名の後にその引数を順番に記述することで、その順序を以てしてどの値がどの引数に対応するかを明示する。
```c:c
int add(int a, int b) {
	return a + b;
}

int main()
{
	int result;
	result = add(5, 3);
}
```
名前付き引数は位置引数に比べると**工事中**
```python:python
def add(a, b):
    return a + b

result = add(a=5, b=3)
```
　一方で位置引数しか持ち合せないような言語においても、名前と値を対応させるような何らかのデータ構造、例えばC言語のstructureやjavascriptのobject、を使えば、関数の内外で引数を名前として指し示しながら授受することができる。工事中
```javascript:javascript
function add(options) {
    return options.a + options.b;
}

result = add({ a: 5, b: 3 });
```
　単純化されたいくつかのプログラミングにおいては、位置引数と名前付き引数が共に合一する。ラムダ計算がその好例で、ラムダ抽象はちょうど1つの引数だけを持ってそれを名前に束縛し、関数適用はまさしく一つの引数の適用を主旨としている。
　**工事中**
```verilog:verilog
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においては全く同じことをモジュールの引数への代入によって表せる。
```verilog:verilog
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) **構造体的アプローチ**：関数は必ず1つの構造体のみを引数に取らなければならない(制約である)。構造体はデータ構造として関数それとは分離される。
2) **関数引数的アプローチ**：構造体は必ずそれが適応される関数と共にしか現れず、関数によって型の中に内包される。一方で、構造体はデータそれ単体で存在しえない(制約である)。

 我々が取るのは他でもなく関数引数的アプローチである。このアプローチをとることで、最終的にオブジェクト指向を内包することに繋がる。すなわち、関数引数的アプローチをとることで、想定された処理を伴わない代入の羅列が登場することが無いようになるのである。
###### 教訓
　我々はもはや構造体を、それを処理する実態から切り離さない。すなわち、構造体を関数引数の座から引き下ろさない。次の構文は我々のプログラムには採用しない文法である。
```:not a program
person := { name : String; age := 20; };
```
**工事中：要するに関数引数的アプローチこそが代数的データ構造そのものなわけ。だって、`zero(), succ(Nat) : Nat`という代数的データ構造(積・和型のデータ構造)があったとして、これ明らかにElimination Ruleで消すとき「無引数の関数」と「1引数Natのみを取る関数」を取るわけではないですか。言いたいことはつまりですね、関数というものを徹底的に言語から除去したいということなんですよ。その代わりに、代数的データ構造の除去則においてのみ、言語構造に関数を登場させたいわけ。(言い換えると、いわゆるアルゴリズム=関数をformationするには必ず型を通して行いたいわけです)そうするとですね、つまり代数的データ構造の除去則にしか関数=「アルゴリズム」が出てこないことになるので、自ずからオブジェクト指向的に、データと処理が分離不能な関係になる、と見込んでいるわけです。**


# 何も決まっていないこと
相互再帰Even, Oddとかをどうするのか。
Nat型のサブタイプとして記述するのか、なんなのか。
依存型ァァアアア！！！お前マジで当初の解決策通りの方策がとれねえじゃねえか！！！

# 実装を参考にすべきプログラミング言語
- Lean4
思うんだけど、Higher Inductive Typeを導入してホモトピー型理論を導入するってことはだよ、基本的にはシステムに内在した強力な定理証明を持つプログラミング言語を開発することに他ならなくて、その定理証明には「型理論は先行計算」のパラダイムに即したコンパイラ最適化が走るという、それが僕の現在の理解だよ。