How to bring a data kind to the value level?

Question

I have something like this in my code:

data SomeKind = Kind1 | Kind2 deriving Eq

data SomeValue (t :: SomeKind) = SomeValue

someValue1 :: SomeValue Kind1
someValue1 = SomeValue

someValue2 :: SomeValue Kind2
someValue2 = SomeValue

I want to get the kind that's in the type level to the value level, perhaps something like:

valueKind :: SomeValue a -> SomeKind

that will:

valueKind someValue1 == Kind1
valueKind someValue2 == Kind2

Is it possible?

Answer 1

valueKind :: SomeValue a -> SomeKind is not possible. The a type parameter isn't present runtime in any shape or form, so we can't branch on it.

The standard method for making use of types both at runtime and compile time is to make so-called singleton types. Singletons are indexed by the type-level version of the original type, and have the property that we can reveal the index by pattern matching on them:

data SSomeKind (i :: SomeKind) where
  SKind1 :: SSomeKind Kind1
  SKind2 :: SSomeKind Kind2

They're called singletons because for each type index there is only a single value. Similarly, for each value there is only a single choice of type index. This correspondence lets us use SSomeKind as a runtime representation of SomeKind.

valueKind' :: SSomeKind a -> SomeKind
valueKind' SKind1 = Kind1
valueKind' SKind2 = Kind2

Creating singleton definitions and associated lifting and lowering functions is a rather mechanical job. The singletons library automates and streamlines it. In our case:

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

import Data.Singletons.TH

$(singletons [d| data SomeKind = Kind1 | Kind2  |])
-- generates a lot of stuff, including the SSomeKind definition.

-- works the same as our previously defined function
valueKind' :: SSomeKind a -> SomeKind
valueKind' = fromSing

-- we can also polymorphically get specific singleton values:
foo :: Sing Kind1
foo = sing -- now foo equals SKind1

There's a lot more in the library. See this page for a quick start and further references.

Answer 2

If you can tolerate a type class constraint, this can be accomplished with instances for each of the kinds in SomeKind. This is very similar to the Kindable typeclass

class SomeKindable (k :: SomeKind) where
    someKindOf :: p k -> SomeKind

instance SomeKindable Kind1 where
    someKindOf _ = Kind1

instance SomeKindable Kind2 where
    someKindOf _ = Kind2

valueKind ::  SomeKindable a => SomeValue a -> SomeKind
valueKind = someKindOf

The compiler can't tell that for all k :: SomeKind there is a SomeKindable k instance. If you need this to be available for every SomeValue without being able to show SomeKindable you can package up the value along with a SomeKindable dictionary in a GADT.

{-# LANGUAGE GADTs #-}

data SomeValue (t :: SomeKind) where
    SomeValue :: SomeKindable t => SomeValue t

valueKind :: SomeValue a -> SomeKind
valueKind (p@SomeValue) = someKindOf p