どつとパタン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を行わないようにしないと、逆に言えば行ってしまうと、ヤバいのかなぁ。

普通に同じ構造かどうかか(勿論パタンマッチする時点で値は決まって無いと行けないので、決まっている値同士を比べれば良いだけだと思うけど)調べれば良いだけだからなんでだろう。

実行効率とかなのかなぁ。