Agda の List と Vec

朝起きてニュースをWebで見たら、首里城のあれだったので、よどよしてました。

それとは関係なく、 授業で、Agda で Automaton ってのをやってるんですが、だいたい r_0 とか r_i とか書いてある。これが Agda と相性が良くない。

List で入力データを表して、Automaton に食わせるとかの方が楽。でも、自然数添字の方も書いてみたんですが、あんまりうまくいかなくて。

でも、授業終わった後で、「そうだ、普通に ℕ → Q と書けば良い?」と思いついて。でも、長さで切らないとだめ。

　　r : (i : ℕ ) → i < suc n → Q

こんな感じか。「そうだよ、Cとかでもポインタでアクセスする時にはちゃんと正しい範囲のアクセスだと明示しろ!」とか思いました。

で、まぁ、それで書けたんですが、そういえば、

　　固定長の Vector ってあったよな?

と思って、Data.Vec を読んでみると、これが、長さ付きのList。そうなのか。そして、

　　Data.Vec と Data.List は両立しない

Agda は Polymorphism ないので、異なる型に同じ関数名を使えない。ま、いいか、全部、Vec で書けば。で、書き直せたんですが、

　　ほとんど、差がない

差があるのは、length を明示的に書く替わりに、引数に長さを表す { n : ℕ } が増えるだけ。あぁ、まぁ、そんなもんだよな。

もっと、ありがたいはずだとと思ったのに〜

まぁ、でも教科書の定義とListを使った定義の同等性とか、正規言語のUnionが正規言語とかできたらいいか。