12

我想为 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在尊重键/值不变量的地方制作安全的 s。

所以这应该类型检查

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

但这应该是编译时错误

test2 = mkRecord [Speed] [VInt 1]

编辑：

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

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

为了在Fooand上强制执行约束，必须有某种方法在类型级别Bar区分 a FooIntand并且类似地 for 。因此我需要两个 GADTFooFloatBar

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类型，这不是我想要的。它看起来相当绝望，除非有一些我不知道的强大的类型类魔法。

4

4 回答 4

5

你可以像这样使用 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)
于 2013-02-28T05:08:19.560 回答
4

使用 Dynamic and 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
-}
于 2013-03-07T16:28:47.687 回答
2

当我第一次阅读这篇文章时，我试图解决在所需情况下强制编译错误的问题，但似乎有些不对劲。然后我尝试了一种具有多张地图和提升功能的方法，但仍有一些事情困扰着我。然而，当我意识到你实际上要做的是创建某种形式的可扩展记录时，它让我想起了几个月前我意识到的一个非常酷的包：Vinyl 包（可在 Hackage 上获得）。这可能是也可能不是您所追求的效果，它确实需要 GHC 7.6，但这里有一个改编自自述文件的示例：

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

import Data.Vinyl

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

现在可以创建包含任意数量的这些字段的记录：

test1 = speed =: 0.2

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

它们属于不同的类型，因此尝试在给定函数中传递错误数量的信息将导致编译错误。类型同义词可以使其更易于使用，但不需要类型注释。

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

该库在不需要模板 Haskell 的情况下为这些类型提供自动镜头，并提供允许轻松处理子类型的铸造功能。例如：

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

（需要额外的勾号才能获得适合单个字段记录的种类）。

这不允许mkRecord您使用确切的类型，但它似乎确实满足了对可扩展记录进行静态检查的要求。如果这对您不起作用，您仍然可以使用 Vinyl 源中的巧妙类型技术来到达您想去的地方。

于 2013-03-03T13:57:10.210 回答
-1

我会用一些 getter 和 setter 创建一个不透明的数据类型。

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 }
于 2013-03-07T19:20:00.897 回答