Copyright | (c) Tom Harding 2019 |
---|---|
License | MIT |
Maintainer | tom.harding@habito.com |
Stability | experimental |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Traditionally in Haskell, we use Either a b
to represent a choice of two
types. If we want to represent three types, we use Either a (Either b c)
,
and this nesting can continue as far as it needs to. However, this approach
comes with some difficulties: it's quite difficult to manipulate, and makes for
some rather unwieldy type signatures.
Thankfully, though, GHC provides us with GADTs, and they allow us to construct
a type that encompasses a coproduct of any number of arguments: the Variant
.
Just as Left 3
and Right True
are of type Either Int Bool
, we can write
Here 3
and There (Here True)
to do the same thing (ignoring Identity
wrappers). We can think of the Here
and There
constructors as an "index":
the index of the type we're storing is the number of occurrences of There
.
$setup >>> :set -XTypeOperators -XDataKinds -XTypeApplications
> > :t [ Here (Identity 'a'), There (There (Here (Identity True))) ]
- Here (Identity
a
), There (There (Here (Identity True))) - :: [VariantF Identity (Char : x : Bool : xs)]
Synopsis
- data VariantF (f :: k -> Type) (xs :: [k]) where
- type Variant (xs :: [Type]) = VariantF Identity xs
- variantF :: (f x -> r) -> (VariantF f xs -> r) -> VariantF f (x ': xs) -> r
- variant :: (x -> r) -> (Variant xs -> r) -> Variant (x ': xs) -> r
- case_ :: Case xs r fold => Variant xs -> fold
- caseF :: CaseF xs f r fold => VariantF f xs -> fold
- class CouldBeF (xs :: [k]) (x :: k) where
- class CouldBeF xs x => CouldBe (xs :: [Type]) (x :: Type) where
- type CouldBeAnyOfF e xs = All (Map (CouldBeF e) xs)
- type CouldBeAnyOf e xs = All (Map (CouldBe e) xs)
- class CatchF x xs ys | xs x -> ys, xs ys -> x, x ys -> xs where
- class CatchF x xs ys => Catch (x :: Type) (xs :: [Type]) (ys :: [Type]) where
- class EithersF (f :: Type -> Type) (xs :: [Type]) (o :: Type) | f xs -> o, o f -> xs where
- toEithersF :: VariantF f xs -> o
- fromEithersF :: o -> VariantF f xs
- class Eithers (xs :: [Type]) (o :: Type) | xs -> o where
- toEithers :: Variant xs -> o
- fromEithers :: o -> Variant xs
- class FoldF (c :: Type -> Constraint) (xs :: [Type]) where
- class FoldF c xs => Fold (c :: Type -> Constraint) (xs :: [Type]) where
- preposterous :: VariantF f '[] -> Void
- postposterous :: Void -> VariantF f '[]
Generalised coproducts
data VariantF (f :: k -> Type) (xs :: [k]) where Source #
The type VariantF f '[x, y, z]
is either f x
, f y
, or f z
. The
We construct these with Here
, There . Here
, and There . There . Here
respectively, and we can think o fthe number of There
-nestings as being
the index of our chosen type in the type-level list of options.
Often, however, we'll want to avoid being too explicit about our list of types, preferring instead to describe it with constraints. See the methods below for more information!
> > :t [ Here (pure "Hello"), There (Here (pure True)) ]
- Here (pure Hello), There (Here (pure True))
- :: Applicative f => [VariantF f ([Char] : Bool : xs)]
Instances
(EithersF f xs nested, Arbitrary nested) => Arbitrary (VariantF f xs) Source # | |
(Monoid (f x), Semigroup (VariantF f (x ': xs))) => Monoid (VariantF f (x ': xs)) Source # | |
AllF Semigroup f xs => Semigroup (VariantF f xs) Source # | |
AllF Show f xs => Show (VariantF f xs) Source # | |
AllF Eq f xs => Eq (VariantF f xs) Source # | |
(AllF Eq f xs, AllF Ord f xs) => Ord (VariantF f xs) Source # | |
Defined in Data.Variant compare :: VariantF f xs -> VariantF f xs -> Ordering # (<) :: VariantF f xs -> VariantF f xs -> Bool # (<=) :: VariantF f xs -> VariantF f xs -> Bool # (>) :: VariantF f xs -> VariantF f xs -> Bool # (>=) :: VariantF f xs -> VariantF f xs -> Bool # |
Scott encodings
variantF :: (f x -> r) -> (VariantF f xs -> r) -> VariantF f (x ': xs) -> r Source #
Remove the first possibility from a variant. One nice possibility here is
a function that tells us whether the first type was the one in our variant:
variantF Left Right
. For example:
>>>
:set -XDataKinds
>>>
variantF Left Right (Here (Identity True) :: Variant '[Bool])
Left (Identity True)
>>>
variantF Left Right (There (Here (Identity 3)) :: Variant '[Bool, Int])
Right (Here (Identity 3))
Church encodings
case_ :: Case xs r fold => Variant xs -> fold Source #
Same as caseF
, but without the functor wrappers. Again, this function
will specialise according to the provided variant:
> > :t case_ (throw True :: Variant '[Bool, Int])
case_ (throw True :: Variant '[Bool, Int]) :: (Bool -> o) -> (Int -> o) -> o
You can also use TypeApplications
to check the specialisation for a
particular variant:
> > :t case_ @'[Int, Bool, String]
case_ @'[Int, Bool, String] :: Variant '[Int, Bool, String] -> (Int -> o) -> (Bool -> o) -> ([Char] -> o) -> o
caseF :: CaseF xs f r fold => VariantF f xs -> fold Source #
The either
function provides us with a way of folding an Either
by
providing a function for each possible constructor: Left
and Right
. In
our case, we could have any number of functions to supply, depending on how
many types are in our type-level index.
This function specialises depending on the variant provided:
> > :t caseF (throw True :: Variant '[Bool])
caseF (throw True :: Variant '[Bool]) :: (Identity Bool -> r) -> r
> > :t caseF (throwF (pure True) :: VariantF IO '[Int, Bool])
caseF (throwF (pure True) :: VariantF IO '[Int, Bool]) :: (IO Int -> o) -> (IO Bool -> o) -> o
Injections
class CouldBeF (xs :: [k]) (x :: k) where Source #
When dealing with larger (or polymorphic) variants, it becomes difficult
(or impossible) to construct VariantF
values explicitly. In that case, the
throwF
function gives us a polymorphic way to lift values into variants.
>>>
throwF (pure "Hello") :: VariantF Maybe '[Bool, Int, Double, String]
There (There (There (Here (Just "Hello"))))
>>>
throwF (pure True) :: VariantF Maybe '[Bool, Int, Double, String]
Here (Just True)
>>>
throwF (pure True) :: VariantF IO '[Int, Double, String]
... ... • Uh oh! I couldn't find Bool inside the variant! ... If you're pretty sure I'm wrong, perhaps the variant type is ambiguous; ... could you add some annotations? ...
throwF :: f x -> VariantF f xs Source #
snatchF :: VariantF f xs -> Either (VariantF f xs) (f x) Source #
class CouldBeF xs x => CouldBe (xs :: [Type]) (x :: Type) where Source #
type CouldBeAnyOfF e xs = All (Map (CouldBeF e) xs) Source #
As with CouldBeAnyOf
, we can also constrain a variant to represent
several possible types, as we might with several CouldBeF
constraints,
using one type-level list.
type CouldBeAnyOf e xs = All (Map (CouldBe e) xs) Source #
Listing larger variants' constraints might amplify the noise of
functions' signatures. The CouldBeAnyOfF
constraint lets us specify
several types a variant may contain in a single type-level list, as opposed
to several independent constraints. So, we could replace,
f :: (e CouldBe
Int, e CouldBe
Bool, e CouldBe
Char) => VariantF IO e
with the equivalent constraint,
f :: e CouldBeAnyOf
'[Int, Bool, Char] => VariantF IO e
As CouldBeAnyOf
is just short-hand, we can use throw
just like when we
have CouldBe
constraints:
>>>
:set -XTypeOperators
>>>
:{
f :: e `CouldBeAnyOf` '[Int, Bool, Char] => Variant e f = throw 'c' :}
... and eliminate constraints in just the same way:
>>>
:{
g :: e `CouldBeAnyOf` '[Int, Bool] => Either (Variant e) Char g = catch @Char f :}
Projections
class CatchF x xs ys | xs x -> ys, xs ys -> x, x ys -> xs where Source #
This is an odd constraint, as you should rarely need to see it. GHC's
partial instantiation tricks should mean that mentions of this class "cancel
out" mentions of CouldBeF
. As an example, let's imagine a function that
represents some business logic that potentially "throws" either an Int
or
Bool
while it runs:
>>>
:set -XFlexibleContexts -XMonoLocalBinds -XTypeOperators
>>>
:{
f :: (e `CouldBe` Int, e `CouldBe` Bool) => VariantF IO e f = throwF (pure True) :}
As we can see, there are two constraints here. However, if we "catch" one of
these possible errors, we don't just add the CatchF
constraint: we /cancel
out/ the constraint corresponding to the type we caught:
>>>
:{
g :: e `CouldBe` Int => Either (VariantF IO e) (IO Bool) g = catchF @Bool f :}
This means that constraints only propagate for uncaught exceptions, just
as Java functions only need declare exceptions they haven't caught. Once
we've caught all the errors, the constraint disappears! This can be a nice
way to work if you combine it with something like ExceptT
.
class CatchF x xs ys => Catch (x :: Type) (xs :: [Type]) (ys :: [Type]) where Source #
throwF
is to catchF
as throw
is to catch
. This function allows us
to discharge constraints for Variant
types. We can revisit the catchF
example without the functor wrapper:
>>>
:{
f :: (e `CouldBe` Int, e `CouldBe` Bool) => Variant e f = throw True :}
... and be similarly excited when we make one of the constraints disappear:
>>>
:{
g :: e `CouldBe` Int => Either (Variant e) Bool g = catch @Bool f :}
Conversions to and from Either
s
class EithersF (f :: Type -> Type) (xs :: [Type]) (o :: Type) | f xs -> o, o f -> xs where Source #
Occasionally, we might want to use our "nested Either
" analogue for
whatever reason. For that situation the functions here allow you to swap
between the two representations.
> > :t toEithersF @IO @'[String, Int, Bool]
toEithersF IO
'[String, Int, Bool]
:: VariantF IO '[String, Int, Bool]
-> Either (IO [Char]) (Either (IO Int) (IO Bool))
In order to maintain the round-tripping property (see below), the functional dependency only goes from the variant to the nested either. This is because the opposite doesn't always necessarily make sense.
If Variant '[a, b]
is converted to Either a b
, it would seem sensible to
say the opposite is equally as mechanical. However, consider a nesting like
Either a (Either b c)
: should this translate to Variant '[a, b, c]
or
Variant '[a, Either b c]
? There's not a unique mapping in this direction,
so we can't add the functional dependency.
toEithersF :: VariantF f xs -> o Source #
fromEithersF :: o -> VariantF f xs Source #
Instances
EithersF f '[x] (f x) Source # | |
Defined in Data.Variant toEithersF :: VariantF f '[x] -> f x Source # fromEithersF :: f x -> VariantF f '[x] Source # | |
(Functor f, EithersF f (y ': xs) zs) => EithersF f (x ': (y ': xs)) (Either (f x) zs) Source # | |
Defined in Data.Variant toEithersF :: VariantF f (x ': (y ': xs)) -> Either (f x) zs Source # fromEithersF :: Either (f x) zs -> VariantF f (x ': (y ': xs)) Source # |
class Eithers (xs :: [Type]) (o :: Type) | xs -> o where Source #
The f
-less analogue of EithersF
. The same properties as described
above will hold, with the same issues around fromEithers
result inference.
> > :t toEithers @'[String, Int, Bool]
toEithers @'[String, Int, Bool] :: Variant '[String, Int, Bool] -> Either [Char] (Either Int Bool)
The round-tripping property is also conserved:
Folds
class FoldF (c :: Type -> Constraint) (xs :: [Type]) where Source #
A constraint-based fold requires a polymorphic function relying on a shared constraint between all members of the variant. If that's a lot of words, let's see a little example:
>>>
foldF @Show (throwF ["hello"] :: VariantF [] '[(), String, Bool]) show
"[\"hello\"]"
If everything in our variant is Show
-friendly, we can fold it with the
show
function, and we just show whatever is in there!
class FoldF c xs => Fold (c :: Type -> Constraint) (xs :: [Type]) where Source #
Similarly, we can fold the wrapper-less version in the same way. As an example, if all the types are the same, we can pull out whatever value is in there using the fold interface.
>>>
:set -XRankNTypes -XScopedTypeVariables
>>>
:{
fold' :: forall x xs. Fold ((~) x) xs => Variant xs -> x fold' xs = fold @((~) x) xs id :}
If all the types in the list are the same, and we can turn values of that type into some result and return it.
Void conversions
preposterous :: VariantF f '[] -> Void Source #
A choice of zero types is an uninhabited type! This means we can convert
it to Void
...
postposterous :: Void -> VariantF f '[] Source #
... and it also means we can convert back!