问题描述
我正在使用GHC的 ConstraintKinds
扩展名.我有以下数据类型,这只是满足某些参数约束 c
的框:
I'm playing around with the ConstraintKinds
extension of GHC.I have the following data type, which is just a box for things fulfilling some one parameter constraint c
:
data Some (c :: * -> Constraint) where
Some :: forall a. c a => a -> Some c
例如,我可以构造一个带有某种数字的盒子(据说不是很有用).
For example, I could construct a box with some kind of number (arguably not very useful).
x :: Some Num
x = Some (1 :: Int)
现在,只要 c
包含约束 Show
,我就可以提供 Show(某些c)
的实例.
Now, as long as c
includes the constraint Show
, I could provide an instance of Show (Some c)
.
instance ??? => Show (Some c) where
show (Some x) = show x -- Show dictionary for type of x should be in scope here
但是我如何在实例上下文(用 ???
标记)中表达此要求?
But how do I express this requirement in the instance context (marked with ???
)?
我不能使用等式约束( c〜Show
),因为两者不一定相等. c
可以是 Num
,这意味着但不等于 Show
.
I cannot use an equality constraint (c ~ Show
), because the two are not necessarily equal. c
could be Num
, which implies, but is not equal to, Show
.
修改
我意识到这通常是不可能的.
I realised that this cannot be possible in general.
如果您有两个类型为 Some Eq
的值,则无法比较它们是否相等.它们可以是不同的类型,每个都有自己的平等概念.
If you have two values of type Some Eq
, it is not possible to compare them for equality. They could be of different types that each have their own notion of equality.
适用于 Eq
的内容适用于类型参数出现在第一个功能箭头右侧的任何类型类(例如 a >(==):: a-> a->布尔).
What applies to Eq
applies to any type class in which the type parameter appears on the right hand side of the first function arrow (like the second a
in (==) :: a -> a -> Bool
).
考虑到无法创建表示未在第一个箭头之外使用此类型变量"的约束,我认为不可能编写我要编写的实例.
Considering that there is no way to create a constraint expressing "this type variable is not used beyond the first arrow", I don't think it is possible to write the instance I want to write.
推荐答案
我们能够获得的最接近的是一个 Class1
类,该类可将一个类与单个超类约束作为一个类进行关系化..它基于 Class
约束中的a>.
The closest we are able to get is a Class1
class that reifys the relationship between a class and a single superclass constraint as a class. It's based on the Class
from constraints.
首先,我们将简短浏览一下约束包. Dict
捕获 约束
的字典a>
First, we'll take a short tour of the constraints package. A Dict
captures the dictionary for a Constraint
data Dict :: Constraint -> * where
Dict :: a => Dict a
:-
捕获一个约束带来另一个约束.如果我们有 a:-b
,则每当我们有约束 a
时,我们都可以为约束 b
生成字典.
:-
captures that one constraint entails another. If we have a :- b
, whenever we have the constraint a
we can produce the dictionary for the constraint b
.
newtype a :- b = Sub (a => Dict b)
我们需要类似于:-
的证明,我们需要知道 forall a.h a:-b a
或 h a =>字典(b a)
.
We need a proof similar to :-
, we need to know that forall a. h a :- b a
, or h a => Dict (b a)
.
实际上,仅通过单个继承就可以为 class
实现此功能,这需要语言扩展的厨房工具,包括 OverlappingInstances
.
Actually implementing this for class
es with just single inheritance requires the kitchen sink of language extensions, including OverlappingInstances
.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE OverlappingInstances #-}
import Data.Constraint
我们将定义类型为 k->的约束类别.约束
,其中约束具有单个超类.
We'll define the class of constraints of kind k -> Constraint
where the constraint has a single superclass.
class Class1 b h | h -> b where
cls1 :: h a :- b a
我们现在有能力解决示例问题.我们有一个类 A
,它需要一个 Show
实例.
We're now equipped to tackle our example problem. We have a class A
that requires a Show
instance.
class Show a => A a
instance A Int
Show
是 A
instance Class1 Show A where
cls1 = Sub Dict
我们要为 Some
data Some (c :: * -> Constraint) where
Some :: c a => a -> Some c
我们可以 Show
一个 Some Show
.
instance Show (Some Show) where
showsPrec x (Some a) = showsPrec x a
只要 h
有一个超类 b
,我们就可以显示
一个h >有些b .
We can Show
a Some h
whenever h
has a single superclass b
and we could show Some b
.
instance (Show (Some b), Class1 b h) => Show (Some h) where
showsPrec x (Some (a :: a)) =
case cls1 :: h a :- b a of
Sub Dict -> showsPrec x ((Some a) :: Some b)
这让我们写信
x :: Some A
x = Some (1 :: Int)
main = print x
这篇关于如何在约束类型的约束上施加约束?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!