受限制的Monoid类型值组成

Question

我有一个数据类型是一个实例,Monoid所以我可以得到很好的值组成:

data R a = R String (Maybe (String ? a))

instance Monoid (R a) where
  mempty = R "" Nothing
  R s f `mappend` R t g = R (s ++ t) (case g of Just _ ? g; Nothing ? f)

接下来,我不想将所有R a值相互组合,在我的域中没有意义.所以我介绍幻像类型t:

{-# LANGUAGE DataKinds, KindSignatures #-}

data K = T1 | T2
data R (t ? K) a = R String (Maybe (String ? a))

instance Monoid (R t a) where …

所以我有"限制"的价值观:

v1 ? R T1 Int
v2 ? R T2 Int
-- v1 <> v2 => type error

和"不受限制的":

v ? R t Int
-- v <> v1 => ok
-- v <> v2 => ok

但现在我有一个问题.当涉及到v30,例如:

• 我会有大量数据类型声明(data K = T1 | … | T30).我可以通过使用类型级自然来获得幻影类型的无限来源(治愈比疾病更糟,不是吗？)
• 我应该记住在依赖代码中编写类型签名时使用哪种值的幻像类型(这真的很烦人)

是否有更简单的方法限制组成？

Answer 1

寻找 ConstrainedMonoid

我最近遇到了一个非常类似的问题，我最终解决了本文末尾描述的方法（不涉及幺半群，而是使用类型上的谓词）。然而，我接受了挑战并尝试编写一ConstrainedMonoid门课程。

想法是这样的：

class ConstrainedMonoid m where
  type Compatible m (t1 :: k) (t2 :: k) :: Constraint
  type TAppend m (t1 :: k) (t2 :: k) :: k
  type TZero m :: k

  memptyC :: m (TZero m)
  mappendC :: (Compatible m t t') => m t -> m t' -> m (TAppend m t t')

好的，这是一个简单的实例，实际上它没有添加任何新内容（我交换了Rs 类型参数）：

data K = T0 | T1 | T2 | T3 | T4
data R a (t :: K) = R String (Maybe (String -> a))

instance ConstrainedMonoid (R a) where
  type Compatible (R a) T1 T1 = ()
  type Compatible (R a) T2 T2 = ()
  type Compatible (R a) T3 T3 = ()
  type Compatible (R a) T4 T4 = ()
  type Compatible (R a) T0 y = ()
  type Compatible (R a) x T0 = ()

  type TAppend (R a) T0 y = y 
  type TAppend (R a) x T0 = x
  type TAppend (R a) T1 T1 = T1
  type TAppend (R a) T2 T2 = T2
  type TAppend (R a) T3 T3 = T3
  type TAppend (R a) T4 T4 = T4
  type TZero (R a) = T0

  memptyC = R "" Nothing
  R s f `mappendC` R t g = R (s ++ t) (g `mplus` f)

不幸的是，这需要大量冗余类型实例（OverlappingInstances似乎不适用于类型系列），但我认为它在类型级别和值级别都满足幺半群定律。

然而，它并没有关闭。它更像是一组不同的幺半群，由 索引K。如果这就是你想要的，那应该足够了。

如果你想要更多

让我们看一下不同的变体：

data B (t :: K) = B String deriving Show

instance ConstrainedMonoid B where
  type Compatible B T1 T1 = ()
  type Compatible B T2 T2 = ()
  type Compatible B T3 T3 = ()
  type Compatible B T4 T4 = ()

  type TAppend B x y = T1
  type TZero B = T3 

  memptyC = B ""
  (B x) `mappendC` (B y) = B (x ++ y)

这可能是在您的领域中有意义的情况——但是，它不再是一个幺半群了。如果您尝试制作其中之一，它将与上面的实例相同，只是具有不同的TZero. 我实际上只是在这里猜测，但我的直觉告诉我，唯一有效的幺半群实例正是像 for R a;这样的实例。仅具有不同的单位值。

否则，你最终会得到一些不一定是关联的东西（我认为可能是一个终端对象），它在组合下不是封闭的。如果您想将组合限制为等于Ks，您将丢失单位值。

更好的方法（恕我直言）

这是我实际解决问题的方法（当时我什至没有想到幺半群，因为它们无论如何都没有意义）。该解决方案本质上剥离了除Compatible“约束生成器”之外的所有内容，“约束生成器”保留为两种类型的谓词：

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 T1 = ()
type instance Matching T2 T1 = ()
type instance Matching T1 T2 = ()
type instance Matching T4 T4 = ()

像这样使用

foo :: (Matching a b) => B a -> B b -> B Int

这使您可以完全控制兼容性的定义，以及您想要什么样的组合（不一定是幺半群），而且它更通用。它也可以扩展到无限种：

-- pseudo code, but you get what I mean
type instance NatMatching m n = (IsEven m, m > n)

回答你的最后两点：

• 是的，您必须在您的同类中定义足够多的类型。但我认为无论如何它们应该是不言自明的。您还可以将它们分成组，或定义递归类型。

• 主要要提醒两个地方索引类型的含义：约束的定义，也许还有工厂方法（mkB1 :: String -> B T1）。但我认为，如果类型命名得好，这不应该是问题。（不过，这可能非常多余——我还没有找到避免这种情况的方法。也许 TH 会起作用。）

这会更容易吗？

我实际上希望能够写的是以下内容：

type family Matching (t1 :: K) (t2 :: K) :: Constraint
type instance Matching T1 y = ()
type instance Matching x T1 = ()
type instance Matching x y = (x ~ y)

我担心这是有严重的理由不允许的；然而，也许，它只是没有实施......

编辑：如今，我们有封闭式家庭，正是这样做的。