9 ms·

This is a very good explaination of that topic, creating languages which are not turing complete but still useful. Also, I recommend reading Harper's throughts

by vog 10y ago

This is a very good explaination of that topic, creating languages which are not turing complete but still useful. Also, I recommend reading Harper's throughts about it: "Old Neglected Theorems Are Still Theorems" https://existentialtype.wordpress.com/2014/03/20/old-neglected-theorems-are-still-theorems/ https://existentialtype.wordpress.com/2014/03/20/old-neglect... It also reminds me of the NASA coding standards, rule 4: "All loops must have a fixed upper-bound", see http://pixelscommander.com/en/javascript/nasa-coding-standarts-for-javascript-performance/ http://pixelscommander.com/en/javascript/nasa-coding-standar... (Related HN discussion: https://news.ycombinator.com/item?id=8856226 https://news.ycombinator.com/item?id=8856226)

wyager 10y ago
The approach given in the paper explicitly allows for Turing completeness through the use of data/codata types. Instead of proving termination over codata you prove that a function "does something useful" every iteration.
- willtim 10y ago
  You would of course need to factor out the outer-loop to do this. But it seems even this is not necessary. This paper discusses using total languages to build generally recursive (Turing complete) computations as an effect monad: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
  - wyager 10y ago
    > You would of course need to factor out the outer-loop to do this What are you referring to? Data/codata checking works with local type inference.
    - mkehrt 10y ago
      Essentially, to get a nonterminating, program, your top level function needs to take a piece of codata to corecurse over to run indefinitely. Since you can't actually write a program that takes no arguments that produces an infinite piece of data, all programs must terminate.
      - wyager 10y ago
        >Since you can't actually write a program that takes no arguments that produces an infinite piece of data Huh? inf = Cons 1 inf
        mkehrt 10y ago
        Hm, you may be right. I though that was going to violate: > Each recursive function call must be on a syntactic subcomponent of its formal parameter. But it doesn't. But you can't actually use that to get a nonterminating program, because you can't recurse over it: > Ordinary recursion is not legal over codata, because it might not terminate.
  - chriswarbo 10y ago
    One nice use of the "general recursion monad" idea is "mtac" ( http://plv.mpi-sws.org/mtac/ http://plv.mpi-sws.org/mtac/ ), a "tactic language" for Coq. This allows meta-programming, to calculate what a value/function/etc. should be, which is really useful for proof objects (i.e. values which are required for compilation, but have no effect on runtime computation). A tactic language doesn't need to be total, since it's only run at compile-time, so no errors can leak into the resulting proof/program. The worst that can happen is the compiler hangs. Coq comes with "ltac", which is a horrible imperative language that leads to very fragile proofs. On the other hand, mtac is just Coq's normal, total FP language ("gallina"). A monad is used to wrap up general recursion, so that gallina can be used un-changed. During compilation, these monadic values are forced, which either leads to a value or causes the compiler to hang. This is a really nice compromise, since you can write Haskell-style FP code which "obviously terminates", without having to prove that it terminates, you still have access to all of the nice dependent type machinery, and the end result (the program, not the meta-program) is guaranteed to be total (unlike, say, an Idris function which turns off the totality checker).
- cousin_it 10y ago
  For me, Turing completeness means being able to implement every computable function of type Integer -> Integer. Total languages can't do that. They need an additional input that bounds the number of steps, but the whole point of Turing completeness is not needing that input, but rather being able to run any Turing machine until it stops on its own. Otherwise you'd be forced to conclude that many languages known to be not Turing complete, like the simply typed lambda calculus, are Turing complete in disguise, and the definition loses all teeth. This is similar to the Brown-Palsberg self-interpreter in a total language, which caused a lot of confusion recently because it's not a self-interpreter (it doesn't take source code as an argument). I think it's better to stick with common definitions and accept that total languages are not Turing complete and can't self-interpret.
  - pron 10y ago
    There's a subtlety here. Total functional languages are necessary when the language is used as a general theorem prover via propositions-as-types (it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations; for all intents and purposes, the halting theorem still holds, as its bounded version -- which is what matters -- does not require self-interpretation for diagonalization). Now, for this to work, any computation that is represented as a function -- how computations are normally represented in functional languages -- must provably terminate, otherwise an inconsistency may be introduced into the logic corresponding to the program (this inconsistency does not apply when actual computations are concerned, only when the program represents a general mathematical theorem). However, computations may be represented not as functions but as monads, too, and introducing a monad that, while not implementable in the language itself, loops forever does not harm the totality that matters to theorem proving.
    - tome 10y ago
      > it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations Is it a common error? Who's commonly saying this? Can you link any examples? It seems a really strange claim to make.

