将单一实例数据类型替换为数据系列

Question

所以在我目前的项目中，我发现自己在做一堆单例类型的类型级逻辑。

例如：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
module TypeBools where
type family (||) (a :: Bool) (b :: Bool) :: Bool where
  'False  || 'False = 'False
  'False  || 'True  = 'True
  'True   || 'False = 'True
  'True   || 'True  = 'True
data OrProof (a :: Bool) (b :: Bool) (c :: Bool) where
  OrProof :: SBool (a || b) -> OrProof a b (a || b)
data SBool (b :: Bool) where
  SFalse  :: SBool 'False
  STrue   :: SBool 'True
class Boolean b where
  sBool :: SBool b
instance Boolean 'False where
  sBool = SFalse
instance Boolean 'True where
  sBool = STrue
orProof :: (Boolean a, Boolean b) => OrProof a b (a || b)
orProof = go sBool sBool where
  go :: SBool a -> SBool b -> OrProof a b (a || b)
  go SFalse SFalse = OrProof SFalse
  go SFalse STrue = OrProof STrue
  go STrue SFalse = OrProof STrue
  go STrue STrue = OrProof STrue

这对我来说效果很好。我喜欢不必在手动单例类型，能够在必要时通过类型类召唤它们（例如上面的Boolean类），但这导致了一堆相当相似的仅为了将类型化为单一实例数据而存在的类型类。

我想也许我可以将这些多个类型类抽象为单个类型族，例如，将上面的SBool和Boolean替换为：

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
-- ...
class Singleton (t :: k) where
  data Sing t
  sing :: Sing t
instance Singleton 'False where
  data Sing 'False = SFalse
  sing = SFalse
instance Singleton 'True where
  data Sing 'True = STrue
  sing = STrue
type SBool b = Sing (b :: Bool)
type Boolean b = Singleton (b :: Bool)
sBool :: Boolean b => SBool b
sBool = sing

但随后我收到模式匹配错误：

TypeBools2.hs:42:13:
    Couldn't match type ‘b1’ with ‘'True’
      ‘b1’ is a rigid type variable bound by
           the type signature for
             go :: SBool a1 -> SBool b1 -> OrProof a1 b1 (a1 || b1)
           at TypeBools2.hs:40:9
    Expected type: SBool b1
      Actual type: Sing 'True
    Relevant bindings include
      go :: SBool a1 -> SBool b1 -> OrProof a1 b1 (a1 || b1)
        (bound at TypeBools2.hs:41:3)
    In the pattern: STrue
    In an equation for ‘go’: go SFalse STrue = OrProof STrue
    In an equation for ‘orProof’:
        orProof
          = go sBool sBool
          where
              go :: SBool a -> SBool b -> OrProof a b (a || b)
              go SFalse SFalse = OrProof SFalse
              go SFalse STrue = OrProof STrue
              go STrue SFalse = OrProof STrue
              go STrue STrue = OrProof STrue

我不确定我是否还有什么可以说服编译器的那个b1应该有善良的Bool，或者如果我只是在这里吠错了树。

Answer 1

您请求的功能以及更多内容可以在singletons中找到。很长一段时间以来，它一直是类型级编程的权威模板。您应该使用它或复制实现。无论如何，我将在这里简要展示一个简化的singletons解决方案。

模式匹配不起作用，因为STrue和SFalse位于不同的数据定义中，而这些定义一开始就不是 GADT。模式匹配仅在正确的 GADT-s 上完成时优化类型。我们需要按种类调度，以便能够将某种类型的所有单例构造函数组合在一起。

我们可以使用适当的类或顶级数据族来执行此操作。后者对于我们现在的目的来说更简单，所以让我们这样做：

data family Sing (x :: k)
data instance Sing (b :: Bool) where
  STrue :: Sing True
  SFalse :: Sing False

有了sing我们不需要 kind dispatch，因为我们只使用它来获取特定的提升值，所以以下工作：

class SingI (x :: k) where
   sing :: Sing x
instance SingI True  where sing = STrue
instance SingI False where sing = SFalse

至于orProof，我们想要的是类型级(||)的单例，这在以下类型中是最直接的实现Sing b1-> Sing b2 -> Sing (b1 || b2)：我们将按照象形文字singletons命名惯例将其命名为(%:||)。

type family (:||) (b1 :: Bool) (b2 :: Bool) :: Bool where
  True  :|| b = True
  False :|| b = b
(%:||) :: Sing b1 -> Sing b2 -> Sing (b1 :|| b2)
(%:||) STrue  b2 = STrue
(%:||) SFalse b2 = b2

OrProof不是很有用，因为它只是一个专门的相等类型以及一个SingI约束或普通Sing c：

type OrProof a b c = SingI c => c :~: (a :|| b)
type OrProof' a b c = (Sing c, c :~: (a :|| b))