嵌套的多参数类

Question

我试图在Haskell:中定义一个新的数据类型，其中包含一个具有多个参数的数据类型(幻影类型(

newtype Dd x y z = ToDd Cudd.Cudd.DdNode deriving (Eq,Show)
data KnowStruct a b c =
KnS Cudd.Cudd.DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
deriving (Eq,Show)

但这给了我错误信息：

• Expected kind ‘k0 -> k1 -> *’, but ‘Dd a’ has kind ‘*’
• In the type ‘(Dd a b c)’

为什么会出现这种情况？

是否也可以在不使用所包含的Dd类型的上下文/参数规范的任何要求的情况下定义KnowStruct？例如：

data KnowStruct =
KnS Cudd.Cudd.DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
deriving (Eq,Show)

我制作了一个函数类来处理Dd的所有变体，并且只在作用于KnowStructs的函数中使用这些变体-所以理论上没有必要指定KnowStruct包含什么类型的Dd。。

Answer 1

第一个对我有效，试着给他们显式的种类签名

{-# Language DerivingStrategies       #-}
{-# Language PolyKinds                #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
data DdManager = DdManager deriving stock (Eq, Show)
data DdNode    = DdNode    deriving stock (Eq, Show)
data Agent     = Agent     deriving stock (Eq, Show)
data Prp       = Prp       deriving stock (Eq, Show)
type    Dd :: k -> j -> i -> Type
newtype Dd x y z = ToDd DdNode
deriving stock (Eq, Show)
type KnowStruct :: k -> j -> i -> Type
data KnowStruct a b c =
KnS DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
deriving stock (Eq, Show)

是否也可以定义KnowStruct，而不使用所包含的Dd类型的上下文/参数规范的任何要求？

这是可能的，并且被称为存在量化，因为类型变量不会出现在返回类型中。

由于存在量化，推导Show需要独立推导，而Eq不容易推导。由于当比较两个KnowStruct时，a、b、c是存在量化的，因此将Dd a1 b1 c1和Dd a2 b2 c2与完全不同的类型变量进行比较。

{-# Language ExistentialQuantification #-}
{-# Language StandaloneDeriving        #-}
import Data.Kind
data DdManager = DdManager deriving stock (Eq, Show)
data DdNode    = DdNode    deriving stock (Eq, Show)
data Agent     = Agent     deriving stock (Eq, Show)
data Prp       = Prp       deriving stock (Eq, Show)
-- I specialize this to some kind (`Type'). Otherwise the
-- kind would have to be an argument to `KnowStruct` below.
type    Dd :: Type -> Type -> Type -> Type
newtype Dd x y z = ToDd DdNode
deriving stock (Eq, Show)
type KnowStruct :: Type
data KnowStruct = forall a b c.
KnS DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
deriving stock
instance Show KnowStruct

我更喜欢(等效的(GADT语法

{-# Language GADTs #-}
type KnowStruct :: Type
data KnowStruct where
KnS :: DdManager -> [Prp] -> Dd a b c -> [(Agent,[Prp])] -> KnownStruct