[obsidian] vault backup: 2023-12-06 19:18:40[

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)
+		}
+	}
+}
+
+```
+
 項でインデックスされた型＝依存型な気がするのよな
 
 [[多段階計算#依存型との組み合わせ]]