I’m happy to share the following paper introducing an abstraction between applicatives and monads. The paper uses Dune as a case study and in particular gives some insights as to how Dune makes use of such abstractions.
One typical example of applicative in OCaml is the Cmdliner library, and one typical example of monad in the Lwt library. Selective functors come in between, allowing to fully analyse a computation beforehand, just as cmdliner does in order to produce man pages, while still allowing to select between different branches at runtime, as one can do with Lwt.
The choice of laws for selective functors seems curious and I know it’s covered in the paper in some detail.
Note that it is not a requirement for selective functors to skip
unnecessary effects. In particular, we do not require that
pure (Right x) <*? y = pure x
In applications for selective functors, I was expecting a discussion of
Function Reactive Programming. The requirment of selective functors
for knowing all effects statically sounds useful for some analysis and
efficiency reasons in a FRP library/application. Is there any parallel to be
drawn between Incremental and these new selective applicative functors?
Would a definition of Incremental in terms of select be useful?
Yaron: I personally got interested in selective functors in the context of hardware design, but after learning from Jeremie about Dune, I got curious about “selective build systems”, which have unique features unavailable to applicative or monadic ones. Haxl came later as a complete surprise.
Selective-like type classes have previously appeared in the context of parsing and web programming. For example, in his dissertation Jeremy Yallop mentions DynamicIdiom type class with the method branch :: f Bool -> f a -> f a -> f a, which is our derived ifS combinator, but doesn’t really explore it (we’ve learned about this after the submission).
Tim: you are right, FRP is relevant and we should have probably mentioned it. I’ve added this to our TODO list.
As for Incremental, I think it relies on monads in a fundamental way. I don’t think it can be made selective.
I’m a bit doubtful of your analysis of Incremental. Incremental has a monadic interface, for sure. But there are big differences between the performance of the applicative subset of that monadic interface, and most Incremental programming is done using the applicative subset alone.
I think this is a common situation with monadic libraries, where the applicative subset is in some sense special. I’m not sure selective would be useful here, but I could imagine it turning out to be helpful in exposing APIs that are more expressive than the applicative subset and more performant than the monadic part of the API. An example that was raised internally is that Incremental.if is special-cased in a way that might fit nicely into Selective.
Thanks, this is cool! It would be awesome if Incremental could push some of the conditional structures into the selective interface and gain some performance benefits.
(Just like with Haxl, I seem to underestimate the usefulness of selective functors in the context where f is both a selective functor and a monad!)
Selective functors are basically adding a pattern matching operation (or finitary bind …). Expressed like that, the pattern is not very new: there is one in mirage’s configuration DSL which we designed 3.5 years ago, for instance, and I can’t honestly claim ownership there. I’m pretty sure Oleg would be able to point to much earlier sources, Jeremy’s thesis nonwistanding. It’s pretty neat to have it developed formally though.
Indeed, because conditionals are so fundamental, it is not surprising that selective-like interfaces have been showing up earlier. We will do our best to cover all prior work in a revision, so if you could point us to a specific piece of code, or even better a write up about it, it would be very helpful.
It is a little bit hard, at the beginning, to grasp the motivation of the paper, since the very first example uses shallow embedding which prevents static analysis. What I mean, is that putStrlLn "pong" is an IO () value, which you still cannot introspect. So, maybe you should define static analysis a little bit more, or use an example with deep embedding, e.g., use values of data Action = Greet String | LaunchMissles.
An alternative approach that enables both static analysis and dynamic analysis is presented by Oleg’s Typed Tagless Final, where the same formulae could be both analyzed statically and evaluated dynamically. It would interesting to see the comparison with it. My main concern, is that the proposed approach doesn’t scale up when the number of primitives is big (or open). For example, in BAP we use final-tagless to model ISA, since in general ISA exposes much more complex set of effects (not just reading and writing, but also address availability, barriers, and lots of different kinds of reads and writes, as well as complex control flow dependencies), which are not expressible in a simple dichotomy of Either.
And thanks for a very nice and easy to understand paper, it was a pleasure to read it
Update: forgot to add the link to the Biokepi project, that albeit being quite domain-specific still has a lot of intersections with Dune.
I see what you mean, although in principle IO could have been implemented via a deep embedding, thus making static analysis possible, as we demonstrate in section 5.
Good point! Typed Tagless Final deserves a discussion. Actually, I think our approach is an example of Typed Tagless Final: it’s a type class that gives you a (generalised version of) if statement, which you can mix&match with other capabilities! In fact, one of the examples in Typed Tagless Final is the type class BoolSYM with if_ method.
Could you please link to your work on ISA modelling? It’s very interesting to have a look.
Note that we are not limited to Either, and can deal with any finite sum type, e.g. a three-way branch taking f (Either a (Either b c)) can be implemented via select.
That’s exactly how I’m seeing it. Not to diminish the value of the work, but just to fit into the mathematical framework, I would say that Selective is a signature of a particular language (structure) and you’re applying the tagless-final approach to investigate its behavior and capabilities.
Also, as a side note, not about the paper, but more about the implementation in OCaml, while select fits nicely in terms of the mathematical beauty, from the perspective of software engineering, if_ or branch would be much better, since select will allocate an extra value on each step, where if_ and branch will not allocate anything. I, personally, favor branch.
Well, it doesn’t really scale It also loses the fact that branches are disjoint (imagine a VSA analysis that gives N possible destinations, which will end up in a comb-like graph, with N extra nodes and edges, instead of one node with N edges). But yes, theoretically with a single branch you can model arbitrary control flows.
Well, this is a work in progress, not yet released (but publically available on my personal repository, links will follow). We employ the tagless-final approach, a little bit adapted to enable scalability. In the original paper they show that they solve the expression extensibility problem, which is indeed true, but they show it on very small languages (we have many languages, the worst one, called The Core Theory. contains about 200 operations and still growing, floating points are hard). Thus instead of using a functor, we actually are using first-class modules, which are all applied in parallel by a Theory Manager and store their interpretations (semantics in our parlance) in a universal dictionary. We use a Knowledge Monad as our base theory (which implements computations with embedded fixed point (we use domains to model data) and nondeterminism (implemented with call/cc monad), which all together enables non-monotone knowledge base). Analyses are implemented as language interpreters (we actually use term theory, akin to SMT theory) and are very easy to write since we have an empty theory for each language, which you can include and then override the necessary operations. Supporting multiple representations fits nicely into this framework, as you can implement unparsing to any language as a reification of the theory (basically, a pretty printer that uses AST to print each operation), while in order to lift an arbitrary AST into a theory, one should write an interpreter of that AST in terms of the said theory. This, basically, allows us to have multiple concrete representations at the same time, so that different developers may choose whatever IR they think suits better to their needs. So this is a very short (and probably confusing) description of our approach, I just don’t want to diverge this thread from the discussion of the paper.
An by the way, back to the paper, our framework is also an instance of Selective of course, (well 1/200 of our signature is Selective , but still all our languages (except Init and Bool), are instances of Selective). And yes, we use it for both static analysis and dynamic interpretation. For example, a static analyzer is able to significantly optimize a trigonometric function based on path constraints, a possible set of values, and user selected assumptions.
1) BIL is the BAP Intermediate language, that we’re using current in BAP 1.x, this module
shows how an arbitrary language could be added to the system. We have other language too, but one is not yet in public, and another is proprietary.
2)We can reinterpret the semantics of BIL language in terms of the core theory (basically, this is the denotation semantics of BIL, where the denotation is the Core Theory values). You don’t need, of course, any intermediate language to give the semantics, and ideally, one should express the semantics of instructions of a particular ISA directly in terms of the Core Theory values, which will also ensure well-typedness property by enforcing the OCaml typechecker to verify the invariants of semantics. But we already have a few lifters that uses BIL, and out in the wild, there are quite a few lifters, which we can and will reuse (Sail and Sledge are fist in the list), so this was our motivation, to enable lifting from other IRs, including our old one.
3) This analysis builds a control flow graph, and reifies branches, while-loops and other abstract control flow operations in terms of graphs.
P.S. Sorry for multiple edits, hit the Post button abruptly
One option is to include both select and branch into the type class (and possibly even bindS). The former is simpler and is often enough, while the latter gives better performance and statically visible mutual exclusion of branches. Does this sound like a good compromise to you?
Many thanks for the rest of your comment – lots of really amazing stuff! It will take us some time to go through your links, and we’ll be in touch if anything is unclear. Hope it’s OK to contact you directly.
Yep, if there will be helper functors (type classes) which will derive Selective from all three possibilities so that an instance could enter the Selective class through either door. Or, in OCaml, something like this:
module M = Selective.Make(Selective.Branch(struct
...
end))
It also loses the fact that branches are disjoint (imagine a VSA analysis that gives N possible destinations, which will end up in a comb-like graph, with N extra nodes and edges, instead of one node with N edges). But yes, theoretically with a single branch you can model arbitrary control flows.
, but still all our languages (except Init and Bool), are instances of Selective). And yes, we use it for both static analysis and dynamic interpretation. For example, a static analyzer is able to significantly optimize a trigonometric function based on path constraints, a possible set of values, and user selected assumptions.