11

我有一个数据类型，它是一个实例，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）。我可以通过使用类型级别的自然来获得无限的幻像类型来解决（治愈比疾病更糟糕，不是吗？）
  • 在依赖代码中编写类型签名时，我应该记住要使用哪种幻像类型（这真的很烦人）

有没有更简单的方法来以某种方式限制构图？

4

1 回答 1

3

寻找 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)

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

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

于 2012-10-28T11:52:53.447 回答