Why can’t it be simplified?Note: I also noticed a different problem with Cedille-Core, which may make it incompatible with the abstract algorithm I mentioned earlier.
I won’t elaborate here, but there is more info on this commit.
Simplifying CedilleCedille can, indeed, be extremely simplified with a single change: replacing dependent intersections and equality primitives by self types and mutual recursion.
Both approaches are actually very similar, but the later achieves two very important feats:Due to mutual recursion, the declaration of the type of a datatype can refer to its constructors before they were defined.
As such, we don’t need anymore two different declarations of the same type, plus a third one to merge both.
We can declare the datatype in a single go.
Since now there is only one type involved, we don’t need to prove reflexivity to prove induction.
This allows us to dispense all equality primitives of the language, which amount to about half of its complexity.
So, in turn, this small change makes the core language roughly 40% smaller, and the implementation of inductive datatypes inside it roughly 60% smaller.
This is what the induction proof becomes (type-checker included on Gist):This is not only much smaller; from 67 to 26 lines; but, most importantly, there is no redundancy anymore.
The declaration of an inductive datatype like Nat includes exactly the information necessary to specify its induction principle.
Of course, this isn’t as terse as Agda, for example; but this time, the added information is there because it is actually necessary.
Agda merely hides it on its implementation.
As an example,Eq reads almost like the J axiom, and deriving it is straightforward:This language also solves many problems Cedille has, such as being unable to prove 1 != 0 without an extra axiom, or being possibly incompatible with the abstract algorithm.
Needless to say, I really like it.
Sadly, though, good things don't come for free.
The researcher who introduced Self-types himself claimed they are too difficult to provide a semantics for, which is why he moved away from them and built Cedille around dependent intersections.
In other words, chances are such language would be inconsistent.
I do wonder, though, if Self-types are inherently problematic, or if it we just didn’t find the proper setup to give a semantics for them.
And even if it is the case that any similar approach would be necessarily inconsistent, we know that “it possible to reason correctly about programs in an inconsistent language, as long as every “proof-like” term is normalized”, as elaborated on on this dissertation.
So, I do still have hopes this language is very close to what I’m looking for.
If anyone has insights on whether it is possible to use such thing as a theorem prover, please let me know, as I do not have enough knowledge to answer that kind of question.
I’m posting this image to prevent Medium from using my face on thumbnails ffs.