snowleopard/selective-ocaml

Understanding Selective through OCaml (specifically ifS and whenS)

Closed this issue · 3 comments

gr-im commented

Preliminary note

In trying to understand and use selective functors, through OCaml, which I understand
relatively better than Haskell, I sent a few questions to @snowleopard who was kind
enough to answer me and invited me not to not hesitate to speak about it in public.
So here I am!

I discovered Selectives by reading the paper (few months ago). Reading the paper, I saw a more general form than the Dynamic Applicatives presented in Jeremy Yallop's thesis (as Dynamic-Idiom). (Cited in the "related work" section of the paper).

Not being very comfortable with Haskell, I was quite satisfied to discover this package which allows me to "more easily" understand what it is all about and I came to a potentially false conclusion.

First of all, I want to emphasize that my purpose is not to criticize anything at all. I just have the intuition that the OCaml library is a "literal" translation of the Haskell implementation and I think that it poses a concern because of the different natures of the two languages (Eager VS Lazy).

My main intuition comes from reading the signatures of ifS and whenS :

  • val ifS : bool t -> 'a t -> 'a t -> 'a t
  • val whenS : bool t -> unit t -> unit t

They are symmetrical with the implementation of Haskell (modulo parametrized module VS typeclasses) :

  • ifS :: Selective f => f Bool -> f a -> f a -> f a
  • whenS :: Selective f => f Bool -> f () -> f ()

My first comment was that when we look at whenS, it was impossible to produce a different effect than My_selective.pure (). To this statement, @snowleopard has provided me with several counter-examples (for example, Option.None and Option.Some () which both have the right type, there are many others).

However, even if I hear the answer perfectly, my proposal would be to change the type of whenS and ifS to:

  • val ifS : bool t -> (unit -> 'a t) -> (unit -> 'a t) -> 'a t
  • val whenS : bool t -> (unit -> unit t) -> unit t

In my opinion, these signatures would actually become isomorphic with Haskell signatures. Without this modification, I have the intuition that the behavior of the two implementations would vary.

For example let's considere a custom if (it is a pretty naive example but I think it is revelant) in Haskell (1) and in OCaml (2):

myIf :: Bool -> a -> a -> a
myIf predicate ifValue elseValue = 
   if predicate then ifTrue else elseValue
let my_if predicate if_value else_value = 
   if predicate then if_value else else_value

If I run in Haskell:

myIf True (print "foo") (print "bar") -- print "foo"
myIf False (print "foo") (print "bar") -- print "bar"

And in OCaml:

my_if true (print_endline "foo") (print_endline "bar") 
(* 
print "bar"
print "foo"
*)

my_if false (print_endline "foo") (print_endline "bar") 
(* 
print "bar"
print "foo"
*)

The two behaviour differ because Haskell is lazy and OCaml evaluate parameters from right to left.
@snowleopard agreed with the suggestion of having "my suggestion" in the API but with an another name (more in the OCaml convention, iter_when or lazy_when. And he asked to me what about select, shoudl we wrap the second parameter of the function in unit -> ... like this: select : ('a, 'b) Either.t t -> (unit -> ('a -> 'b) t) -> 'b t. In my understanding, I think it is unecessary since the value wrapped into the selective is a function.

Even the usage of other name (iter_when) could be a solution, I'm not in favor of that because, in my order of understanding, the desired behaviour is to be "like in Haskell", so wrapping the parameters of ifS and whenS (in a function from unit to 'a t or unit t or using Lazy.t) seems necessary to fit with the Haskell behaviour.

By the way, there are a lot of aspects that I don't understand, so it's possible that I say a lot of nonsense (sorry for that). But @snowleopard told me :

In all of these cases whenS, as well as ifS, have the right semantics, but one has to evaluate all branches unconditionally. They are not like OCaml's if-then and if-then-else built-in primitives that evaluate branches only when needed.

I don't really understand what evaluate all branches unconditionally means.

Here was my two cents. Thanks a lot for your time (and I really enjoyed watching the Selectives and graphs presentations!)

(I'm not very fluent in English so sometimes my way of speaking can be awkward).

In Haskell monadic programming, it is idiomatic to consider that an expression of a monadic type m a can be evaluated to a value without performing any effect; programs of these types are pure descriptions of the computation.

Indeed, in your myIf example you could try forcing print "true" and print "false" before passing them to myIf (using seq or a bang-pattern), and you would still observe the same result: the printing does not result from "evaluating" those terms, but later from interpreting them in the IO monad.

When you do monadic programming in a language that exposes impure primitives, there are two distinct notions of effects: the "primitive" effects that you observe during computation, and the "monadic" effects that are contained in the monadic value.

Now the question is whether you want ifS to delay only monadic effects (it always does even with the existing API) or to also delay "primitive" effects. Personally I think that both choices may make sense, but by default I would have expected to only delay "monadic" effects, and thus the current API. It makes sense to me to be explicit if we also want to delay "primitive" effects, with a different combinator. Another approach to do this would be, in some monads only, to expose a combinator to turn primitive effects into monadic effects:

val thunk : (unit -> 'a t) -> 'a t

Then instead of ifS_lazy p (fun () -> a) (fun () -> b) you would write ifS p (thunk (fun () -> a)) (thunk (fun () -> b)). But that only works if the designers of the monad want to let you integrate primitive effects in their monadic values.

Personally I would prefer to avoid programming with impure monadic terms (that both perform primitive and monadic effects), and prefer to write either impure non-monadic fragments (for the IO parts at the boundaries of my program) or pure monadic fragments (for the internal working, if the monadic style provides engineering benefits). But there are existing precedents for it in the OCaml world, typically Lwt-using programs have a mix of both primitive and monadic effects, which may be a reason why having explicit combinators for those makes sense. But I would recommend maybe looking for real-world examples of it, or at least believable applications of them; the print examples feels a bit artificial.

gr-im commented

Thanks a lot for your answer. It is really more clear in my mind!

@gasche Thanks for the great explanation!

@Pytre Don't hesitate to ask further questions. These are subtle issues, and I often get confused about them myself :)