Open robrix opened 8 years ago
Some examples of equalities in Real a => Layout a (Size a)
that we’d like to be able to use to optimize:
identity laws
let empty = pure (Size 0 0)
inset (Size 0 0) x = x
offset (Point 0 0) x = x
stack empty x = x
stack x empty = x
adjacent x empty = x
adjacent empty x = x
distributive laws
inset s (offset p a) = offset p (inset s a)
align a b `stack` align a c = align a (b `stack` c)
align a b `adjacent` align a c = align a (b `adjacent` c)
associativity laws
(a `stack` b) `stack` c = a `stack` (b `stack` c)
(a `adjacent` b) `adjacent` c = a `adjacent` (b `adjacent` c)
Per a conversation with Jeremy Gibbons at ICFP2016, one approach might be to add a constructor to Freer encoding the Applicative
operation (either <*>
or liftA2
; they’re equivalent, and pure
is already represented in Freer
). Jeremy presented his paper Free Delivery, which focuses on batching network requests. This can’t be done with free monads, for the same reason discussed at top, but can with free applicatives.
In the questions following the talk, @simonmar asked about comparisons to the Haxl monad [1, 2, 3], which also addresses this problem, allowing both batched (applicative) and dependent (monadic) requests. I don’t think the implementation of the Haxl monad at [2] will apply directly to this domain (tho note that at [3], @simonmar uses Haxl to develop a parallel build system, and further that it plays nicely with GADTs). Even if not, it’s possible that its approach will, so that’s another promising avenue.
We’d like to be able to aggressively optimize languages by applying certain equalities to reduce the term tree. However, you can’t in general do optimizations (or more broadly, analyses) of languages in
Freer
, becauseFreer
(being an encoding of>>=
) has to perform its effects in order to traverse subterms. This is actually the mechanism by which some surface terms (e.g.stack
&adjacent
) operate.