17 - Scala. Identity type. Curry–Howard correspondence
•
0 likes•103 views
This document discusses identity types in dependent type theory. It defines identity types as an equivalence relation, satisfying reflexivity, symmetry, and transitivity. It also outlines the formation, construction, elimination, computation rules, and uniqueness principle of identity types, describing them as types whose elements are proofs that two terms are equal/identical.
17 - Scala. Identity type. Curry–Howard correspondence
- 1. Identity type Dmytro Mitin https://stepik.org/course/Introduction-to-programming- with-dependent-types-in-Scala-2294/ March 2017 Dmytro Mitin Identity type
- 2. Equivalence relation An equivalence relation ∼ 1 Reflexivity a ∼ a 2 Symmetry a ∼ b =⇒ b ∼ a 3 Transitivity a ∼ b , b ∼ c =⇒ a ∼ c Dmytro Mitin Identity type
- 3. Identity type 1 Type Formation Γ A : ∗ Γ a1 : A Γ a2 : A Γ a1 =A a2 : ∗ 2 Constructor Γ a : A Γ refl a : a =A a 3 Eliminator . . . 4 Computation rules (”β-reduction“) . . . 5 Uniqueness principle (”η-conversion“) Dmytro Mitin Identity type