Static Guarantee on Key/Value Relationships in Data.Map

Question

I want to make a special smart constructor for Data.Map with a certain constraint on the types of key/value pair relationships. This is the constraint I tried to express:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DataKinds #-}

data Field = Speed | Name | ID
data Value = VFloat Float | VString ByteString | VInt Int

class Pair f b | f -> b where
    toPair :: f -> b -> (f, b)
    toPair = (,)

instance Pair Speed (VFloat f) 
instance Pair ID (VInt i)

for each field, there is only one type of value that it should be associated with. In my case, it does not make sense for a Speed field to map to a ByteString. A Speed field should uniquely map to a Float

But I get the following type error:

Kind mis-match
The first argument of `Pair' should have kind `*',
but `VInt' has kind `Value'
In the instance declaration for `Pair Speed (VFloat f)'

using -XKindSignatures:

class Pair (f :: Field) (b :: Value) | f -> b where
    toPair :: f -> b -> (f, b)
    toPair = (,)

Kind mis-match
Expected kind `OpenKind', but `f' has kind `Field'
In the type `f -> b -> (f, b)'
In the class declaration for `Pair'

I understand why I get the Kind mis-match, but how can I express this constraint so that it is a compile time type-checker error to use toPair on an non-matching Field and Value.

It was suggested to me by #haskell to use a GADT, but I havent been able to figure it out yet.

The goal of this is to be able to write

type Record = Map Field Value

mkRecord :: [Field] -> [Value] -> Record
mkRecord = (fromList .) . zipWith toPair

so that I can make safe Maps where the key/value invariants are respected.

So this should type-check

test1 = mkRecord [Speed, ID] [VFloat 1.0, VInt 2]

but this should be a compile time error

test2 = mkRecord [Speed] [VInt 1]

EDIT:

I'm beginning to think that my specific requirements aren't possible. Using my original example

data Foo = FooInt | FooFloat
data Bar = BarInt Int | BarFloat Float

In order to enforce the constraint on Foo and Bar, there must be some way to differentiate between a FooInt and FooFloat at the type level and similarly for Bar. Thus I instead need two GADTs

data Foo :: * -> * where
    FooInt   :: Foo Int
    FooFloat :: Foo Float

data Bar :: * -> * where
    BarInt   :: Int   -> Bar Int
    BarFloat :: Float -> Bar Float

now I can write an instance for Pair that only holds when the Foo and Bar are both tagged with the same type

instance Pair (Foo a) (Bar a)

and I have the properties I want

test1 = toPair FooInt (BarInt 1)   -- type-checks
test2 = toPair FooInt (BarFloat 1) -- no instance for Pair (Foo Int) (Bar Float)

but I lose the ability to write xs = [FooInt, FooFloat] because that would require a heterogeneous list. Furthermore if I try to make the Map synonym type FooBar = Map (Foo ?) (Bar ?) I'm stuck with a Map of either only Int types or only Float types, which isnt what I want. It's looking rather hopeless, unless theres some powerful type class wizardry I'm not aware of.

Answer 1

You could use a GADT like so,

data Bar :: * -> * where
   BarInt   :: Int -> Bar Int
   BarFloat :: Float -> Bar Float

now you have 2 distinct types of Bar available (Bar Int) and (Bar Float).You could then just split Foo into 2 types unless there is a reason not to.

data FooInt 
data FooFloat

class Pair f b c| f b -> c where
    toPair :: f -> b -> c

instance Pair FooInt (Bar Int) (FooInt,Int) where
    toPair a (BarInt b)= (a,b) 

This is sort of a clumsy example but it shows how you can specialize the type using a GADT. The idea is that they carry a "phantom type" along. It is described pretty well on this page and with DataKinds on this page.

EDIT:

If we make both Foo and Bar GADT's we can use a type or data family as described here. So, this combination allows us to set the type of Map based on the key type. Still feels like there are other possibly simpler ways to accomplish this, but it does showcase 2 great GHC extensions!

data Foo :: * -> * where
   FooInt   :: Int   -> Foo Int
   FooFloat :: Float -> Foo Float

data Bar :: * -> * where
   BarInt   :: Int   -> Bar Int
   BarFloat :: Float -> Bar Float

class Pair f b c| f b -> c where
    toPair :: f -> b -> c

instance Pair (Foo Int) (Bar Int) ((Foo Int),Int) where
   toPair a (BarInt b)= (a,b)    


type family FooMap k :: *

type instance FooMap (Foo Int) = Map (Foo Int) (Bar Int)

Answer 2

An oldschool version using Dynamic and Typeable and FunDeps. To keep it safe, you just need to not export the abstraction-breaking things like the SM constructor and the SMKey typeclass.

{-# LANGUAGE DeriveDataTypeable, MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, FlexibleInstances #-}
module Main where
import qualified Data.Map as M
import Data.Dynamic
import Data.Typeable

data SpecialMap = SM (M.Map String Dynamic)

emptySM = SM (M.empty)

class (Typeable a, Typeable b) => SMKey a b | a -> b

data Speed = Speed deriving Typeable
data Name = Name deriving Typeable
data ID = ID deriving Typeable

instance SMKey Speed Float
instance SMKey Name String
instance SMKey ID Int

insertSM :: SMKey k v => k -> v -> SpecialMap -> SpecialMap
insertSM k v (SM m) = SM (M.insert (show $ typeOf k) (toDyn v) m)

lookupSM :: SMKey k v => k -> SpecialMap -> Maybe v
lookupSM k (SM m) =  fromDynamic =<< M.lookup (show $ typeOf k) m

-- and now lists

newtype SMPair = SMPair {unSMPair :: (String, Dynamic)}
toSMPair :: SMKey k v => k -> v -> SMPair
toSMPair k v = SMPair (show $ typeOf k, toDyn v)

fromPairList :: [SMPair] -> SpecialMap
fromPairList = SM . M.fromList . map unSMPair

{-
*Main> let x = fromPairList [toSMPair Speed 1.2, toSMPair ID 34]
*Main> lookupSM Speed x
Just 1.2
-}