どつとパタン2
data Nat : Set0 where zero : Nat succ : Nat -> Nat data Ty {A : Set0} : A -> Set0 where ty : (a : A) -> Ty a f : Ty zero -> Nat f (ty .zero) = zero {- f (ty zero) = zeroだとすると a != zero of type Nat when checking that the pattern ty zero has type Ty zero と言われる -} f2 : {a : Nat} -> Ty a -> Nat f2 (ty zero) = zero f2 (ty a) = (succ zero) f3 : {a : Nat} -> Ty a -> Nat f3 {zero} (ty .zero) = zero f3 {a} (ty .a) = (succ zero) v1 = f2 (ty (succ zero))
f2とf3は意味的に全く同じ?
f2は、パタンマッチを実際に行って値を変えている。
f3は、dot patternを使うという意味で(ty .zero)と(ty .a)で区別が付かなくて死ぬんじゃないかと思うけれども・・・これは多分{zero}と{a}の方で何かが起こってるんだろうなぁ。
で、f1はなんていうか・・・やっぱり(ty zero)と書けるべきだと思う。
で、a != zeroが出て来てるのが一番不安で、結局なんでdot patternを使わないといけないのかが分からない。
ただ、Repeated Variableが「出てしまう」ケースでは止むなし(でもそれにしても、最初からdot patternを「使わなくても良い」ようにして欲しいけど・・・)かなーとは思う。
というか、Repeated Variableの時にpattern matchingを行わないようにしないと、逆に言えば行ってしまうと、ヤバいのかなぁ。
普通に同じ構造かどうかか(勿論パタンマッチする時点で値は決まって無いと行けないので、決まっている値同士を比べれば良いだけだと思うけど)調べれば良いだけだからなんでだろう。
実行効率とかなのかなぁ。