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 functionIsBananaColor :: Color -> Bool
:If we like, we can even add
We then repeat this for every fruit color, and define
Fruit
as in your second example:(If you want, you can get rid of
-XConstraintKinds
and thetype XYZColor c = IsXYZColor c ~ True
types, and just define the constructors ofFruit
asXYZ :: 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 typeFruit 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 eachIsXYZColor
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
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: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):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 ofIsBananaColor :: Color -> Bool
, we have a type classIsBananaColor :: Color -> Bool -> Constraint
, and we add a functional dependency from the color to the boolean. ThenIsBananaColor c b
is satisfiable if and only ifIsBananaColor c ~ b
in the nicer version; becauseColor
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: