Can anyone familiar with Idris (or a different language with dependent types) confirm that types can *not* be used as values. For example, I can't make a list of types (a List that contains Int, Bool, and String directly). I also can't make a record that stores a type and an instance of that type (Like record TypeInstancePair { a :: Type, b :: a }). If so, is there a language that *does* allow this, and what is this feature called (other than "first-class types" which seems overloaded).

@tolmasky I didn't go into details of your use-case, sorry, but the mind-bending bit about dependently typed languages is that there are no value-type dichotomy. Just sone expressions with those are expressible, and some are not.

I take a lot of pride in this code:

https://github.com/argumentcomputer/Wasm.lean/blob/main/Wasm/Wast/Num.lean#L85-L89

Observe how function invocation is a type. (Feel free to ignore Cached constructor, it's an optimisation).

Sorry for a non-answer, I hope it helps. But based on what I understand about the things you describe, it should be somehow possible and I hope my snippet will get you moving in the right direction.

@jonn Right, but the frustrating thing is that there *is* a dichotomy. Types still only exist at compile time, and while types can depend on values, values can't depend on types. You're still running Program 1 first (the type/value program), THEN running Program 2 (the value program). Which means you still have to do indirection like Enum TBool | TInt | TBlah, etc. What I am more or less looking for is a type-safe version of reflection. So you could do something like fields(myType)