I’ve spent a lot of time over the last few years thinking about the different classes we use for sequencing effects. The ones we have work pretty well, but I think we’re stuck in a local maxima right now and need to keep looking! Here’s a post encompassing my initial thoughts, more to come soon.
16 Likes
Nice explanation. Monads essentially allow you to do all that is possible in free-form imperative programming, but that is not needed in many use cases, we can use a less powerful (i.e. more restrictive) abstractions which give you other benefits.
An important point that I would want to highlight is the performance which is usually inversely proportional to the power of the abstraction. In many cases, Applicatives can potentially give you many times better performance than Monads, and this is because of the static analysis which allows the compiler to have better visibility at the compile time so that optimizations like stream fusion can occur.
For example, the crossWith operation in streamly is the applicative equivalent of concatMap, and it is order of magnitude faster due to fusion.
Similarly, the unfoldEach operation is less powerful than concatMap but it can fuse due to static visibility of the operation and provides many times better performance than concatMap. Because of the power it provides we cannot fuse concatMap and that is why we created the less powerful but fusible Unfold abstraction to address the nested fusion issue.
6 Likes
In my PhD research I wanted to write program transformations (e.g. optimizations) over free monads. Obviously that is not possible if we use the traditional continuation based representation, for example this:
data M a
= Pure a
| Get (Int -> M a)
| Put Int (M a)
The Int -> M a continuation in the Get constructor prevents analysis and transformation.
The solution I’m now working with uses explicit variables instead:
-- Well-typed De Bruijn indices
data Var e a where
Here :: Var (a : e) a
There :: Var e a -> Var (b : e) a
data M e a
= Pure (Var e a)
| Get (M (Int : e) a)
| Put (Var e Int) (M e a)
Now this representation is fully inspectable and transformable, but we’ve lost the ability to use Haskell functions to manipulate the variables directly. If we want to increment an integer, for example, we have to add arithmetic operations:
| Const Int (M (Int : e) a)
| Add (Var e Int) (Var e Int) (M (Int : e) a)
Another difficulty is that Haskellers like to write infinite coprograms, especially when using monads, but that also prevents inspection and transformation. To write any practical programs, we need to add some looping mechanism too:
| Repeat (Var e Int) (M e a)
Now we can write a nontrivial function:
-- compute 2 ^ n
exponentiate :: M (Int : e) Int
exponentiate =
Const 1 $
Put Here $
Repeat (There Here)
(Get $
Add Here Here $
Put Here $
Pure Here)
This is fully inspectable and transformable! The De Bruijn indices may make it look a bit ugly, but you can go pretty far with things like rebindable syntax to make it look much more like normal Haskell. Sadly, it is still quite limited. I wanted to define fibonacci numbers or the factorial function, but I think I need more than one state variable or some other kind of looping for that. That’s all possible to add, but it gets pretty complicated and it takes some work.
Zooming out, I also want to note that we are now basically defining a deeply embedded DSL. Is there still any benefit to using this free monad form or could we just as well write more traditional ASTs? I’m not sure.
5 Likes
Zooming out, I also want to note that we are now basically defining a deeply embedded DSL. Is there still any benefit to using this free monad form or could we just as well write more traditional ASTs? I’m not sure.
I’ll be exploring these ideas in greater detail in blog posts to come, but there are ways to model most Haskell programs using structured classes without needing to rely on →, which we can’t inspect.
Specifically I’ll be exploring and explaining how to use Category typeclass Hierarchies to model this, and how you can model looping and recursion using CoChoice and CoStrong constraints.
These are concrete, well-studied Category-Theory primitives which allow us to model infinite programs by representing For-loops/recursion and Fixed-point computations respectively. And because we capture the structure of the loop directly it doesn’t limit our ability to inspect the effects contained within, or get stuck in an infinite analysis loop.
Check out this talk I gave, it’s from 5 years ago so my opinions have changed a bit, most notably switching from a Profunctor class hierarchy to using the Category class hierarchy, and I’m relatively imprecise in my language and names for things, but most of the ideas still apply 
1 Like
That’s an interesting exploration, but it seems pretty much like the same thing.
Here’s how you could write the isPalindrome example using a DSL:
{-# LANGUAGE DataKinds #-}
data Var e a where
Here :: Var (a : e) a
There :: Var e a -> Var (b : e) a
data E e a where
(:$) :: E e (a -> b) -> E e a -> E e b
Lam :: E (a : e) b -> E e (a -> b)
Var :: Var e a -> E e a
PrimEq :: Eq a => E e (a -> a -> Bool)
PrimReverse :: E e (String -> String)
infixl :$
isPalindrome :: E e (String -> Bool)
isPalindrome = Lam (PrimEq :$ Var Here :$ (PrimReverse :$ Var Here))
Even nicer syntax with named variables
class e <= e' where
to :: Var e a -> Var e' a
instance e <= e where
to = id
instance {-# INCOHERENT #-} e <= e' => e <= (a : e') where
to = There . to
lam :: (Var (a : e) a -> E (a : e) b) -> E e (a -> b)
lam f = Lam (f Here)
var :: e <= e' => Var e a -> E e' a
var = Var . to
isPalindrome :: E e (String -> Bool)
isPalindrome = lam $ \xs -> PrimEq :$ var xs :$ (PrimReverse :$ var xs)
This can also be interpreted however you want.
You could even use typeclasses with the tagless final stye, but I’m not a huge fan of that. If you want to make this modular, just use Datatypes a la Carte.
You could also easily add a Y combinator for recursion:
Y :: E (a : e) a -> E e a
To me this seems more straightforward than going through all the category typeclasses.
We can’t use results from previous effects in future effects.
you can if you know all possibilities and just branch right? I guess it don’t work with infinite types?
We can’t express things like loops or recursion which require effects
If you know the amount of potential recursion beforehand, isn’t this also possible? Everything below infinity is fine?
The syntax for writing programs using Selective Applicatives is a bit rough, and there’s no do-notation equivalent.
Applicative do fails here I guess… Someone should pick that one up, it’s so useful.
1 Like
No because that would mean you know which m you have picked. Fwiw this is exactly what Selective gives you
2 Likes
I have thought the same thing, but I used a phoas encoding instead.
data Comp f -- ^ Type of the local variables
g -- ^ Type of the effects of the DSL
m -- ^ Type of the base monad
a where
-- Lift a Haskell-level action in m.
Pure :: m a -> Comp f g m a
-- Return a pure expression.
Return :: Expr f a -> Comp f g m a
-- Primitive bind: sequence two computations.
Bind :: Comp f g m a -> (f a -> Comp f g m b) -> Comp f g m b
-- Lift an effect of type g a into the computation.
LiftE :: g a -> Comp f g m a
2 Likes
Yes, exactly. Basically when a is finite in the sense that it can be enumerated or bisected, then you can bindS it.
I’d also have said that you can recurse! Obviously, you can just recurse in Haskell, but then static analysis of the program defined with recursion might hang, taking potentially infinite time to analyse it because the program itself may be infinite.
Maybe it would be interesting to have something analogous to MonadFix instead?
class Selective f => SelectiveFix f where
sfix :: (a -> f (Either a b)) -> f b
But that type signature just speculation. No idea whether there are sensible implementations that allow us to write programs we want. Maybe there is a better type signature for sfix.
Again, I agree. Programs like this should be desugarable into Selective:
main = do
number <- (readMaybe :: String -> Maybe Int) <$> getLine
case number of
Just _dontuseme -> putStrLn "Yes, that's a number"
Nothing -> putStrLn "Nope, not a number"
As long as we branch into ifs and cases, and don’t use bound variables in cases, it should work.
See Do you want a SelectiveDo proposal? · Issue #40 · snowleopard/selective · GitHub and Efficient SelectiveDo and binary search - #3 by turion for discussion.
2 Likes
Something funny I noticed, you can compose selective applicatives and get a selective applicative. Monads do not compose, but selective do.
I don’t think this is true for arrows though.
2 Likes