4 ms·

The drawback is that if you also have (parametric) polymorphism (and you do, unless you’re strictly standard Pascal and impossible to write libraries in), your

The drawback is that if you also have (parametric) polymorphism (and you do, unless you’re strictly standard Pascal and impossible to write libraries in), your typechecker now needs to answer arbitrary questions of the form “are there natural numbers that make this equality true?” in order to tell if something is well-typed or not. And that is of course impossible in general (per Gödel and Turing), so now it’s one on you to give the proofs. So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems and, though it’s perfectly possible to write useful programs in them, it requires a more disciplined and restricted approach than usual, and you’re going have to spend some time proving things. There are also languages—notably C++ and Haskell—that do this less seriously, in that their systems are capable of expressing naturals but are either unsound (allowing some programs that passed the typechecker to misbehave due to type-related problems), semidecidable (allowing the typechecker to hang on erroneous programs), too weak (not allowing you to prove equalities you need), or all of the above. On the upside, those are also the ones flexible enough that normal people can program in them (as long as they don’t try typing every length and size they see, then it becomes as painful as ever). (Other responses have mentioned interesting type systems for dynamic languages, such as those in Racket and Common Lisp. I think those mostly fall into the “unsound” bucket above, due to runtime checks, but I don’t know much about them. Should be worth looking into as well.)

biorach 4y ago
> So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right?
- xavxav 4y ago
  Both, but almost more importantly the languages themselves are all strictly terminating. Long story short, these languages are based on the “Howard-Curry isomorphism” which says that we can view type signatures as theorems and programs with that signature proofs of that theorem. A program which runs forever is a proof of false (you could see it as saying “after infinity time I’ll have your answer I swear”). So these languages are designed to prevent that from being possible.
  - Smaug123 4y ago
    This is pretty misleading, isn't it? Idris and Agda, for example, have coinductive types, which you could in principle use to write a "coprogram" that provably never terminates, such as an operating system (where "terminate" really means "put myself into a clean state and then turn off the power"). See e.g. http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html and the links therein; Conor McBride is constantly railing about this; see e.g. https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T... .
    - xavxav 4y ago
      I explicitly ignored codata/coinduction as they are complex and rather niche. Even so, they come with their own notion of 'termination' (progress / wfo) and don't magically let you write random non-terminating programs. Depending on what you want to achieve there are plenty of tricks and techniques to encode a divergent program in a sound dependent-type theory, but the best approach to use will depend on the problem statement.
  - still_grokking 4y ago
    ATS is "strictly terminating"? Really?
- mananaysiempre 4y ago
  > you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right? Either is a possibility. Agda and Idris have full dependent types, that is every value computation is allowed to be used as a type parameter, so all value computations are forced to terminate in a way apparent to the typechecker and are consequently not Turing-complete. (As a sibling comment mentions, aside from hanging your compile when run an infinite loop is an example of empty so a proof of false, thus if the compiler decides it’s uninterested in the details and trusts it to work instead of actually running it it’s actually worse.) ATS I think has a Turing-incomplete proof language distinct from the Turing-complete program language, but I’ve never been able to get through its rather arcane documentation so I’m not sure. Frama-C or SPARK is one example where I’m certain that’s the case (the program language is C or Ada, respectively), except the proof language is “throw intermediate statements at the SAT solver and see what sticks”.

biorach 4y ago

> So languages that do this seriously—Agda, Idris, ATS—are usually somewhat Turing-incomplete in order to sidestep this and related problems of too-expressive (sound) type systems you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right?

xavxav 4y ago
Both, but almost more importantly the languages themselves are all strictly terminating. Long story short, these languages are based on the “Howard-Curry isomorphism” which says that we can view type signatures as theorems and programs with that signature proofs of that theorem. A program which runs forever is a proof of false (you could see it as saying “after infinity time I’ll have your answer I swear”). So these languages are designed to prevent that from being possible.
- Smaug123 4y ago
  This is pretty misleading, isn't it? Idris and Agda, for example, have coinductive types, which you could in principle use to write a "coprogram" that provably never terminates, such as an operating system (where "terminate" really means "put myself into a clean state and then turn off the power"). See e.g. http://blog.sigfpe.com/2007/07/data-and-codata.html http://blog.sigfpe.com/2007/07/data-and-codata.html and the links therein; Conor McBride is constantly railing about this; see e.g. https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_Turing_completeness_totally_free.pdf https://strathprints.strath.ac.uk/60166/1/McBride_LNCS2015_T... .
  - xavxav 4y ago
    I explicitly ignored codata/coinduction as they are complex and rather niche. Even so, they come with their own notion of 'termination' (progress / wfo) and don't magically let you write random non-terminating programs. Depending on what you want to achieve there are plenty of tricks and techniques to encode a divergent program in a sound dependent-type theory, but the best approach to use will depend on the problem statement.
- still_grokking 4y ago
  ATS is "strictly terminating"? Really?
mananaysiempre 4y ago
> you mean that the _type systems_ of these languages are somewhat Turing-incomplete, not the languages themselves, right? Either is a possibility. Agda and Idris have full dependent types, that is every value computation is allowed to be used as a type parameter, so all value computations are forced to terminate in a way apparent to the typechecker and are consequently not Turing-complete. (As a sibling comment mentions, aside from hanging your compile when run an infinite loop is an example of empty so a proof of false, thus if the compiler decides it’s uninterested in the details and trusts it to work instead of actually running it it’s actually worse.) ATS I think has a Turing-incomplete proof language distinct from the Turing-complete program language, but I’ve never been able to get through its rather arcane documentation so I’m not sure. Frama-C or SPARK is one example where I’m certain that’s the case (the program language is C or Ada, respectively), except the proof language is “throw intermediate statements at the SAT solver and see what sticks”.