7

在 Haskell 中，有没有一种方法可以将多个类型约束组合在一起，这样如果满足其中任何一个约束，联合就可以满足？

例如，假设我有一个由 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]，除非被告知。

4

2 回答 2

4

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

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

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

如果我们喜欢，我们甚至可以添加

type BananaColor c = IsBananaColor c ~ True

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

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}

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

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

type family   IsAppleColor (c :: Color) :: Bool
type instance IsAppleColor Red    = True
type instance IsAppleColor Green  = True
type instance IsAppleColor White  = False
type instance IsAppleColor Blue   = False
type instance IsAppleColor Yellow = False
type instance IsAppleColor Tawny  = False
type instance IsAppleColor Purple = False
type instance IsAppleColor Black  = False
type AppleColor c = IsAppleColor c ~ True

type family   IsGrapeColor (c :: Color) :: Bool
type instance IsGrapeColor Red    = True
type instance IsGrapeColor Green  = True
type instance IsGrapeColor White  = True
type instance IsGrapeColor Blue   = False
type instance IsGrapeColor Yellow = False
type instance IsGrapeColor Tawny  = False
type instance IsGrapeColor Purple = False
type instance IsGrapeColor Black  = False
type GrapeColor c = IsGrapeColor c ~ True

-- For consistency
type family   IsOrangeColor (c :: Color) :: Bool
type instance IsOrangeColor Tawny  = True
type instance IsOrangeColor White  = False
type instance IsOrangeColor Red    = False
type instance IsOrangeColor Blue   = False
type instance IsOrangeColor Yellow = False
type instance IsOrangeColor Green  = False
type instance IsOrangeColor Purple = False
type instance IsOrangeColor Black  = False
type OrangeColor c = IsOrangeColor c ~ True

（如果你愿意，你可以去掉-XConstraintKindsandtype XYZColor c = IsXYZColor c ~ True类型，只定义Fruitas的构造函数XYZ :: IsXYZColor c ~ True => Fruit c。）

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

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

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

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

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

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

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

该type family ... where { ... }块以您想要定义的方式定义类型系列；它表示这个类型族是封闭的、有序的和重叠的，如上所述。因此，代码在 GHC 7.8 中将变为如下所示（未经测试，因为我的机器上没有安装它）：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

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

data Fruit (c :: Color) where
  Banana :: IsBananaColor c ~ True => Fruit c
  Apple  :: IsAppleColor  c ~ True => Fruit c
  Grape  :: IsGrapeColor  c ~ True => Fruit c
  Orange :: IsOrangeColor c ~ True => Fruit c

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

type family IsAppleColor (c :: Color) :: Bool where
   IsAppleColor Red   = True
   IsAppleColor Green = True
   IsAppleColor c     = False

type IsGrapeColor (c :: Color) :: Bool where
  IsGrapeColor Red   = True
  IsGrapeColor Green = True
  IsGrapeColor White = True
  IsGrapeColor c     = False

type family IsOrangeColor (c :: Color) :: Bool where
  IsOrangeColor Tawny = True
  IsOrangeColor c     = False

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

但是，让我们反其道而行之，让这段代码更丑陋。为什么？好吧，GHC 7.4（唉，我的机器上还有什么）不支持非*结果类型的类型族。我们能做些什么呢？我们可以使用类型类和函数依赖来伪造它。这个想法是IsBananaColor :: Color -> Bool，我们有一个类型类IsBananaColor :: Color -> Bool -> Constraint，而不是 ，我们添加了一个从颜色到布尔值的函数依赖。IsBananaColor c b当且仅当IsBananaColor c ~ b在更好的版本中，then是可满足的；因为Color是封闭的并且我们有一个函数依赖，这仍然给我们相同的属性，它只是更丑陋（尽管在概念上大多如此）。废话不多说，完整代码：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}

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    IsBananaColor (c :: Color) (b :: Bool) | c -> b
instance IsBananaColor Green  True
instance IsBananaColor Yellow True
instance IsBananaColor Black  True
instance IsBananaColor White  False
instance IsBananaColor Red    False
instance IsBananaColor Blue   False
instance IsBananaColor Tawny  False
instance IsBananaColor Purple False
type BananaColor c = IsBananaColor c True

class    IsAppleColor (c :: Color) (b :: Bool) | c -> b
instance IsAppleColor Red    True
instance IsAppleColor Green  True
instance IsAppleColor White  False
instance IsAppleColor Blue   False
instance IsAppleColor Yellow False
instance IsAppleColor Tawny  False
instance IsAppleColor Purple False
instance IsAppleColor Black  False
type AppleColor c = IsAppleColor c True

class    IsGrapeColor (c :: Color) (b :: Bool) | c -> b
instance IsGrapeColor Red    True
instance IsGrapeColor Green  True
instance IsGrapeColor White  True
instance IsGrapeColor Blue   False
instance IsGrapeColor Yellow False
instance IsGrapeColor Tawny  False
instance IsGrapeColor Purple False
instance IsGrapeColor Black  False
type GrapeColor c = IsGrapeColor c True

class    IsOrangeColor (c :: Color) (b :: Bool) | c -> b
instance IsOrangeColor Tawny  True
instance IsOrangeColor White  False
instance IsOrangeColor Red    False
instance IsOrangeColor Blue   False
instance IsOrangeColor Yellow False
instance IsOrangeColor Green  False
instance IsOrangeColor Purple False
instance IsOrangeColor Black  False
type OrangeColor c = IsOrangeColor c True
于 2013-08-22T04:54:24.927 回答
0

以下是我对问题进行编码的尝试。主要思想是将水果表示为一个类型类，并将各种类型的水果表示为实现该类型类的类型

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

class Fruit a where
  getColor :: a -> Color

data Banana where
  GreenBanana :: Banana
  YellowBanana :: Banana
  BlackBanana :: Banana

instance Fruit Banana where
  getColor GreenBanana = Green
  getColor YellowBanana = Yellow
  getColor BlackBanana = Black

data Apple where
  GreenApple :: Apple
  RedApple :: Apple

instance Fruit Apple where
  getColor GreenApple = Green
  getColor RedApple = Red

您的问题最后一行表明您想要某种类型[Fruit Green]，这显然意味着Fruit Green应该是上面代码中的 Green 是值构造函数的类型。我们必须将其Green作为一种类型，如下所示：

data Red = Red
data Green = Green
data Black = Black

data Fruit c where
  GreenBanana :: Fruit Green
  BlackBanana :: Fruit Black
  RedApple :: Fruit Red
  GreenApple :: Fruit Green


greenFruits :: [Fruit Green]
greenFruits = [GreenBanana, GreenApple]
于 2013-08-22T05:07:28.770 回答