なぜなにあぐだ

髪の毛が乾くまで暇なので書く。

data Unit : Set0 where
  unit : Unit

data Ty : Unit -> Set0 where
  ty : (u : Unit) -> Ty u

f : (Ty unit) -> Unit
f (ty unit) = unit

g : Ty unit -> Unit
g (ty x) = unit

この型チェックエラーメッセージ

fの型チェック
u != unit of type Unit
when checking that the pattern ty unit has type Ty unit

gの型チェック
x != unit of type Unit
when checking that the pattern ty x has type Ty unit

gの型チェックで、
typeof (ty x) == Ty X これがTy unitと常に同じく成るかというと、実はこれも案外微妙な問題なんじゃないかなぁ・・・みたいな・・・。
まず決定的に明らかなのは、tyの引数の型はUnitであるから、x∈Unitとなるという。
次に、Ty (x∈Unit) と Ty unitって、Unitの値ってunitしか無いんだから出来るやないかみたいなソレじゃないかなぁ・・・という。

まぁ、１つしか値が無いんだったら、それを書けば良いでしょうに(つまりこの場合はxじゃなくて、unitを書く。つまり関数fなんですけど...)っていうのは話が分かります。

まぁ準公理使ってなぞの何かを作り出すとかだと困るんですけど。
それは例えば、

data Unit : Set0 where
  unit : Unit

data Ty : Unit -> Set0 where
  ty : (u : Unit) -> Ty u

postulate nanka : Unit

h1 : Unit -> Unit
h1 unit = unit

h2 : Unit -> Unit
h2 x = x

v1 : Ty (h1 nanka) -- これ！
v1 = ty (h1 nanka)

v2 : Ty nanka -- と、これ！
v2 = ty (h2 nanka)

っていうのがあって、んっふっふー。まぁこういう頭が悪いのは良いとして・・・。

ともかく、gの型チェックエラーのメッセージが、理解出来るものだというのは分かります。

ところが、fの型チェックエラーのメッセージ

u != unit of type Unit
when checking that the pattern ty unit has type Ty unit

このuっていうのは

data Ty : Unit -> Set0 where
ty : (u : Unit) -> Ty u

ここのuの事です。

なんでコレが絡むのかを考えて

-- Agda2ではcaseじゃなくてwithを使わないといけないのですが便宜上
f : (Ty unit) -> Unit
f a = case a of
        ty u -> case u of -- <- このty uが元のgと同じ！で、ここでエラー出ちゃう。
                  unit -> unit

g : Ty unit -> Unit
g a = case a of
        ty u -> case u of
                  u -> unit -- 元のxはどうした！！１

と同じなのかなーと思ったりします。

しかしこれだと、fのエラーメッセージとは揃うのですが、gのエラーメッセージが今度はfと同じに成って再現出来ません。

だからこれはもしかして、型コンストラクタの引数が変数かそうでないか、で処理を分けてるんじゃないかなーというのがあって、つまり

f : (Ty unit) -> Unit
f a = case a of
        ty u -> case u of
                  unit -> unit

g : Ty unit -> Unit
g a = case a of
        ty x -> case x of
                  x -> unit

みたいにα変換(α-conversion)してるからじゃないかなーみたいな。
なんていうか、有る意味で、元のgのパターン変数として書いたxを尊重する形でやってくれてるのかなぁみたいな・・・。

これらの意味で、引数部でのパターンマッチっていうのは、case式の構文糖みたいなソレで、こういう風にexpandされるんじゃないかなーっていうのは、勿論ML(http://article.gmane.org/gmane.comp.lang.agda/1019)のお陰です。

すっかり髪の毛は乾きました。

f : (Ty unit) -> Unit
f (ty u) = case u of -- (ty u)は、tyの定義から持って来ている。
             unit -> unit

g : Ty unit -> Unit
g (ty x) = case x of
             _ -> unit

の方が良いかも。

で、dot-patternで何故解決出来るのか！！みたいなそれは、今回のケースでは、(ty u)にされちゃう段階で死ぬので、その展開をなんとかして止めなければ成りません。

で、それを止めて型シグネチャからの制約で何とか解決してくれるのがdot-patternさんなんではないかなーと。