型コンストラクタはパタンマッチで使えない?
Haskellの話じゃなくて、またもAgda2の話です。
具体的には
data Nat : Set0 where zero : Nat succ : Nat -> Nat data Bool : Set0 where true : Bool false : Bool
とかでまぁ、データ型を定義して、その上で次のような関数
nonsense : Set0 -> Nat nonsense Bool = zero nonsense Nat = succ zero nonsense _ = succ (succ zero)
nonsenseを定義して、これはまぁ気持ち的には型コンストラクタでパタンマッチして、Boolなら0、Natなら1、それ以外であれば2を返すという感じのまぁそれなんですが、こいつで型チェックをかけると
Unreachable clauses when checking the definition of nonsense
と言われます。
これは何かって言うと、nonsenseの引数に出現しているBoolを、型コンストラクタと見なしていないからですね。つまり単なる変数とBoolが見なされてしまう。
なんでこんな事を考えたかというと、このNatとかBoolっていうのは、Set0に対する「データ構築子」として見れないかなーとかで、そうすると、同じデータ構築子であるzero,succ,true,falseはパターンとしての出現が許されているのにうーんみたいな・・・。