日々の流転

λ. Coq の extraction

<URL:http://d.hatena.ne.jp/syd_syd/20070622#p1> と <URL:http://www.eva-01.jp/d/?date=20070623#p03> あたりを読んで、なるほどと思った。 Coqではextractionをそういう風に使うのね。 AgdaだとそもそもSetとPropの区別が無いから、extractionのようなことをあまり意識したことがなかった(Agdaで書くと下みたいになっちゃうし*1)。考え方の違いが面白い。

Decidable :: Set -> Set
Decidable P = P `Or` (Not P)

lemma :: (C::Context) -> (e::Expr) -> (t::Type) -> Decidable (C |- e : t))
lemma = ...

typeCheck :: (C::Context) -> (e::Expr) -> (t::Type) -> Bool
typeCheck C e t =
  case lemma C e t of
  (inl x) -> true
  (inr y) -> false