日々の流転

λ. case on non-var!?

Propositional Equality の型である Id の使い方がいまいち良くわからない。例えば、

Cat :: #2
  = sig
      Obj :: Type
      Hom :: (A::Obj) -> (B::Obj) -> Set
      id  :: (A::Obj) |-> Hom A A
      o   :: (A::Obj) |-> (B::Obj) |-> (C::Obj) |->
             (f::Hom B C) -> (g::Hom A B) -> Hom A C
      leftUnit  :: (A::Obj) |-> (B::Obj) |-> (f::Hom A B) -> Id (id `o` f) f
      rightUnit :: (A::Obj) |-> (B::Obj) |-> (f::Hom A B) -> Id (f `o` id) f
      Assoc :: (A::Obj) |-> (B::Obj) |-> (C::Obj) |-> (D::Obj) |->
               (f::Hom C D) -> (g::Hom B C) -> (h::Hom A B) ->
               Id ((f `o` g) `o` h) (f `o` (g `o` h))
 
test1 (C::Cat) (A,B::C.Obj) (f::C.Hom A B) :: { }150
  = {C.leftUnit f }151
 
test2 (C::Cat) (A,B::C.Obj) (f,g::C.Hom A B) (z::Id f g) :: { }152
  = {z }153

という状態で、goal 151 で C-c C-c しても、「case on non-var C.leftUnit |? |? f」と言われてしまう。「C.leftUnit f」を「C.leftUnit |A |B f」としても、やはり「case on non-var C.leftUnit |A |B f」と言われてしまう。letを使って一度変数に入れても同じエラーが出る。一方、goal 153 で C-c C-c すると、ちゃんとcaseが挿入される。どっちも型は同じなのに、何故このようになるのだろう?

(2005-09-11 追記) 「型は同じ」と書いたが全然同じじゃないな(汗)。
ところで、落ち着いて考えてみて、何らかの制約があること自体は当然だと気づいた。何故ならば、「case (Id α β) of { ref x -> ... }」という式の「...」の部分はα=β(=x)を仮定して型検査を行うわけだけど、α,βに任意の式を許すと型検査が決定可能でなくなってしまうから。
では、どのくらいの制約が必要か?　αとβがユニフィケーション可能な式であるならば良さそうに思える。だが、実際にはAgdaはαとβが相異なる変数の場合しか受け付けない。これは必要以上に強い制約に思えるが、何故こうなっているのだろうか?

ちなみに、HaskellのGADTはユニフィケーション可能な型でありさえすれば良かったはず。なので、例えば以下のような定義は正しい。

data T a b where
    T :: x -> T x x
 
test :: (T (a,Int) (Int,b)) -> Int
test x =
    case x of
    T (a,b) -> a+b

(2005-09-18 追記) 「ユニフィケーション可能な式ならば〜」というのは安易だった。Haskellの型の場合と違って、higher-order unification が必要だから、決定不可能になってしまう。Functional Programming with Overloading and Higher-Order Polymorphism には higher-order unification が不要な理由として「This is possible because the language of constructors is built up from constants and applications; in particular, there are no abstractions.」と書いてあったのを読んでいたのに、何を馬鹿なことを考えてるんだ、俺は……

——となると、残る疑問はαとβが同じ変数の場合が何故ダメかだな。池上さんが紹介してくれたスライドに「Use elimination rules and not case for inductive families.」と書いてあったし、単に「idata に対しては case よりも elimination rule を使わせる方針なので、case は elimination rule を実装するのに十分な最小限の実装しかされていない」という可能性もあるけど、何か他の理由はあるだろうか?

(2005-09-28 追記) あ、いや、αとβが同じ変数の場合も、一般のidataを考えると無理っぽいな。だいたい納得。

λ. Saunders Mac Lane 1909-2005

亡くなっていたとは知りませんでした。ご冥福をお祈りします。