by vog 10y ago

wyager 10y ago

The approach given in the paper explicitly allows for Turing completeness through the use of data/codata types. Instead of proving termination over codata you prove that a function "does something useful" every iteration.

willtim 10y ago
You would of course need to factor out the outer-loop to do this. But it seems even this is not necessary. This paper discusses using total languages to build generally recursive (Turing complete) computations as an effect monad: https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree.pdf https://personal.cis.strath.ac.uk/conor.mcbride/TotallyFree....
- wyager 10y ago
  > You would of course need to factor out the outer-loop to do this What are you referring to? Data/codata checking works with local type inference.
  - mkehrt 10y ago
    Essentially, to get a nonterminating, program, your top level function needs to take a piece of codata to corecurse over to run indefinitely. Since you can't actually write a program that takes no arguments that produces an infinite piece of data, all programs must terminate.
    - wyager 10y ago
      >Since you can't actually write a program that takes no arguments that produces an infinite piece of data Huh? inf = Cons 1 inf
      - mkehrt 10y ago
        Hm, you may be right. I though that was going to violate: > Each recursive function call must be on a syntactic subcomponent of its formal parameter. But it doesn't. But you can't actually use that to get a nonterminating program, because you can't recurse over it: > Ordinary recursion is not legal over codata, because it might not terminate.
- chriswarbo 10y ago
  One nice use of the "general recursion monad" idea is "mtac" ( http://plv.mpi-sws.org/mtac/ http://plv.mpi-sws.org/mtac/ ), a "tactic language" for Coq. This allows meta-programming, to calculate what a value/function/etc. should be, which is really useful for proof objects (i.e. values which are required for compilation, but have no effect on runtime computation). A tactic language doesn't need to be total, since it's only run at compile-time, so no errors can leak into the resulting proof/program. The worst that can happen is the compiler hangs. Coq comes with "ltac", which is a horrible imperative language that leads to very fragile proofs. On the other hand, mtac is just Coq's normal, total FP language ("gallina"). A monad is used to wrap up general recursion, so that gallina can be used un-changed. During compilation, these monadic values are forced, which either leads to a value or causes the compiler to hang. This is a really nice compromise, since you can write Haskell-style FP code which "obviously terminates", without having to prove that it terminates, you still have access to all of the nice dependent type machinery, and the end result (the program, not the meta-program) is guaranteed to be total (unlike, say, an Idris function which turns off the totality checker).
cousin_it 10y ago
For me, Turing completeness means being able to implement every computable function of type Integer -> Integer. Total languages can't do that. They need an additional input that bounds the number of steps, but the whole point of Turing completeness is not needing that input, but rather being able to run any Turing machine until it stops on its own. Otherwise you'd be forced to conclude that many languages known to be not Turing complete, like the simply typed lambda calculus, are Turing complete in disguise, and the definition loses all teeth. This is similar to the Brown-Palsberg self-interpreter in a total language, which caused a lot of confusion recently because it's not a self-interpreter (it doesn't take source code as an argument). I think it's better to stick with common definitions and accept that total languages are not Turing complete and can't self-interpret.
- pron 10y ago
  There's a subtlety here. Total functional languages are necessary when the language is used as a general theorem prover via propositions-as-types (it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations; for all intents and purposes, the halting theorem still holds, as its bounded version -- which is what matters -- does not require self-interpretation for diagonalization). Now, for this to work, any computation that is represented as a function -- how computations are normally represented in functional languages -- must provably terminate, otherwise an inconsistency may be introduced into the logic corresponding to the program (this inconsistency does not apply when actual computations are concerned, only when the program represents a general mathematical theorem). However, computations may be represented not as functions but as monads, too, and introducing a monad that, while not implementable in the language itself, loops forever does not harm the totality that matters to theorem proving.
  - tome 10y ago
    > it is a common error -- but an error nonetheless -- to believe that totality has a non-negligible effect on proving correctness of computations Is it a common error? Who's commonly saying this? Can you link any examples? It seems a really strange claim to make.