Reflecting Heterogeneous Promoted Types back to Values, Compositionally

Question

I've been playing with -XDataKinds recently, and would like to take a promoted structure build with type families and pull it back down to the value level. I believe this is possible because the compositional components are very simple, and the terminal expressions are just as straight forward.

Background

I would like to demote / reflect simple rose trees of Strings, which become types of kind Tree Symbol (when using GHC.TypeLits.Symbol as a type-level string). Here is my boilerplate code:

{-# LANGUAGE DataKinds #-}

import GHC.TypeLits
import Data.Proxy

data Tree a = Node a [Tree a]

type TestInput = '[ 'Node "foo" '[ 'Node "bar" '[]
                                 , 'Node "baz" '[]
                                 ]
                  , 'Node "bar" '[]
                  ]

It's a simple type-level rose forest that looks like this very detailed diagram:

 *-- "foo" -- "bar"
 |         \_ "baz"
  \_ "bar"

Attempted Solution

Ideally, I would like to traverse this structure and give a 1-to-1 mapping back to values of kind *, but it's not very obvious how to do this heterogeneously while still carrying-over the (necessary) instances due to overloading.

vanila on #haskell suggested I use type classes to bind the two worlds, but it seems a bit trickier than I thought. My first attempt tried to encode the contents of a type-level pattern match via an instance head constraint, but my associated type (to encode the *-kinded type result of the mapping) overlapped - apparently instance heads are somewhat ignored by GHC.

Ideally, I would also like the reflection of lists and trees to be generic, which seems to be causing problems - it's like using type classes to organize the type/kind strata.

Here is a non-functional example of what I would like:

class Reflect (a :: k) where
  type Result :: *
  reflect :: Proxy a -> Result

class ReflectEmpty (empty :: [k]) where
  reflectEmpty :: forall q. Proxy empty -> [q]
  reflectEmpty _ = []

instance ReflectEmpty '[] where

instance ReflectEmpty a => Reflect a where
  type Result = forall q. [q]
  reflect = reflectEmpty

-- | The superclass constraint is where we get compositional
class Reflect (x :: k) => ReflectCons (cons :: [x]) where
  reflectCons :: PostReflection x ~ c => Proxy cons -> [c]

