3 ms·
Both, but almost more importantly the languages themselves are all strictly terminating. Long story short, these languages are based on the “Howard-Curry isomo
by 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 agoThis 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 agoI 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 agoATS is "strictly terminating"? Really?