DataKind 联盟

Question

我不确定这是否是正确的术语，但是是否可以声明接受 'union' 数据种类的函数类型？

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

{-# 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' 种类，或者让我允许每个数据有多个数据种类定义？

编辑：

union 的用法似乎不起作用：

{-# 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

您可以使用类型类：

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

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

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

这对我来说并不是特别 'complete' 的解决方案 - 任何人都可以返回并添加另一个 instance MyOpClass Triangle' - 但我想不出任何其他解决方案。然而，您可以通过不导出类型类来避免这个问题。

Answer 2

这有点糟糕，但我想您可能需要使用 Data.Type.Equality:

来证明它是圆形还是正方形

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

现在用户必须给出一个额外的参数（"proof term"）来说明它是哪一个。

事实上，您可以将证明项想法用于 "complete" bradm 的解决方案，其中：

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

现在没有人可以再添加实例（除非他们使用 undefined，这是不礼貌的）。

Answer 3

您可以（我认为）使用类型族以及 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

上面的()是空约束（它就像一个class约束类型的空"list"）。

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

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

旁注（我永远不记得这个，我不得不查找它以获得这个答案）：通过从 GHC.Exts.[=29= 导入它，你得到 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 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

这里，三角形会匹配失败：

    • 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
   |       ^^^^^^^^^^^

遗憾的是，我不认为你可以把这个写成记录，这样可能更清楚并且避免了特征的排序。

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

DataKind 联盟

DataKind Unions

haskell

data-kinds

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