Can we derive function extensionality from self types only?

[VictorTaelin]

The main insight behind self types is easy to explain. Simple functions can be written as A -> B, and an application f a has type B. Dependent functions can be written as (x: A) -> B x, and an application f a has type B a. The insight is that the type returned by an application has access to the value of the argument a. Self dependent functions can be written as s(x: A) -> B s x, and an application f a has type B f a. The insight is that the type returned by an application can also access the value of the function f! This simple, elegant extension allow us to construct inductive datatypes with lambdas.

It is not rare for generalisations to allow us to do things beyond the concrete reasons they were discovered. So, a question is, what else self-types allow us to do? A very interesting thing we just found is the concept of smart-constructors, i.e., constructors that compute. With them, we can define an Int type as a pair of Nat such that the constructor itself canonicalizes its values, i.e., (4,2) becomes (2,0), (3,5) becomes (0,2), etc. We can then trivially prove that (a,b) == (succ(a), succ(b)). This is as elegant as the quotiented formalization, without the computational blowup.

What would be really great is an implementation of intervals, i.e., a type inhabited by two definitionally equal values, i0 and i1 such that i0 == i1. We've got surprisingly close by adding a phantom constructor ie : i0 == i1 to the self encoding. It works as expected: to eliminate an interval, one must provide a proof that both returned values are equal. But there is one thing missing: the construction ie itself, left as an axiom. If we managed to construct it, then Funext would follow trivially. Even if we don't, this might point to a simple primitive that could allow us to have it without needing to add i0 and i1 as native concepts.

If anyone is willing to try, I've made this self-sufficient Formality-Core file:

// 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 [email protected]
// 
// Then download this file:
// $ curl https://gist.githubusercontent.com/MaiaVictor/28e3332c19fbd80747a0dceb33896b6b/raw/638d0ee9b623b02e5484d18c2be593fbc40183f2/intervals_with_self_types.fmc.c >> main.fmc
// 
// Then just run `fmc` in the same dir:
// $ fmc

// The syntax is simple.
// `(x) x`        is a lambda
// `f(x)`         is an application
// `f|x;`         is an alternative syntax for a multi-line application
// `s(x: A) -> B` is a dependent function type
// `<x> x`        is a computationally irrelevant lambda
// `f<x>`         is a computationally irrelevant application
// `s<x: A> -> B` is a computationally irrelevant dependent function type

// The main insight behind self-types is easy to explain. Simple functions can
// be written as `A -> B`, and an application `f a` has type `B`. Dependent
// functions can be written as `(x: A) -> B x`, and an application `f a` has
// type `B a`. The great insight behind dependent functions is that the type
// returned by an application has access to the value of the argument `a`.  Self
// dependent functions can be written as `s(x: A) -> B s x`, and an application
// `f a` has type `B f a`. The insight is that the type returned by an
// application can also access the value of the function `f`! This simple,
// elegant extension allow us to construct inductive datatypes with lambdas.

// 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`?

Formality-Core is just an implementation of a dependently typed language with self types, a fast type checker and nice error messages. Running it is extremely easy (5 commands in a Linux environment), so give it a try! If you have any reason to suspect this is either possible or not, or any pointers to how we could change the language as slightly as possible to complete this proof, we'd be thrilled to know.

Note: you need to use [email protected] since it considered the application of an erased f to f(x) equal to x. We don't do that anymore (erasures don't affect type-checking at all and may even be removed from core soon).

[VictorTaelin]

I think this is relevant (UIP):

same
  : <A: Type> ->
    <a: A> ->
    <b: A> ->
    <e0: Id(A)(a)(b)> ->
    <e1: Id(A)(a)(b)> ->
    Id(Id(A)(a)(b))(e0)(e1)
  <A> <a> <b> <e0> <e1>
  e0<(x) (e) (e1: Id(A)(a)(x)) -> Id(Id(A)(a)(x))(e)(e1)>
  | (e1) e1<(x) (e)
      Id(Id(A)(a)(x))
      | rewrite<A><a><x><(x) Id(A)(a)(x)><e>(refl<A><a>);
      | e;>
    | refl<Id(A)(a)(a)><refl<A><a>>;;
  | e1;

