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)
@tolmasky if I had to implement reflection in Lean4 or Agda, I would try to mimic #Haskell's typeable.
But also, I think there must be a very important point here! In dependently typed languages, entities can have more than one type!
(frac 1 2) : Frac 2 4, but also (frac 1 2) : Frac 4 8, for instance.
[1] : ListLE 1, but also [1]: ListLE 42.
So, perhaps the whole idea of general reflaction is defeated by this property. And this is why #haskell offers superior reflection[1]. Note that #Typeable is in #GHC itself!
I don't know if I'm mansplaining here or if you're aware of haskell's Typeable, but here is a simple demo of its capabilities: https://github.com/cognivore/typeable-haskell-demo/blob/main/app/Main.hs
In #Lean, I would emulate it by defining asking the user to provide explict instances over an enum, just as you wrote! The existential quantification trick can be done in #Lean by carrying the instance inside a structure that ties the knot between the type and an entity which has this type:
```
structure Stuff where
α : Type
val : α
inst : Reflect α
```
You won't be able to construct it unless α is Reflect.
* * *
[1]: https://hackage.haskell.org/package/base-4.21.0.0/docs/Type-Reflection.html#t:TypeRep
@tolmasky fwiw, you are absolutely correct: https://lean-lang.org/lean4/doc/dev/ffi.html?highlight=import#the-lean-abi