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 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 ]