4 ms·

Haskell's type system isn't Turing-complete or even particularly sophisticated. There are extensions to its type system implemented in GHC that in theory give y

Haskell's type system isn't Turing-complete or even particularly sophisticated. There are extensions to its type system implemented in GHC that in theory give you unbounded computation, but a) those aren't actually Haskell and b) nobody does any real work with them and c) it gives up trying to typecheck if it takes too long. I don't know much about Idris but a few seconds of searching tells me its type theory is not Turing-complete either.[1] [1] http://cs.stackexchange.com/questions/19577/what-can-idris-not-do-by-giving-up-turing-completeness/23916#23916 http://cs.stackexchange.com/questions/19577/what-can-idris-n...

mrkgnao 10y ago
If you're talking about things like UndecidableInstances or FlexibleContexts, um, they are n't exactly uncommon! In any case, saying that Haskell 98 is the One True Haskell(TM) isn't accurate. Almost all code (beyond the LYAH level) written today uses a few Haskell 2010 extensions, mostly for ergonomics (things like OverloadedStrings are a good example of this), not to mention all the extensions that make mtl let you write "lift whatever" instead of "lift . lift . lift ..." and infer how "high" you want to go up the monad transformer stack.
tathougies 10y ago
UndecidableInstances is used in more libraries than you would think. In general, it doesn't inpact safety although certain programs may fail to compile because the compiler gives up after a while. However, this won't result in the acceptance of ill typed programs. Ultimately, the compiler is just acting like any other language run time -- at some point, your Python interpreter will give up (run time type error), your browser will give up (that annoying stop script pop up), and your operating system will give up (out of memory exception). Also, your link indicates idris's type system is Turing complete.
- Oxitendwe 10y ago
  >Idris won't reduce partial functions at the type level, in order to keep type checking decidable. Totality precludes Turing-completeness. Specifically, functions that don't terminate are by definition partial, and if you can't express functions that don't terminate then it isn't Turing-complete.

mrkgnao 10y ago

If you're talking about things like UndecidableInstances or FlexibleContexts, um, they are n't exactly uncommon! In any case, saying that Haskell 98 is the One True Haskell(TM) isn't accurate. Almost all code (beyond the LYAH level) written today uses a few Haskell 2010 extensions, mostly for ergonomics (things like OverloadedStrings are a good example of this), not to mention all the extensions that make mtl let you write "lift whatever" instead of "lift . lift . lift ..." and infer how "high" you want to go up the monad transformer stack.

tathougies 10y ago

UndecidableInstances is used in more libraries than you would think. In general, it doesn't inpact safety although certain programs may fail to compile because the compiler gives up after a while. However, this won't result in the acceptance of ill typed programs. Ultimately, the compiler is just acting like any other language run time -- at some point, your Python interpreter will give up (run time type error), your browser will give up (that annoying stop script pop up), and your operating system will give up (out of memory exception). Also, your link indicates idris's type system is Turing complete.

Oxitendwe 10y ago
>Idris won't reduce partial functions at the type level, in order to keep type checking decidable. Totality precludes Turing-completeness. Specifically, functions that don't terminate are by definition partial, and if you can't express functions that don't terminate then it isn't Turing-complete.