こわくない Idris (3) - Ryusei’s Notes (a.k.a. M59のブログ)ハロー、依存型プログラミングの世界 (3) 依存ペア 依存ペア dependent pair とは、ある値と、その値に依存した型を持つ値のペアのことだ。 data Exists : (a : Type) -> (P : a -> Type) -> Type where Ex_intro : {P : a -> Type} -> (x : a) -> P x -> Exists a PEx_introによって作られたペアは、aという型の値xと、xに依存した P x という型を持った値を保持している。なぜこのデータ型の型コンストラクタがExistsという名前なのかと言えば、Exists A Pという型が という命題に対応するからだ。型と命題の対応関係については後に述べる。 REPLでExistsを使ってみると、たとえばこうなる。 Idris> the (Exists Nat (\n => Ve
いつTypeScriptを始めるのか
