类型代数

Question

我们可以使用“数据类型提升”来定义类型上的函子。

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

它将一类m映射为3种类型的和类Product m，即空类型、类型m和类型(Product m, Product m)。

我们可以在*上为这个带类型族的函子定义一个代数。

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

但是我们能定义这个函子的代数类吗？

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 = ?

Answer 1

类型族具有一个一致性，即它可能“模式匹配”上的参数数，它是通过将这些参数放在::声明的左边来指定的。

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

实际上这和

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