2013-09-06から1日間の記事一覧

こわくない Idris (3)

ハロー、依存型プログラミングの世界 (3) 依存ペア 依存ペア dependent pair とは、ある値と、その値に依存した型を持つ値のペアのことだ。 data Exists : (a : Type) -> (P : a -> Type) -> Type where Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Ex…