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