时间戳

首页 > 解决方案 > 数据种类联盟

haskell - 数据种类联盟

问题描述

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

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

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

上面的部分编译

标签： haskelldata-kinds

解决方案

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

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

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

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

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

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

推荐阅读