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

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
-}

Answer 2

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 3

When I first read this I attempted to solve the problem of forcing compile errors in the required cases, but something seemed wrong. I then tried an approach with multiple maps and a lifting function, but something was still nagging me. However, when I realised that essentially what you are trying to do is create some form of extensible record, it reminded me of a very cool package I had become aware of a few months ago: the Vinyl package (available on Hackage). This may or may not be exactly the effects you were after, and it does require GHC 7.6, but here is an example adapted from the readme:

{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE FlexibleContexts, NoMonomorphismRestriction #-}

import Data.Vinyl

speed = Field :: "speed" ::: Float
name  = Field :: "name"  ::: String
iD    = Field :: "id"    ::: Int

Now a record can be made containing any number of these fields:

test1 = speed =: 0.2

test2 = speed =: 0.2 
    <+> name  =: "Ted"
    <+> iD    =: 1

These are of different types, so an attempt to pass the wrong amount of information in a given function will cause a compile error. A type synonym can make this easier to use, but type annotations are not required.

type Entity = Rec ["speed" ::: Float, "name" ::: String, "id" ::: Int]
test2 :: Entity

The library provides automatic lenses on these types without the need for Template Haskell, and a casting function that allows for subtypes to be handled with ease. For example:

test2Casted :: Rec '["speed" ::: Float]
test2Casted = cast test2

(The extra tick is required to get the kind right for the single field record).

This doesn't allow the exact type for mkRecord you were after, but it does seem to capture the requirements of static checking of extensible records. If this doesn't work for you, you might nevertheless be able to use of the clever type techniques found in the Vinyl source to get where you want to go.

Answer 4

I would make an opaque datatype with some getters and setters.

module Rec (Rec, getSpeed, getName, getID, setSpeed, setName, setID, blank) where

data Rec = R { speed :: Maybe Double; name :: Maybe String; id :: Maybe Int }

getSpeed :: Rec -> Maybe Double
getSpeed = speed

setSpeed :: Double -> Rec -> Rec
setSpeed s r = r { speed = s }

blank = R { speed = Nothing, name = Nothing, id = Nothing }