haskell - 数据种类联盟

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)。类型族还利用了这样一个事实，即如果没有一个案例匹配，它不会给你一个有效的约束。

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

旁注(我不记得了，我不得不查找这个答案):你得到 Constraint通过从 GHC.Exts 导入在范围内.

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

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

修改 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 之后参数以使其起作用(无论如何，完全如所描述的那样)。