有没有办法结合类型约束？

Question

在Haskell中,有没有办法将几个类型约束一起OR,这样如果满足其中任何一个,就会满足并集？

例如,假设我有一个由a参数化的GADT DataKind,我希望一些构造函数只返回给定类型的某些构造函数的值,伪Haskell将是:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module Temp where

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black

data Fruit (c :: Color) where
  Banana :: (c ~ Green | c ~ Yellow | c ~ Black)  => Fruit c
  Apple  :: (c ~ Red | c ~ Green )                => Fruit c
  Grape  :: (c ~ Red | c ~ Green | c ~ White)     => Fruit c
  Orange :: (c ~ Tawny )                          => Fruit c

我可以尝试使用类型类来实现OR:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module Temp where

data Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black

data Fruit (c :: Color) where
  Banana :: BananaColor c => Fruit c
  Apple  :: AppleColor c  => Fruit c
  Grape  :: GrapeColor c  => Fruit c
  Orange :: OrangeColor c => Fruit c

class BananaColor (c :: Color)
instance BananaColor Green
instance BananaColor Yellow
instance BananaColor Black

class AppleColor (c :: Color)
instance AppleColor Red
instance AppleColor Green

class GrapeColor (c :: Color)
instance GrapeColor Red
instance GrapeColor Green
instance GrapeColor White

class OrangeColor (c :: Color)
instance OrangeColor Tawny

但这不仅是冗长的,而且与我原先的联盟关闭时的意图略有不同,但是类型类都是开放的.没有什么可以阻止某人定义

instance OrangeColor Blue

因为它是开放的,除非被告知[Apple, Grape, Banana],[Fruit Green]否则编译器无法推断出必须是类型.

Answer 1

不幸的是，我想不出一种方法来真正实现 or for Constraints，但是如果我们只是将等式或在一起，就像在您的示例中一样，我们可以为您的类型类方法增添趣味，并使其以类型封闭家庭和提升布尔值。这仅适用于 GHC 7.6 及更高版本；最后，我提到它在 GHC 7.8 中如何变得更好以及如何将其向后移植到 GHC 7.4。

\n\n

这个想法是这样的：就像我们可以声明一个值级函数一样isBananaColor :: Color -> Bool，我们也可以声明一个类型级函数IsBananaColor :: Color -> Bool：

\n\n

type family IsBananaColor (c :: Color) :: Bool\ntype instance IsBananaColor Green  = True\ntype instance IsBananaColor Yellow = True\ntype instance IsBananaColor Black  = True\ntype instance IsBananaColor White  = False\ntype instance IsBananaColor Red    = False\ntype instance IsBananaColor Blue   = False\ntype instance IsBananaColor Tawny  = False\ntype instance IsBananaColor Purple = False\n

\n\n

如果我们愿意，我们甚至可以添加

\n\n

type BananaColor c = IsBananaColor c ~ True\n

\n\n

然后，我们对每种水果颜色重复此操作，并Fruit按照第二个示例中的定义进行定义：

\n\n

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE TypeFamilies #-}\n\ndata Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black\n\ndata Fruit (c :: Color) where\n  Banana :: BananaColor c => Fruit c\n  Apple  :: AppleColor  c => Fruit c\n  Grape  :: GrapeColor  c => Fruit c\n  Orange :: OrangeColor c => Fruit c\n\ntype family   IsBananaColor (c :: Color) :: Bool\ntype instance IsBananaColor Green  = True\ntype instance IsBananaColor Yellow = True\ntype instance IsBananaColor Black  = True\ntype instance IsBananaColor White  = False\ntype instance IsBananaColor Red    = False\ntype instance IsBananaColor Blue   = False\ntype instance IsBananaColor Tawny  = False\ntype instance IsBananaColor Purple = False\ntype BananaColor c = IsBananaColor c ~ True\n\ntype family   IsAppleColor (c :: Color) :: Bool\ntype instance IsAppleColor Red    = True\ntype instance IsAppleColor Green  = True\ntype instance IsAppleColor White  = False\ntype instance IsAppleColor Blue   = False\ntype instance IsAppleColor Yellow = False\ntype instance IsAppleColor Tawny  = False\ntype instance IsAppleColor Purple = False\ntype instance IsAppleColor Black  = False\ntype AppleColor c = IsAppleColor c ~ True\n\ntype family   IsGrapeColor (c :: Color) :: Bool\ntype instance IsGrapeColor Red    = True\ntype instance IsGrapeColor Green  = True\ntype instance IsGrapeColor White  = True\ntype instance IsGrapeColor Blue   = False\ntype instance IsGrapeColor Yellow = False\ntype instance IsGrapeColor Tawny  = False\ntype instance IsGrapeColor Purple = False\ntype instance IsGrapeColor Black  = False\ntype GrapeColor c = IsGrapeColor c ~ True\n\n-- For consistency\ntype family   IsOrangeColor (c :: Color) :: Bool\ntype instance IsOrangeColor Tawny  = True\ntype instance IsOrangeColor White  = False\ntype instance IsOrangeColor Red    = False\ntype instance IsOrangeColor Blue   = False\ntype instance IsOrangeColor Yellow = False\ntype instance IsOrangeColor Green  = False\ntype instance IsOrangeColor Purple = False\ntype instance IsOrangeColor Black  = False\ntype OrangeColor c = IsOrangeColor c ~ True\n

