gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-04 01:04:16 24 4
gpt4 key购买 nike

我想为 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 建议我使用 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

为了对 Foo 实现约束和 Bar ,必须有某种方法来区分 FooIntFooFloat在类型级别,对于 Bar 也是如此.因此我需要两个 GADT
data Foo :: * -> * where
FooInt :: Foo Int
FooFloat :: Foo Float

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

现在我可以为 Pair 编写一个实例仅当 FooBar都被标记为相同的类型
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类型,这不是我想要的。它看起来相当绝望,除非有一些我不知道的强大的类型类魔法。

最佳答案

你可以像这样使用 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 专门化类型。这个想法是他们随身携带“幻影类型”。描述得很好 on this page和 DataKinds on this page.

编辑:

如果我们同时制作 Foo 和 Bar GADT,我们可以使用类型或数据系列 as described here .因此,这种组合允许我们根据键类型设置 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)

关于haskell - Data.Map中键/值关系的静态保证,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/15126902/

24 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com