I am trying to define a new data type containing a data type with multiple parameters (phantom types) in 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)
But this gives me the error message:
• Expected kind ‘k0 -> k1 -> *’, but ‘Dd a’ has kind ‘*’
• In the type ‘(Dd a b c)’
Why is this the case?
Is it also possible to define KnowStruct without using any requirement of context / parameter specification for the contained Dd type? e.g. :
data KnowStruct =
KnS Cudd.Cudd.DdManager [Prp] (Dd a b c) [(Agent,[Prp])]
deriving (Eq,Show)
I made a function class dealing with all variations of Dds, and only use these in the functions acting on KnowStructs - so in theory there is no need to specify what kind of Dd the KnowStruct contains..
CodePudding user response:
The first one works for me, try giving them explicit kind signatures
{-# 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)
Is it also possible to define
KnowStruct
without using any requirement of context / parameter specification for the contained Dd type?
This is possible, and is called existential quantification because the type variables don't appear in the return type.
Deriving Show
requires standalone deriving because of the existential quantification and Eq
can't be easily derived. Since a
, b
, c
are existentially quantified when you are comparing two KnowStruct
s you are comparing Dd a1 b1 c1
and Dd a2 b2 c2
with completely different type variables.
{-# 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
I prefer the (equivalent) GADT syntax
{-# Language GADTs #-}
type KnowStruct :: Type
data KnowStruct where
KnS :: DdManager -> [Prp] -> Dd a b c -> [(Agent,[Prp])] -> KnownStruct