From 127e160394a8ed59091cdd303c647d993214143a Mon Sep 17 00:00:00 2001
From: Xie Yuheng <xyheme@gmail.com>
Date: Fri, 17 Nov 2023 17:25:46 +0800
Subject: [PATCH] 2023-11-17-type-system.md

---
 TODO.md                              |  4 ++--
 docs/diary/2023-11-17-type-system.md | 28 ++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 docs/diary/2023-11-17-type-system.md

diff --git a/TODO.md b/TODO.md
index bc6d3d8..c1f4554 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,6 @@
-DefineType & TypeDefinition
+DefineDatatype & DatatypeDefinition
 
-- `type <name>` -- to define trivial type for now
+- `datatype <name>` -- to define trivial type for now
 - pass parser `tests/`
 
 # net
diff --git a/docs/diary/2023-11-17-type-system.md b/docs/diary/2023-11-17-type-system.md
new file mode 100644
index 0000000..32e1178
--- /dev/null
+++ b/docs/diary/2023-11-17-type-system.md
@@ -0,0 +1,28 @@
+---
+title: Type system
+author: Xie Yuheng
+date: 2023-11-17
+---
+
+We want algebraic datatype,
+but we also want the data to be easily usable in JavaScript.
+
+We can use named record data:
+
+```petri-net
+datatype Exp {
+  Var { name: String }
+  Fn { name: String, body: Exp }
+  Ap { target: Exp, arg: Exp }
+}
+```
+
+Corresponding to the following TypeScript types:
+
+```typescript
+type Exp = Var | Fn | Ap
+
+type Var = { "@type": "Exp", "@kind": "Var", name: String }
+type Fn = { "@type": "Exp", "@kind": "Fn", name: String, body: Exp }
+type Ap = { "@type": "Exp", "@kind": "Ap", target: Exp, arg: Exp }
+```