Ancestors

Written by Francisco Tolmasky on 2025-01-08 at 02:16

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).

=> More informations about this toot | More toots from tolmasky@mastodon.social

Written by Jons Mostovojs on 2025-01-08 at 15:20

@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.

=> More informations about this toot | More toots from jonn@social.doma.dev

Written by Francisco Tolmasky on 2025-01-08 at 15:32

@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)

=> More informations about this toot | More toots from tolmasky@mastodon.social

Toot

Written by Jons Mostovojs on 2025-01-08 at 18:22

@tolmasky ah! "Type-safe version of reflection" makes a lot of sense. I will think more.

=> More informations about this toot | More toots from jonn@social.doma.dev

Descendants

Written by Jons Mostovojs on 2025-01-08 at 18:23

@tolmasky fwiw, you are absolutely correct: https://lean-lang.org/lean4/doc/dev/ffi.html?highlight=import#the-lean-abi

=> More informations about this toot | More toots from jonn@social.doma.dev

Written by Jons Mostovojs on 2025-01-08 at 19:14

@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.

=> More informations about this toot | More toots from jonn@social.doma.dev