Skip to content

Instantly share code, notes, and snippets.

@johnchandlerburnham
Last active May 7, 2020 03:02
Show Gist options
  • Save johnchandlerburnham/3f972bc481c41f142add2b3c9087d5e6 to your computer and use it in GitHub Desktop.
Save johnchandlerburnham/3f972bc481c41f142add2b3c9087d5e6 to your computer and use it in GitHub Desktop.
Functional extionality in Formality (almost)
// To type-check, install npm:
// $ curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.35.3/install.sh | bash
// $ nvm install 13.10.1
//
// Then install Formality-Core:
// $ npm i -g formality-core
//
// Then download this file:
// $ curl https://gist.githubusercontent.com/MaiaVictor/28e3332c19fbd80747a0dceb33896b6b/raw/ae8d798225d2e6cc600e158f27d1b83ff384c262/intervals_with_self_types.fmc.c >> main.fmc
//
// Then just run `fmc` in the same dir:
// $ fmc
// Bool
// ====
// Bools can be defined as their dependent eliminations, using a self var `b`.
Bool: Type
b<P: Bool -> Type> ->
(True: P(true)) ->
(False: P(false)) ->
P(b)
true: Bool
<P> (t) (f) t
false: Bool
<P> (t) (f) f
// Nat
// ===
// Nats can be defined as their dependent eliminations, using a self var `n`.
Nat: Type
n<P: Nat -> Type> ->
(Zero: P(zero)) ->
(Succ: (pred: Nat) -> P(succ(pred))) ->
P(n)
zero: Nat
<P> (z) (s) z
succ: Nat -> Nat
(n) <P> (z) (s) s(n)
// Equality
// ========
// Equality can be defined as its dependent elimination, i.e., the J-axiom.
Id: (A: Type) -> A -> A -> Type
(A) (a) (b)
e<P: (b: A) -> Id(A)(a)(b) -> Type> ->
(Refl: P(a)(refl<A><a>)) ->
P(b)(e)
// A proof that a value is equal to itself.
refl: <A: Type> -> <a: A> -> Id(A)(a)(a)
<A> <a>
<P> (refl) refl
// If `a == b`, then `P(a)` implies `P(b)`.
rewrite: <A: Type> -> <a: A> -> <b: A> -> <P: A -> Type> -> <e: Id(A)(a)(b)> -> P(a) -> P(b)
<A> <a> <b> <P> <e> (x)
e<(b) (a) P(b)>(x)
// Ints
// ====
// Integers can be defined as a pair of nats quotiented by `(x,y) == (x+1,y+1)`.
// With self-types, we can do it with a smart constructor that normalizes both
// numbers to canonical form, i.e., (4,2) becomes (2,0), (3,5) becomes (0,2)...
Int: Type
i<P: Int -> Type> ->
(New: (x: Nat) -> (y: Nat) -> P(int(x)(y))) ->
P(i)
int: Nat -> Nat -> Int
(x) (y)
<P> (new)
x<(x) P(int(x)(y))>
| new(zero)(y);
| (x.pred) y<(y) P(int(succ(x.pred))(y))>
| new(succ(x.pred))(zero);
| (y.pred) int(x.pred)(y.pred)<P>(new);;
// Proof that `int(x)(y) == int(succ(x))(succ(y))`.
theorem: (x: Nat) -> (y: Nat) -> Id(Int)(int(x)(y))(int(succ(x))(succ(y)))
(x) (y) refl<Int><int(x)(y)>
// Intervals
// =========
// Intervals can be defined with an extra constructor for `i0 == i1`, as in:
// data I : Set where
// i0 : I
// i1 : I
// ie : i0 == i1
I: Type
i<P: I -> Type> ->
(I0: P(i0)) ->
(I1: P(i1)) ->
(Ie: Id(P(i0))(I0)(rewrite<I><i1><i0><P><ie>(I1))) ->
P(i)
i0: I
<P> (a) (b) (e)
a
i1: I
<P> (a) (b) (e)
b
// But this is left as an axiom. Can we actually construct it?
ie: Id(I)(i1)(i0)
ie
// Tests
// =====
// We can convert `i` to `true`.
i_to_true: (i: I) -> Bool
(i)
i<() Bool>
| true;
| true;
| refl<Bool><true>;
// We can convert `i` to `false`.
i_to_false: (i: I) -> Bool
(i)
i<() Bool>
| false;
| false;
| refl<Bool><false>;
// But we can't convert `i` to `true` or `false` depending on its value.
// distinguish_i: (i: I) -> Bool
// (i)
// i<() Bool>
// | true;
// | false;
// | Type; // impossible: demands a proof that `true == false`
// Problem: can we define `ie`?
mirror :
<A : Type> ->
<a : A> ->
<b : A> ->
(e : Id(A)(a)(b)) ->
Id(A)(b)(a)
<A> <a> <b> (e)
e<(b) () Id(A)(b)(a)>
| refl<A><a>;
apply:
<A : Type> ->
<B : A -> Type> ->
(a : A) ->
(b : A) ->
(f : (x : A) -> B(x)) ->
(e : Id(A)(a)(b)) ->
Id(B(a))(f(a))(rewrite<A><b><a><B><mirror<A><a><b>(e)>(f(b)))
<A> <B> (a) (b) (f) (e)
e<(eb) (e) Id(B(a))(f(a))(rewrite<A><eb><a><B><mirror<A><a><eb>(e)>(f(eb)))>
| refl<B(a)><f(a)>;
funext_helper:
<A : Type> ->
<B : A -> Type> ->
(f : (x : A) -> B(x)) ->
(g : (x : A) -> B(x)) ->
(H : (x : A) -> Id(B(x))(f(x))(g(x))) ->
(i : I) ->
(x : A) ->
B(x)
<A> <B> (f) (g) (H) (i) (x)
i<() B(x)>(f(x))(g(x))(H(x))
ie2 : Id(I)(i0)(i1)
mirror<I><i1><i0>(ie)
// non-eta-reduced extentionaly, proving that `∀x:A. f(x) == g(x) -> λx.f(x) == λx.g(x)`
funext:
<A : Type> ->
<B : A -> Type> ->
(f : (x : A) -> B(x)) ->
(g : (x : A) -> B(x)) ->
(H : (x : A) -> Id(B(x))(f(x))(g(x))) ->
Id((x : A) -> B(x))((x) f(x))((x) g(x))
<A> <B> (f) (g) (H)
apply<I><() ((x : A) -> B(x))>(i0)(i1)((x) funext_helper<A><B>(f)(g)(H)(x))(ie2)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment