Opt-in consistency in Kind

[sbp]

Kind has a "how I learned to stop worrying and love the Type:Type" vibe. That doesn't make it invalid as a proof language. It just inverts the priority: instead of consistency being the default and expressivity being opt-in (as in Agda, with the type-in-type pragma), it is expressive by default, and consistency is an opt-in. I strongly believe that is the right way. It is still not implemented, but the language is completely ready for that.

— /u/LangMakers

I couldn't find any issue tracking this feature, so I thought I'd submit one. That way updates can be posted here, discussions can potentially take place, and people can more easily track the outcome. And by people I mean me ;)

[caotic123]

I agree with Victor, I would like to augment that (i am guessing here) we have no intentions to fall into some trivial inconsistency (I mean talking of the trading of consistency vs expressivity). Well, as far I know, Girard's proof is not trivially derived, and if you have no intention of writing this, so you won't easily fall into this, this is also true for a bunch of new problems (UIP+HOTT, injection...).

I am moving this to the discussion section, but @rigille might confirm this later.

[rigille]

Alright we'll post here as soon as we have some updates on that front. It might take a while 🙂

[wkolowski]

I think that currently consistency is not only a matter of type-in-type and Girard's paradox, since it can be easily derived from nontermination.

type Empty {}

loop : Empty
  loop

> kind loop --norm
> Segmentation fault (core dumped)

Since it's rather easy to write a nonterminating program by mistake, it would also be easy to "prove" something that shouldn't hold under a proper termination checker and then inadvertently use that to prove even more subtly false theorems.