\n\n

（如果需要，您可以去掉-XConstraintKinds和类型，而只定义astype XYZColor c = IsXYZColor c ~ True的构造函数。）FruitXYZ :: IsXYZColor c ~ True => Fruit c

\n\n

现在，这会给你带来什么，不会给你带来什么？从好的方面来说，您确实能够根据需要定义自己的类型，这绝对是一个胜利；由于Color已关闭，没有人可以添加更多类型族实例并打破它。

\n\n

然而，也有缺点。您不会自动得到您想要的推断，该推断[Apple, Grape, Banana]属于 type Fruit Green；更糟糕的是它[Apple, Grape, Banana]具有完全有效的类型(AppleColor c, GrapeColor c, BananaColor c) => [Fruit c]。是的，没有办法将其单态化，但 GHC 无法弄清楚这一点。老实说，我无法想象任何解决方案可以为您提供这些属性，尽管我总是准备好感到惊讶。此解决方案的另一个明显问题是它有多长\xe2\x80\x94，您需要为每个IsXYZColor类型系列定义所有八种颜色情况！（为每个类型使用全新的类型系列也很烦人，但对于这种形式的解决方案来说是不可避免的。）

\n\n\n\n

我上面提到 GHC 7.8 会让这一切变得更好；它不需要列出每个IsXYZColor类的每个案例来做到这一点。如何？好吧，理查德·艾森伯格等人。将封闭重叠有序类型族引入 GHC HEAD，并将在 7.8 中提供。POPL 2014（及其扩展版本）上有一篇关于该主题的论文，Richard 还写了一篇介绍性博客文章（语法似乎已经过时）。

\n\n

这个想法是允许像普通函数一样声明类型族实例：方程必须全部声明在一个地方（删除开放世界假设）并按顺序尝试，这允许重叠。就像是

\n\n

type family IsBananaColor (c :: Color) :: Bool\ntype instance IsBananaColor Green  = True\ntype instance IsBananaColor Yellow = True\ntype instance IsBananaColor Black  = True\ntype instance IsBananaColor c      = False\n

\n\n

是不明确的，因为IsBananaColor Green匹配第一个和最后一个方程；但在普通功能中，它可以正常工作。所以新的语法是：

\n\n

type family IsBananaColor (c :: Color) :: Bool where\n  IsBananaColor Green  = True\n  IsBananaColor Yellow = True\n  IsBananaColor Black  = True\n  IsBananaColor c      = False\n

\n\n

该块按照您想要的type family ... where { ... }方式定义类型族；它表明该类型族是封闭的、有序的和重叠的，如上所述。因此，GHC 7.8 中的代码将类似于以下内容（未经测试，因为我没有在我的计算机上安装它）：

