David Christiansen - Coding for Types: The Universe Patern in Idris - Curry On

[@FreeScience]

One of the most interesting languages at the moment.

[@cynocephalusw]

I think it is still today. It allows even more concise code than most other languages.

[@preveenpadmanabhan7994]

Great audio. Thanks

[@mortenbrodersen8664]

Brilliant talk. Thanks!

[@timh.6872]

I'm probably being a pedant and/or asking for trouble, but couldn't you theoretically make a code type for the Idris Universe(s) and then use that to pattern match on Idris types? Sure, it breaks theorems for free (which is just the fact that parametric polymorphism must be natural), but you need something like that for a self-hosting compiler. If HoTT got folded in, then you could even attempt naturality proofs for non-parametric polymorphic functions in the places where it needs to be ensured.

[@joomyk]

btw Idris 2 has type-case, in case you want to give it a try: gist.github.com/edwinb/25cd0449aab932bdf49456d426960fed github.com/edwinb/Idris2

[@digama0]

This basically hits up against Goedel's incompleteness theorem. You will necessarily need a more powerful induction principle than whatever the language provides to express everything the language provides. Idris has induction-recursion, so you would need induction-induction-recursion to express the induction-recursion scheme itself. If you added IIR you would need IIIR, etc. If you added III..R you would need some omega-inductive-recursive scheme, I'm not sure anyone has ever worked out what that is. You can still represent the full type system in the style of a compiler, but you won't be able to go full dependent types here, there will be expressions that you can't observe are well typed within the language itself. Most compilers for dependent type theories are written in simpler type theories, so they just have to play fast and loose with assert and unreachable stuff for places where the type system is insufficiently smart to argue that those things are actually unreachable.