+ <.icon name="hero-exclamation-circle-mini" class="mt-0.5 h-5 w-5 flex-none" />
+ <%= render_slot(@inner_block) %>
+
+ """
+ end
+
+ @doc """
+ Renders a header with title.
+ """
+ attr :class, :string, default: nil
+
+ slot :inner_block, required: true
+ slot :subtitle
+ slot :actions
+
+ def header(assigns) do
+ ~H"""
+
+ <.link
+ navigate={@navigate}
+ class="text-sm font-semibold leading-6 text-zinc-900 hover:text-zinc-700"
+ >
+ <.icon name="hero-arrow-left-solid" class="h-3 w-3" />
+ <%= render_slot(@inner_block) %>
+
+
+ """
+ end
+
+ @doc """
+ Renders a [Heroicon](https://heroicons.com).
+
+ Heroicons come in three styles – outline, solid, and mini.
+ By default, the outline style is used, but solid and mini may
+ be applied by using the `-solid` and `-mini` suffix.
+
+ You can customize the size and colors of the icons by setting
+ width, height, and background color classes.
+
+ Icons are extracted from your `assets/vendor/heroicons` directory and bundled
+ within your compiled app.css by the plugin in your `assets/tailwind.config.js`.
+
+ ## Examples
+
+ <.icon name="hero-x-mark-solid" />
+ <.icon name="hero-arrow-path" class="ml-1 w-3 h-3 animate-spin" />
+ """
+ attr :name, :string, required: true
+ attr :class, :string, default: nil
+
+ def icon(%{name: "hero-" <> _} = assigns) do
+ ~H"""
+
+
Effect Systems
+
20 Mar 2022
+
+
As I’ve begun exploring the world of so-called algebraic
+ effect systems , I’ve become increasingly frustrated in the
+ level of documentation around them. Learning to use them (and moreso
+ understanding how they work) requires diving into library internals,
+ watching various videos, and hoping to grok why certain effects aren’t
+ being interpreted the way you might have hoped. My goal in this post
+ is to address this issue, at least to some degree, in a focused,
+ pedagogical fashion. fused-effects
+ library, chosen because it seems to have the most active development,
+ the smallest dependency footprint, and minimal type machinery. In
+ turn, this library was largely inspired by Nicolas Wu, Tom Schrijvers,
+ and Ralf Hinze’s work in Effect Handlers in
+ Scope . As such, we’ll discuss choice parts of this paper as well.
+ this git
+ repository .
+
+
+
+
+
♤♠♤♠♤
+
Free Monads
+
To begin our exploration, let’s pose a few questions:
+
+ How can we go about converting a simple algebraic data type into a
+ monad?
+ Does there exist some set of minimal requirements the data type
+ must fulfill to make this conversion “free”?
+
+
To help guide our decision making, we’ll examine the internals of
+ some arbitrary monad. More concretely, let’s see what
+ 1 + 2 could look like within a monadic context:
+
onePlusTwo :: forall m. Monad m => m Int = do <- pure 1 <- pure 2 pure $ a + b
+
The above won’t win any awards, but it should be illustrative
+ enough for our purposes. do is just syntactic sugar for
+ repeated bind applications (>>=), so we could’ve
+ written the above alternatively as:
+
onePlusTwo' :: forall m. Monad m => m Int = pure 1 >>= (\a -> pure 2 >>= (\b -> pure (a + b)))
+
This is where we’ll pause for a moment and squint. We see that
+ do syntax desugars into something that looks awfully
+ close to a (non-empty) list! Let’s compare the above with how we might
+ define that:
+
data NonEmptyList a = Last a | Cons a (a -> NonEmptyList a)onePlusTwo'' :: NonEmptyList Int = Cons 1 (\a -> Cons 2 (\b -> Last (a + b)))runNonEmptyList :: NonEmptyList Int -> Int Last a) = aCons a f) = runNonEmptyList (f a)-- >>> runIdentity onePlusTwo' -- 3 -- >>> runNonEmptyList onePlusTwo'' -- 3
+
Take a moment to appreciate the rough pseudo-equivalence of
+ NonEmptyList and a monad. Also take a moment to
+ appreciate the differences. Because we no longer employ the bind
+ operator anywhere within our function definitions, we have effectively
+ separated the syntax of our original function from
+ its semantics . That is, onePlusTwo'' can
+ be viewed as a program in and of itself, and the
+ runNonEmptyList handler can be viewed as
+ the interpretation of said program.
+
Making a Monad
+
NonEmptyList was formulated from a monad, so it’s
+ natural to think perhaps it too is a monad. Unfortunately this is not
+ the case - it isn’t even a functor! Give it a try or use
+ {-# LANGUAGE DeriveFunctor #-} to ask the compiler to
+ make an attempt on your behalf.
+ <.tip>
+
Type variable a is said to be contravariant with
+ respect to Cons. That is, a resides in a negative
+ position within Cons’s function.
+
+
If we can’t make this a monad as is, are there a minimal number of
+ changes we could introduce to make it happen? Ideally our changes
+ maintain the “shape” of the data type as much as possible, thereby
+ maintaining the integrity behind the original derivation. Since our
+ current roadblock stems from type variable a’s position
+ in Cons, let’s see what happens if we just abstract it
+ away:
+
data NonEmptyList' f a = Last' a | Cons' a (f (NonEmptyList' f a))
+
With general parameter f now in the place of
+ (->) a, a functor derivation becomes possible provided
+ f is also a Functor:
+
instance (Functor f) => Functor (NonEmptyList' f) where fmap f (Last' a) = Last' (fmap f a)fmap f (Cons' a ts) = Cons' (f a) (fmap (fmap f) g)
+
And though we needed to modify our syntax and semantics slightly,
+ the proposed changes do not lose us out on anything of real
+ consequence:
+
twoPlusThree :: NonEmptyList' (Reader Int ) Int = Cons' 2 (reader (\a -> Cons' 3 (reader (\b -> Last' (a + b)))))runNonEmptyList' :: NonEmptyList' (Reader Int ) Int -> Int Last' a) = aCons' a f) = runNonEmptyList' (runReader f a)-- >>> runNonEmptyList' twoPlusThree -- 5
+
Compare the above snippet with onePlusTwo'.
+
+
The Applicative instance is slightly more involved so
+ we’ll hold off on that front for the time-being. For the sake of
+ forging ahead though, assume it exists. With the Functor
+ instance established and the Applicative instance
+ assumed, we are ready to tackle writing the Monad
+ instance. A first attempt would probably look like the following:
+
instance (Functor f) => Monad (NonEmptyList' f) where (>>=) :: NonEmptyList' f a -> (a -> NonEmptyList' f b) -> NonEmptyList' f bLast' a >>= g = g aCons' a f >>= g = Cons' _ (fmap (>>= g) f)
+
Defining bind (>>=) on Last' is
+ straightforward, but Cons' again presents a problem. With
+ g serving as our only recourse of converting an
+ a into anything, how should we fill in the hole
+ (_)? One approach could be:
+
instance (Functor f) => Monad (NonEmptyList' f) where Cons' a f >>= g = let ts = fmap (>>= g) fin case g a of Last' b -> Cons' b tsCons' b f' -> Cons' b (f' <> ts)
+
but this is pretty unsatisfactory. This definition requires a
+ Semigroup constraint on f, which in turn
+ requires some lifting operator. After all, how else could we append
+ Last a1 <> Last a2 together? Suddenly the list of
+ constraints on f is growing despite our best intentions.
+ Let’s take a step back and see if there is something else we can
+ try.
+
The insight falls from the one constraint we had already added
+ (admittedly without much fanfare). That is, we are requiring type
+ variable f to be a Functor! With this in
+ mind, we can actually massage our first parameter into a
+ bind-compatible one by simply omitting it altogether.
+
To elaborate, it is well
+ known simple algebraic data types are isomorphic to “primitive”
+ functors (Identity and Const) and that
+ (co)products of functors yield more functors. We can therefore
+ “absorb” the syntax of a into f by
+ using a product type as a container of sorts:
+
data NonEmptyList'' f a = Last'' a | Cons'' (f (NonEmptyList'' f a))data Container a m k = Container a (m k) deriving Functor threePlusFour :: NonEmptyList'' (Container Int (Reader Int )) Int = Cons'' Container 3 (reader (\a -> Cons'' Container 4 (reader (\b -> Last'' (a + b)))))))runNonEmptyList'' :: NonEmptyList'' (Container Int (Reader Int )) Int -> Int Last'' a) = aCons'' (Container a f)) = runNonEmptyList'' (runReader f a)-- >>> runNonEmptyList'' threePlusFour -- 7
+
The above demonstrates NonEmptyList' was in fact
+ overly specific for our purposes. By generalizing further still, we
+ lose no expressivity and gain the capacity to finally write our
+ Monad instance:
+
instance (Functor f) => Monad (NonEmptyList'' f) where Last'' a >>= g = g aCons'' f >>= g = Cons'' (fmap (>>= g) f)
+
Making an
+ Applicative
+
The NonEmptyList'' variant actually has another well
+ known name within the community:
+
data Free f a = Pure a | Free (f (Free f a))
+
We favor this name over NonEmptyList'' from here on
+ out. In the last section we deferred writing the
+ Applicative instance for Free but we can now
+ present its implementation. First, let’s gather some intuition around
+ how we expect it to work by monomorphizing Free over
+ Maybe and Int:
+
>>> a = Free (Just (Free (Just (Pure (+ 1 )))))>>> b = Pure 5 >>> c = Free (Just (Pure 5 ))
+
What should the result of a <*> b be? An
+ argument could probably be made for either:
+
+ Free (Just (Free (Just (Pure 6))))Pure 6
+
What about for a <*> c? In this case, any one of
+ the three answers is a potentially valid possibility:
+
+ Free (Just (Free (Just (Free (Just (Pure 6))))))Free (Just (Free (Just (Pure 6))))Free (Just (Pure 6))
+
This ambiguity is why we waited until we finished defining the
+ Monad instance. Instead of trying to reason about which
+ instance makes sense, we choose the interpretation that aligns with
+ our monad.
+
ap :: forall f a b. Functor f => Free f (a -> b) -> Free f a -> Free f b= do <- f<- gpure (f' g')
+
Examining the results of ap a b and
+ ap a c, we determine the first entries of the above two
+ lists must be the answer. Thus it is consistent to define our
+ Applicative like so:
+
instance (Functor f) => Applicative (Free f) where pure = Pure Pure f <*> g = fmap f gFree f <*> g = Free (fmap (<*> g) f)
+
Algebraic Data
+ Types
+
Let’s revisit our original questions:
+
+
+ How can we go about converting a simple algebraic data type into a
+ monad?
+ Does there exist some set of minimal requirements the data type
+ must fulfill to make this conversion “free”?
+
+
+
We have shown that a data type must be a Functor for
+ us to build up a Free monad. Additionally, as mentioned earlier , simple algebraic data
+ types are already functors, thereby answering both questions.
+ To drive this point home, consider the canonical Teletype
+ example:
+
data Teletype k = Read k | Write String k deriving Functor
+
Armed with this data type, we can generate programs using the
+ Teletype DSL. For instance,
+
read :: Free Teletype String read = Free (Read (Pure "hello" ))write :: String -> Free Teletype ()= Free (Write s (Pure ()))readThenWrite :: Free Teletype ()= do <- read
+
Smart constructors read and write are
+ included to abstract away the boilerplate and help highlight
+ readThenWrite’s role of syntax. Invoking this function
+ does not actually do anything, but reading the function makes
+ it very obvious what we at least want it to do. A
+ corresponding handler provides the missing semantics:
+
runReadThenWrite :: Free Teletype () -> IO ()Free (Write s f)) = putStrLn s >> runReadThenWrite fFree (Read f)) = runReadThenWrite fPure _) = pure ()
+
Composing Effects
+
Though neither impressive nor particularly flexible,
+ readThenWrite is an example of a DSL corresponding to our
+ Teletype effect . This is only half the
+ battle though. As mentioned at the start, we want to be able to
+ compose effects together within the same program. After all, a program
+ with just one effect doesn’t actually end up buying us much except a
+ lot of unnecessary abstraction.
+
As we begin our journey down this road, let’s depart from
+ Teletype and meet up with hopefully a familiar
+ friend:
+
data State s k = Get (s -> k) | Put s kderiving Functor
+
In the above snippet, State has been rewritten from
+ our usual MTL-style to a pseudo continuation-passing style compatible
+ with Free. An example handler might look like:
+
runState :: forall s a. s -> Free (State s) a -> (s, a)Free (Get f)) = runState s (f s)Free (Put s' f)) = runState s' fPure a) = a
+
We can then run this handler on a sample program like so:
+
increment :: Free (State Int ) ()= Free (Get (\s -> Free (Put (s + 1 ) (Pure ()))))-- >>> runState 0 increment -- (1, ())
+
Let’s raise the ante a bit. Suppose now we wanted to pass around a
+ second state, e.g. a String. How might we go about doing
+ this? Though we could certainly rewrite increment to have
+ state (Int, String) instead of Int, this
+ feels reminiscient to the expression
+ problem . Having to update and recompile every one of our programs
+ every time we introduce some new effect is a maintenance burden we
+ should not settle on shouldering. Instead, we should aim to write all
+ of our programs in a way that doesn’t require modifying source.
+
Sum Types
+
Let’s consider what it would take to compose effects
+ State Int and State String together. In the
+ world of data types, we usually employ either products or coproducts
+ to bridge two disjoint types together. Let’s try the latter and see
+ where we end up:
+
data (f :+: g) k = L (f k) | R (g k)deriving (Functor , Show )infixr 4 :+:
+
This allows us to join types in the following manner:
+
>>> L (Just 5 ) :: (Maybe :+: Identity ) Int L (Just 5 )>>> R (Identity 5 ) :: (Maybe :+: Identity ) Int R (Identity 5 )
+
We call this chain of functors a signature . We can
+ compose a signature containing our Int and
+ String state as well as a handler capable of interpreting
+ it:
+
:: forall s1 s2 a. s1-> s2-> Free (State s1 :+: State s2) a-> (s1, s2, a)Free (L (Get f))) = runTwoState s1 s2 (f s1)Free (R (Get f))) = runTwoState s1 s2 (f s2)Free (L (Put s1 f))) = runTwoState s1 s2 fFree (R (Put s2 f))) = runTwoState s1 s2 fPure a) = (s1, s2, a)
+
It’s functional but hardly a solution. It requires manually writing
+ every combination of effects introduced by :+: - a
+ straight up herculean task as the signature gets longer. It also does
+ not address the “expression problem”. That said, it does
+ provide the scaffolding for a more polymorphic solution. We can bypass
+ this combinatorial explosion of patterns by focusing on just one
+ effect at a time, parameterizing the remainder of the signature.
+ Handlers can then “peel” an effect off a signature, over and over,
+ until we are out of effects to peel:
+
runState' :: forall s a sig. Functor sig => -> Free (State s :+: sig) a -> Free sig (s, a)Pure a) = pure (s, a)Free (L (Get f))) = runState' s (f s)Free (L (Put s f))) = runState' s fFree (R other)) = Free (fmap (runState' s) other)
+
The above function combines the ideas of runState and
+ runTwoState into a more general interface. Now programs
+ containing State effects in any order can be interpreted
+ by properly ordering the handlers:
+
threadedState :: Free (State Int :+: State String ) ()= Free (L (Get (\s1 -> Free (R (Get (\s2 -> Free (L (Put (s1 + 1 )Free (R (Put (s2 ++ "a" )Pure ()))))))))))))threadedState' :: Free (State String :+: State Int ) ()= ... -- >>> runState "" . runState' @Int 0 $ threadedState -- ("a",(1,())) -- >>> runState @Int 0 . runState' "" $ threadedState' -- (1,("a",()))
+
Membership
+
We can do better still. Our programs are far too concerned with the
+ ordering of their corresponding signatures. The only thing they should
+ care about is whether the effect exists at all. We can relax this
+ coupling by introducing a new recursive typeclass:
+
class Member sub sup where inj :: sub a -> sup a prj :: sup a -> Maybe (sub a)
+
Here sub is said to be a subtype of
+ sup. inj allows us to promote that subtype
+ to sup and prj allows us to dynamically
+ downcast back to sub. This typeclass synergizes
+ especially well with :+:. For instance, we expect
+ State Int to be a subtype of
+ State Int :+: State String. Importantly, we’d expect the
+ same for State String. Let’s consider how instances of
+ Member might look. First is reflexivity:
+
instance Member sig sig where = id = Just
+
This instance should be fairly straightforward. We want to be able
+ to cast a type to and from itself without issue. Next is
+ left-occurrence:
+
instance Member sig (sig :+: r) where = L L f) = Just f= Nothing
+
This is the pattern we’ve been working with up until now. Casting
+ upwards is just a matter of using the L data constructor
+ while projecting back down works so long as we are within the
+ L context. Likewise there exists a right-recursion
+ rule:
+
instance (Member sig r) => Member sig (l :+: r) where = R . injR g) = prj g= Nothing
+
Lastly, as a convenience, we introduce left-recursion:
+
instance Member sig (l1 :+: (l2 :+: r)) => Member sig ((l1 :+: l2) :+: r) where = case inj sub of L l1 -> L (L l1)R (L l2) -> L (R l2)R (R r) -> R r= case sup of L (L l1) -> prj (L l1)L (R l2) -> prj (R (L l2))R r -> prj (R (R r))
+
The above allows us to operate on a tree of types rather
+ than a list. We can read this as saying “subtying is not affected by
+ how :+: is associated.”
+ <.warning>
+
These instances will not compile as is. A mix of
+ TypeApplications and OVERLAPPING pragmas
+ must be used. Refer to the git repository
+ for the real implementation.
+
+
With the above instances in place, we can now create a more
+ flexible implementation of threadedState above:
+
data Void k deriving Functor run :: forall a. Free Void a -> aPure a) = a= error (pack "impossible" )threadedState'' :: Functor sig => Member (State Int ) sig => Member (State String ) sig => Free sig ()= Free (inj (Get @ Int (\s1 -> Free (inj (Get (\s2 -> Free (inj (Put (s1 + 1 )Free (inj (Put (s2 ++ "a" )Pure ()))))))))))))-- >>> run . runState' "" . runState' @Int 0 $ threadedState'' -- ("a",(1,())) -- >>> run . runState' @Int 0 . runState' "" $ threadedState'' -- (1,("a",()))
+
A few takeaways:
+
+ The program now stays polymorphic in type sig,
+ We no longer explicitly mention L or R
+ data constructors, and
+ We use run to peel away the final effect.
+
+
This flexibility grants us the ability to choose the order
+ we handle effects at the call site. By writing a few additional smart
+ constructors, we could have a nicer program still:
+
inject :: (Member sub sup) => sub (Free sup a) -> Free sup a= Free . injproject :: (Member sub sup) => Free sup a -> Maybe (sub (Free sup a))Free s) = prj s= Nothing get :: Functor sig => Member (State s) sig => Free sig s= inject (Get pure )put :: Functor sig => Member (State s) sig => s -> Free sig ()= inject (Put s (pure ()))threadedStateM'' :: Functor sig => Member (State Int ) sig => Member (State String ) sig => Free sig ()= do <- get @ Int <- get @ String + 1 )++ "a" )pure ()
+
Higher-Order Effects
+
This composition provides many benefits, but in certain situations
+ we end up hitting a wall. To continue forward, we borrow an example
+ from Effect Handlers in
+ Scope . In particular, we discuss exception handling and how we can
+ use a free monad to simulate throwing and catching exceptions.
+
newtype Throw e k = Throw e deriving (Functor )= inject (Throw e)
+ <.info>
+
To avoid too many distractions, we will sometimes skip writing type
+ signatures.
+
+
This Throw type should feel very intuitive at this
+ point. We take an exception and “inject” it into our program using the
+ throw smart constructor. What’s the
+ catch?
+
catch (Pure a) _ = pure acatch (Free (L (Throw e))) h = h ecatch (Free (R other)) h = Free (fmap (`catch` h) other)
+
In this scenario, catch traverses our program, happily
+ passing values through until it encounters a Throw. Our
+ respective “peel” looks like so:
+
runThrow :: forall e a sig. Free (Throw e :+: sig) a -> Free sig (Either e a)Pure a) = pure (Right a)Free (L (Throw e))) = pure (Left e)Free (R other)) = Free (fmap runThrow other)
+
We now have the requisite tools needed to build up and execute a
+ sample program that composes some State Int effect with a
+ Throw effect:
+
countDown :: forall sig. Functor sig => Member (State Int ) sig => Member (Throw ()) sig => Free sig ()= do {- 1 -} catch (decr {- 2 -} >> decr {- 3 -} ) pure where = do <- get @ Int if x > 0 then put (x - 1 ) else throw ()
+
This program calls a potentially dangerous decr
+ function three times, with the last two attempts wrapped around a
+ catch.
+
Scoping
+ Problems
+
How should the state of countDown be interpreted?
+ There exist two reasonable options:
+
+ If state is considered global , then successful
+ decrements in catch should persist. That is, our final state would be
+ the initial value decremented as many times as decr
+ succeeds.
+ If state is considered local , we expect
+ catch to decrement state twice but to rollback
+ if an error is raised. If an error is caught, our final state would be
+ the initial value decremented just the once.
+
+
This is what it means for an operation to be
+ scoped . In the local case, within the semantics of
+ exception handling, the nested program within catch
+ should not affect the state of the world outside of it in the case of
+ an exception. Let’s see if we can somehow write and invoke handlers
+ accordingly:
+
>>> run . runThrow @ () . runState' @ Int 3 $ countDownRight (0 ,())
+
The above snippet demonstrates a result we expect in either
+ interpretation. The nested decr >> decr raises no
+ error. Likewise
+
>>> run . runThrow @ () . runState' @ Int 0 $ countDownLeft ()
+
should also feel correct, regardless of interpretation.
+ decr {- 1 -} ends up returning a throw ()
+ which the subsequent runThrow handler interprets as
+ Left. What about the following?
+
>>> run . runThrow @ () . runState' @ Int 2 $ countDownRight (0 ,())
+
This is an example of a global interpretation. Here we throw an
+ error on decr {- 3 -} but decr {- 2 -}’s
+ effects persist despite existing within the catch. So can
+ we scope the operation? As it turns out, local semantics are out of
+ reach. “Flattening” the program hopefully makes the reason
+ clearer:
+
= Free (inj (Get @ Int (\x -> let a = \k -> if x > 0 then Free (inj (Put (x - 1 ) k)) else throw ()in a (catch (Free (inj (Get @ Int (\y -> let b = \k -> if y > 0 then Free (inj (Put (y - 1 ) k)) else throw ()in b (Free (inj (Get @ Int (\z -> let c = \k -> if z > 0 then Free (inj (Put (z - 1 ) k)) else throw ()in c (Pure ()))))))))) pure ))))
+
It’s noisy, but in the above snippet we see there exists no
+ mechanism that “saves” the state prior to running the nested
+ program.
+
A Stronger Free
+
Somehow we need to ensure a nested (e.g. the program scoped within
+ catch) does not “leak” in any way. To support programs
+ within programs (within programs within programs…) within the already
+ recursively defined free monad, we look towards a higher-level
+ abstraction for help. According to Wu, Schrijvers, and Hinze,
+
+ A more direct solution [to handle some self-contained context] is
+ to model scoping constructs with higher-order syntax, where the syntax
+ carries those syntax blocks directly.
+
+
What would such a change look like? To answer that, it proves
+ illustrative understanding why our current definition of
+ Free is insufficient. Consider what it means to “run” our
+ program. We have a handler that traverses the program, operates on
+ effects it knows how to operate on, and then returns a slightly less
+ abstract program for the next handler to process. To save state, we
+ somehow need each handler to refer to a context
+ containing state as defined by the handler prior.
+
As a starting point, review our current definition of
+ Free:
+
data Free f a = Pure a | Free (f (Free f a))
+
We see a is not something we, the effects library
+ author, are in a position to manipulate. To actually extract a value
+ to be saved and threaded in a context though, we at the very least
+ need this ability. So can we introduce some change that give us this
+ freedom? One idea is:
+
data Free f a = Pure a | Free (f (Free f) a)
+
The change is subtle but has potential provided we can get all the
+ derived type machinery working on this type instead. Take note!
+ Previously the kind of f was
+ Type -> Type. In this new definition, we see it is now
+ (Type -> Type) -> (Type -> Type). That is,
+ f is now a function that maps one type function to
+ another. We have entered the world of higher-order kinds.
+ <.info>
+
f is usually a natural transformation, mapping one
+ functor to another. The specifics regarding natural transformations
+ aren’t too important here. Just note when we use the term going
+ forward, we mean a functor to functor mapping.
+
+
Ideally we can extrapolate our learnings so far to this
+ higher-order world. Of most importance is our
+ Functor-constrained type variable f. Let’s
+ dive a bit deeper into what it currently buys us. First, take another
+ look at how fmap is used within Free’s
+ Monad instance:
+
instance (Functor f) => Monad (Free f) where Pure a >>= g = g aFree f >>= g = Free (fmap (>>= g) f)
+
Its purpose is to allow extending our syntax, chaining
+ different DSL terms together into a bigger program. When we write
+ e.g.
+
= do <- read
+
it is fmap that is responsible for piecing the
+ read and write together. Second, re-examine
+ a sample handler, e.g.
+
Pure a) = pure (s, a)Free (L (Get f))) = runState' s (f s)Free (L (Put s f))) = runState' s fFree (R other)) = Free (fmap (runState' s) other)
+
In this case, fmap is responsible for weaving
+ the state semantics throughout the syntax. This is what allows us to
+ interpret programs comprised of multiple different syntaxes. Whatever
+ we end up building at the higher level needs to keep both these
+ aspects in mind.
+
Higher-Order
+ Syntax
+
Syntax is the easier of the two to resolve so that’s where we’ll
+ first avert out attention. Extension requires two things:
+
+ A higher-level concept of a functor to constrain our new
+ f, and
+ An fmap-like function capable of performing the
+ extension.
+
+
Building out (1) is fairly straightforward. Since f
+ corresponds to a natural transformation, we create a mapping between
+ functors like so:
+
class HFunctor f where hmap :: Functor m, Functor n) => forall x. m x -> n x) -> forall x. f m x -> f n x)
+
This allows us to lift transformations of
+ e.g. Identity -> Maybe into
+ f Identity -> f Maybe. Take a moment to notice the
+ parallels between fmap and hmap. Building
+ (2) is equally simple:
+
class HFunctor f => Syntax f where emap :: (m a -> m b) -> (f m a -> f m b)
+
We designate emap as our fmap-extending
+ equivalent. This is made obvious by seeing how Free ends
+ up using emap:
+
instance Syntax f => Monad (Free f) where Pure a >>= g = g aFree f >>= g = Free (emap (>>= g) f)
+
Once again, note the parallels betwen the Monad
+ instances of both Frees.
+
Higher-Order
+ Semantics
+
The more difficult problem lies on the semantic side of the
+ equation. This part needs to manage the threading of functions
+ throughout potentially nested effects. To demonstrate, consider a
+ revision to our Throw type that includes a
+ Catch at the syntactic level:
+
data Error e m a = Throw e| forall x. Catch (m x) (e -> m x) (x -> m a)
+
We can create Error instances of our
+ HFunctor and Syntax classes as follows:
+
instance HFunctor (Error e) where Throw x) = Throw xCatch p h k) = Catch (t p) (t . h) (t . k)instance Syntax (Error e) where Throw e) = Throw eCatch p h k) = Catch p h (f . k)
+
This is all well and good, but now suppose we want to write a
+ handler in the same way we wrote runThrow earlier:
+
runError :: forall e a sig. Syntax sig => Free (Error e :+: sig) a -> Free sig (Either e a)Pure a) = pure (Right a)Free (L (Throw e))) = pure (Left e)Free (L (Catch p h k))) = >>= \case Left e -> >>= \case Left e' -> pure (Left e')Right a -> runError (k a)Right a -> runError (k a)Free (R other)) = Free _
+
Make sure everything leading up to the last pattern makes sense and
+ then ask yourself how you might fill in the hole (_). We
+ only have a few tools at our disposal, namely hmap and
+ emap. But, no matter how we choose to compose them,
+ hmap will let us down. In particular, our only means of
+ “peeling” the signature is runError which is incompatible
+ with the natural transformation hmap expects.
+
+
We need another function specific for this weaving behavior, which
+ we choose to add to the Syntax typeclass:
+
class HFunctor f => Syntax f where emap :: (m a -> m b) -> (f m a -> f m b) weave :: Monad m, Monad n, Functor ctx) => -> Handler ctx m n -> -> f n (ctx a))type Handler ctx m n = forall x. ctx (m x) -> n (ctx x)
+
Pay special attention to Handler. By introducing a
+ functorial context (i.e. ctx), we have defined a function
+ signature that more closely reflects that of runError.
+ This is made clearer by instantiating ctx to
+ Either e:
+
type Handler m n = forall x. Either e (m x) -> n (Either e x)runError :: Free (Error e :+: sig) a -> Free sig (Either e a)
+
Without ctx, weave would look just like
+ hmap, highlighting how it’s particularly well-suited to
+ bypassing the hmap’s limitations. With weave
+ also comes expanded Syntax instances:
+
instance (Syntax f, Syntax g) => Syntax (f :+: g) where L f) = L (weave ctx hdl f)R g) = R (weave ctx hdl g)instance Syntax (Error e) where Throw x) = Throw xCatch p h k) = -- forall x. Catch (m x) (e -> m x) (x -> m a) Catch fmap (const p) ctx))-> hdl (fmap (const (h e)) ctx)). fmap k)
+
const is used solely to wrap our results in a way that
+ hdl expects. With these instances fully defined, we can
+ now finish our runError handler:
+
Free (R other)) = Free $ weave (Right ()) (either (pure . Left ) runError) other
+
Lifting
+
The solution we’ve developed so far wouldn’t be especially useful
+ if it was weaker than the previous. As mentioned before, our new
+ solution splits the functionality of fmap into extension
+ and weaving. But nothing is stopping us from defining an instance that
+ continues using fmap for both. Consider the
+ following:
+
newtype Lift sig (m :: Type -> Type ) a = Lift (sig (m a))
+
Here sig refers to the lower-order data type we want
+ to elevate to our higher-order Free,
+ e.g. State s:
+
type HState s = Lift (State s)hIncrement :: Free (Lift (State Int )) ()= Free (Lift (Get (\s -> Free (Lift (Put (s + 1 ) (Pure ()))))))type HVoid = Lift Void run :: Free HVoid a -> aPure a) = a= error (pack "impossible" )
+
Here hIncrement is a lifted version of
+ increment defined before. Likewise, run
+ remains nearly identical to its previous definition. Making
+ Lift an instance of Syntax is a equally
+ straightforward:
+
instance Functor sig => HFunctor (Lift sig) where Lift f) = Lift (fmap t f)instance Functor sig => Syntax (Lift sig) where Lift f) = Lift (fmap t f)Lift f) = Lift (fmap (\p -> hdl (fmap (const p) ctx)) f)
+
The corresponding smart constructors and state handler should look
+ like before, but with our ctx now carrying the state
+ around:
+
get :: forall s sig. HFunctor sig => Member (HState s) sig => Free sig s= inject (Lift (Get Pure ))put :: forall s sig. HFunctor sig => Member (HState s) sig => s -> Free sig ()= inject (Lift (Put s (pure ())))runState :: forall s a sig. Syntax sig => -> Free (HState s :+: sig) a -> Free sig (s, a)Pure a) = pure (s, a)Free (L (Lift (Get f)))) = runState s (f s)Free (L (Lift (Put s f)))) = runState s fFree (R other)) = Free (weave (s, ()) hdl other)where hdl :: forall x. (s, Free (HState s :+: sig) x) -> Free sig (s, x)= uncurry runState
+
With all this in place, we can finally construct our
+ countDown example again:
+
countDown :: forall sig. Syntax sig => Member (HState Int ) sig => Member (Error ()) sig => Free sig ()= do {- 1 -} catch (decr {- 2 -} >> decr {- 3 -} ) pure where = do <- get @ Int if x > 0 then put (x - 1 ) else throw ()
+
Now if we encounter an error within our catch
+ statement, the local state semantics are respected:
+
>>> run . runError @ () . runState @ Int 2 $ countDownRight (1 ,())
+
Pay attention to why this works - we first use our
+ runState handler and eventually encounter
+ decr {- 3 -} which returns throw () instead
+ of put (x - 1). During this process, weave was invoked on
+ a Catch with context (s, ) used to maintain
+ the state at the time. Next runError is invoked which
+ sees the Catch, encounters the returned
+ Throw after running the scoped program, and invokes the
+ error handler which has our saved state.
+
Limitations
+
Though the higher-order free implementation is largely a useful
+ tool for managing effects, it is not perfect. I’ve had an especially
+ hard time getting resource-oriented effects working, e.g. with custom
+ effects like so:
+
data Server hdl conn (m :: * -> * ) k where Start :: SpawnOptions -> Server hdl conn m hdlStop :: hdl -> Server hdl conn m ExitCode GetPort :: hdl -> Server hdl conn m PortNumber Open :: Text -> PortNumber -> Server hdl conn m connClose :: conn -> Server hdl conn m ()
+
The issue here being running the custom Server handler
+ invokes start and stop when wrapped
+ in some bracket -like
+ interface, even if the bracketed code has not yet finished. I have
+ settled on workarounds, but these workarounds consist of just
+ structuring these kind of effects differently.
+
In general, modeling asynchronous or IO-oriented
+ operations feel “unsolved” with solutions resorting to some forklift
+ strategy or other ad-hoc solutions that don’t feel as cemented in
+ literature. I don’t necessarily think these are the wrong
+ approach (I frankly don’t know enough to have a real opinion here),
+ but it’d be nice to feel there was some consensus as to what a
+ non-hacky solution theoretically looks like.
+
Additionally, it is cumbersome remembering the order handlers
+ should be applied to achieve the desired global vs. local state
+ semantics. This is not exclusively a problem of free effect systems
+ (e.g. MTL also suffers from this), but the issue feels more prominent
+ here.
+
Conclusion
+
I will continue exploring effect systems à la free, but I am
+ admittedly not yet convinced they are the right way forward.
+ Unfortunately, they can be hard to reason about with unexpected
+ interactions between effects if not careful. I am sure a large
+ contributing factor to this conclusion is the lack of
+ beginner-oriented documentation regarding proper use and edge cases.
+ Just to build up this post required reading source code of multiple
+ effects libraries and scattered blog posts, watching various YouTube
+ videos, etc. And, despite all that, I am still not confident I
+ understand the implementation details behind certain key abstractions.
+ Hopefully this entry threads the needle between exposition and overt
+ jargon to get us a little closer though.
+
+
+
Tagless Final Parsing
+
25 Dec 2021
+
+
In his introductory
+ text , Oleg Kiselyov discusses the tagless final
+ strategy for implementing DSLs. The approach permits leveraging the
+ strong typing provided by some host language in a performant way. This
+ post combines key thoughts from a selection of papers and code written
+ on the topic. We conclude with an implementation of an interpreter for
+ a toy language that runs quickly, remains strongly-typed, and can be
+ extended without modification.
+
+
+
+
+
♤♠♤♠♤
+
Introduction
+
To get started, let’s write what our toy language will look
+ like.
+
digit = ? any number between 0-9 ? ;
+
+(* We ignore any leading 0s *)
+integer = digit, { digit } ;
+e_integer = [ e_integer, ("+" | "-") ]
+ , ( "(", e_integer, ")" | integer )
+ ;
+
+boolean = "true" | "false" ;
+e_boolean = [ e_boolean, ("&&" | "||") ]
+ , ( "(", e_boolean, ")" | boolean )
+ ;
+
+expr = e_integer | e_boolean ;
+
The above expresses addition, subtraction, conjunction, and
+ disjunction, to be interpreted in the standard way. All operations are
+ left-associative, with default precedence disrupted via parenthesis
+ (()). Our goal is to use megaparsec
+ to interpret programs in this language, raising errors on malformed or
+ invalidly-typed inputs. We will evaluate interpreter performance on
+ inputs such as those generated by
+
echo { 1 .. 10000000 } | sed 's/ / + /g' > input.txt
+ <.info>
+
To support inputs like above, ideally we mix lazy and strict
+ functionality. For example, we should lazily load in a file but
+ strictly evaluate its contents. Certain languages struggle without
+ this more nuanced evaluation strategy, e.g.
+
$ ( echo -n 'print(' && echo -n { 1 .. 10000000 } && echo ')' ) | sed 's/ / + /g' > input.py$ python3 input.pySegmentation fault: 11
+
Note it’d actually be more efficient on our end to not use
+ megaparsec at all! The library loads in the entirety of to-be-parsed
+ text into memory, but using it will hopefully be more representative
+ of projects out in the wild.
+
+
Initial Encoding
+
How might we instinctively choose to tackle an interpreter of our
+ language? As one might expect, megaparsec already has all the tooling
+ needed to parse expressions. We can represent our expressions and
+ results straightforwardly like so:
+
data Expr = EInt Integer | EBool Bool | EAdd Expr Expr | ESub Expr Expr | EAnd Expr Expr | EOr Expr Expr deriving (Show )data Result = RInt Integer | RBool Bool deriving (Eq )
+
We use a standard ADT to describe the structure of our program,
+ nesting the same data type recursively to represent precedence. For
+ instance, we would expect a (so-far fictional) function
+ parse to give us
+
>>> parse "1 + 2 + 3" EAdd (EAdd (EInt 1 ) (EInt 2 )) (EInt 3 )
+
We can then evaluate expressions within our Expr type.
+ Notice we must wrap our result within some Error-like
+ monad considering the ADT does not necessarily correspond to a
+ well-typed expression in our language.
+
asInt :: Result -> Either Text Integer RInt e) = pure e= Left "Could not cast integer." asBool :: Result -> Either Text Bool RBool e) = pure e= Left "Could not cast boolean." toResult :: Expr -> Either Text Result EInt e) = pure $ RInt eEBool e) = pure $ RBool eEAdd lhs rhs) = do <- toResult lhs >>= asInt<- toResult rhs >>= asIntpure $ RInt (lhs' + rhs')ESub lhs rhs) = do <- toResult lhs >>= asInt<- toResult rhs >>= asIntpure $ RInt (lhs' - rhs')EAnd lhs rhs) = do <- toResult lhs >>= asBool<- toResult rhs >>= asBoolpure $ RBool (lhs' && rhs')EOr lhs rhs) = do <- toResult lhs >>= asBool<- toResult rhs >>= asBoolpure $ RBool (lhs' || rhs')
+
With the above in place, we can begin fleshing out our first
+ parsing attempt. A naive solution may look as follows:
+
parseNaive :: Parser Result = expr >>= either (fail . unpack) pure . toResultwhere = E.makeExprParser term"+" EAdd , binary "-" ESub ]"&&" EAnd , binary "||" EOr ]= E.InfixL (f <$ symbol name)= parens expr <|> EInt <$> integer <|> EBool <$> boolean
+
There are certainly components of the above implementation that
+ raises eyebrows (at least in the context of large inputs), but that
+ could potentially be overlooked depending on how well it runs. Running
+ parseNaive against input.txt
+ shows little promise though:
+
$ cabal run --enable-profiling exe:initial-encoding -- input.txt +RTS -s 50000005000000 ... 4126 MiB total memory in use ( 0 MB lost due to fragmentation) ... Total time 25.541s ( 27.121s elapsed) ... Productivity 82.3% of total user, 78.9% of total elapsed
+
A few immediate takeaways from this exercise:
+
This solution
+
+ has to run through the generated AST twice. First to build the AST
+ and second to type-check and evaluate the code
+ (i.e. toResult).
+ is resource intensive. It consumes a large amount of memory
+ (approximately 4 GiB in the above run) and is far too
+ slow. A stream of 10,000,000 integers should be quick and cheap to sum
+ together.
+ is unsafe. Packaged as a library, there are no typing guarantees
+ we leverage from our host language. For example, expression
+ EAnd (EInt 1) (EInt 2) is valid.
+ suffers from the expression
+ problem . Developers cannot extend our language with new operations
+ without having to modify the source.
+
+
Let’s tackle each of these problems in turn.
+
Single Pass
+
Our naive attempt separated parsing from evaluation because they
+ fail in different ways. The former raises a
+ ParseErrorBundle on invalid input while the latter raises
+ a Text on mismatched types. Ideally we would have a
+ single error type shared by both of these failure modes.
+ Unfortunately, this is not so simple - the Operator types
+ found within makeExprParser have incompatible function
+ signatures. In particular, InfixL is defined as
+
InfixL :: m (a -> a -> a) -> Operator m a
+
instead of
+
InfixL :: (a -> a -> m a) -> Operator m a
+
To work around these limitations, we define our binary functions to
+ operate and return on values of type Either Text Expr. We
+ then raise a Left on type mismatch, deferring error
+ reporting at the Parser level until the current
+ expression is fully parsed:
+
parseSingle :: Parser Result = expr >>= either (fail . unpack) pure where = E.makeExprParser term"+" asInt EInt EAdd , binary "-" asInt EInt ESub ]"&&" asBool EBool EAnd , binary "||" asBool EBool EOr ]= E.InfixL do $ symbol namepure $ \lhs rhs -> do <- lhs >>= cast<- rhs >>= cast$ bin (f lhs') (f rhs')= parens expr <|> Right . RInt <$> integer <|> Right . RBool <$> boolean
+
Resource Usage
+
Though our above strategy avoids two explicit passes
+ through the AST, laziness sets it up so that we build this intertwined
+ callstack without actually evaluating anything until we interpret the
+ returned Result. The generated runtime statistics are
+ actually worse as a result:
+
cabal run --enable-profiling exe:initial-encoding -- \ -m single +RTS -s
+
We’ll use a heap profile to make the implementation’s shortcomings
+ more obvious:
+
cabal run --enable-profiling exe:initial-encoding -- \ -m single +RTS -hr
+ <.tip>
+
To iterate faster, reduce the number of integers in
+ input.txt. The resulting heap profile should remain
+ proportional to the original. Just make sure the program runs for long
+ enough to actually perform meaningful profiling. This section works on
+ inputs of 100,000 integers.
+
+
The generated heap profile, broken down by retainer set, looks as
+ follows:
+
+ parser-initial-100k-heap-hr-single
+
+
Our top-level expression parser continues growing in size until the
+ program nears completion, presumably when the expression is finally
+ evaluated. To further pinpoint the leaky methods, we re-run the heap
+ generation by cost-centre stack to get:
+
+ parser-initial-100k-heap-hc-single
+
+
Even our straightforward lexing functions are holding on to memory.
+ The laziness and left associative nature of our grammar hints that we
+ may be dealing with a thunk stack reminiscient of foldl . This
+ implies we could fix the issue by evaluating our data strictly with
+ e.g. deepseq . The
+ problem is unfortunately deeper than this though. Consider the
+ definition of InfixL ’s
+ parser:
+
pInfixL :: MonadPlus m => m (a -> a -> a) -> m a -> a -> m a= do <- op<- plet r = f x y<|> return r
+
Because this implementation uses the backtracking alternative
+ operator (<|>), we must also hold onto each
+ <|> return r in memory “just in case” we need to
+ use it. Since we are working with a left-factored
+ grammar, we can drop the alternatives and apply strictness with a
+ custom expression parser:
+
parseStrict :: Parser Result = term >>= exprwhere = do <- M.option Nothing $ Just <$> opscase op of Just OpAdd -> nest t asInt EInt EAdd Just OpSub -> nest t asInt EInt ESub Just OpAnd -> nest t asBool EBool EAnd Just OpOr -> nest t asBool EBool EOr -> pure t :: forall a. Result -> (Result -> Either Text a)-> (a -> Expr )-> (Expr -> Expr -> Expr )-> Parser Result = do <- term<- either (fail . unpack) pure do <- cast t<- cast t'$ bin (f lhs) (f rhs)`deepseq` expr a= do <- M.option Nothing $ Just <$> symbol "(" if isJust p then (term >>= expr) <* symbol ")" else RInt <$> integer <|> RBool <$> boolean
+
This implementation runs marginally faster and uses a constant
+ amount of memory:
+
+ parser-initial-100k-heap-hd-strict
+
+ <.info>
+
ARR_WORDS corresponds to the ByteString
+ constructor and is unavoidable so long as we use megaparsec.
+
+
To get a better sense of where runtime tends to reside, let’s
+ re-run our newly strict implementation on our 10,000,000 file again
+ alongside a time profile:
+
echo { 1 .. 10000000 } | sed 's/ / + /g' > input.txtcabal run --enable-profiling exe:initial-encoding -- \ -m strict +RTS -p
+
space Text.Megaparsec.Lexer Text/Megaparsec/Lexer.hs:(68,1)-(71,44) 54.9 57.3
+decimal Text.Megaparsec.Char.Lexer Text/Megaparsec/Char/Lexer.hs:363:1-32 24.7 21.4
+lexeme Text.Megaparsec.Lexer Text/Megaparsec/Lexer.hs:87:1-23 12.6 15.7
+ops Parser.Utils src/Parser/Utils.hs:(69,1)-(74,3) 2.6 2.7
+toResult Parser.Initial src/Parser/Initial.hs:(62,1)-(79,29) 2.3 2.2
+run Main app/Main.hs:(42,1)-(54,58) 1.6 0.6
+readTextDevice Data.Text.Internal.IO libraries/text/src/Data/Text/Internal/IO.hs:133:39-64 1.3 0.0
+
Surprisingly, the vast majority of time (roughly 95%) is spent
+ parsing. As such, we won’t worry ourselves about runtime any
+ further.
+
Type Safety
+
Let’s next explore how we can empower library users with a stricter
+ version of the Expr monotype. In particular, we want to
+ prohibit construction of invalid expressions. A common strategy is to
+ promote our ADT to a GADT:
+
data GExpr a where GInt :: Integer -> GExpr Integer GBool :: Bool -> GExpr Bool GAdd :: GExpr Integer -> GExpr Integer -> GExpr Integer GSub :: GExpr Integer -> GExpr Integer -> GExpr Integer GAnd :: GExpr Bool -> GExpr Bool -> GExpr Bool GOr :: GExpr Bool -> GExpr Bool -> GExpr Bool
+
By virtue of working with arbitrary, potentially mis-typed input,
+ we must eventually perform some form of type-checking on our
+ input. To get the GADT representation working requires additional
+ machinery like existential datatypes and Rank2Types. The
+ end user of our library reaps the benefits though, acquiring a
+ strongly-typed representation of our AST:
+
data Wrapper = forall a. Show a => Wrapper (GExpr a)parseGadt :: Parser Wrapper = term >>= exprwhere ... :: forall b. Show b=> Wrapper -> (forall a. GExpr a -> Either Text (GExpr b))-> (b -> GExpr b)-> (GExpr b -> GExpr b -> GExpr b)-> Parser Wrapper Wrapper t) cast f bin = do Wrapper t' <- termcase (cast t, cast t') of Right lhs, Right rhs) -> do let z = eval $ bin lhs rhs`seq` expr (Wrapper $ f z)Left e, _) -> fail $ unpack eLeft e) -> fail $ unpack e
+
We hide the full details here (refer to the linked Github
+ repository for the full implementation), but note the changes are
+ minimal outside of the signatures/data types required to make our
+ existentially quantified type work. Users of the parser can now unwrap
+ the Wrapper type and resume like normal.
+ <.warning>
+
This is an arguable "improvement" considering convenience
+ takes a dramatic hit. It is awkward working with the
+ Wrapper type.
+
+
Expression
+ Problem
+
Lastly comes the expression problem, and one that is fundamentally
+ unsolvable given our current implementation. By nature of (G)ADTs, all
+ data-types are closed . It is not extensible since that would
+ break any static type guarantees around e.g. pattern matching. To fix
+ this (and other problems still present in our implementation), we
+ contrast our initial encoding to that of tagless final.
+
Tagless Final
+
Let’s re-think our GADT example above and refactor it into a
+ typeclass:
+
class Symantics repr where eInt :: Integer -> repr Integer eBool :: Bool -> repr Bool eAdd :: repr Integer -> repr Integer -> repr Integer eSub :: repr Integer -> repr Integer -> repr Integer eAnd :: repr Bool -> repr Bool -> repr Bool eOr :: repr Bool -> repr Bool -> repr Bool
+
This should look familiar. Instances of GExpr have
+ been substituted by a parameter repr of kind
+ * -> *. Kiselyov describes typeclasses used this way
+ as a means of defining a class of interpreters . An example
+ interpreter could look like evaluation from before:
+
newtype Eval a = Eval {runEval :: a}instance Symantics Eval where = Eval = Eval Eval lhs) (Eval rhs) = Eval (lhs + rhs)Eval lhs) (Eval rhs) = Eval (lhs - rhs)Eval lhs) (Eval rhs) = Eval (lhs && rhs)Eval lhs) (Eval rhs) = Eval (lhs || rhs)
+
To belabor the similarities between the two a bit further, compare
+ the following two examples side-by-side:
+
let expr = foldl' eAdd (eInt 0 ) $ take count (eInt <$> [1 .. ])let expr = foldl' EAdd (EInt 0 ) $ take count (EInt <$> [1 .. ])
+
Outside of some capitalization, the encodings are exactly the same.
+ Considering these similarities, it’s clear type safety is not a
+ concern like it was with Expr. This new paradigm also
+ allows us to write both an implementation that parallels the memory
+ usage of above as well as a proper
+ solution to the expression problem. To follow along though first
+ requires a quick detour into leibniz equalities .
+
Leibniz
+ Equality
+
Leibniz equality states that two objects are equivalent provided
+ they can be substituted in all contexts without issue. Consider the
+ definition provided by the eq package:
+
newtype a := b = Refl {subst :: forall c. c a -> c b}
+
Here we are saying two types a and b
+ actually refer to the same type if it turns out that
+ simultaneously
+
Maybe a ~ Maybe bEither String a ~ Either String bIdentity a ~ Identity b...
+
and so on, where ~ refers to equality
+ constraints . Let’s clarify further with an example. Suppose we had
+ types A and B and wanted to ensure they were
+ actually the same type. Then there must exist a function
+ subst with signature c A -> c B for
+ all c. What might that function look like? It turns
+ out there is only one acceptable choice: id.
+
This might not seem particularly valuable at first glance, but what
+ it does permit is a means of proving equality at the
+ type-level and in a way Haskell’s type system respects. For instance,
+ the following is valid:
+
>>> import Data.Eq.Type ((:=)(..))>>> : set - XTypeOperators -- Type-level equality is reflexive. I can prove it since -- `id` is a suitable candidate for `subst`. >>> refl = Refl id >>> : t reflrefl :: b := b-- Haskell can verify our types truly are the same. >>> a = refl :: (Integer := Integer )>>> a = refl :: (Integer := Bool )< interactive>: 7 : 5 : error : Couldn't match type ‘Integer ’ with ‘Bool ’
+
We can also prove less obvious things at the type-level and take
+ advantage of this later on. As an exercise, consider how you might
+ express the following:
+
:: a1 := a2-> b1 := b2-> (a1 -> b1) := (a2 -> b2)
+
That is, if a1 and a2 are the same types,
+ and b1 and b2 are the same types, then
+ functions of type a1 -> b1 can equivalently be
+ expressed as functions from a2 -> b2.
+ <.accordion header="Answer">
+
I suggest reading from the bottom up to better understand why this
+ works.
+
import Data.Eq.Type ((:=)(..), refl)newtype F1 t b a = F1 {runF1 :: t := (a -> b)}newtype F2 t a b = F2 {runF2 :: t := (a -> b)} :: forall a1 a2 b1 b2. a1 := a2-> b1 := b2-> (a1 -> b1) := (a2 -> b2)Refl s1) -- s1 :: forall c. c a1 -> c a2 Refl s2) -- s2 :: forall c. c b1 -> c b2 = runF2 -- (a1 -> b1) := (a2 -> b2) . s2 -- F2 (a1 -> b1) a2 b2 . F2 -- F2 (a1 -> b1) a2 b1 . runF1 -- (a1 -> b1) := (a2 -> b1) . s1 -- F1 (a1 -> b1) b1 a2 . F1 -- F1 (a1 -> b1) b1 a1 $ refl -- (a1 -> b1) := (a1 -> b1)
+
+
Dynamics
+
Within our GADTs example, we introduced data type
+ Wrapper to allow us to pass around GADTs of internally
+ different type (e.g. GExpr Integer vs.
+ GExpr Bool) within the same context. We can do something
+ similar via Dynamics in the tagless final world. Though
+ we could use the already available dynamics
+ library, we’ll build our own for exploration’s sake.
+
First, let’s create a representation of the types in our
+ grammar:
+
class Typeable repr where pInt :: repr Integer pBool :: repr Bool newtype TQ t = TQ {runTQ :: forall repr. Typeable repr => repr t}instance Typeable TQ where = TQ pInt= TQ pBool
+
TQ takes advantage of polymorphic constructors to
+ allow us to wrap any compatible Typeable member function
+ and “reinterpret” it as something else. For example, we can create new
+ Typeable instances like so:
+
newtype AsInt a = AsInt (Maybe (a := Integer ))instance Typeable AsInt where = AsInt (Just refl)= AsInt Nothing newtype AsBool a = AsBool (Maybe (a := Bool ))instance Typeable AsBool where = AsBool Nothing = AsBool (Just refl)
+
We can then use TQ to check if something is of the
+ appropriate type:
+
>>> import Data.Maybe (isJust)>>> tq = pInt :: TQ Integer >>> case runTQ tq of AsInt a -> isJust aTrue >>> case runTQ tq of AsBool a -> isJust aFalse
+
Even more interestingly, we can bundle this type representation
+ alongside a value of the corresponding type, yielding our desired
+ Dynamic:
+
import qualified Data.Eq.Type as EQ data Dynamic repr = forall t. Dynamic (TQ t) (repr t)class IsDynamic a where type' :: forall repr. Typeable repr => repr a lift' :: forall repr. Symantics repr => a -> repr a cast' :: forall repr t. TQ t -> Maybe (t := a)instance IsDynamic Integer where = pInt= eIntTQ t) = case t of AsInt a -> ainstance IsDynamic Bool where = pBool= eBoolTQ t) = case t of AsBool a -> atoDyn :: forall repr a. IsDynamic a => Symantics repr => a -> Dynamic repr= Dynamic type' . lift'fromDyn :: forall repr a. IsDynamic a => Dynamic repr -> Maybe (repr a)Dynamic t e) = case t of -> r) -> do <- rpure $ EQ . coerce (EQ . lift r') e
+
+
>>> a = toDyn 5 :: Dynamic Expr >>> runExpr <$> fromDyn a :: Maybe Integer Just 5
+
By maintaining a leibniz equality within our Dynamic
+ instances (i.e. AsInt), we can internally coerce the
+ wrapped value into the actual type we care about. With this background
+ information in place, we can finally devise an expression parser
+ similar to the parser we’ve written using initial encoding:
+
:: forall repr. NFData (Dynamic repr)=> Symantics repr=> Parser (Dynamic repr)= term >>= exprwhere expr :: Dynamic repr -> Parser (Dynamic repr)= do <- M.option Nothing $ Just <$> opscase op of Just OpAdd -> nest t eAdd OpAdd Just OpSub -> nest t eSub OpSub Just OpAnd -> nest t eAnd OpAnd Just OpOr -> nest t eOr OpOr -> pure t :: forall a. IsDynamic a=> Dynamic repr-> (repr a -> repr a -> repr a)-> Op -> Parser (Dynamic repr)= do <- termcase binDyn bin t t' of Nothing -> fail $ "Invalid operands for `" <> show op <> "`" Just a -> a `deepseq` expr a term :: Parser (Dynamic repr)= do <- M.option Nothing $ Just <$> symbol "(" if isJust p then (term >>= expr) <* symbol ")" else <$> integer <|> toDyn <$> boolean
+
Interpretations
+
So far we’ve seen very little benefit switching to this strategy
+ despite the level of complexity this change introduces. Here we’ll
+ pose a question that hopefully makes at least one benefit more
+ obvious. Suppose we wanted to interpret the parsed expression in two
+ different ways. First, we want a basic evaluator, and second we want a
+ pretty-printer. In our initial encoding strategy, the evaluator has
+ already been defined:
+
+
We say eval is one possible interpreter over
+ GExpr. It takes in GExprs and reduces them
+ into literal values. How would a pretty printer work? One candidate
+ interpreter could look as follows:
+
pPrint :: GExpr a -> Text GInt e) = pack $ show eGBool e) = pack $ show eGAdd lhs rhs) = "(" <> pPrint lhs <> " + " <> pPrint rhs <> ")" ...
+
Unfortunately using this definition requires fundamentally changing
+ how our GADT parser works. parseGadt currently makes
+ certain optimizations based on the fact only eval has
+ been needed so far, reducing the expression as we traverse the input
+ stream. Generalizing the parser to take in any function of signature
+ forall b. (forall a. GExpr a) -> b (i.e. the signature
+ of some generic interpreter) would force us to retain memory or accept
+ additional arguments to make our function especially generic to
+ accommodate.
+
On the other hand, our tagless final approach expects multiple
+ interpretations from the outset. We can define a newtype
+ like
+
newtype PPrint a = PPrint {runPPrint :: a}instance Symantics PPrint where = PPrint . pack . show = PPrint . pack . show PPrint lhs) (PPrint rhs) = PPrint $ "(" <> lhs <> " + " <> rhs <> ")" ...
+
and interpret our
+
parseStrict :: forall repr. Symantics repr => Parser (Dynamic repr)
+
Parser as a Dynamic PPrint instead of a
+ Dynamic Eval without losing any previously acquired
+ gains.
+
Expression
+ Revisited
+
There does exist a major caveat with our tagless final
+ interpreters. If owning a single Dynamic instance, how
+ exactly are we able to interpret this in multiple ways? After all, a
+ Dynamic cannot be of type Dynamic Eval
+ and Dynamic PPrint. What we’d like to be able to
+ do is maintain a generic Dynamic repr and reinterpret it
+ at will.
+
One solution comes in the form of another newtype
+ around a polymorphic constructor:
+
newtype SQ a = SQ {runSQ :: forall repr. Symantics repr => repr a}instance Symantics SQ where = SQ (eInt e)= SQ (eBool e)SQ lhs) (SQ rhs) = SQ (eAdd lhs rhs)SQ lhs) (SQ rhs) = SQ (eSub lhs rhs)SQ lhs) (SQ rhs) = SQ (eAnd lhs rhs)SQ lhs) (SQ rhs) = SQ (eOr lhs rhs)
+
We can then run evaluation and pretty-printing on the same
+ entity:
+
data Result = RInt Integer | RBool Bool runBoth :: Dynamic SQ -> Maybe (Result , Text )= case fromDyn d of Just (SQ q) -> pure ( case q of Eval a -> RInt acase q of PPrint a -> aNothing -> case fromDyn d of Just (SQ q) -> pure ( case q of Eval a -> RBool acase q of PPrint a -> aNothing -> Nothing
+
This has an unintended side effect though. By using
+ SQ, we effectively close our type universe. Suppose we
+ now wanted to extend our Symantics type with a new
+ multiplication operator (*). We could do so by writing
+ typeclass:
+
class MulSymantics repr where eMul :: repr Integer -> repr Integer -> repr Integer instance MulSymantics Eval where Eval lhs) (Eval rhs) = Eval (lhs * rhs)instance MulSymantics PPrint where PPrint lhs) (PPrint rhs) = PPrint $ "(" <> lhs <> " * " <> rhs <> ")"
+ <.warning>
+
Naturally we also need to extend our parser to be aware of the new
+ operator as well. To avoid diving yet further into the weeds, we do
+ not do that here.
+
+
But this typeclass is excluded from our SQ type. We’re
+ forced to write yet another SQ-like wrapper, e.g.
+
newtype MSQ a = MSQ {runMSQ :: forall repr. MulSymantics repr => repr a}
+
just to keep up. This in turn forces us to redefine all functions
+ that operated on SQ.
+
Copy Symantics
+
We can reformulate this more openly, abandoning any sort of
+ Rank2 constructors within our newtypes by
+ choosing to track multiple representations simultaneously:
+
data SCopy repr1 repr2 a = SCopy (repr1 a) (repr2 a)instance (Symantics repr1, Symantics repr2)=> Symantics (SCopy repr1 repr2) where = SCopy (eInt e) (eInt e)= SCopy (eBool e) (eBool e)SCopy a1 a2) (SCopy b1 b2) = SCopy (eAdd a1 b1) (eAdd a2 b2)SCopy a1 a2) (SCopy b1 b2) = SCopy (eSub a1 b1) (eSub a2 b2)SCopy a1 a2) (SCopy b1 b2) = SCopy (eAnd a1 b1) (eAnd a2 b2)SCopy a1 a2) (SCopy b1 b2) = SCopy (eOr a1 b1) (eOr a2 b2)instance (MulSymantics repr1, MulSymantics repr2)=> MulSymantics (SCopy repr1 repr2) where SCopy a1 a2) (SCopy b1 b2) = SCopy (eMul a1 b1) (eMul a2 b2)
+
As we define new classes of operators on our Integer
+ and Bool types, we make SCopy an instance of
+ them. We can then “thread” the second representation throughout our
+ function calls like so:
+
:: forall repr. Dynamic (SCopy Eval repr)-> Maybe (Result , Dynamic repr)= case fromDyn d :: Maybe (SCopy Eval repr Integer ) of Just (SCopy (Eval a) r) -> pure (RInt a, Dynamic pInt r)Nothing -> case fromDyn d :: Maybe (SCopy Eval repr Bool ) of Just (SCopy (Eval a) r) -> pure (RBool a, Dynamic pBool r)Nothing -> Nothing :: forall repr. Dynamic (SCopy PPrint repr)-> Maybe (Text , Dynamic repr)= case fromDyn d :: Maybe (SCopy PPrint repr Text ) of Just (SCopy (PPrint a) r) -> pure (a, Dynamic pText r)Nothing -> Nothing :: forall repr. Dynamic (SCopy Eval (SCopy PPrint repr))-> Maybe (Result , Text , Dynamic repr)= do <- runEval' d<- runPPrint' d'pure (r, p, d'')
+
Notice each function places a Dynamic repr of unknown
+ representation in the last position of each return tuple. The caller
+ is then able to interpret this extra repr as they wish,
+ composing them in arbitrary ways (e.g. runBoth').
+
Limitations
+
The expression problem is only partially solved with our
+ Dynamic strategy. If for instance we wanted to add a new
+ literal type, e.g. a String, we would unfortunately need
+ to append to the Typeable and Dynamic
+ definitions to support them. The standard dynamics
+ package only allows monomorphic values so in this sense we are stuck.
+ If only needing to add additional functionality to the existing set of
+ types though, we can extend at will.
+
Conclusion
+
I was initially hoping to extend this post further with a
+ discussion around explicit sharing as noted here ,
+ but this post is already getting too long. I covered only a portion of
+ the topics Oleg Kiselyov wrote about, but covered at least the
+ majority of topics I’ve so far been exploring in my own personal
+ projects. I will note that the tagless final approach, while certainly
+ useful, also does add a fair level of cognitive overhead in my
+ experience. Remembering the details around dynamics especially is what
+ prompted me to write this post to begin with.
+
+
-
- 
-
-