This post showcases an upcoming addition to the contravariant
package that permits programming in a “co-Applicative
” (Divisible
) style that greatly resembles Applicative
style.
This post assumes that you are already familiar with programming in an Applicative
style, but if you don’t know what that is then I recommend reading:
Example
The easiest way to motivate this is through a concrete example:
{-# LANGUAGE NamedFieldPuns #-}
import Data.Functor.Contravariant (Predicate(..), (>$<))
import Data.Functor.Contravariant.Divisible (Divisible, divided)
nonNegative :: Predicate Double
= Predicate (0 <=)
nonNegative
data Point = Point { x :: Double, y :: Double, z :: Double }
nonNegativeOctant :: Predicate Point
= adapt >$< nonNegative >*< nonNegative >*< nonNegative
nonNegativeOctant where
Point{ x, y, z } = (x, (y, z))
adapt
-- | This operator will be available in the next `contravariant` release
(>*<) :: Divisible f => f a -> f b -> f (a, b)
>*<) = divided
(
infixr 5 >*<
This code takes a nonNegative
Predicate
on Double
s that returns True
if the double is non-negative and then uses co-Applicative
(Divisible
) style to create a nonNegativeOctant
Predicate
on Point
s that returns True
if all three coordinates of a Point
are non-negative.
The key part to zoom in on is the nonNegativeOctant
Predicate
, whose implementation superficially resembles the Applicative
style that we know and love:
= adapt >$< nonNegative >*< nonNegative >*< nonNegative nonNegativeOctant
The difference is that instead of the <$>
and <*>
operators we use >$<
and >*<
, which are their evil twins dual operators1. For example, you can probably see the resemblance to the following code that uses Applicative
style:
readDouble :: IO Double
= readLn
readDouble
readPoint :: IO Point
= Point <$> readDouble <*> readDouble <*> readDouble readPoint
Types
I’ll walk through the types involved to help explain how this style works.
First, we will take this expression:
= adapt >$< nonNegative >*< nonNegative >*< nonNegative nonNegativeOctant
… and explicitly parenthesize the expression instead of relying on operator precedence and associativity:
= adapt >$< (nonNegative >*< (nonNegative >*< nonNegative)) nonNegativeOctant
So the smallest sub-expression is this one:
nonNegative >*< nonNegative
… and given that the type of nonNegative
is:
nonNegative :: Predicate Double
… and the type of the (>*<)
operator is:
(>*<) :: Divisible f => f a -> f b -> f (a, b)
… then we can specialize the f
in that type to Predicate
(since Predicate
implements the Divisible
class):
(>*<) :: Predicate a -> Predicate b -> Predicate (a, b)
… and further specialize a
and b
to Double
:
(>*<) :: Predicate Double -> Predicate Double -> Predicate (Double, Double)
… and from that we can conclude that the type of our subexpression is:
>*< nonNegative
nonNegative :: Predicate (Double, Double)
In other words, nonNegative >*< nonNegative
is a Predicate
whose input is a pair of Double
s.
We can then repeat the process to infer the type of this larger subexpression:
>*< (nonNegative >*< nonNegative))
nonNegative :: Predicate (Double, (Double, Double))
In other words, now the input is a nested tuple of three Double
s.
However, we want to work with Point
s rather than nested tuples, so we pre-process the input using >$<
:
>$< (nonNegative >*< (nonNegative >*< nonNegative))
adapt where
adapt :: Point -> (Double, (Double, Double))
Point{ x, y, z } = (x, (y, z)) adapt
… and this works because the type of >$<
is:
(>$<) :: Contravariant f => (a -> b) -> f b -> f a
… and if we specialize f
to Predicate
, we get:
(>$<) :: (a -> b) -> Predicate b -> Predicate a
… and we can further specialize a
and b
to:
>$<)
( :: (Point -> (Double, (Double, Double)))
-> Predicate (Double, (Double, Double))
-> Predicate Point
… which implies that our final type is:
nonNegativeOctant :: Predicate Point
= adapt >$< (nonNegative >*< (nonNegative >*< nonNegative))
nonNegativeOctant where
Point{ x, y, z } = (x, (y, z)) adapt
Duals
We can better understand the relationship between the two sets of operators by studying their types:
-- | These two operators are dual to one another:
(<$>) :: Functor f => (a -> b) -> f a -> f b
(>$<) :: Contravariant f => (a -> b) -> f b -> f a
-- | These two operators are similar in spirit, but they are not really dual:
(<*>) :: Applicative f => f (a -> b) -> f a -> f b
(>*<) :: Divisible f => f a -> f b -> f (a, b)
Okay, so (>*<)
is not exactly the dual operator of (<*>)
. (>*<)
is actually dual to liftA2 (,)
2:
(>*<) :: Divisible f => f a -> f b -> f (a, b)
:: Applicative f => f a -> f b -> f (a, b) liftA2 (,)
In fact, if we were to hypothetically redefine (<*>)
to be liftA2 (,)
then we could write Applicative
code that is even more symmetric to the Divisible
code (albeit less ergonomic):
import Control.Applicative (liftA2)
import Prelude hiding ((<*>))
<*>) = liftA2 (,)
(
infixr 5 <*>
readDouble :: IO Double
= readLn
readDouble
readPoint :: IO Point
= adapt <$> readDouble <*> readDouble <*> readDouble
readPoint where
= Point{ x, y, z }
adapt (x, (y, z))
-- Compare to:
nonNegativeOctant :: Predicate Point
= adapt >$< nonNegative >*< nonNegative >*< nonNegative
nonNegativeOctant where
Point{ x, y, z } = (x, (y, z)) adapt
It would be nice if we could create a (>*<)
operator that was dual to the real (<*>)
operator, but I could not figure out a good way to do this.
If you didn’t follow all of that, the main thing you should take away from this going into the next section is:
- the
Contravariant
class is the dual of theFunctor
class - the
Divisible
class is the dual of theApplicative
class
Syntactic sugar
GHC supports the ApplicativeDo
extension, which lets you use do
notation as syntactic sugar for Applicative
operators. For example, we could have written our readPoint
function like this:
{-# LANGUAGE ApplicativeDo #-}
readPoint :: IO Point
= do
readPoint <- readDouble
x <- readDouble
y <- readDouble
z return Point{ x, y, z }
… which behaves in the exact same way. Actually, we didn’t even need the ApplicativeDo
extension because IO
has a Monad
instance and anything that has a Monad
instance supports do
notation without any extensions.
However, the ApplicativeDo
language extension does change how the do
notation is desugared. Without the extension the above readPoint
function would desugar to:
=
readPoint >>= \x ->
readDouble >>= \y ->
readDouble >>= \z ->
readDouble return Point{ x, y, z }
… but with the ApplicativeDo
extension the function instead desugars to only use Applicative
operations instead of Monad
operations:
-- I don't know the exact desugaring logic, but I imagine it's similar to this:
= adapt <$> readDouble <*> readDouble <*> readDouble
readPoint where
= Point{ x, y, z } adapt x y z
So could there be such a thing as “DivisibleDo
” which would introduce syntactic sugar for Divisible
operations?
I think there could be such an extension, and there are several ways you could design the user experience.
One approach would be to permit code like this:
{-# LANGUAGE DivisibleFrom #-}
nonNegativeOctant :: Predicate Point
=
nonNegativeOctant Point{ x, y, z }
from -> nonNegative
x -> nonNegative
y -> nonNegative z
… which would desugar to the original code that we wrote:
= adapt >$< nonNegative >*< nonNegative >*< nonNegative
nonNegativeOctant where
Point{ x, y, z } = (x, (y, z)) adapt
Another approach could be to make the syntax look exactly like do
notation, except that information flows in reverse:
{-# LANGUAGE DivisibleDo #-}
nonNegativeOctant :: Predicate Point
= do
nonNegativeOctant <- nonNegative
x <- nonNegative
y <- nonNegative
r return Point{ x, y, z } -- `return` here would actually be a special keyword
I assume that most people will prefer the from
notation, so I’ll stick to that for now.
If we were to implement the former DivisibleFrom
notation then the Divisible
laws stated using from
notation would become:
-- Left identity
from x-> m
x -> conquer
x
= m
-- Right identity
from x-> conquer
x -> m
x
= m
-- Associativity
from (x, y, z)-> from (x, y)
(x, y) -> m
x -> n
y -> o
z
= from (x, y, z)
-> m
x -> from (y, z)
(y, z) -> n
y -> o
z
= from (x, y, z)
-> m
x -> n
y -> o z
This explanation of how DivisibleFrom
would work is really hand-wavy, but if people were genuinely interested in such a language feature I might take a stab at making the semantics of DivisibleFrom
sufficiently precise.
History
The original motivation for the (>*<)
operator and Divisible
style was to support compositional RecordEncoder
s for the dhall
package.
Dhall’s Haskell API defines a RecordEncoder
type which specifies how to convert a Haskell record to a Dhall syntax tree, and we wanted to be able to use the Divisible
operators to combine simpler RecordEncoder
s into larger RecordEncoder
s, like this:
data Project = Project
name :: Text
{ description :: Text
, stars :: Natural
,
}
injectProject :: Encoder Project
=
injectProject
recordEncoder>$< encodeFieldWith "name" inject
( adapt >*< encodeFieldWith "description" inject
>*< encodeFieldWith "stars" inject
)where
Project{..} = (name, (description, stars)) adapt
The above example illustrates how one can assemble three smaller RecordEncoder
s (each of the encodeFieldWith
functions) into a RecordEncoder
for the Project
record by using the Divisible
operators.
If we had a DivisibleFrom
notation, then we could have instead written:
=
injectProject Project{..}
recordEncoder from -> encodeFieldWith "name" inject
name -> encodeFieldWith "description" inject
description -> encodeFieldWith "stars" inject stars
If you’d like to view the original discussion that led to this idea you can check out the original pull request.
Conclusion
I upstreamed this (>*<)
operator into the contravariant
package, which means that you’ll be able to use the trick outlined in this post after the next contravariant
release.
Until then, you can define your own (>*<)
operator inline within your own project, which is what dhall
did while waiting for the operator to be upstreamed.
Alright, they’re not categorically dual in a rigorous sense, but I couldn’t come up with a better term to describe their relationship to the original operators.↩︎
I feel like
liftA2 (,)
should have already been added toControl.Applicative
by now since I believe it’s a pretty fundamental operation from a theoretical standpoint.↩︎