数据种类联盟

Question

我不确定这是否是正确的术语，但是否可以声明接受数据类型“联合”的函数类型？

例如，我知道我可以做到以下几点：

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}

...

data Shape'
  = Circle'
  | Square'
  | Triangle'

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape Circle'
  Square :: { side :: Int} -> Shape Square'
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape Triangle'

test1 :: Shape Circle' -> Int
test1 = undefined

但是，如果我想采用圆形或方形的形状怎么办？如果我还想为一个单独的函数采用所有形状怎么办？

有没有办法让我定义一组Shape' 来使用，或者让我允许每个数据有多个数据类型定义？

编辑：

工会的使用似乎不起作用：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE GADTs           #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE PolyKinds       #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE TypeOperators   #-}

...

type family Union (a :: [k]) (r :: k) :: Constraint where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

data Shape'
  = Circle'
  | Square'
  | Triangle'

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape Circle'
  Square :: { side :: Int} -> Shape Square'
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape Triangle'

test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 Circle {} = undefined
test1 Triangle {} = undefined
test1 Square {} = undefined

上面部分编译

Answer 1

您可以（我认为）使用类型族以及ConstraintKinds 和PolyKinds 以相当干净的方式完成类似的事情：

type family Union (a :: [k]) (r :: k) :: Constraint where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 = undefined

上面的() 是空约束（它就像一个类型类约束的空“列表”）。

类型族的第一个“方程式”利用了类型族中可用的非线性模式匹配（它在左侧使用了两次x）。类型族还利用了这样一个事实，即如果没有一个案例匹配，它不会给你一个有效的约束。

您还应该能够使用类型级别的布尔值而不是 ConstraintKinds。这会有点麻烦，我认为最好避免在此处使用类型级别的布尔值（如果可以的话）。

旁注（我不记得了，我不得不查找这个答案）：您可以通过从GHC.Exts 导入Constraint 在范围内。

编辑：部分禁止无法访问的定义

这是一个修改，使其（部分）禁止无法访问的定义以及无效调用。它稍微迂回一些，但似乎可行。

修改Union 以提供* 而不是约束，如下所示：

type family Union (a :: [k]) (r :: k) :: * where
  Union (x ': xs) x = ()
  Union (x ': xs) y = Union xs y

类型是什么并不重要，只要它有一个你可以模式匹配的居民，所以我返回()类型（单位类型）。

这就是你将如何使用它：

test1 :: Shape s -> Union [Circle', Triangle'] s -> Int
test1 Circle {}   () = undefined
test1 Triangle {} () = undefined
-- test1 Square {} () = undefined -- This line won't compile

如果您忘记匹配它（例如，如果您在 () 构造函数上放置一个变量名称，如 x 而不是匹配），则可能会定义一个无法到达的案例。但是，当您实际尝试处理这种情况时，它仍然会在调用站点出现类型错误（因此，即使您在 Union 参数上不匹配，调用 test1 (Square undefined) () 也不会进行类型检查）。

请注意，Union 参数似乎必须在 Shape 参数之后才能使其工作（无论如何，完全如所述）。

Answer 2

这有点糟糕，但我想您可能需要使用 Data.Type.Equality 证明它是圆形还是方形：

test1 :: Either (s :~: Circle') (s :~: Square') -> Shape s -> Int

现在用户必须给出一个额外的参数（一个“证明术语”）来说明它是哪一个。

事实上，您可以使用证明术语的想法来“完成”bradm 的解决方案，其中：

class MyOpClass sh where
    myOp :: Shape sh -> Int
    shapeConstraint :: Either (sh :~: Circle') (sh :~: Square')

现在没有人可以再添加任何实例（除非他们使用undefined，否则会很不礼貌）。

Answer 3

你可以使用类型类：

class MyOpClass sh where
    myOp :: Shape sh -> Int

instance MyOpClass Circle' where
    myOp (Circle r) = _

instance MyOpClass Square' where
    myOP (Square s) = _

我觉得这不是一个特别“完整”的解决方案 - 任何人都可以返回并添加另一个 instance MyOpClass Triangle' - 但我想不出任何其他解决方案。但是，您可能只需不导出类型类即可避免此问题。

Answer 4

我注意到的另一个解决方案虽然很冗长，但它是创建一种具有特征布尔值列表的种类。然后，您可以在限制类型时对特征进行模式匹配：

-- [circleOrSquare] [triangleOrSquare]
data Shape' =
  Shape'' Bool
          Bool

data Shape :: Shape' -> * where
  Circle :: { radius :: Int} -> Shape (Shape'' True False)
  Square :: { side :: Int} -> Shape (Shape'' True True)
  Triangle
    :: { a :: Int
       , b :: Int
       , c :: Int}
    -> Shape (Shape'' False True)

test1 :: Shape (Shape'' True x) -> Int
test1 Circle {}   = 2
test1 Square {}   = 2
test1 Triangle {} = 2

这里，Triangle 会匹配失败：

    • Couldn't match type ‘'True’ with ‘'False’
      Inaccessible code in
        a pattern with constructor:
          Triangle :: Int -> Int -> Int -> Shape ('Shape'' 'False 'True),
        in an equation for ‘test1’
    • In the pattern: Triangle {}
      In an equation for ‘test1’: test1 Triangle {} = 2
   |
52 | test1 Triangle {} = 2
   |       ^^^^^^^^^^^

很遗憾，我认为你不能把这个写成记录，这样可能会更清晰，避免特征的排序。

这可能与类示例结合使用以提高可读性。