どつとパタン

昨日のアレはMLで質問してみました
http://thread.gmane.org/gmane.comp.lang.agda/1015

すると、Wouterさんが、
http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.DatatypeAndFunctionDefinitions
ここにdot patternがあるからそれを使えば良いんじゃね！！という事を教えてくれました。

When pattern matching on an element of an inductive family we get information about the index.

To distinguish parts of a pattern which are determined by pattern matching (the inaccessible patterns)
and the parts which constitutes the actual pattern matching,
the inaccessible patterns are prefixed with a dot.

これはなんだか様子がおかしそうです。訳してみよう。

inductive familyの要素でのパターンマッチをする時に、インデクスについての情報を得る。(どういう事?)

2つのパターンを見分けられるようにしている。
1.パターンマッチにより決定されるパターン(the inaccessible patterns)と
2.実際のパターンマッチを構成するパート
である。

the inaccessible patternには、dot(.)がプレフィクスとして付けられる。

謎だなー。

実例として

even+ : (n m : Nat) → IsEven n → IsEven m → IsEven (n + m)
even+ .zero          m  evenZ        em = em
even+ .(suc (suc n)) m (evenSS n en) em = evenSS (n + m) (even+ n m en em)

というのがあって、2つ目のパターンで、nが(succ (succ n))と、(evenSS n en)の2箇所で出現している(repeated variableどうのこうのと普通は起こられる)とか謎がある。

The proof is by recursion on the proof that n is even.
Pattern matching on this proof will force the value of n
and hence the patterns for n are prefixed with a dot to indicate that they are not part of the pattern matching.

ふむ。

indicate that they are not part of the pattern matching.か・・・。

例えば

-- dot patternを使わない
even+ : (n m : Nat) → IsEven n → IsEven m → IsEven (n + m)
even+ zero m evenZ em = em
even+ (succ (succ n)) m (evenSS n en) em = evenSS (n + m) (even+ n m en em)

と、

Repeated variables in left hand side: n
when scope checking the left-hand side
even+ (succ (succ n)) m (evenSS n en) em in the definition of even+

とか言われちゃうワケですね。

かと言って

even+ : (n m : Nat) → IsEven n → IsEven m → IsEven (n + m)
even+ zero m evenZ em = em
even+ (succ (succ n)) m (evenSS n' en) em = evenSS (n + m) (even+ n m en em)

こう書けば、

n' != n of type Nat
when checking that the pattern evenSS n' en has type
IsEven (succ (succ n))

こう叱られてしまう。
これは、型シグネチャ的には当然なアレで(succ (succ n)) と IsEven (succ (succ n'))から n と n'のunifyになって、これは失敗してダメだと。

まずなんとかして型チェックをくぐり抜けないと行けないが、かといってRepeated variableには出来ない・・・として、dot patternの登場という感じなのかな。

で、「実行時」にはdotが付いている所とはパタンマッチは行わないと・・・。そんな感じなのかな。

手元で書いたのは

data Unit : Set0 where
  unit : Unit

data Bool : Set0 where
  true : Bool
  false : Bool

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

data Vh {A : Set0} : A -> Set0 where
  vh : (a : A) -> Vh a

postulate dummy1 : Ty unit

f : Ty unit -> Bool -> Ty unit
f (ty .unit) true = (ty unit)
f (ty .unit) false = dummy1
{-
f a _ = a これを書くと
Unreachable clause
when checking the definition of f
などと出る
-}

v1 = f (ty unit) true
v1' = vh v1
-- Vh (ty unit)

v2 = f dummy1 false
v2' = vh v2
-- Vh (f dummy1 false)

なんだろう・・・。

f a _ = aが書けないのが嫌だし・・・。

もう一度Coq

Inductive Unit : Set := unit : Unit | unit2 : Unit. (* 何故かunit2を付けないと、fで _ が書けない *)

Inductive Bool : Set := true : Bool | false : Bool.

Inductive Ty {A : Set} : A -> Set := ty (a : A) : Ty a.

Axiom nanka : Ty unit.

Definition f (arg : Ty unit) :=
  match arg with
    | ty unit => true
    | _ => false
  end.

Definition x1 := Eval compute in ty (f (ty unit)).
(* Check x1 -> x1 : Ty true *)

Definition x2 := Eval compute in ty (f nanka).
(*Check x2 ->
x2
     : Ty
         match
           nanka in (Ty u)
           return match u with
                  | unit => Bool
                  | unit2 => Bool
                  end
         with
         | ty a =>
             match
               a as a0
               return match a0 with
                      | unit => Bool
                      | unit2 => Bool
                      end
             with
             | unit => true
             | unit2 => false
             end
         end
*)

これじゃなくて

Inductive Unit : Set := unit : Unit.

Inductive Bool : Set := true : Bool | false : Bool.

Inductive Ty {A : Set} : A -> Set := ty (a : A) : Ty a.

Axiom nanka : Ty unit.

Definition f (arg : Ty unit) :=
  match arg with
    | ty unit => true
  end.

Definition x1 := Eval compute in ty (f (ty unit)).

Definition x2 := Eval compute in ty (f nanka).
(*
Check x2 ->
x2
     : Ty
         match nanka in (Ty u) return match u with
                                      | unit => Bool
                                      end with
         | ty a =>
             match a as a0 return match a0 with
                                  | unit => Bool
                                  end with
             | unit => true
             end
         end
*)

ううーん・・・。これなんで型チェック通るんだろう。

そもそも、型に対する値を必要とするパターンマッチ(match)で、値が無い謎の物体Xを持って来ても、パターンマッチのやりようが無い・・・のか・・・。とすると、後者は分かった。

でも、前者の例、何故unit2がパタンマッチに現れているんだろう。