Search code examples
haskelltype-constraints

Is there a way to union type constraints?

In Haskell, is there a way to OR together several type constraints, such that the union is satisfied if any one of them are satisfied?

For example, suppose I had a GADT parameterized by a DataKind, and I wanted some constructors to only return values for certain constructors of the given kind, the pseudo-Haskell would be:

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

I can try to implement the OR using typeclasses:

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

But not only is this verbose, it's also slightly different than what I intended in that the original union was closed, but the typeclasses are all open. There's nothing to stop someone from defining

instance OrangeColor Blue

And because it's open, there's no way the compiler could infer that [Apple, Grape, Banana] must be of type [Fruit Green] unless told.

Solution

  • I can't think of a way to literally implement or for Constraints, unfortunately, but if we're just or-ing together equalities, as in your example, we can spice up your type class approach and make it closed with type families and lifted booleans. This will only work in GHC 7.6 and up; at the end, I mention both how it'll be nicer in GHC 7.8 and how to backport it to GHC 7.4.

    The idea is this: Just as we could declare a value-level function isBananaColor :: Color -> Bool, so too can we declare a type-level function 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

    If we like, we can even add

    type BananaColor c = IsBananaColor c ~ True

    We then repeat this for every fruit color, and define Fruit as in your second example:

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

    (If you want, you can get rid of -XConstraintKinds and the type XYZColor c = IsXYZColor c ~ True types, and just define the constructors of Fruit as XYZ :: IsXYZColor c ~ True => Fruit c.)

    Now, what does this buy you, and what doesn't it buy you? On the plus side, you do get the ability to define your type as you want to, which is definitely a win; and since Color is closed, nobody can add more type family instances and break this.

    However, there are downsides. You don't get the inference you wanted telling you automatically that [Apple, Grape, Banana] is of type Fruit Green; what's worse is that [Apple, Grape, Banana] has the perfectly valid type (AppleColor c, GrapeColor c, BananaColor c) => [Fruit c]. Yes, there's no way to monomorphize this, but GHC can't figure that out. To be perfectly honest, I can't imagine any solution giving you these properties, although I'm always ready to be surprised. The other obvious problem with this solution is how long it is—you need to define all eight color cases for each IsXYZColor type family! (The use of a brand new type family for each is also annoying, but unavoidable with solutions of this form.)

    I mentioned above that GHC 7.8 is going to make this nicer; it'll do that by obviating the need to list every single case for every single IsXYZColor class. How? Well, Richard Eisenberg et al. introduced closed overlapping ordered type families into GHC HEAD, and it'll be available in 7.8. There's a paper in sumbission to POPL 2014 (and an extended version) on the topic, and Richard also wrote an introductory blog post (which appears to have outdated syntax).

    The idea is to allow type family instances to be declared like ordinary functions: the equations must all be declared in one place (removing the open world assumption) and are tried in order, which allows overlap. Something like

    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

    is ambiguous, because IsBananaColor Green matches both the first and last equations; but in an ordinary function, it'd work fine. So the new syntax is:

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

    That type family ... where { ... } block defines the type family the way you want to define it; it signals that this type family is closed, ordered, and overlapping, as described above. Thus, the code would become something like the following in GHC 7.8 (untested, as I don't have it installed on my machine):

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

    Hooray, we can read this without falling asleep from boredom! In fact, you'll notice I switched to the explicit IsXYZColor c ~ True version for this code; I did that because because the boilerplate for the extra four type synonyms became a lot more obvious and annoying with these shorter definitions!

    However, let's go in the opposite direction and make this code uglier. Why? Well, GHC 7.4 (which is, alas, what I still have on my machine) doesn't support type families with non-* result type. What can we do instead? We can use type classes and functional dependencies to fake it. The idea is that instead of IsBananaColor :: Color -> Bool, we have a type class IsBananaColor :: Color -> Bool -> Constraint, and we add a functional dependency from the color to the boolean. Then IsBananaColor c b is satisfiable if and only if IsBananaColor c ~ b in the nicer version; because Color is closed and we have a functional dependency from it, this still gives us the same properties, it's just uglier (although mostly conceptually so). Without further ado, the complete code:

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