3 ms·

Contrary to what many comments here state, I don’t think this is only useful in a dynamic runtime kind-of environment. I often think I could use some form of th

Contrary to what many comments here state, I don’t think this is only useful in a dynamic runtime kind-of environment. I often think I could use some form of this in Rust and/or Haskell. In a very specific way: I often want a single constructor/branch of an enum (sum type) to a be a type as well, specifically a sub-type of the full enum. So once I learn about what branch a value is, I can treat it like that and even first class pass it around – without unpacking. I think this should be implementable in Rust without any runtime overhead as pure syntactic sugar. You get the same effect by creating a new struct for every set of values per branch and using those wrappers instead.

IshKebab 5y ago
Yeah this would definitely be useful in Rust. It isn't in Rust currently because enum variants aren't distinct types, but that's definitely on the to-do list. I suspect Rust will get this eventually.
marcosdumay 5y ago
You want something like Haskell's Typeable class?
chowells 5y ago
You can do this in Haskell with GADTs. data Up data Down data Foo tag a where Up :: a -> Foo Up a Down :: String -> Int -> Foo Down a When you enable all the necessary extensions for this to compile, it gives you exactly what you've asked for. If you leave the tag variable polymorphic in a function argument, you can receive values of either constructor. If you specify Foo Up a, you can only receive values with the Up constructor. It might be a bit more verbose than you want, with needing to declare types to use as the type level tags. (I looked into using PolyKinds and DataKinds to use the constructor as its own type argument, but GHC doesn't allow that type of recursion.) But it does do exactly what you've requested - it allows you to treat each constructor as a separate type in some contexts, and allow any of them in other contexts.
- sfvisser 5y ago
  Definitely yes! It's a loooong time ago, but the pattern exhaustiveness checker of GHC wasn't up to this last time I tried. But my guess is things are much better now and this might actually work.
  - chowells 5y ago
    There have been big improvements in the exhaustiveness checker. I know that it's not fully decideable with GADTs, so it will always have some holes, but it can handle this case now.

IshKebab 5y ago

Yeah this would definitely be useful in Rust. It isn't in Rust currently because enum variants aren't distinct types, but that's definitely on the to-do list. I suspect Rust will get this eventually.

marcosdumay 5y ago

You want something like Haskell's Typeable class?

chowells 5y ago

You can do this in Haskell with GADTs. data Up data Down data Foo tag a where Up :: a -> Foo Up a Down :: String -> Int -> Foo Down a When you enable all the necessary extensions for this to compile, it gives you exactly what you've asked for. If you leave the tag variable polymorphic in a function argument, you can receive values of either constructor. If you specify Foo Up a, you can only receive values with the Up constructor. It might be a bit more verbose than you want, with needing to declare types to use as the type level tags. (I looked into using PolyKinds and DataKinds to use the constructor as its own type argument, but GHC doesn't allow that type of recursion.) But it does do exactly what you've requested - it allows you to treat each constructor as a separate type in some contexts, and allow any of them in other contexts.

sfvisser 5y ago
Definitely yes! It's a loooong time ago, but the pattern exhaustiveness checker of GHC wasn't up to this last time I tried. But my guess is things are much better now and this might actually work.
- chowells 5y ago
  There have been big improvements in the exhaustiveness checker. I know that it's not fully decideable with GADTs, so it will always have some holes, but it can handle this case now.