Algebras for types-CodePudding

One can define a functor on kinds, using "data kind promotion"

data Product m = E| I m | P (Product m, Product m)

It maps a kind m to the sum kind Product m which has 3 types, the empty type, a type of kind m and a type of kind (Product m, Product m)

We can define an algebra at * for this functor with the type family

type family MHask (mp :: Product (*)) :: * where
  MHask E = ()
  MHask (P '(m, n)) = (MHask m, MHask n)
  MHask (I m) = m

But can we define the class of algebras for this functor ?

class MK m where
  --type To (Product m) ::  m -- type family declaration should have form "type family To a"
  type To :: Product m -> m

-- instance MonoidalK (*) where
--   -- type To = MonoidalHask -- type family ‘MonoidalHask’ should have 1 argument
--   -- type To m = MonoidalHask m -- Number of parameters must match family declaration; expected 0
--   type To = ?

CodePudding user response：

Type families have an arity, which is the number of arguments it may "pattern-match" on, and it is specified by putting those arguments to the left of :: in its declaration.

class MK m where
  type To (x :: Product m) :: m

which is practically the same as

type family To (x :: Product m) :: m