Note this only holds if we allow the erasure of functions (i.e., accept f(x) ~> x for an erased argument f instead of raising an error). This causes rewrite to become identity (note that the e argument of rewrite is erased). I just experimentally added this on the last version (0.2.71). But if I understand correctly, UIP is incompatible with intervals. To revert, we just need to remove this change and convert rewrite back to its former representation (since we'll not be able to erase e anymore).

[jasoncarr0]

But if I understand correctly, UIP is incompatible with intervals

I don't believe this is true. Intervals have no more than 1 equality between two values, and there have been systems with quotient types and UIP iirc.

Of note: the standard proof of funext from the existence of an interval requires that you have eta-equivalence (i.e. f = \x -> f x definitionally) in addition to definitional pattern matching on the interval.

That said I think it's not easy to answer one way or another easily without proper consistency, but pretending that it was consistent, you most likely you cannot prove function extensionality as it implies the existence of non-canonical identity proofs (that is, closed terms of type f = g which are not an application of refl), so the way you can prove one way or another is by proving the existence/non-existence of such equalities. There's no evidence to me that they exist (besides non-terminating examples), and you very likely do not want them to exist.

[johnchandlerburnham]

@MaiaVictor Here is my proof that given ie : Id(I)(i1)(i0) we can prove the non-eta-reduced version of functional extensionality: https://gist.github.com/johnchandlerburnham/3f972bc481c41f142add2b3c9087d5e6

@jasoncarr0 It's true that the usual funext proof (I've adapted mine from here: https://people.csail.mit.edu/jgross/CSW/csw_paper_template/paper.pdf) uses the eta-reduced form, but even without eta-reduction I think that ∀x:A. f(x) == g(x) -> λx.f(x) == λx.g(x) is still meaningful (and we can always add eta-reduction to Formality later on if we want the usual form).

That said, your comment about non-canonical identity proofs is exactly in line with my thinking as to why we won't actually be able to instantiate ie. I think that proving that all x : Equal... are refl (which it probably is) is effectively just proving the K axiom, which does imply UIP.

[jasoncarr0]

I think that proving that all x : Equal... are refl (which it probably is) is effectively just proving the K axiom, which does imply UIP.

The difference here is UIP/K is an internal statement, whereas canonicity is an external statement. Here since you have UIP you could still prove propositional equality of any proofs of equality. I don't know that you'll get any farther with that eta-expanded funext form.

[johnchandlerburnham]

We have internal proofs of UIP/K with erased rewrite, Victor's proof above, but also

K: Type
  (A : Type) ->
  (x : A) ->
  (p: Id(A)(x)(x)) ->
  Id(Id(A)(x)(x))(p)(refl<A><x>)

k : K
  (A) (x) (p)
  p<(eb) (e) Id(Id(A)(x)(eb))(e)(rewrite<A><x><eb><(y) Id(A)(x)(y)><e>(refl<A><x>))>
  | refl<Id(A)(x)(x)><refl<A><x>>;

Non-erased rewrite can't be proven internally, due to the p in K being a variable you can't expand. Formality gets stuck on

Reduced to... e<P: (b: Id(A)(x)(x)) -> Id(Id(A)(x)(x))(p)(b) -> Type> -> (Refl: P(p)(refl)) -> P(rewrite(p)(refl))(e)
Instead of... e<P: (b: Id(A)(x)(x)) -> Id(Id(A)(x)(x))(p)(b) -> Type> -> (Refl: P(p)(refl)) -> P(refl)(e)

However, I think an external statement of canonicity would follow from noticing that if e : Id(A)(x)(y) then

e : <A: Type> -> <a : A> -> <b: A> -> 
     e<P: (b: A) -> Id(A)(a)(b) -> Type> -> 
     (Refl: P(a)(refl<A><a>)) ->
     P(b)(e)
<A> <a> <b> <P> (Refl) Refl

which, unless you break consistency, has to be structurally equal after erasure to (x) x (I did a short write-up here that explains a little why that expansion of e makes sense: https://gist.github.com/johnchandlerburnham/1ac8ee3690917a144b69667359afd6a7)

[jasoncarr0]

@johnchandlerburnham Ah I think I misread your comment a bit. Thanks for the great write-up

[johnchandlerburnham]

@MaiaVictor The linked gist https://gist.github.com/MaiaVictor/28e3332c19fbd80747a0dceb33896b6b now type errors on latest formality-core with

Inside i_to_true:
Found type... Id(Bool)(true)(true)
Instead of... Id(Bool)(true)(rewrite<I><i1><i0><() Bool><ie>(true))
With context:
- i : I
On line 145:
   141|   (i)
   142|   i<() Bool>
   143|   | true;
   144|   | true;
   145|   | refl<Bool><true>;
   146| 

[johnchandlerburnham]

Having investigated this, the issue is caused by the removal of an experimental typechecking feature that allowed an application of an erased lambda to equal its argument: <f> f(x) ~> x.

So you have to use [email protected] to run the file. (If this conflicts with your global fm/fmc executable, run npm i [email protected] in your local directory without the -g flag and run with `./node_modules/formality-core/bin/fmc.js)