Funext from self?
Can we derive function extensionality from self types only?
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:
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 on this Github issue or in our Telegram chat.
