Prop vs. Set vs. Type

これを見ればカリー・ハワード対応の神髄が見える……かもしれない。

そのものの種類での比較
PropSetType
I : Truett : unit
FalseEmpty_set
true, false : bool
Some _, None : option A
or_introl _, or_intror _ : or P Qleft _, right _ : sumbool P Qinl _, inr _ : sum A B
inleft _, inright _ : sumor A Q
conj _ _ : and P Qpair _ _ : prod A B
proj1 : and P Q -> Pfst : prod A B -> A
proj2 : and P Q -> Qsnd : prod A B -> B
ex_intro _ : ex Pexist _ : sig P
existT _ : sigT B
proj1_sig : sig P -> A
projT1 : sigT B -> A
proj2_sig : sig P -> P x
projT2 : sigT B -> B x
ex_intro2 _ : ex2 P Qexist2 _ : sig2 P Q
existT2 _ : sigT2 B C
refl_equal : eq a arefl_identity : identity a a
inhabits _ : inhabited A
引数の種類での比較
PropType
not : Prop -> PropnotT : Type -> Prop
sig : forall A : Type, (A -> Prop) -> TypesigT : forall A : Type, (A -> Type) -> Type
© 2010 Magicant / 初出 2010-06-20