Last active
June 27, 2020 21:26
-
-
Save VictorTaelin/6f0ad6665bcefc6cd2997538e7c6c185 to your computer and use it in GitHub Desktop.
The difference between boolean equality and type-level equality in Formality
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Equality with values | |
// ==================== | |
// A Boolean is a set with two values | |
T Bool | |
| true; | |
| false; | |
// Boolean not is a function that receives a bool and returns a bool | |
bool_not(a: Bool): Bool | |
case a: | |
| false; | |
| true; | |
// Boolean and is a function that receives 2 bools and returns a bool | |
bool_and(a: Bool, b: Bool): Bool | |
case a: | |
| case b: | |
| false; | |
| false;; | |
| case b: | |
| false; | |
| true;; | |
// Boolean or is a function that receives 2 bools and returns a bool | |
bool_or(a: Bool, b: Bool): Bool | |
case a: | |
| case b: | |
| false; | |
| false;; | |
| case b: | |
| false; | |
| true;; | |
// Boolean equal is a function that receives 2 bools and returns a bool | |
// The compiler doesn't connect it to the concept of "equality" because it could | |
// be any other `Bool -> Bool -> Bool` function. It can't use it for rewrites. | |
bool_equal(a: Bool, b: Bool): Bool | |
case a: | |
| case b: | |
| true; | |
| false;; | |
| case b: | |
| false; | |
| true;; | |
// This is just the boolean "true" | |
bool_true_is_true: Bool | |
bool_equal(true, true) | |
// This is just the boolean "false" | |
bool_true_is_false: Bool | |
bool_equal(true, false) | |
// This is just the boolean "false" | |
bool_false_is_true: Bool | |
bool_equal(false, true) | |
// This is just the boolean "true" | |
bool_false_is_false: Bool | |
bool_equal(false, false) | |
// ... | |
// Equality with types | |
// =================== | |
// Type-level False is represented by an empty type (Empty on Prelude.fm). | |
T False | |
// Type-level True is represented by a non-empty type (Unit on Prelude.fm). | |
T True | |
| truth; | |
// Type-level Not is a function from a type `A` to the empty type (False). | |
Not(A: Type): Type | |
A -> False | |
// Type-level And is just a pair (Pair on Prelude.fm). | |
T And<A: Type, B: Type> | |
| and(a: A, b: B); | |
// Type-level Or is just an either (Either on Prelude.fm). | |
T Or<A: Type, B: Type> | |
| or_a(a: A); | |
| or_b(b: B); | |
// Type-level Equal is a datatype with two indices assigned to the same var. | |
// This is the information the compiler needs to learn the concept of equality. | |
// \/ polymorphic on a type A | |
T Equal<A: Type> ~ (a: A, b: A) // <- with two indices | |
| same<a: A> ~ (a, a); // <- both indices assigned to the same variable `a` | |
// Note:, now I see the problem with explaining the Equal type (and, thus, how | |
// it is different from an Equal function). The user must know how indexed | |
// datatypes work first. Once he does, Equal(A,a,b) becomes much clearer. | |
// Since the Equal type teaches the compiler the notion of sameness, we can use | |
// it to implement "rewrite", which converts `a` to `b` inside a type, as long as | |
// `a == b`. For example, if we have `vec : Vector(Nat, 3 + x)`, we can use it | |
// to convert it to `vec : Vector(Nat, x + 3)` (if we prove `3 + x == x + 3`). | |
Equal.rewrite<A: Type, a: A, b: A, P: A -> Type>(e: Equal(A,a,b)): P(a) -> P(b) | |
case e: | |
| (x) x; | |
: P(e.a) -> P(e.b); | |
// A proof that true == true is the constructor same applied to true | |
true_is_true: Equal(Bool, true, true) | |
same<Bool, true> | |
// A proof that false == false is the constructor same applied to false | |
false_is_false: Equal(Bool, false, false) | |
same<Bool, false> | |
// A proof that true == false is a function that receives `tf: true == false`. | |
// It returns `truth : if true then True else False`, and uses `tf` to rewrite | |
// `true` by `false` on that type, resulting in `truth : False`. | |
true_isnt_false: Not(Equal(Bool, true, false)) | |
(tf) Equal.rewrite<_, true, false, (x) if x then True else False>(tf, truth) | |
// A proof that false == true is a function like the one above. | |
false_isnt_true: Not(Equal(Bool, false, true)) | |
(tf) Equal.rewrite<_, false, true, (x) if x then False else True>(tf, truth) | |
// A decision of A is either an element of A, or a proof that A is empty. | |
T Decision<A: Type> | |
| Decision.yep(proof: A); | |
| Decision.nop(proof: Not(A)); | |
// A logical equality function is a function that receives 2 bools, and returns | |
// either a proof that `a == b` or `a != b`, depending on their values. | |
Compare(a: Bool, b: Bool): Decision(Equal(Bool, a,b)) | |
case a: | |
| case b: | |
| Decision.yep<>(true_is_true); | |
| Decision.nop<>(true_isnt_false); | |
: Decision(Equal(Bool, true, b.self));; | |
| case b: | |
| Decision.nop<>(false_isnt_true); | |
| Decision.yep<>(false_is_false); | |
: Decision(Equal(Bool, false, b.self));; | |
: Decision(Equal(Bool, a.self, b)); |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Tabularised, to make it easier to compare them.