4 ms·
The Pac-Man Complete bit is tongue-in-cheek. It's an observation that TC is rarely (if ever) actually needed in practice. (This might sound strange to people u
by Quekid5 3y ago
The Pac-Man Complete bit is tongue-in-cheek. It's an observation that TC is rarely (if ever) actually needed in practice.
(This might sound strange to people unfamiliar with dependently typed langs, but infinite streams etc., servers that "loop forever" doing request-repsonse can still be modeled without TC.)
- mangodrunk 3y agoWhat is “TC”?
- nextaccountic 3y agoTuring complete However it appears that Idris is Turing complete https://cs.stackexchange.com/questions/19577/what-can-idris-not-do-by-giving-up-turing-completeness https://cs.stackexchange.com/questions/19577/what-can-idris-... https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53dfcec086 https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53d... so I'm confused.
- Quekid5 3y agoNote the "codata" and also note that "main" is marked as "partial". Only the total subset of Idris is non-TC. Note also the use of Fuel -- this is to provide "fuel" for the computation, but it's a data structure which can only decrease in 'size' -- which is used by the compiler to prove totality (termination). ("codata" is a way to model 'infinite' computations as data structures.)