3 ms·

If you're fine with 'stupid' refinement types in the form of subset types without coercion, not only do you get them 'for free' from the core type theory withou

If you're fine with 'stupid' refinement types in the form of subset types without coercion, not only do you get them 'for free' from the core type theory without introducing another language element, I personally also think they're quite intuitive. Using a subset type of non-zero nats or providing a proof that the argument isn't zero to define a 'proper divsion' just 'makes the most sense' in my opinion, but that may just be ultimately down to personal taste. I really do think though that no single part of dependent type theory is actually all that complex. It's not as simple as TLA+, but there's nothing really hard about it till you start proving. And I'm not saying that all this is feasible right now, but I'm fairly certain that this is at least fundamentally possible. You can't 'truly' separate specifications from proofs in dependent type theory, but you also definitely don't need to really understand how to write actual proofs to write even complex specifications in it. All of this of course depends on stronger automation for a good subset (possibly by also integrating strongly with other provers), but I don't think that's a total pipe dream (though I am definitely personally biased on this). >The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions I'm just talking about the 'well-behaved' subset, but let me go at this from another angle. If Lean tomorrow introduced a Sort Omega to type universes, the set of programs that you can write wouldn't change. It's essentially just a syntactic change. Would that really be enough to make you say that these are functions now while they previously weren't? >But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? If you quantify over a universe, a constraint gets introduced as part of the type checker. These constraints can be viewed as a graph that is checked for cycles, so not having a specific universe isn't an issue.

pron 6y ago
> but I don't think that's a total pipe dream You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a model and its proof theory aesthetically unappealing (not that I find everything in formal FO set theories appealing). Of course, it may have other advantages. > Would that really be enough to make you say that these are functions now while they previously weren't? Yes, provided that `id` wouldn't be a function that could operate on that type. But any operator with a truly universal domain cannot be, itself, a quantifiable object without introducing a Russell paradox (perhaps constructiveness can save it, but assuming the system allows non-computable objects, too). As it is, `id` is universal, but it isn't a function. This isn't just a philosophical or even a purely syntactic difference. Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. > so not having a specific universe isn't an issue. Does that require forbidding full recursion, or can you still introduce non-computable objects?
- ImprobableTruth 6y ago
  >Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. That's true, but I don't think you necessarily need a type for all universes (excluding itself), just some other way to denote that type is supposed to be universe polymorphic. >Does that require forbidding full recursion, or can you still introduce non-computable objects? I'm not sure what you mean exactly. The core type theory assumes that all functions are terminating. You can 'cheat in' full recursion by providing a non-computational termination proof, but the type checker would still be assuming that its actually terminating. I think if that wasn't the case, it'd need to be restricted (unless you did something really weird like introducing infinite negative universe levels).

pron 6y ago

> but I don't think that's a total pipe dream You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a model and its proof theory aesthetically unappealing (not that I find everything in formal FO set theories appealing). Of course, it may have other advantages. > Would that really be enough to make you say that these are functions now while they previously weren't? Yes, provided that `id` wouldn't be a function that could operate on that type. But any operator with a truly universal domain cannot be, itself, a quantifiable object without introducing a Russell paradox (perhaps constructiveness can save it, but assuming the system allows non-computable objects, too). As it is, `id` is universal, but it isn't a function. This isn't just a philosophical or even a purely syntactic difference. Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. > so not having a specific universe isn't an issue. Does that require forbidding full recursion, or can you still introduce non-computable objects?

ImprobableTruth 6y ago
>Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. That's true, but I don't think you necessarily need a type for all universes (excluding itself), just some other way to denote that type is supposed to be universe polymorphic. >Does that require forbidding full recursion, or can you still introduce non-computable objects? I'm not sure what you mean exactly. The core type theory assumes that all functions are terminating. You can 'cheat in' full recursion by providing a non-computational termination proof, but the type checker would still be assuming that its actually terminating. I think if that wasn't the case, it'd need to be restricted (unless you did something really weird like introducing infinite negative universe levels).