Retrieving information from DataKinds constrained existential types

If I have a type constrained by a finite DataKind

{-# LANGUAGE DataKinds #-}

data K = A | B

data Ty (a :: K) = Ty { ... }

and an existential type which forgets the exact choice of K in the type... but remembers it in a passed dictionary.

class AK (t :: K) where k :: Ty t -> K
instance AK A where k _ = A
instance AK B where k _ = B

data ATy where ATy :: AK a => Ty a -> ATy

it's genuinely the case that ATy <-> Either (Ty A) (Ty B), but if I want to write one of those witnesses I need to use unsafeCoerce

getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy it) = case k it of
  A -> Left  (unsafeCoerce it)
  B -> Right (unsafeCoerce it)

So generally this works—I can forget the choice of K using ATy and remember it partially using getATy. Altogether this takes advantage of as much type information as I have available.

However, this type information feels as though it ought to be "obvious" if done correctly.

Is there a way to achieve the above without the use of unsafeCoerce? Is there a way to get rid of that AK constraint in the existential? Can this technique be performed based entirely off the information constraints provided by the data kind?

If you want to do runtime case analysis on the existential type, you need a singleton representation too:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables #-}

data K = A | B

-- runtime version of K. 
data SK (k :: K) where
    SA :: SK A
    SB :: SK B

-- ScopedTypeVariables makes it easy to specify which "k" we want. 
class AK (k :: K) where
    k :: SK k 

instance AK A where k = SA
instance AK B where k = SB

data Ty (a :: K) = Ty

data ATy where
    ATy :: AK k => Ty k -> ATy

getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy (ty :: Ty k)) = case (k :: SK k) of
    SA -> Left ty
    SB -> Right ty

The singletons package can be used here to do away with the boilerplate:

{-# LANGUAGE DataKinds, GADTs, TypeFamilies, TemplateHaskell, ScopedTypeVariables #-}

import Data.Singletons.TH

$(singletons [d| data K = A | B |])

data Ty (a :: K) = Ty

data ATy where
    ATy :: SingI k => Ty k -> ATy

getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy (ty :: Ty k)) = case (sing :: Sing k) of
    SA -> Left ty
    SB -> Right ty

As to your last question:

Is there a way to get rid of that AK constraint in the existential? Can this technique be performed based entirely off the information constraints provided by the data kind?

As long as we have a data kind only as a type parameter, the information doesn't exist runtime, and we can't do any analysis on it. For example, take this type:

data ATy where
    ATy :: Ty k -> ATy

we can never instantiate the k in Ty k; it must remain polymorphic.

There are multiple ways to provide runtime type information; implicitly passed dictionaries is one option, as we've seen:

data ATy where
   ATy :: AK k => Ty k -> ATy

Here AK k is just a pointer to an SK (since the AK class only has a single method, we don't have a dictionary for the class, just a plain pointer to the method), an extra field in the constructor. We could also choose to make that field explicit:

data ATy where
    ATy :: SK k -> Ty k -> ATy

and the runtime representation would be pretty much the same.

A third option would be using GADT constructors to encode the types:

data ATy where
    ATyA :: Ty A -> ATy
    ATyB :: Ty B -> ATy

This solution is pretty nice performance wise, since there is no space overhead, as the constructors already encode the types. It's like an Either with hidden type parameters.

Recommended topics

Hot tags