DataKind工会

Question

我不确定它是否是正确的术语,但是可以声明接受datakinds"联合"的函数类型吗？

例如,我知道我可以执行以下操作:

{-# 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'要使用的种类,或者让我允许每个数据允许多个datakind定义？

编辑:

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

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

这有点糟糕,但我想你可能要求证明它是圆形或正方形,使用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 2

你可以在(我认为)使用类型系列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.这会有点麻烦,我认为最好避免在这里使用类型级布尔值(如果可以的话).

旁注(我永远不会记住这个,我不得不查看这个答案):你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) ()也不会键入check).

请注意,似乎Union参数必须在Shape参数之后才能使其工作(完全如所描述的那样).