Extract parameters from Haskell types with `DataKinds`

Question

GHC's DataKinds extension allows for defining types that are parametrized by some data. Is there some possible way to use these these parameters on the RHS of a function definition? For example, in Agda I could extract the length of a vector directly from its type without computing on its constructors:

length : Vec A n -> Nat
length {n = n} _ = n

Is there a possible way to do this in Haskell?

The reason I am interested in this is because I think it would be helpful for a project I'm doing, which is a custom Haskell library for calling Java in a type-safe way (as safe as it is possible to achieve). I thought instead of having a single type representing all Java objects I could have a type parametrized by a Java class name as a string (e.g. JObject "java.math.BigDecimal"), so that instances of different classes in Java would also have different types in their representations in Haskell. And if what I am asking here is possible, then it would allow for automatically computing the JNI type-signature string from the given Haskell type of a method, so that I could write something like

method <- findMethod "toString" :: IO (JMethod (JObject "java.math.BigDecimal") (IO JString))

Answer 1

In Haskell, types are erased, they do not exist at run time. DataKinds lets you use data constructors in types, but they are still erased. In a function of type forall n. Vec A n -> Nat, it's not possible to return n because it will be erased.

For n to not be erased, you would have a type Vec A n which depends on a run-time value n, which is what dependent types are about.

Dependent types are not a native feature of Haskell (yet). However, it is possible to emulate them using singletons. The type of length would then be forall n. SingI n => Vec A n -> Nat, where the SingI constraint provides a run-time reflection of n.

Answer 2

In Haskell, types don't exist at runtime. They are used only to classify expressions in the source code, not values at runtime.

You can certainly have data JObject (className :: Symbol) = ..., and use that to enforce that a function that only works on objects of some particular Java class is never given a JObject for a different class name. You can even make sure that code that combines two Java objects of the same class is never given JObjects of mismatched classes, even in a polymorphic context where you don't know what the actual class name is. But all of that is talking about your code. At runtime when an actual JObject exists in memory, it simply does not contain the className. There's nothing to extract.

It is however possible to make something that has the effect of giving you access to the className as if it were a value rather than a type. What you need is a function you can call, parameterised on the className Symbol that will produce a runtime String value. In Haskell, the standard way to make a function that has different behaviour for each possible value of a type parameter is to use a type class. You just need a class with a method that gives you a String value, and then an instance for every possible Symbol that implements the method by returning a corresponding String. Simple!

Fortunately GHC actually has a builtin class with magic instances for every Symbol, so nobody has to write all these instances by hand. It's called KnownSymbol. The method symbolSing @s actually gives you an SSymbol s rather than directly giving you the String, but you can get it out by calling fromSymbol.

Apart from magically having an infinite number of discrete instances, the KnownSymbol class is a perfectly ordinary class. This means that you can't automatically get a KnownSymbol instance if all you have is a type parameterised on an unknown Symbol; you will have to ensure that you use the right constraints on your functions to flow through the KnownSymbol instance from where the Symbol was actually chosen into the place where you want to know what it was.

The SSymbol type is an example of a technique known as "singletons" (not to be confused with the "singleton pattern" in OO languages). It just mean a parameterised type whose values are in one-to-one correspondence with choice of the type parameter. i.e. SSymbol s is a separate type for each choice of a Symbol s; each of those types has only a single value (hence "singletons"), so knowing which value we have reveals what its corresponding Symbol was, even though the Symbol technically doesn't exist at runtime. Using these singleton types as the link allows more options than just having a class that directly links a type and a value, even though that isn't necessarily required in simple cases. If you're interested, the singletons library is a framework for defining and working with singleton types more generally (as opposed to the very few ones provided by base because they need compiler support for the "magic instances").