我已经将整个数据系列封装在一个单独的存在主义中:
data Type = Numeric | Boolean
data family Operator (t :: Type)
data instance Operator 'Numeric = Add | Sub
data instance Operator 'Boolean = And | Or
data AnyOp where
AnyOp :: Operator t -> AnyOp
现在我想在上面做一些模式匹配。
pp :: AnyOp -> String
pp op = case op of
AnyOp Add -> "+"
AnyOp Sub -> "-"
AnyOp And -> "&"
AnyOp Or -> "|"
但打字员对我大喊大叫
‘t’ is a rigid type variable bound by a pattern with constructor: AnyOp :: forall (t :: TType). Operator t -> AnyOp, in a case alternative at somesource/somefile/someposition Expected type: Operator t Actual type: Operator 'Boolean ```
为什么?怎样才是正确的方法呢?
发布于 2019-10-28 17:27:02
从远处看,数据族看起来有点像GADT,因为一个数据族的两个构造函数可以生成不同类型的结果。但是数据族与GADT不一样!他们真的更像类型的家庭。在您知道您有一个Add
或Sub
之前,实际上无法在Operator 'Numeric
上进行匹配。为什么会这样呢?你可以从操作上来想。每个构造函数都必须有一个“标记”,以便case
表达式能够区分它们。如果在不同的模块中定义了两个数据实例,那么它们很可能会对不同的构造函数使用相同的标记!此外,newtype实例甚至没有一个标记,因此根本无法区分它们!正如chi所指出的,您可以通过在存在主义中封装一个单例来跟踪您拥有的数据实例来解决这个问题。
我的理解是,如果没有数据家族的话,数据家族并没有提供太多的能量,如果没有它们,它们是无法获得的。让我们看看如何使用newtype、类型族和模式同义词来表示比您的数据家族稍微复杂一些的数据族。
import Data.Kind (Type)
data Typ = Numeric Bool | Boolean
newtype Operator t = Operator (OperatorF t)
type family OperatorF (t :: Typ) :: Type
type instance OperatorF ('Numeric b) = OpNum b
type instance OperatorF 'Boolean = OpBool
-- This makes no sense; it's just for demonstration
-- purposes.
data OpNum b where
Add' :: OpNum 'True
Sub' :: OpNum 'False
data OpBool = And' | Or'
pattern Add :: () => (b ~ 'True) => Operator ('Numeric b)
pattern Add = Operator Add'
pattern Sub :: () => (b ~ 'False) => Operator ('Numeric b)
pattern Sub = Operator Sub'
pattern And :: Operator 'Boolean
pattern And = Operator And'
pattern Or :: Operator 'Boolean
pattern Or = Operator Or'
https://stackoverflow.com/questions/58590189
复制相似问题