[retrac]

> Idris is primarily a research project, led by Edwin Brady at the University of St Andrews, and has benefited from SICSA (https://www.sicsa.ac.uk) and EPSRC (https://www.epsrc.ac.uk/) funding. This does influence some design choices and implementation priorities, and means that some things are not as polished as we’d like. Nevertheless, we are still trying to make it as widely usable as we can!

-- https://idris2.readthedocs.io/en/latest/faq/faq.html

At this point, the creator has described it as "Pac-Man complete", able and easy to implement a game like Pac Man. (Or itself - it compiles to Scheme but is written in itself.)

Dependent types are still rather new; I believe Idris and its libraries are one of the largest, if not the largest, body of general-purpose software that uses them. (F* maybe?) How to use dependent types properly in a standard library seems be an ongoing development.

[Quekid5]

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]

What is “TC”?

[nextaccountic]

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.

[Quekid5]

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.)

[bmitc]

Thanks for the correction. I misremembered reading something by Brady.