トップ «前の日記(2005-09-24) 最新 次の日記(2005-09-29)» 月表示 編集

日々の流転


2005-09-28 [長年日記]

λ. signature の equality に???

β変換すれば同じになるはずの(signatureで定義された)型が同一と見なされなくて、困ってしまった。例えば以下のコードのtestの定義では、「fm A (f x)」と「fm (Ty_m f A) x」はβ変換すれば同じシグネチャになるので、一見して型チェックは通りそうに見える。だが、実際には「t has type fm A (f x) but should have type that is equal to fm (Ty_m f A) x」と型エラーになってしまう。

Ty_o (X::Set) :: Type
  = X -> Set
 
Ty_m (|X,|Y::Set) (f::X->Y) (A::Ty_o Y) :: Ty_o X
  = \(x::X) -> A (f x)
 
fm (|X::Set) (A::Ty_o X) (x::X) :: Set
  = sig
      c :: A x
 
test (|X,|Y::Set) (|A::Ty_o Y) (f::X->Y) (x::X)
     (t::fm A (f x))
  :: fm (Ty_m f A) x
  = t

半日ほど悩んだ結果、この型エラーはfmの定義を以下のように書き換えれば回避出来ることに気づいた。しかし、このように書き換えなくてはならないのは直観的でないし、それに参照透明でもないように思う。何故このようになっているのだろうか?

fm' (Ax::Set) :: Set
  = sig
      c :: Ax
 
fm (|X::Set) (A::Ty_o X) (x::X) :: Set
  = fm' (A x)

【2006-05-03追記】 「薔薇色の明日」「Agdaの型チェック通らず」というエントリで書かれていた以下の話(パーマリンクが機能していないようなので勝手に引用)は、ひょっとして同じことで悩んでいるんじゃないかという気がする。

Agdaでちくちくと証明を実装していたのだが、エラーメッセージによると型が合っていない。しかし、私の記述は、システムが「この型であるべきですよー」という型の略記でしかないので、普通は同じ型とみなしてくれてもよさそうである。

仕方がないから先生にお尋ねしたところ、「ここを変えてみたら?」という助言のままに書き換えたところ、エラーメッセージが変わった。「ここは型Aと記述されてますけど、型Aになるように記述しないと駄目ですよー」と。

Tags: agda

λ. iPod nano

注文してみた。学割いいね。届くのが楽しみだ。

(2005-10-02 追記) 出荷予定日は2005-10-14か。とほほ……

Tags: 音楽