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.
I can't think of a way to literally implement or for Constraint
s, 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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With