なぜなにあぐだ

data D : Set0 -> Set0 where
  nat : D Nat
  bool : D Bool

f : {A : Set0} -> A -> D A -> Unit
f (zero) (nat) = unit

Cannot split on argument of non-datatype @0
when checking the definition of f

これは、Agda2のnotesディレクトリの中、"inductive-families"から取って来ました。

なんだろうなぁコレ・・・。

implicitを使わないとどうなる??

f : (A : Set0) -> A -> D A -> Unit
f Nat (zero) (nat) = unit

実はこれは残念賞で、Agda2では型コンストラクタはパタンマッチの項で最左に持ってこられないので出来ませんし、覚えたてのdot patternを使っても

f : (A : Set0) -> A -> D A -> Unit
f .Nat (zero) (nat) = unit

Cannot split on argument of non-datatype @0
when checking the definition of f

なんかdot patternって、Implicit parameterをどうだこうだみたいな為にあるのかなぁ。いや分からん。というか多分dot pattern使って出来ないものはimplicit parameter使ってもダメなんじゃないかなぁ。

あぐだ滅茶苦茶難しいっていうか、これがどういう理由でなんだろうみたいになってないと、自分の処理系はどうしようみたいな。ちなみにimplicitの事とか私は全く考えてないので、上のf関数は出来ませんね。

また型コンストラクタもパタンマッチでバリバリ使えるようにするっていうか、都合良い感じにすると良いのかもしれませんけど・・・。