DataKind联盟 [英] DataKind Unions

问题描述

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

I'm not sure if it is the right terminology, but is it possible to declare function types that take in an 'union' of datakinds?

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

For example, I know I can do the following:

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

但是，如果我想采用圆形或正方形的形状怎么办?如果我还想采用所有形状来实现单独的功能怎么办?

However, what if I want to take in a shape that is either a circle or a square? What if I also want to take in all shapes for a separate function?

我是否可以定义一组要使用的Shape'类型，还是可以对每个数据允许多个datakind定义?

Is there a way for me to either define a set of Shape' kinds to use, or a way for me to allow multiple datakind definitions per data?

使用工会似乎无效:

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

上面的部分编译

推荐答案

您可以使用类型家族以及ConstraintKinds和PolyKinds:

You can accomplish something like this in (I think) a reasonably clean way using a type family together with ConstraintKinds and 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

上面的()是空约束(就像类型类型约束的空列表"一样).

The () above is the empty constraint (it's like an empty "list" of type class constraints).

类型族的第一个等式"利用类型族中可用的非线性模式匹配(它在左侧两次使用x).类型族还利用了以下事实:如果所有情况都不匹配，它将不会为您提供有效的约束.

The first "equation" of the type family makes use of the nonlinear pattern matching available in type families (it uses x twice on the left hand side). The type family also makes use of the fact that if none of the cases match, it will not give you a valid constraint.

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

You should also be able to use a type-level Boolean instead of ConstraintKinds. That would be a bit more cumbersome and I think it would be best to avoid using a type-level Boolean here (if you can).

旁注(我永远都记不清了，不得不为这个答案查询它):通过从GHC.Exts导入Constraint，可以在范围内获得Constraint.

Side-note (I can never remember this and I had to look it up for this answer): You get Constraint in-scope by importing it from GHC.Exts.

这里是对它的修改，以(部分)禁止不可达的定义以及无效的调用.环形交叉路口稍微多一点，但似乎可行.

Here is a modification to get it to (partially) disallow unreachable definitions as well as invalid calls. It is slightly more roundabout, but it seems to work.

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

Modify Union to give a * instead of a constraint, like this:

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

类型的大小无关紧要，只要它具有您可以在其上进行模式匹配的居民，那么我就退回()类型(单元类型).

It doesn't matter too much what the type is, as long as it has an inhabitant you can pattern match on, so I give back the () type (the unit type).

这是您将如何使用它:

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) ()也不会进行类型检查).

If you forget to match on it (like, if you put a variable name like x instead of matching on the () constructor), it is possible that an unreachable case can be defined. It will still give a type error at the call-site when you actually try to reach that case, though (so, even if you don't match on the Union argument, the call test1 (Square undefined) () will not type check).

请注意，看来Union自变量必须位于Shape自变量之后，这样才能正常工作(无论如何完全如所述).

Note that it seems the Union argument must come after the Shape argument in order for this to work (fully as described, anyway).

这篇关于DataKind联盟的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！