Comment by jonsterling | Hacker News Reader

Comment by jonsterling | Hacker News Reader

Parent Full thread

After numerous discussions with Bob Harper (and reading Derek Dreyer's work, who has been the biggest proponent for applicative functors), I have come to understand that there are only two compelling use-cases for applicative functors:

1. higher order functors.

2. modular type classes

Higher order functors are kind of cool, but IMO Standard ML does not seem to be suffering too much from the lack of them. I'm not too interested in it, since it gets super gnarly super fast, and this happens to be pretty much the main use-case for applicative functors. I suspect that most use-cases of higher order functors in OCaml could be reformulated to be first order, with a lot less monkeying around in the module system. There may be compelling use-cases though.

The other use-case is possibly a version of modular type classes that behaved a bit more like Haskell's. The idea is that if functors are going to be applied automatically during elaboration to provide something like type classes, you'll get MkWelp(S) called in multiple places, and you would prefer that any type members of the resulting structure be compatible. Applicative functors would do this.

I am not too convinced by this use-case, though I could see that people would find it useful.

In all other cases, generative functors have the correct semantics. Pretty much the whole use-case of putting abstract types in a functor is that you can then reason intensionally about them (i.e. distinguish them based on their access path). This is super useful, for instance, if you have a notion of "index" or something and you want to prevent yourself from using indexes from one table in another one, or something along those lines.

This is what the Scala people mystifyingly call "path dependent types". It's just generative abstraction.

So maybe it is an interesting feature to have applicative functors, but these should be added post facto, and generative functors should be the default. OCaml now supports generative functors if you add an extra () parameter; it's strange syntax, but it's good enough for me! :)

I think I disagree with this. Your functors should generally be pure, and for pure functors applicative is a nicer semantics.

Consider the case of a set implemented as a binary tree. The type of such a set should be parametrised by the type of the elements and the ordering used. With applicative functors this is the case as your set type will be `Set(O).t` where `O` is a structure containing the type and the ordering. With generative functors each individual set type is abstract -- so the type itself is not parameterised by the ordering.

You could consider this to be just an example of what you are calling "Modular Type Classes", but there doesn't need to be a system of implicit module parameters for it to be useful.

lps25:

> Consider the case of a set implemented as a binary tree. The type of such a set should be parametrised by the type of the elements and the ordering used. With applicative functors this is the case as your set type will be `Set(O).t` where `O` is a structure containing the type and the ordering. With generative functors each individual set type is abstract -- so the type itself is not parameterised by the ordering.

You make a good point about this not being strictly about type classes. But I'd say that the issue is only a problem in the presence of implicit resolution, since otherwise, you can just bind the result of the functor to a structure once and be done with it. It becomes an issue with type classes, because you don't have the choice to share a single structure during elaboration.

IMO, the generative version is still better for most use-cases (pure or not), but it's nice that you can have both in OCaml.

>> since otherwise, you can just bind the result of the functor to a structure once..

My understanding was that of lpw25's. I wanted to use applicative functors in the same way type classes (or OCaml's modular implicits) would make use of them, but even without type class's implicit resolution (explicitly specifying them). I agree there isn't too much difference from doing the same with generative functors, but the main difference is, as you said, I would need to find a place (some appropriately accessible location in the namespace) by which to access the result of these generative functor applications, and that's just an extra point of friction (if I understand correctly). It's not the end of the world as you said either way because we can do either.

Thanks for the help, jonsterling/lpw25.

Reply on news.ycombinator.com