[thinkpad20]

Why is this there? Is it to facilitate things like Typeable? I believe that there's no language-level way to do things like runtime type reflection. And even if there were, how would one express a complex type like (Vector (forall a. MyTypeClass a => a -> Int, String))?

I'm also curious if dependently typed languages like Idris, which presumably must be able to have runtime access to type information, handle this stuff.

[chadaustin]

For values, laziness means there is a tag bit for whether a value is a thunk or evaluated. Sum types use tags to determine which variant is active.

For functions, because a function that takes two arguments and returns a value (a -> a -> a) has the same type as a function that takes one argument and returns a function that takes another argument that returns a value (a -> a -> a), the arity of functions is stored in the tag.

Some of these tags are eliminated by inlining but if you sit down and read some typical Haskell output you'll see a _whole lot_ of tag checks.

Source: spent a lot of time reading GHC output and writing high-performance Haskell code.

[15155]

In Idris, as far as I know, runtime type information is kept around by default and erased through usage-based optimization (and possibly annotation?)

http://docs.idris-lang.org/en/latest/reference/erasure.html