From ad163b4cddd7b94db04ce0780b2ec5ae59b76820 Mon Sep 17 00:00:00 2001
From: Xie Yuheng <xyheme@gmail.com>
Date: Fri, 28 Jul 2023 18:28:24 +0800
Subject: [PATCH] [note] Dependent Types

---
 TODO.md                                       | 45 +++++--------------
 docs/notes/dependent-types.md                 | 13 ++++++
 .../design-of-new-syntax.md                   |  0
 3 files changed, 25 insertions(+), 33 deletions(-)
 create mode 100644 docs/notes/dependent-types.md
 rename docs/{articles => notes}/design-of-new-syntax.md (100%)

diff --git a/TODO.md b/TODO.md
index 251fc7a4..4cd5dda0 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,5 +1,3 @@
-`Type` should be type instead of class
-
 [maybe] quit using `def/` and `defs/`
 
 - but maybe to use `def/` is to have one namespace -- which is better
@@ -24,10 +22,16 @@ quit using `Action`
 
 use new syntex
 
-use named port
+`Node` with optionally named port
+
+- `NetRenderer` show free port names
 
 `NetRenderer` -- format to simple text representation of graph
 
+- learn from knuth's c code
+
+change the `render` command to simple `run` command
+
 # the paper
 
 phase space and monoid -- understand the model theory of linear logic
@@ -40,8 +44,6 @@ understand proof-nets for all connectives
 - "The linear abstract machine", Lafont, 1990.
 - "From proof-nets", Lafont, 1995
 
-command change render command to simple run command
-
 # simple types
 
 > linear logic as type system of inet
@@ -53,44 +55,21 @@ i.e. without dependent type -- not as a foundation of mathematics
 
 # linear prolog
 
-From the example of `diff-list`,
-we know that inet is like linear logic programming.
-
-# later
-
-`Node` with optionally named port
-
-- `NetRenderer` show free port names
-
-stmt.format
-
-`NetRenderer` control order
-
-- need to use builder pattern, just like building SQL query
+From the example of `diff-list`, we know that
+inet is like linear logic programming.
 
 # experiments
 
 use inet to encode lambda calculus
-use inet to encode class, object and message sending
-
-# dependent types
-
-Two levels of computations, execute and cut.
 
-`Word.cut` & `Word.execute`
-
-equality between `Net`
-use `Net` as type
+use inet to encode class, object and message sending
 
 # type check
 
-`type-def.ts` -- `apply`
-
-`deftype` -- `TermType`
-
-`forall` for generic type variables
+`deftype` -- `TermType` -- use `'a` for name of pattern like in haskell
 
 `defnode` -- type check
+
 `defnet` -- type check words composition
 
 `Edge` -- type check the two ports
diff --git a/docs/notes/dependent-types.md b/docs/notes/dependent-types.md
new file mode 100644
index 00000000..faee544d
--- /dev/null
+++ b/docs/notes/dependent-types.md
@@ -0,0 +1,13 @@
+---
+title: Dependent Types
+---
+
+Simple type system is easy to implement,
+how about dependent type system?
+
+If we can implement equality between `Net`s,
+we can use `Net` as value,
+and use "two levels of composition" -- execute and cut,
+to view type declaration in a node
+the same as rule declaration
+and thus implement dependent types.
diff --git a/docs/articles/design-of-new-syntax.md b/docs/notes/design-of-new-syntax.md
similarity index 100%
rename from docs/articles/design-of-new-syntax.md
rename to docs/notes/design-of-new-syntax.md