From e47e4bd56f266b6466d46eba4aff07229a9329a2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=E6=9D=BE=E6=B5=A6=20=E7=9F=A5=E4=B9=9F=20Matsuura=20Tomoy?=
 =?UTF-8?q?a?= <me@matsuuratomoya.com>
Date: Wed, 6 Dec 2023 19:18:40 +0900
Subject: [PATCH] [obsidian] vault backup: 2023-12-06 19:18:40[

---
 content/音楽プログラミング言語の形式化.md | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/content/音楽プログラミング言語の形式化.md b/content/音楽プログラミング言語の形式化.md
index 603f504e..8dff53f1 100644
--- a/content/音楽プログラミング言語の形式化.md
+++ b/content/音楽プログラミング言語の形式化.md
@@ -152,6 +152,28 @@ process = hmtx(16);
 
 この辺は、多段階計算を使ったとしても生成したコードの型を変えるみたいなことは出来ないのでは？
 
+```rust
+fn hmtx(n:int)-> <[float;n]->[float;n]>{
+	assert!(n>=2 && n%2 == 0);
+	if(n==2){
+		`|list|{ [list[0]+list[1], list[0]-list[1]] }
+	}else{
+		`|list:[float]|{ 
+			let mixer = interleave 
+			|> |(l1,l2)| {zipwith(l1,l2).map(|(a,b)| a + b)};
+			|> ~hmtx(n/2);
+			let upper = list |> mixer;
+			let lower = list
+			|> split(_,2)
+			|>|(l1,l2)| {(l1,l2.map(|a| -a))}
+			|> mixer;
+			join(upper,lower)
+		}
+	}
+}
+
+```
+
 項でインデックスされた型＝依存型な気がするのよな
 
 [[多段階計算#依存型との組み合わせ]]