限制含半幺群类型值组成

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

好了，还有的小例子，这实际上不添加任何新的东西（我换R S型参数）：

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似乎不适用于类型族），但我认为它在类型级别和值级别上满足幺半群法则。

但是，它并没有关闭。它更像是一组不同的monoid，索引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，你将失去单位价值。

一个更好的办法（恕我直言）

以下是我真正解决我的问题（我根本就没想到类群的当年，因为他们没有任何意义，无论如何）。该解决方案主要剥掉以外的所有Compatible“约束制片人”，这是留给作谓语两类：使用像

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

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 =() 

这使您完全控制您的兼容性的定义，以及你想要什么类型的作品（不一定是monoidal），而且更一般。它可以扩展到无限种，太：

-- 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，正是这样做。