Toot

Written by Joey Eremondi on 2025-01-08 at 16:15

@tolmasky You can absolutely use types as values! For example, Heterogeneous lists, which are indexed by a list of types, to make a kind of extensible tuple. You can see these under HList at https://www.idris-lang.org/docs/idris2/0.6.0/base_docs/docs/Data.List.Quantifiers.html

Typically, those types are erased at run-time. This is necessary to guarantee some properties like parametricity, and it helps with performance, but it is not strictly necessary. Idris lets you do stuff with types at compile-time.

Idris allows types at run-time, and many languages allow this is a weakened way using something called a "Universe ala Tarski," where you have a type Code and a decoding El : Code -> Type. I think you need to allow induction-recursion (e.g. an inductive type mutually defined with a recursive function) to encode dependent types this way.

There are some systems where disallowing runtime types is necessary to avoid proofs of False, e.g. anything with HoTT or univalence, since you need to guarantee that isomomrphic types behave identically at run-time.

=> More informations about this toot | View the thread | More toots from joey@mathstodon.xyz

Mentions

=> View tolmasky@mastodon.social profile

Tags