Why Dhall advertises the absence of Turing-completeness: http://www.haskellforall.com/2020/01/why-dhall-advertises-absence-of-turing.html …
Usually I understand "Turing-complete" to mean that the language can not only implement but also run the Turing-machine
-
-
Yes, Agda can do that! The type signature just doesn't lie about the fact that the machine will necessarily terminate is all.
-
My understanding is that this approach to running a Turing machine in a total language requires an out-of-band way to continue a partiality monad, which seems not in the spirit of being Turing complete. Or in other words, if Agda is Turing-complete then the term is meaningless
- Još 6 drugih odgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.