有没有一种方法可以联合类型约束？

Question

有没有一种方法可以联合类型约束？

7

在Haskell中，是否有一种方法可以将多个类型约束进行OR运算，以便如果其中任何一个满足，则满足联合？

例如，假设我有一个由DataKind参数化的GADT，并且我希望某些构造函数仅针对给定种类的某些构造函数返回值，伪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]类型，除非被告知。

- rampion

2个回答

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]

- Ankur

你看过GHC 7.4+的种类提升特性吗？它允许将类型视为种类，将值视为类型。使用-XDataKinds，Green是一个完全有效的类型级别的东西，其种类为Color。这使得类型级别编程更加类型安全（因为你有编码的东西，Fruit Int是良种的），并且消除了定义虚假data Green = Green类型的需要。 - Antal Spector-Zabusky

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Antal Spector-Zabusky · Accepted Answer

我不知道如何实现或者约束，但是如果我们只是将等式进行逻辑或操作，就像你的例子一样，我们可以使用类型族和提升布尔值来改进你的类型类方法并使其封闭。这仅适用于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

（如果你愿意，你可以放弃 -XConstraintKinds 和 type XYZColor c = IsXYZColor c ~ True 类型，并将 Fruit 的构造函数定义为 XYZ :: IsXYZColor c ~ True => Fruit c。) 这样做的好处是什么，坏处又是什么呢？优点是你可以按照自己的方式定义类型，这肯定是个胜利；由于颜色是封闭的，没有人可以添加更多的类型家族实例并破坏此类实例。

然而，这种方法也有缺点。你无法获得所需的推理，告诉你[Apple, Grape, Banana]自动属于Fruit Green; 更糟糕的是，[Apple, Grape, Banana]具有完全有效的类型(AppleColor c, GrapeColor c, BananaColor c) => [Fruit c]。是的，没有办法单态化它，但GHC无法弄清楚它。坦率地说，我无法想象任何解决方案能给您这些属性，尽管我随时准备惊喜。这个解决方案的另一个明显问题是它太长了——你需要为每个IsXYZColor类型族定义所有八个颜色情况！（对于这种形式的解决方案，使用全新的类型族也很恼人，但不可避免。）

我之前提到过，GHC 7.8将会使这个过程更加方便；它将通过消除需要为每个IsXYZColor类列出每一个情况的需求来实现这一点。如何做到的呢？Richard Eisenberg等人在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才能被满足；由于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