Ancestors

Toot

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

Descendants

Written by penguin42 on 2025-01-08 at 13:02

@tolmasky I'd bet smalltalk can do this; it's many years since I've used it, but each class in smalltalk is an instance of 'class class', so I assume you can have a list of those instances.

=> More informations about this toot | More toots from penguin42@mastodon.org.uk

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

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

@jonn I'm not familiar with Lean in particular, but having just quickly looked at the docs, it seems "as powerful" as Idris, IOW, dependently-typed, not this other thing that I don't know the word for, or if there is a word for it.

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

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

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

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 | More toots from joey@mathstodon.xyz

Proxy Information
Original URL
gemini://mastogem.picasoft.net/thread/113790327274715151
Status Code
Success (20)
Meta
text/gemini
Capsule Response Time
306.690979 milliseconds
Gemini-to-HTML Time
2.323747 milliseconds

This content has been proxied by September (ba2dc).