search

HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

Is Formality assuming Type : Type? #62

Closed be5invis closed 4 years ago

be5invis commented 4 years ago

I do not see TypData has any "sort level" compared to Agda or Idris.

johnchandlerburnham commented 4 years ago

Correct, Formality has Type : Type. This has many advantages for practical programming, but can lead to logical inconsistency via Girard's paradox. We can recover consistency by using the termination checker to write proofs in the terminating subset of the language

be5invis commented 4 years ago

The irony is that if Formality is targeting safe then it should not have logical inconsistency, at least for the total subset. Idris has a sort hierarchy, sound "total" subset and it is still expressive in practical programming.

johnchandlerburnham commented 4 years ago

So, I dearly love Idris. It was the first dependently typed language I used. Formality is not Idris, and isn't going to be a better Idris than Idris. We've made different design decisions which reflect the different priorities we have as a project.

One of those priorities is simplicity. Type universe hierarchies are extremely subtle and unsimple. Here's some open universe related issues (some consistency breaking) on Idris and Agda to illustrate.

Our approach, instead of universes, is to allow Type : Type, but to require proofs to terminate. Originally, we required all programs to terminate, i.e. Formality used to be a non-Turing-Complete language, but we recently decided to relax that restriction to improve usabiltiy: https://github.com/moonad/Formality/commit/5d1af1d023105a4c2eb51b0cd8be1a911c7a0d44

We conjecture that the terminating subset of Formality is sound, and are in the process of formalizing that in Agda: https://github.com/moonad/Formality-Agda/blob/master/Formality.agda

Also, for another example of a simple dependently typed language with Type in Type, check out PiSigma: https://www.andres-loeh.de/PiSigma/PiSigma.pdf

be5invis commented 4 years ago

@johnchandlerburnham Interesting, I will take a look. Thank you for your explanation. I know ΠΣ, and making Σ types first-class is interesting.

ice1000 commented 3 years ago

I remember @MaiaVictor told me that with linearity the construction of the Girard's paradox would fail

VictorTaelin commented 3 years ago

That is true. In a linear language it is impossible to construct Girard's, or any other, paradox, since these are looping programs, which don't exist in a terminating language such as the linear λ-calculus.