instance ( Reflect x
         , ReflectCons xs ) => ReflectCons (x ': xs) where
  reflectCons _ = reflect (Proxy :: Proxy x) :
    reflectCons (Proxy :: Proxy xs)

instance ( Reflect x
         , ReflectEmpty e ) => ReflectCons (x ': e) where
  reflectCons _ = reflect (Proxy :: Proxy x) :
    reflectEmpty (Proxy :: Proxy e)

...

There are a couple of thing generally wrong about this code. Here is what I see:

• I need some form of look-ahead to know the result of a higher-kinded reflection for generic type-level list reflection - PostReflection type function
• I'm needing to create and destroy Proxy's on the fly. I'm not sure if this won't compile currently, but I don't feel confident that the types will unify as I expect them to.

But, this typeclass heirarchy feels like the only way to capture a heterogeneous grammar, so this may still be a start. Any help with this would be tremendous!

Heartfelt

I only understand a tiny bit of this, but what is the point of the ReflectEmpty class? – Cental

By "reflect generically" do you mean you want to lower any promoted type to whatever type it came from? This will be impossible, because the compiler sees no relation between Node and 'Node - likewise for all promoted types. They simply share the same name. But for any concrete objects, say Proxy [Symbol] -> [String] or even Reflect a a' => Proxy [a] -> [a'] is probably doable. – Miscarry

@Cental Honestly just completeness, I feel like there is a common pattern here that could be captured. I think you're right though - it could be eliminated. This feels like the analogue of simple pattern-matching on a normal AST grammar algebraic data type for homogeneous languages / tree-like structures, except... like across the universe instead of just a data type. The type-classes almost simulate manual pattern-matching for heterogeneous types, and the inheritance (in theory) allows for the reduction of the type (all in the one type-class Reflect) – Heartfelt

Do you have a (functional) equivalent of this in Idris, Agda or another dep. typed language? – Heuer

@ErikAllik You wouldn't need a type-level tree in the first place! Because you could always make predicates that are bound to the value level. As a container, the rose tree should be polymorphic enough to take any type. – Heartfelt

I simply wanted a comparison of how simple this would be on a deptyped language, that's all :) thought you might have something. – Heuer

Answer 1

The lazy solution

Install the singletons package:

{-# LANGUAGE
  TemplateHaskell, DataKinds, PolyKinds, TypeFamilies,
  ScopedTypeVariables, FlexibleInstances, UndecidableInstances, GADTs #-}

import GHC.TypeLits
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Proxy

$(singletons [d|
  data Tree a = Node a [Tree a] deriving (Eq, Show)
  |])

reflect ::
  forall (a :: k).
  (SingI a, SingKind ('KProxy :: KProxy k)) =>
  Proxy a -> Demote a
reflect _ = fromSing (sing :: Sing a)

-- reflect (Proxy :: Proxy (Node "foo" '[])) == Node "foo" []

And we're done.

Unfortunately, the library is sparsely documented and quite complex too. I advise looking at the project homepage for some additional documentation. I try to explain the basics below.

Sing is the data family that defines the singleton representations. Singletons are structurally the same as the unlifted types, but their values are indexed by the corresponding lifted values. For example, the singleton of data Nat = Z | S Nat would be

data instance Sing (n :: Nat) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)

singletons is the template function that generates the singletons (and it also lifts the derived instances, and can lift functions as well).

SingKind is essentially a kind class which provides us the Demote type and fromSing. Demote gives us the corresponding unlifted type for a lifted value. For example, Demote False is Bool, while Demote "foo" is Symbol. fromSing converts a singleton value to the corresponding unlifted value. So fromSing SZ equals Z.

SingI is a class which reflects the lifted values into singleton values. sing is its method, and sing :: Sing x gives us the singleton value of x. This is almost what we want; to complete the definition of reflect we only need to use fromSing on sing to get the unlifted value.

KProxy is an export of Data.Proxy. It allows us to capture kind variables from the environment and use them inside definitions. Note that any promotable data type of kind (* -> *) can be used in place of KProxy. For details of datatype promotion see this.

Note though that there is a weaker form of dispatching on kinds, which doesn't require KProxy:

type family Demote (a :: k)
type instance Demote (s :: Symbol) = String
type instance Demote (b :: Bool)   = Bool

So far so good, but how do we write the instance for lifted lists?

type instance Demote (xs :: [a]) = [Demote ???] 

Demote a is not allowed, of course, because a is a kind, not a type. So we need KProxy in order to be able to make use of a in the right hand side.

The do-it-yourself solution

This proceeds similarly to the singletons solution, but we deliberately skip the singleton representations and go directly for reflection. This should be somewhat more performant, and we might even learn a bit in the process (I certainly did!).

import GHC.TypeLits
import Data.Proxy

data Tree a = Node a [Tree a] deriving (Eq, Show)

We implement the kind dispatch as an open type family, and provide a type synonym for convenience:

type family Demote' (kparam :: KProxy k) :: *  
type Demote (a :: k) = Demote' ('KProxy :: KProxy k)  

The general pattern is that we use 'KProxy :: KProxy k whenever we want to mention a kind k.

type instance Demote' ('KProxy :: KProxy Symbol) = String
type instance Demote' ('KProxy :: KProxy (Tree a)) = Tree (Demote' ('KProxy :: KProxy a))
type instance Demote' ('KProxy :: KProxy [a]) = [Demote' ('KProxy :: KProxy a)]

Doing the reflection is pretty straightforward now:

class Reflect (a :: k) where
  reflect :: Proxy (a :: k) -> Demote a

instance KnownSymbol s => Reflect (s :: Symbol) where
  reflect = symbolVal

instance Reflect ('[] :: [k]) where
  reflect _ = []

instance (Reflect x, Reflect xs) => Reflect (x ': xs) where
  reflect _ = reflect (Proxy :: Proxy x) : reflect (Proxy :: Proxy xs)

instance (Reflect n, Reflect ns) => Reflect (Node n ns) where
  reflect _ = Node (reflect (Proxy :: Proxy n)) (reflect (Proxy :: Proxy ns))

Thora

I don't think KProxy is treated specially. Your code works the same (for me) when I defined my own KProxy. – Miscarry

The special treatment is somehow bound to the name KProxy. Try to rename it to FooProxy or something else, and it won't work. – Glass

@AndrásKovács, youch! That sounds like a bug to me. GHC has no business caring about what names things have. – Cental

@dfeuer: RebindableSyntax is already about looking at specific names, so I don't think this one sticks out in comparison. – Glass

I changed the name to other things and it still worked. Anything of the form data A (a :: *) = B seems to work. Even data KP (a :: *) = KP_ Bool worked! What version of GHC are you using? I would be very surprised if a name that isn't defined in one of the "core" modules is given special treatment. – Miscarry

@Miscarry you're right! I mixed up my renaming of the proxies, therefore getting an error that I shouldn't have got. Will edit answer. – Glass

@AndrásKovács Do you ever run into issues where the singleton's implementation of Demote won't automatically reduce? It's strange, I can witness the reflected values, but they type of the values is still encoded as Demote <crazy type-level-tree>. Is this because the kinds (and also types) overlap? Your answer is a diamond in the rough, by the way :) – Heartfelt

@AthanClark where do you get those types? If you use :kind! Type in ghci, you get the normal form of the type along with the kind. With :t you get unreduced types. – Glass

@AndrásKovács Wow!! That's so crazy!! But in a GHC script, how would one force the reduction so that it is associated with a value-level term? Maybe a poly-kinded coerce? – Heartfelt

Actually, if you just assume the structure is what it should reduce to, and operate on the data with head or something like that, the reduction happens. @AndrásKovács needs a promotion – Heartfelt

Yep, it's always the normal forms of types that get checked, so don't worry about reduction. – Glass