Is it possible to promote a value to type level?

Question

Doing this just for fun but I don't end up figuring this out.

Say I have a typeclass that unifies coordinate system on squares and hexagons:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Proxy

data Shape = Square | Hexagon

class CoordSystem (k :: Shape) where
  type Coord k

  -- all coordinates arranged in a 2D list
  -- given a side length of the shape
  allCoords :: forall p. p k -> Int -> [[Coord k]]

  -- neighborhoods of a coordinate.
  neighborsOf :: forall p. p k -> Int -> Coord k -> [Coord k]

-- omitting implementations
instance CoordSystem 'Square
instance CoordSystem 'Hexagon

Now suppose I want to use this interface with a s :: Shape that is only known at runtime. But to make use of this interface, at some point I'll need a function like this:

-- none of those two works:
-- promote :: CoordSystem k => Shape -> Proxy (k :: Shape) -- signature 1
-- promote :: Shape -> forall k. CoordSystem k => Proxy (k :: Shape)

promote s = case s of
  Square -> Proxy @'Square
  Hexagon -> Proxy @'Hexagon

However this does not work, if signature 1 is uncommented:

    • Couldn't match type ‘k’ with ‘'Square’
      ‘k’ is a rigid type variable bound by
        the type signature for:
          promote :: forall (k :: Shape). CoordSystem k => Shape -> Proxy k
        at SO.hs:28:1-55
      Expected type: Proxy k
        Actual type: Proxy 'Square

Understandably, none of 'Square, 'Hexagon, k :: Shape unifies with others, so I have no idea whether this is possible.

I also feel type erasure shouldn't be an issue here as alternatives of Shape can use to uniquely identify the instance - for such reason I feel singletons could be of use but I'm not familiar with that package to produce any working example either.

Answer 1

The usual way is to use either an existential type or its Church encoding. The encoded version is actually easier to understand at first, I think, and closer to what you already attempted. The problem with your forall k. CoordSystem k => {- ... thing mentioning k -} is that it promises to polymorph into whatever k the user likes (so long as the user likes CoordSystems!). To fix it, you can demand that the user polymorph into whatever k you like.

                              -- `a` must not mention `k`, since `k` is not
                              -- in scope in the final return type
promote :: forall a. Shape -> (forall k. CoordSystem k => Tagged k a) -> a
promote Square a = unTagged (a @Square)
promote Hexagon a = unTagged (a @Hexagon)

-- usage example
test = promote Hexagon (unproxy $ \p -> length (allCoords p 15))

Note that on the right hand side of the = sign, a has the type forall k. CoordSystem k => {- ... -} that says the user gets to choose k, but this time you're the user.

Another common option is to use an existential:

data SomeSystem where
    -- Proxy to be able to name the wrapped type when matching on a SomeSystem;
    -- in some future version of GHC we may be able to name it via pattern-matching
    -- on a type application instead, which would be better
    SomeSystem :: CoordSystem k => Proxy k -> SomeSystem

Then you would write something like

promote :: Shape -> SomeSystem
promote Square = SomeSystem (Proxy @Square)
promote Hexagon = SomeSystem (Proxy @Hexagon)

-- usage example
test = case promote Hexagon of SomeSystem p -> length (allCoords p 15)

and then the user would pattern match to extract the CoordSystem instance from it.

A final choice is singletons:

data ShapeS k where
    SquareS :: ShapeS Square
    HexagonS :: ShapeS Hexagon

Here we have made a direct connection between SquareS at the computation level and Square at the type level (resp. HexagonS and Hexagon). Then you can write:

                       -- N.B. not a rank-2 type, and in particular `a` is
                       -- now allowed to mention `k`
promote :: ShapeS k -> (CoordSystem k => a) -> a
promote SquareS a = a
promote HexagonS a = a

The singletons package offers tools for automatically deriving the singleton types that correspond to your ADTs.