3 ms·

> 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 (

> 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”.

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”.