\n\n

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeFamilies #-}\n\ndata Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black\n\ndata Fruit (c :: Color) where\n  Banana :: IsBananaColor c ~ True => Fruit c\n  Apple  :: IsAppleColor  c ~ True => Fruit c\n  Grape  :: IsGrapeColor  c ~ True => Fruit c\n  Orange :: IsOrangeColor c ~ True => Fruit c\n\ntype family IsBananaColor (c :: Color) :: Bool where\n  IsBananaColor Green  = True\n  IsBananaColor Yellow = True\n  IsBananaColor Black  = True\n  IsBananaColor c      = False\n\ntype family IsAppleColor (c :: Color) :: Bool where\n   IsAppleColor Red   = True\n   IsAppleColor Green = True\n   IsAppleColor c     = False\n\ntype IsGrapeColor (c :: Color) :: Bool where\n  IsGrapeColor Red   = True\n  IsGrapeColor Green = True\n  IsGrapeColor White = True\n  IsGrapeColor c     = False\n\ntype family IsOrangeColor (c :: Color) :: Bool where\n  IsOrangeColor Tawny = True\n  IsOrangeColor c     = False\n

\n\n

万岁，我们可以读到这篇文章而不会因为无聊而睡着！事实上，您会注意到我已切换IsXYZColor c ~ True到此代码的显式版本；我这样做是因为额外的四种类型同义词的样板变得更加明显，并且这些较短的定义令人烦恼！

\n\n\n\n

然而，让我们朝相反的方向走，让这段代码变得更难看。为什么？好吧，GHC 7.4（唉，我的机器上仍然有这个）不支持非结果*类型的类型族。我们能做什么呢？我们可以使用类型类和函数依赖来伪造它。IsBananaColor :: Color -> Bool我们的想法是，我们有一个类型 class ，而不是IsBananaColor :: Color -> Bool -> Constraint，并且添加从颜色到布尔值的函数依赖关系。那么IsBananaColor c b当且仅当IsBananaColor c ~ b在更好的版本中时是可满足的；因为Color是封闭的，并且我们对它有函数依赖，这仍然给我们提供了相同的属性，只是更丑陋（尽管主要是概念上的）。废话不多说，上完整代码：

\n\n

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE KindSignatures #-}\n{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE ConstraintKinds #-}\n{-# LANGUAGE FunctionalDependencies #-}\n{-# LANGUAGE FlexibleContexts #-}\n\ndata Color = White | Red | Blue | Yellow | Green | Tawny | Purple | Black\n\ndata Fruit (c :: Color) where\n  Banana :: BananaColor c => Fruit c\n  Apple  :: AppleColor  c => Fruit c\n  Grape  :: GrapeColor  c => Fruit c\n  Orange :: OrangeColor c => Fruit c\n\nclass    IsBananaColor (c :: Color) (b :: Bool) | c -> b\ninstance IsBananaColor Green  True\ninstance IsBananaColor Yellow True\ninstance IsBananaColor Black  True\ninstance IsBananaColor White  False\ninstance IsBananaColor Red    False\ninstance IsBananaColor Blue   False\ninstance IsBananaColor Tawny  False\ninstance IsBananaColor Purple False\ntype BananaColor c = IsBananaColor c True\n\nclass    IsAppleColor (c :: Color) (b :: Bool) | c -> b\ninstance IsAppleColor Red    True\ninstance IsAppleColor Green  True\ninstance IsAppleColor White  False\ninstance IsAppleColor Blue   False\ninstance IsAppleColor Yellow False\ninstance IsAppleColor Tawny  False\ninstance IsAppleColor Purple False\ninstance IsAppleColor Black  False\ntype AppleColor c = IsAppleColor c True\n\nclass    IsGrapeColor (c :: Color) (b :: Bool) | c -> b\ninstance IsGrapeColor Red    True\ninstance IsGrapeColor Green  True\ninstance IsGrapeColor White  True\ninstance IsGrapeColor Blue   False\ninstance IsGrapeColor Yellow False\ninstance IsGrapeColor Tawny  False\ninstance IsGrapeColor Purple False\ninstance IsGrapeColor Black  False\ntype GrapeColor c = IsGrapeColor c True\n\nclass    IsOrangeColor (c :: Color) (b :: Bool) | c -> b\ninstance IsOrangeColor Tawny  True\ninstance IsOrangeColor White  False\ninstance IsOrangeColor Red    False\ninstance IsOrangeColor Blue   False\ninstance IsOrangeColor Yellow False\ninstance IsOrangeColor Green  False\ninstance IsOrangeColor Purple False\ninstance IsOrangeColor Black  False\ntype OrangeColor c = IsOrangeColor c True\n

\n