How to compile heterogeneous hash map like object using type level keys in Haskell?

Question

I want to use something like "heterogeneous hash map using type level keys". After struggling, I wrote a code bellow (though in fact, it is just a list like structure rather than hash map), but it does not be successfully complied.

The error message is as follows.

• Couldn't match expected type ‘ValueType
                                  (Proxy k') (NamedVal v k :. b)’
              with actual type ‘ValueType (Proxy k') b’
  NB: ‘ValueType’ is a type function, and may not be injective
• In the expression: get (Proxy :: Proxy k') b

It seems type family declaration is not understood by compiler as I meant. How do I compile this code?

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE IncoherentInstances #-}

module TypeLevelKV where

{- | The goal of this module is to get the value with a type level key.

>>> get (Proxy :: Proxy "foo") sampleList
"str"

>>> get (Proxy :: Proxy "bar") sampleList
34
-}

import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable)
import GHC.TypeLits (KnownSymbol, symbolVal)

sampleList =
  (namedVal "str"   :: NamedVal String "foo") :.
  (namedVal 34      :: NamedVal Int "bar") :.
  (namedVal True    :: NamedVal Bool "baz") :. Null

{- | A value with type level index.
 -}
type NamedVal v key = (Proxy key, v)

{- | Type level list cons
 -}
data a :. b = a :. b
    deriving (Typeable, Eq, Show)
infixr 8 :.

{- | Type level @[]@
 -}
data Null = Null
    deriving (Typeable, Eq, Show)

type family ValueType pkey list where
  ValueType (Proxy k) (NamedVal v k :. b) = v
  ValueType (Proxy k') (NamedVal v k :. b) = ValueType (Proxy k') b
  ValueType (Proxy k) Null = Null

class HasKey pkey list where
  get :: pkey -> list -> (ValueType pkey list)

instance (KnownSymbol k) =>
  HasKey (Proxy k) (NamedVal v k :. b) where
  get _ ((_, a) :. _) = a

instance (KnownSymbol k, KnownSymbol k', HasKey (Proxy k') b) =>
  HasKey (Proxy k') (NamedVal v k :. b) where
  get _ (_ :. b) = get (Proxy :: Proxy k') b

instance (KnownSymbol k) =>
  HasKey (Proxy k) Null where
  get _ Null = Null

namedVal :: forall k v
         . (KnownSymbol k)
         => v -> NamedVal v k
namedVal a = (Proxy, a)

Followings are reply for the @Benjamin Hodgson 's comment

One of the reason I need this is that I want to use it with template haskell as follows and ensure that all the variables required by sampleQ is same type as needed.

withDict :: [String] -> Q Exp -> Q Exp
withDict keys q = undefined
-- e.g., `withDict (Proxy :: Proxy MyType) sampleQ` generates
-- \(dict :: MyType) ->
--   let
--     foo = get (Proxy :: Proxy "foo") dict
--     bar = get (Proxy :: Proxy "bar") dict
--     baz = get (Proxy :: Proxy "baz") dict
--     defaultValue = "If no \"defaultValue\" key exists, this default value is provided to sampleQ"
--   in
--     $(sampleQ)

type MyType =
  NamedVal String "foo" :.
  NamedVal Int "bar" :.
  NamedVal Bool "baz" :. Null

After defining this, we can inject any values with variable name into a Q Exp such as Shakespearen template.

renderWith :: IO ()
renderWith = do
  foo <- getLine
  bar <- readLn
  baz <- readLn
  let
    sampleList :: MyType
    sampleList =
      (namedVal foo   :: NamedVal String "foo") :.
      (namedVal bar   :: NamedVal Int "bar") :.
      (namedVal baz   :: NamedVal Bool "baz") :. Null
  putStrLn $ $(withDict (Proxy :: Proxy MyType) renderSomeFile) sampleList

Answer 1

I've found that following code works well and released type-level-kv-list module using this.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE IncoherentInstances #-}

module Type where

import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable)
import GHC.TypeLits (KnownSymbol, symbolVal)

{- | A value with type level index.
 -}
type NamedVal v key = (Proxy key, v)

{- | Type level list cons
 -}
data a :. b = a :. b
    deriving (Typeable, Eq, Show)
infixr 8 :.

{- | Type level @[]@
 -}
data Null = Null
    deriving (Typeable, Eq, Show)

type family Lookup pkey list where
  Lookup pk ((pk, v) :. b) = v
  Lookup pk ((px, v) :. b) = Lookup pk b
  Lookup pk Null = Null

class HasKey list pkey value where
  get' :: pkey -> list -> value

instance (KnownSymbol k) =>
  HasKey (NamedVal v k :. b) (Proxy k) v where
  get' :: forall b0 k0 v0
      .  (KnownSymbol k0)
      => Proxy k0 -> NamedVal v0 k0 :. b0 -> v0
  get' _ ((_, a) :. _) = a

instance (NamedList b, KnownSymbol k, HasKey b (Proxy k) v) =>
  HasKey (a :. b) (Proxy k) v where
  get' _ (_ :. b) = get' (Proxy :: Proxy k) b

instance (KnownSymbol k, v ~ Null) =>
  HasKey Null (Proxy k) v where
  get' _ Null = Null

get :: (HasKey list pkey (Lookup pkey list))
    => pkey -> list -> Lookup pkey list
get (pkey :: pkey) (list :: list) =
  get' pkey list :: Lookup pkey list