From 5a17d2858e51a7c99cd60dbed5b6318922005ae2 Mon Sep 17 00:00:00 2001
From: Xie Yuheng <xyheme@gmail.com>
Date: Wed, 22 May 2024 21:08:11 +0800
Subject: [PATCH] up

---
 TODO.md                                       |  3 ++
 ...ending-function-of-subtype-to-supertype.md | 44 ++++++++++++++++---
 2 files changed, 41 insertions(+), 6 deletions(-)

diff --git a/TODO.md b/TODO.md
index e7e1ab6..c7f8806 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,5 +1,8 @@
 # system-a
 
+[system-a] `flatten`
+[system-a] test `extend1` by `flatten`
+
 # the-book
 
 Interlude V: Extensio Magnifico!
diff --git a/docs/diary/2024-05-22-extending-function-of-subtype-to-supertype.md b/docs/diary/2024-05-22-extending-function-of-subtype-to-supertype.md
index e271f1a..7b370d3 100644
--- a/docs/diary/2024-05-22-extending-function-of-subtype-to-supertype.md
+++ b/docs/diary/2024-05-22-extending-function-of-subtype-to-supertype.md
@@ -91,13 +91,13 @@ function extend1(
   implicit outputRank: Nat,
   x: Tensor(inputRank)
 ) => Tensor(outputRank) {
-  return function extendedFn(implicit inputRank, implicit outputRank, x) {
+  function extendedFn(implicit inputRank, implicit outputRank, x) {
     if (inputRank === baseRank) {
-      return fn(x)
+      fn(x)
     }
 
     let Tensor::Array(xs) = x
-    return arrayMap(xs, extendedFn)
+    arrayMap(xs, extendedFn)
   }
 }
 ```
@@ -127,13 +127,45 @@ function extend1(
   fn: (Tensor) -> Tensor,
   baseRank: Nat
 ): (Tensor) -> Tensor {
-  return function extendedFn(x) {
+  function extendedFn(x) {
     if (natEqual(rank(x), baseRank)) {
-      return fn(x)
+      fn(x)
     }
 
     let Tensor::Array(xs) = x
-    return arrayMap(xs, extendedFn)
+    arrayMap(xs, extendedFn)
+  }
+}
+```
+
+也许 Tensor 应该直接被定义为一个函数：
+
+```cicada
+function Tensor(n: Nat): Type {
+  match (n) {
+    case Nat::Zero => Scalar
+    case Nat::Add1(prev) => Array(Tensor(prev))
+  }
+}
+
+check 1: Tensor(0)
+check [1, 2, 3]: Tensor(1)
+```
+
+好像还是不行，并且没法用 implicit 了。
+
+```cicada
+function extend1(
+  baseRank: Nat
+  resultRank: Nat
+  fn: (Tensor(baseRank)) -> Tensor(resultRank),
+): (Tensor) -> Tensor {
+  function extendedFn(x) {
+    if (natEqual(rank(x), baseRank)) {
+      fn(x)
+    }
+
+    TODO
   }
 }
 ```