我正在尝试在类型级别构建一个列表,但在弄清楚如何强制执行约束时遇到了一些麻烦。
我的基本代码是:
data Foo z q = Foo1 (z q)
| Foo2 (z q)
class Qux q -- where ...
class Baz z -- where ...
class Bar a where -- a has kind *->*
type BCtx a q :: Constraint -- using ConstraintKinds to allow constraints on the concrete type
f :: (BCtx a q) => a q -> a q -> a q
g :: (BCtx a q, BCtx a q') => a q -> a q'
instance (Baz z) => Bar (Foo z) where
type BCtx (Foo z) q = (Num (z q), Qux q) -- for example
f (Foo1 x) (Foo1 y) = Foo1 $ x+y -- these functions need access to the type q to do arithmetic mod q
f (Foo1 x) (Foo2 y) = Foo2 $ x-y
-- ...
您可以认为上面的q
代表素数幂。我还想使用 qi 的类型列表来表示合数。我想象的是这样的:
data QList qi qs = QCons qi qs
| QNil
数据
data FList c q = FNil
| FCons (c (Head q)) (FList c (Tail q))
其中(Head q)
应对应于qi
,(Tail q)
应对应于qs
。请注意,FList
的 q
参数(不一定)不是 (Qux q)
,而是一个列表 (Qux qi)
。 (我不想进一步充实这个列表,因为这是我提出的设计问题之一)。我想在 FList
上“按模数”工作:
instance (Bar c) => Bar (FList c) where
type BCtx (FList c) q = () -- Anything I put here is not enough
f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)
-- the left call to `f` calls a concrete instance, the right call to `f` is a recursive call on the rest of the list
-- ...
在 GHC 中将这些代码片段编译在一起会导致(模转录、抽象和打字错误):
Could not deduce (BCtx c (Head q), BCtx c (Tail q))
然后
Could not deduce (BCtx c (Head (Tail q)), BCtx c (Tail (Tail q)))
等等
我知道为什么会出现此错误,但不知道如何修复它。
具体来说,我期待一个 FList c q
类型,其中 c~Foo z
和 q~QCons q1 (QCons q2 QNil)
,当然,我的列表将满足每个级别的所有 BCtx 约束。
我不确定修复这些特定错误是否会导致编译代码,但这是一个开始。整个Bar类基本是固定的(需要Constraint种类,并且Bar的实例必须有kind * -> *)。我不相信我可以使用存在类型来创建通用对象列表,因为我需要访问 qi
参数。我愿意更改 FList
和 QList
的类型,以允许我在一组 Bar 上按模进行工作。
感谢您的宝贵时间!
最佳答案
要处理类型列表,有必要区分空列表和非空列表并分别处理它们。代码中出现“无法推断”错误是因为您的实例假定一个非空列表,而实际上该列表可能为空,也可能不为空。这是使用扩展 TypeFamilies
的解决方案, TypeOperators
, DataKinds
,和GADTs
.
与 DataKinds
,类型列表是预定义的。他们有善良[*]
,但它们将在类型 *
的上下文中使用是预期的,因此需要一个运算符来转换它们:
data InjList (qs :: [*])
使用类型列表,FList
定义为
data FList c q where
FNil :: FList c (InjList '[])
FCons :: c h -> FList c (InjList t) -> FList c (InjList (h ': t))
它被定义为 GADT 来表达如何只能构造 FList
超过类型InjList q'
对于某些类型列表 q'
。例如,术语 FCons [True] FNil
类型为FList [] (InjList (Bool ': '[]))
。另一方面,由于Bool
不是 InjList q'
形式,没有 FList [] Bool
类型的项(⊥ 除外) 。通过 FList
上的模式匹配,函数可以验证它是否被赋予了非⊥参数,并进一步确定它是否被传递了一个空类型列表。
Bar
的一个实例对于 FList
s 必须分别处理 nil 列表和 cons 列表。 nil 列表有一个空的上下文。
cons 列表具有列表头部和尾部的组件。这是通过 BCtx
关联类型实例中的类型列表上的模式匹配来表达的。 。函数f
检查其参数以验证它不是 ⊥ 并确定它是否为空列表。
instance (Bar c) => Bar (FList c) where
-- Empty context for '[]
type BCtx (FList c) (InjList '[]) = ()
-- Context includes components for head and tail of list
type BCtx (FList c) (InjList (h ': t)) = (BCtx c h, BCtx (FList c) (InjList t))
f FNil FNil = FNil
f (FCons x xs) (FCons y ys) = FCons (f x y) (f xs ys)
我们可以将代码加载到 GHCi 中以验证其是否有效:
instance Bar [] where
type BCtx [] q = Num q
f xs ys = zipWith (+) xs ys
instance Show (FList c (InjList '[])) where
show FNil = "FNil"
instance (Show (c h), Show (FList c (InjList t))) => Show (FList c (InjList (h ': t))) where
show (FCons h t) = "FCons (" ++ show h ++ ") (" ++ show t ++ ")"
$ ghci
> :load Test
> f (FCons [1,2] FNil) (FCons [3,4] FNil)
FCons ([4,6]) (FNil)
关于haskell - 带有约束的类型列表,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/14250212/