类型代数

Algebras for types

可以使用“数据种类提升”在种类上定义仿函数

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

它将一个种类m映射到总和种类Product m,它有3种类型,空类型,一个种类m和一个种类(Product m, Product m)

我们可以在 * 处为这个 family

类型的函子定义一个代数
type family MHask (mp :: Product (*)) :: * where
  MHask E = ()
  MHask (P '(m, n)) = (MHask m, MHask n)
  MHask (I m) = m

但是我们可以为这个函子定义代数的 class 吗?

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

类型族有一个元数,这是它可以“pattern-match”的参数的数量,它是通过在其声明中将这些参数放在 :: 的左侧来指定的。

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

实际上与

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