haskell - 受限 Monoid 类型值组合

Question

我有一个数据类型是 Monoid 的实例所以我可以得到很好的值(value)观组合:

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彼此值(value)观，这在我的领域没有意义。所以我介绍幻象类型 t :

{-# LANGUAGE DataKinds, KindSignatures #-}

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

instance Monoid (R t a) where …

所以我有“限制”的值(value)观:

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)。

这是想法:

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')

好的，有一个简单的实例，它实际上并没有添加任何新内容(我交换了 R 的类型参数):

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 .我实际上只是在这里推测，但我的直觉告诉我，唯一有效的幺半群实例正是 R a 的实例。 ;仅具有不同的单位值。

否则，您最终会得到一些不一定具有关联性的东西(我认为可能还有一个终端对象)，它在合成下不会关闭。如果你想限制组成等于 K s，你会失去单位值(value)。

更好的方法(恕我直言)

以下是我实际解决问题的方法(当时我什至没有想到幺半群，因为它们无论如何都没有意义)。该解决方案基本上剥离了除 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)

我担心这有严重的理由不被允许；但是，也许，它只是没有实现......

编辑:如今，我们有 closed type families , 正是这样做的。