News for hackers. Stuff that matters.

A comment on My resignation letter as R7RS-large chair. Parent comment

Re:My resignation letter as R7RS-large chair by Quekid5 on Thursday August 17, 2023 @05:19PM (#37168256)
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 people unfamiliar with dependently typed langs, but infinite streams etc., servers that "loop forever" doing request-repsonse can still be modeled without TC.)

[ Parent | on HN ]
Re:My resignation letter as R7RS-large chair by mangodrunk on Thursday August 17, 2023 @09:43PM (#37170567)
What is “TC”?
[ Parent | on HN ]
Re:My resignation letter as R7RS-large chair by nextaccountic on Thursday August 17, 2023 @10:06PM (#37170692)
Turing complete

However it appears that Idris is Turing complete https://cs.stackexchange.com/questions/19577/what-can-idris-... https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53d... so I'm confused.

[ Parent | on HN ]
Re:My resignation letter as R7RS-large chair by Quekid5 on Friday August 18, 2023 @02:06AM (#37171852)
Note 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.)

[ Parent | on HN ]