Data.Map中键/值关系的静态保证

Question

我想为Data.Map创建一个特殊的智能构造函数,对键/值对关系的类型有一定的约束.这是我试图表达的约束:

{-# 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)

对于每个字段,只应该与其关联的一种类型的值.就我而言,一个Speed字段映射到一个字段是没有意义的ByteString.一个Speed字段应该唯一映射到一个Float

但是我收到以下类型错误:

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)'

使用-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'

我理解为什么我得到Kind不匹配,但是我如何表达这个约束,以便它是一个编译时类型检查器错误,用于toPair非匹配Field和Value.

#haskell向我建议使用a GADT,但我还没能弄明白.

这样做的目的是能够写作

type Record = Map Field Value

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

这样我就可以确保Map密钥/值不变量得到遵守的安全性.

所以这应该打字检查

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

但这应该是编译时错误

test2 = mkRecord [Speed] [VInt 1]

编辑:

我开始认为我的具体要求是不可能的.用我原来的例子

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

为了加强对约束Foo和Bar,必须有某种方式来区分FooInt,并FooFloat在类型级别和类似的Bar.因此,我需要两个GADT

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

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

现在我可以编写一个实例Pair,只有当Foo和Bar被标记为相同类型时才会成立

instance Pair (Foo a) (Bar a)

我有我想要的属性

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

但是我失去了写作能力,xs = [FooInt, FooFloat]因为这需要一个异构列表.此外,如果我尝试制作Map同义词,type FooBar = Map (Foo ?) (Bar ?)我会遇到Map一种只有Int类型或只有Float类型,这不是我想要的.它看起来相当无望,除非有一些我不知道的强大的类型级魔法.

Answer 1

你可以像这样使用GADT,

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

现在你有2种不同类型的Bar可用(Bar Int)和(Bar Float).你可以将Foo分成2种类型,除非有理由不这样做.

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) 

这是一个笨拙的例子,但它显示了如何使用GADT专门化类型.这个想法是他们携带一个"幽灵类型".在此页面上以及在此页面上使用DataKinds 进行了很好的描述.

编辑:

如果我们同时制作Foo和Bar GADT,我们可以使用此处描述的类型或数据族.因此,这种组合允许我们根据键类型设置Map的类型.仍然感觉还有其他可能更简单的方法来实现这一点,但它确实展示了2个很棒的GHC扩展!

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

使用 Dynamic 和 Typeable 以及 FunDeps 的老式版本。为了保证安全，您只需要不要导出破坏抽象的东西，例如SM构造函数和SMKey类型类。

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