New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add "monadic" let operators #1947

Merged
merged 4 commits into from Nov 27, 2018

Conversation

Projects
None yet
@lpw25
Copy link
Contributor

lpw25 commented Jul 31, 2018

Based on a few recent comments and PRs, I thought it might be a good time to revive the idea of adding some support for "monadic" syntax to OCaml. I can't find the last attempt at this on GitHub or Mantis, but like last time the idea is to allow people to define "let" operators like let* and let+. The general form of the operators is let followed by a sequence of infix operator characters. (Note that this deliberately excludes let! -- the existence of open! and method! would make that too confusing).

Outline

This proposal aims to be fully general whilst making it easy to implement the common cases. In particular, it focuses on supporting functors, applicatives and monads easily. The translation chosen is a generalisation of the one used by ppx_let. Essentially, given a let binding like:

let+ x = A
and++ y = B
and+++ z = C in
  expr

it is translated directly to:

let def = A
and def2 = B
and def3 = C
and func = fun ((x, y), z) -> expr
and (bind, single) = (let+) in
bind func ((and+++) ((and++) (single def) def2) def3)

This translation essentially treats the input to a let binding as a pair of a tagged list of bindings and a function. The bind function handles pairing the bindings with the function, whilst the single, and++ and and+++ functions create the list of bindings. The bind and single functions are combined to form the (let+) value.

Example

For a monad, I suggest the following approach to using these let operators, using list as an example:

let id x = x

module List = struct

  type 'a t = 'a list

  let map = List.map

  let bind f l =
    let l = List.map f l in
    List.concat l

  let product xs ys =
    List.fold_right
      (fun x acc -> List.map (fun y -> x, y) ys @ acc)
      xs []

  let (let+) = map, id
  let (and+) = product
  let ( let* ) = bind, id
  let ( and* ) = product

end

So we use let+ for map, let* for bind and set both the ands to the monoidal product. This gives the expected behaviours:

# let map =
     List.(
       let+ x = [1; 2; 3] in
       x + 1
     );;
val map : int list = [2; 3; 4]

# let map_and =
     List.(
       let+ x = [1; 2; 3]
       and+ y = [7; 8; 9] in
       x + y
     );;
val map_and : int list = [8; 9; 10; 9; 10; 11; 10; 11; 12]

# let bind =
     List.(
       let* x = [1; 2; 3] in
       let* y = [7; 8; 9] in
       [x + y]
     );;
val bind : int list = [8; 9; 10; 9; 10; 11; 10; 11; 12]

# let bind_and =
     List.(
       let* x = [1; 2; 3]
       and* y = [7; 8; 9] in
       [x + y]
     );;
val bind_and : int list = [8; 9; 10; 9; 10; 11; 10; 11; 12]

# let bind_map =
     List.(
       let* x = [1; 2; 3] in
       let+ y = [7; 8; 9] in
       x + y
     );;
val bind_map : int list = [8; 9; 10; 9; 10; 11; 10; 11; 12]

(I've never found list to be a particularly useful monad and I think it makes these examples a bit less compelling than if they were using a more useful monad like lwt or async, however list is the simplest monad that makes clear how these operators work so I used it anyway).

Observe that this approach aligns cleanly for the functor and applicative cases: for functors we can define let+, for applicatives we can define let+ and and+, and for monads we can define all four operators. This also naturally supports monads for which the applicative operations are more efficient than the equivalent monadic operations -- i.e. where let+ ... and+ ... is more efficient than let* ... let+ ....

Differences from ppx_let

For comparision, the ppx_let translation essentially takes:

let+ x = A
and y = B
and z = C in
  expr

and translates it to:

let def = A
and def2 = B
and def3 = C
and func = fun ((x, y), z) -> expr
and (bind, and_) = (let+) in
bind func (and_ (and_ def def2) def3)

A key difference between the translation in this PR and the one used by ppx_let is the addition of the single part of the let operators. Note that it was always id in the example above. One reason for this addition is that with some monads it is more efficient to gather together multiple computations and bind/map them all at once rather than to merge them together using their monoidal product and then bind/map that -- one notable example is Deferred.t in the async library. Having the single combinator allows the type of the argument to bind to differ from the type of the things being bound.

Another difference from ppx_let is the support for mixing different let and and operators together. This is partly to allow the direct alignment from operators to the functor, applicative and monad use cases -- as described above. It also makes the construct more general allowing, for example, a computation that can bind on multiple sorts of things to mix them together in a single let ... and ... construct.

match operators

These have now been split into #1955

Open questions

  • Currently the implementation is entirely as a translation in the parser, much as other operators are. I generally prefer to avoid elaboration and instead to give things their own AST nodes, but I wanted to keep its implementation in line with other operators for this initial attempt. Should I change the implementation before we merge? Should I give all operators there own AST nodes -- that would certainly make pprintast.mls job a lot easier?

  • Is there any reasonable way to support qualified versions of these operators? By this I mean allowing you to use List.(let*) without opening List. I personally think it will be quite difficult to find an aesthetic syntax, and I think that much of the value of these operators does not require it. Once we have implicits this will be much less of an issue.

  • Currently, the let* is a single token from the lexer. Should it instead be two separate tokens?

  • How should this be integrated into the standard library? My personal preference is not to do any such integration yet, and to wait for the arrival of implicits before adding generic support for monads etc.

@yallop

This comment has been minimized.

Copy link
Member

yallop commented Jul 31, 2018

I can't find the last attempt at this on GitHub or Mantis, but like last time the idea is to allow people to define "let" operators like let* and let+.

One place this was once supported was MetaOCaml:

$ metaocaml
BER MetaOCaml toplevel, version N 102
        OCaml version 4.02.1

# let (let*) m k = List.(concat (map k m));;
val let* : 'a list -> ('a -> 'b list) -> 'b list = <fun>
# let* x = [1; 2; 3] in
  let* y = [7; 8; 9] in
  [x + y];;
- : int list = [8; 9; 10; 9; 10; 11; 10; 11; 12]
@diml

This comment has been minimized.

Copy link
Member

diml commented Jul 31, 2018

I'm in favor of such a feature. We started using applicative parsers in dune and it's really painful to write applicative code without something like this.

@yminsky

This comment has been minimized.

Copy link

yminsky commented Jul 31, 2018

It would be lovely if ppx_let could be entirely obsoleted by this new syntax. Some missing features:

  • if%map and if%bind
  • Qualified operators, e.g., let%map.Command.Let_syntax
  • let%map_open% and let%bind_open

I suspect we could quite easily live without support for if, but the second and especially third are pretty deeply ingrained in a lot of our code.

@xavierleroy

This comment has been minimized.

Copy link
Contributor

xavierleroy commented Jul 31, 2018

I'd be very happy to see basic syntactic support for monads. By which I mean a "let"-like construct for monadic "bind" and nothing else. There is no "and" in any theory of monads I know of. Not to mention the other stuff that @yminsky mentions.

Could we leave the extra syntax to existing PPXs, for people who can't live without, and just have basic monads that everyone understands in the core system?

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

It's probably worth me describing some alternative translations that are worth considering.

One possibility is to use something halfway between this PR and ppx_lets translation. It would take:

let+ x = A
and y = B
and z = C in
  expr

and translate it to:

let def = A
and def2 = B
and def3 = C
and func = fun ((x, y), z) -> expr
and (bind, single, and_) = (let+) in
bind func (and_ (and_ (single def) def2) def3)

This prevents supporting let+ for functors because they have nothing they can use for and_, although it is not clear how useful that feature is. It also does not allow for mixing different sorts of bound thing, although again it is not clear whether that is useful in practice -- you can always bind a single sort of thing and use some injection functions on the things being bound. Unlike the ppx_let translation, it does support the case where you want to use a different type for bound values and the collection of bound values that bind operates on -- which allows for more efficient handling of monads like Deferred.t.

A slight variation would be to use the same translation but to force people to write it as:

let+ x = A
and+ y = B
and+ z = C in
  expr

which I think is aesthetically nicer, although I don't like that there is no actual and+ value being referred to.

Another possibility would be to separate out the let case from the let ... and case by allowing something like:

let (let+) = map
let (let+..and+) = (map, id, product)

with individual let+ handled by the first and let+ ... and+ handled by the second. That would allow using let+ with functors.

@xavierleroy

This comment has been minimized.

Copy link
Contributor

xavierleroy commented Jul 31, 2018

Could we [...] just have basic monads that everyone understands in the core system?

In particular, monads where bind has the correct type 'a mon -> ('a -> 'b mon) -> 'b mon.

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

There is no "and" in any theory of monads I know of.

Sure there is. and is the fundamental operation of an applicative. An applicative is just a functor with

val pure : 'a -> 'a t
val prod : 'a t -> 'b t -> ('a * 'b) t

If you don't support and then you cannot use the syntax with applicatives, which is one of its main use cases. Haskell do notion supports applicatives, and there is just as much code using ppx_let for applicatives as for monads.

In addition, in most useful monads the applicative operations are cheaper than the monad operations. This is true of: lwt, async, incremental, build monads in Jenga and dune, monadic parsers etc. Which means that writing efficient code requires you to use and.

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

In particular, monads where bind has the correct type 'a mon -> ('a -> 'b mon) -> 'b mon.

I'm not really sure how to enforce that without using higher-order unification or requiring the operator to be defined as a module. It also rules out using the construct for applicatives. Beyond that I don't think it is really a necessary restriction. I prefer to view these operations as interpretations of the let syntax, if a user wishes to uses an esoteric interpretation I don't see why we should stop them.

@bluddy

This comment has been minimized.

Copy link

bluddy commented Jul 31, 2018

I'm not used to thinking about the let-based syntax and its translation to monads/applicatives in OCaml - unfortunately, these things work pretty well if you just treat them as black boxes - but I think this suggestion is great.

Can't wait for the chapter in the manual about monads and applicatives :)

@xavierleroy

This comment has been minimized.

Copy link
Contributor

xavierleroy commented Jul 31, 2018

An applicative is just a functor with prod

Well, call me old-school and fixated on the literature, but in the original McBride-Patterson definition of applicatives, there is no product but there is a <*>.

I agree applicatives are very useful, nearly as much as monads. I'd still like either or both to be supported in a way that is closer to established literature and formalizations.

Efficiency considerations come second to understandability.

@hcarty

This comment has been minimized.

Copy link
Contributor

hcarty commented Jul 31, 2018

Is there a clean way to support exception branches in the match sugar?

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

but in the original McBride-Patterson definition of applicatives, there is no product but there is a <*>

See section 7 of that paper, where the "Monoidal" typeclass is described as isomorphic to the other signature they present.

I've always preferred the monoidal presentation because it makes the nature of applicatives much clearer. For example, the laws for the monoidal presentation are basically just the monoid laws, which I find easier to follow than the laws for the application-based presentation.

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Jul 31, 2018

I feel a bit more mellow than @xavierleroy about the proposal. I suspect that there is a large part we all agree on (but it requires a bit of time and effort to find it out), but that maybe this is blurred by dubious salesmanship -- making your first example an ASCII christmas tree was maybe not the best move.

One thing that would be nice is to not look at mixed-operator settings at first, and show and discuss examples that correspond to the use of a single monad (bind and return) and a single applicative (pure and (and)), with the types of everything involved. If we agree on what the proposed design implies on this reasonable subset, it's easier to discuss the general less-principled setting.

@bluddy

This comment has been minimized.

Copy link

bluddy commented Jul 31, 2018

I think inserting any syntactic sugar into OCaml is going to be hard, since the language doesn't currently have much sugar as a precedent. It may be worth considering putting the minimal amount into the language at first to get people used to the idea and expanding later.

Also, while let+ looks ok, and++ and and+++ look terrible, and looks matter here because we're talking about replacing ppxs, which are functional but generally look ugly. Is there a need for them in the given example? Shouldn't and+ be enough?

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

Shouldn't and+ be enough?

Yes, I was just using different names for each and to show where they appear in the output.

@diml

This comment has been minimized.

Copy link
Member

diml commented Jul 31, 2018

Regarding examples of applicatives, a good example is the cmdliner library. It is a widely used command line parsing library that uses an applicative parser. Using an applicative allows in particular to extract the man page from the parsing code, which is really nice. It is used by 190 packages in opam, and we have a similar library at Jane Street that is used by hundrerds (possibly thousands) of our programs.

Code using it usually looks like this:

let x1 = flag "-x1" type1 in
let x2 = flag "-x2" type2 in
...
let  xn = flag "-xn" typen in
let make x1 x2 ... xn =
  { x1; x2; ...; xn }
in
Term.(const make $ x1 $ x2 $ ... $ xn)

where Term.const is the pure operation and $ is the <*> one. While this code works well, it's easy to see the maintainability issue: the order of argument of make as to match exactly the order of the $ xi on the last line. It is up to the developer to ensure that, which is painful. With a let syntax, we could simply write:

let+ x1 = flag "-x1" type1
and+ x2 = flag "-x2" type2
...
and+ xn = flag "-xn" typen
in
{ x1; x2; ...; xn }

Just to give a real life example, here is some code extracted from opam:

let create_global_options
    git_version debug debug_level verbose quiet color opt_switch yes strict
    opt_root external_solver use_internal_solver
    cudf_file solver_preferences best_effort safe_mode json no_auto_upgrade
    working_dir ignore_pin_depends =
  let debug_level = OpamStd.Option.Op.(
      debug_level >>+ fun () -> if debug then Some 1 else None
    ) in
  let verbose = List.length verbose in
  { git_version; debug_level; verbose; quiet; color; opt_switch; yes;
    strict; opt_root; external_solver; use_internal_solver;
    cudf_file; solver_preferences; best_effort; safe_mode; json;
    no_auto_upgrade; working_dir; ignore_pin_depends; }

...

let global_options =
  let section = global_option_section in
  let git_version =
    mk_flag ~section ["git-version"]
      "Print the git version of opam, if set (i.e. you are using a development \
       version), and exit."
  in
  let debug =
    mk_flag ~section ["debug"]
      "Print debug message to stderr. \
       This is equivalent to setting $(b,\\$OPAMDEBUG) to \"true\"." in

  ... about a 100 lines of code like this ...

  Term.(const create_global_options
        $git_version $debug $debug_level $verbose $quiet $color $switch $yes
        $strict $root $external_solver
        $use_internal_solver $cudf_file $solver_preferences $best_effort
        $safe_mode $json_flag $no_auto_upgrade $working_dir
        $ignore_pin_depends)
@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

I'd still like either or both to be supported in a way that is closer to established literature and formalizations

So it is probably worth me describing how I arrived at the current proposal, or at least arrived at the general idea of the current proposal.

The translation used in ppx_let was my attempt to stick closely to the literature on monads and applicatives. It essentially represents the applicative let...and... as the pair (map, prod) and the monadic let...and... as the pair (bind, prod), which I find theoretically satisfying because it manages to represent both forms through a simple translation whose inputs are fundamental operations from the associated structures.

In practice, this worked pretty well but it couldn't capture some useful cases which was frustrating. This encouraged me to try a slightly different approach. This time I'm trying to essentially define the operators as eliminators of the let syntax. If you consider the let to be a constructor in the expression language which takes a term with free variables along with a non-empty list of bound terms then the eliminator for that constructor should be something along the lines of:

val elim_let : single:(term -> 'a) -> cons:(term -> 'a -> 'a) -> pair:('a -> term -> 'b) -> 'b

Obviously, there are other ways you could structure this eliminator, but by choosing this form we still get that the applicative let and the monadic let are built out of fundemental components. This time they are (map, prod, id) and (bind, prod, id) respectively. In neither case do we care about the single part of the eliminator, but by including it I think we get something that is in some sense completely general, since it amounts to the data required to eliminate the let syntax.

is blurred by dubious salesmanship

Yeah, I jumped somewhat into the middle of my train of thought without including details from my considerations of this subject over the last few years.

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

One thing that would be nice is to not look at mixed-operator settings at first, and show and discuss examples that correspond to the use of a single monad (bind and return) and a single applicative (pure and (and)), with the types of everything involved.

The unmixed applicative case needs to translate:

let+ x = a
and+ y = b
and+ z = c in
  body

into

map (fun ((x, y), z) -> body) (prod (prod a b) c)

where

val map : ('a -> 'b) -> 'a t -> 'b t
val prod : 'a t -> 'b t -> ('a * 'b) t

are the map and monoidal product respectively.

The unmixed monadic case needs to translate:

let* x = a in
  expr

into:

bind (fun x -> expr) a

where:

val bind : ('a -> 'b t) -> 'a t -> 'b t

is the bind operation of the monad.

However, I would really like to emphasize how important the mixed monadic case is. One of my favorite papers in this area is "Idioms are oblivious, arrows are meticulous, monads are promiscuous" by Lindley, Wadler and Yallop. It really emphasizes how the relationship between monads and applicatives is all about dependencies between computations. Accurately expressing the dependencies in your computations is really important, and from this perspective:

let* x = a in
let* y = b in
  expr

is not a suitable replacement for:

let* x = a
and* y = b in
   expr

because they do not really represent the same computations. For some simple monads like option or list it's not an important distinction, but for many monads the distinction is key to using them effectively.

For this mixed monadic case we need to translate:

let* x = a
and* y = b in
  expr

into

bind (fun (x, y) -> expr) (prod a b)

where

val bind : ('a -> 'b t) -> 'a t -> 'b t
val prod : 'a t -> 'b t -> ('a * 'b) t

are the bind and monoidal product respectively.

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Jul 31, 2018

(Note that the above translation are a bit simpler than the ones I have been giving before because they ignore the issue of evaluation order. Since OCaml evaluates lets top-to-bottom, but function arguments right-to-left, you need to first bind the arguments in a let to make sure not to surprise users. I know technically all these evaluation orders are undefined, but I'd still rather not needlessly confuse people)

@yminsky

This comment has been minimized.

Copy link

yminsky commented Jul 31, 2018

To make Leo's point about dependencies more concrete, consider the case of Incremental. The whole point of Incremental is to optimize the recomputation of the calculation in question, and dependency tracking is critical. So, the following two computations:

let+ x = f a
and+ y = g b 
in 
x + y
let* x = f a in
let+ y = g b in
x + y

Have very different recomputation semantics. In particular, if the value of f a changes, then the function application g b will need to be re-evaluated in the second case, but not in the first. These are not small efficiencies, but potentially large changes to asymptotic complexity.

Similarly, moving from the applicative subset of an API to the full monadic one gives up on the analyzability of the resulting object, which goes to things like the Commandliner example the @diml mentioned.

Generally speaking, I think there is now a decent amount of prior art (at least ppx_let and Haskell) that suggests that one should make it possible to be explicit about when one is using the applicative subset of a monad, vs when one is using the full power of bind. Leo's proposal allows that, but only providing a monadic let binding does not.

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Jul 31, 2018

My pay grade is not high enough to comment on the specifics of the proposal. However, I will note that there are no corresponding changes to the documentation included in your patches. I think writing the documentation, in addition to its more obvious use, also has the effect of helping one think through whether one's feature is optimal. If it's hard to explain, it might be not quite right...

@yallop

This comment has been minimized.

Copy link
Member

yallop commented Jul 31, 2018

Is there a clean way to support exception branches in the match sugar?

I expect there are a few possible ways to handle that. For example, you could translate

match+ expr with
| pat1 -> case1
| pat2 -> case2
| exception E1 -> case3
| exception E2 -> case4

to something like this:

(match+)
  (function Ok pat1 -> case1 | Ok pat2 -> case2 | Error E1 -> case3 | Error E4 -> case4)
  (match expr with v -> Ok v | exception e -> Error e)

or perhaps to something like this:

match expr with
  | v -> (match+) (function pat1 -> case1 | pat2 -> case2) v
  | exception e -> (match+) (function E1 -> case3 | E4 -> case4) e

Personally, I think it'd be useful to see the match syntax proposed & discussed in a separate PR, since

  1. it's useful in various non-monadic situations (e.g. I have a ppx extension for match that I use in staged programming)
  2. the match sugar raises additional questions that aren't related to monads, such as
  • forwards compatibility with effects
  • handling of backtraces
  • duplication of continuation expressions
@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jul 31, 2018

Personally, I think it'd be useful to see the match syntax proposed & discussed in a separate PR

Second that.

@keleshev

This comment has been minimized.

Copy link
Contributor

keleshev commented Jul 31, 2018

Sorry to add to the volume of the discussion, but it so happens that I have been obsessively thinking about such feature for quite some time and wanted to compare notes. So, how about this:

For any identifier ⟨foo⟩, let let.⟨foo⟩ x = y in z translate to ⟨foo⟩ y ~f:(fun x -> z). For example:

let.bind x = y in z   ⇒   bind y ~f:(fun x -> z)
let.map  x = y in z   ⇒   map  y ~f:(fun x -> z)
let.lwt  x = y in z   ⇒   lwt  y ~f:(fun x -> z)
let.foo  x = y in z   ⇒   foo  y ~f:(fun x -> z)

This allows for easier mixing of, for example, lwt with a List.map in the same scope. Also, you can arguably guess what the syntax means.

Mixed monadic case:

let.bind a = x
and.prod b = y
and.prod c = z in e

⇒

bind ~f:(fun ((a, b), c) -> e) (prod (prod x y) z)

This assumes the following:

val map  : 'a m -> f:('a -> 'b)   -> 'b m
val bind : 'a m -> f:('a -> 'b m) -> 'b m

val prod : 'a t -> 'b t -> ('a * 'b) t

Importantly, it requires map and bind to be symmetric in their signatures. For example, like this:

val map  : 'a m -> ('a -> 'b)   -> 'b m
val bind : 'a m -> ('a -> 'b m) -> 'b m

But not like this:

val map  : ('a -> 'b) -> 'a m  -> 'b m
val bind : 'a m -> ('a -> 'b m) -> 'b m

If nothing else, I second the support for the mixed monadic case, which I use a lot with ppx_let.

@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Aug 1, 2018

We use some internal parsing library, using applicative-style combinators, but "postfix style":

  val ( @@ ): 'a t -> ('a -> 'b) t -> 'b t
  val ( @@@ ): unit t -> 'a t -> 'a t
  val (!!): 'a -> 'a t

leading to code such as:

  str "(" @@@ number @@ str "," @@@ number @@ str ")" @@@ !!(fun y x -> (x, y))
  • Does the reverse-style fit in the current proposal?

  • Can we do better than let-binding () instead of using @@@? Do we want to support custom sequencing as well?

Ideally the code above could be written as:

str "(";@
let@ x = number in
str ",";@
let@ y = number in
str ")";@
(x, y)
@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Aug 1, 2018

That feels oddly reminiscent of #508 , which I still find ugly as hell.

@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Aug 1, 2018

I don't find that particularly nice either, but the alternative would be quite heavy:

let@ () = str "(" in
let@ x = number in
let@ () = str "," in
let@ y = number in
let@ () = str ")" in
(x, y)

(at this point, using the original infix combinator syntax would probably work better in practice)

We don't necessarily need to support ad hoc sequencing; one could also interpret e1 ;+ e2 as let+ () = e1 in e2.

@diml

This comment has been minimized.

Copy link
Member

diml commented Aug 1, 2018

@alainfrisch we are now using an applicative s-expression parser in Dune, and to avoid to do positional argument matching we introduced a text preprocessor to interpret let%map. Personally, I don't find the result too bad for sequence things. For instance this is extracted from the current code of dune:

let%map loc = loc
and () = keyword "select"
and result_fn = file
and () = keyword "from"
and choices = repeat choice in
Select { result_fn; choices; loc }
@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Aug 1, 2018

With the current proposal, would you be able to use let ... and, or would you need to rewrite that to just a sequence of let? Also, you'd need to use operator suffixes on all symbols, not just the initial let, right? Wouldn't that become too heavy?

While writing my example above, it occurred to me that let@ x = y in e looks a bit weird, since it suggests that x and y are "equal", while they usually have different types. @lpw25 : did you consider adding the operator characters to the = sign instead (let x =@ e1 and y =@ e2 in e3)?

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Aug 1, 2018

@alainfrisch Personally, I quite like the form using (). However, I think if you used slightly different combinators you could get:

let+ (x, y) = str "(" @@ number  @@@ str "," @@ number @@@@ str ")" in
...

which might be more to your taste.

With the current proposal, would you be able to use let ... and, or would you need to rewrite that to just a sequence of let?

With this proposal it has to be let ... and because a sequence of lets does not make sense for an applicative. A sequence of lets implies that you could use the result of the first element in the definition of the second, which is the very thing that applicatives forbid.

did you consider adding the operator characters to the = sign instead (let x =@ e1 and y =@ e2 in e3)?

No, and to be honest I don't like the look of that. If people want to avoid equals then I would rather we use the fairly traditional:

let+ x <= ... in

although personally I think = is fine.

@lpw25 lpw25 merged commit d7a1c20 into ocaml:trunk Nov 27, 2018

1 of 2 checks passed

continuous-integration/appveyor/pr Waiting for AppVeyor build to complete
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@texastoland

This comment has been minimized.

Copy link

texastoland commented Nov 27, 2018

To reiterate a couple confusing points in the syntax (I like the theoretical treatment) of the PR as a Haskell hobbyist learning OCaml:

let+ x <= ... in

although personally I think = is fine.

= confused me (still) in ppx_let too. Using a list comprehension for example:

let range2D ~w ~h =
  let%map i = 0 -- (h - 1) in
  i * w + 1 -- (i + 1) * w

Clearly i : int is not equivalent to (0 -- (h - 1)) : int list. It seems to contradict the maths. I like the intuition in Haskell of <- as a CPS reversing the regular function arrow. <= wouldn't convey the same intuition and would conflict with the font ligature for less-than-or-equal-to.

a) XXX is a string of operator symbols and YYY is (letXXX) -- as in the current proposal
b) XXX is something like .foo and YYY is (letXXX)
c) XXX is something like .foo and YYY is foo

For me a) is the only option that removes all intuition from reading even having a background in other MLs and languages with typeclasses. Am I missing a connection between + for map and * for bind? You mentioned that do notation (only recently) supports applicative functors but they added it without changing let semantics or adding new symbols.

My only other question is about let+ .. and+. I understand the range analogy but without single could it just be destructuring i.e. let (let+, and+) = (map, product). Thank you for all you do for OCaml!

@ejgallego

This comment has been minimized.

Copy link

ejgallego commented Nov 28, 2018

Yup, those coming from Haskell (such as myself) will find the <- or <= easier to read.

Also, I tend to find:

let x = foo in

and

let+ x = foo in

too similar. I think the eye tends to focus much more on the assignment part x = foo which is natural as this is a normal vision optimization like the one musicians do when reading scores. But of course, YMMV.

@OvermindDL1

This comment has been minimized.

Copy link

OvermindDL1 commented Nov 28, 2018

Just as another voice, as a non-haskell user but primarily OCaml and C++, my eye is more drawn to the = operator as well and not the let+ token. I'd more easily see let x <some-custom-operator> foo in ... like let x <= foo in ... as well.

@andrejbauer

This comment has been minimized.

Copy link

andrejbauer commented Dec 12, 2018

Just chiming in to say that Andromeda is written in a monadoc style, with explicit ... >>= fun x -> ... and we'd love OCaml support for monads. We've been considering using one of the ppx extensions to get a saner syntax, but anything that is actually built into OCaml is of course a big advantage.

@nilsbecker

This comment has been minimized.

Copy link

nilsbecker commented Dec 12, 2018

I was alerted to this PR by a reddit post. As a non-Haskell-knowledgeable and non-CS user of OCaml, I find the proposed let* notation not immediately easy to digest. From the proposed documentation:

let find_and_sum tbl k1 k2 =
  let* x1 = Hashtbl.find_opt tbl k1 in
  let* x2 = Hashtbl.find_opt tbl k2 in
    return (x1 + x2)

This becomes parseable for me after reading the translation that is given shortly afterwards. However, what I find surprising is that after the let* bindings, x1 and x2 are apparently not bound values as usual in OCaml. For instance, replacing the last line with (x1 + x2) would not type-check. This goes against the expectation I had, that let* ... = ... in maybe does something else as well, but definitely binds x1 to a value. I'm wondering if the documentation can do something specifically to prevent this incorrect but in my opinion, plausible, expectation. For instance, by stating that on the last line, x1 and x2 are arguments of a function whose type is already fixed by the type of let*, and not arbitrary values.

A related point is that the terms 'monad' and 'applicative' are used in the documentation to motivate the notation. Is the knowledge of both these terms something that (new) users of OCaml should be required to have before they can understand the manual? Personally, I never knew what an applicative was until today. I concede that the examples are understandable without these terms; but would it make sense to give a module signature for a monad and for an applicative in the documentation to make it more accessible?

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Dec 12, 2018

However, what I find surprising is that after the let* bindings, x1 and x2 are apparently not bound values as usual in OCaml. For instance, replacing the last line with (x1 + x2) would not type-check.

I'm not sure I follow you here. x1 and x2 are bound to values just as in an ordinary let. They are indeed translated to arguments of a function, but there is no real difference between arguments and values bound by let.

I concede that the examples are understandable without these terms; but would it make sense to give a module signature for a monad and for an applicative in the documentation to make it more accessible?

There's a delicate line to walk here. I'm reluctant to put a full blown tutorial on monads and applicatives inside the manual -- there are plenty of those already and many are better than what I would write -- but at the same time we don't want to confuse users who don't know what they mean. Your suggestion of including module signatures seems reasonable, I'll have a go at fitting them into the description somewhere.

@ELLIOTTCABLE

This comment has been minimized.

Copy link

ELLIOTTCABLE commented Dec 12, 2018

Perhaps more complicated details, such as the relevance to monadic modules and whatnot, could be moved to a ‘rationale’ section below the simple, straightforward explanation of the mechanism?

@nilsbecker

This comment has been minimized.

Copy link

nilsbecker commented Dec 13, 2018

For instance, replacing the last line with (x1 + x2) would not type-check.

I'm not sure I follow you here. x1 and x2 are bound to values just as in an ordinary let.

I might be wrong, or may have worded it badly. Let me try again. The translation is this:

let find_and_sum tbl k1 k2 =
  ( let* ) (Hashtbl.find_opt tbl k1)
    (fun x1 ->
       ( let* ) (Hashtbl.find_opt tbl k2)
         (fun x2 -> return (x1 + x2)))

Here, the last line is a function of type int -> int option but a function of type int -> int would not type-check. So replacing the last line with (fun x2 -> x1 + x2) would not type-check, yes? If so, then also

let find_and_sum tbl k1 k2 =
  let* x1 = Hashtbl.find_opt tbl k1 in
  let* x2 = Hashtbl.find_opt tbl k2 in
    (x1 + x2)

is not accepted. My naive expectation was that let*, like let would not in itself restrict the return type of the function find_and_sum. Basically, the expectation was that after the let* lines I could still write f (x1 + x2) for arbitrary f : int -> 'a. If you compare a similar version with exceptions instead of option types:

let find_and_sum tbl k1 k2 =
  let x1 = Hashtbl.find tbl k1 in
  let x2 = Hashtbl.find tbl k2 in
    f (x1 + x2)

should be fine.

I'm not saying anything should be different about the semantics, of course, just that the syntax might suggest a wrong analogy to the (naive) user.

@texastoland

This comment has been minimized.

Copy link

texastoland commented Dec 13, 2018

@lpw25 would you mind commenting on #1947 (comment)? I like it conceptually yet I feel like a strength of OCaml relative to Haskell is limiting use of mysterious symbols (= for binding as much as let*/let+).

@OvermindDL1

This comment has been minimized.

Copy link

OvermindDL1 commented Dec 13, 2018

Just to note, I'm really not a fan of this syntax the more I look at it. I think I'd prefer something like:

let.SomeModule a = 4 in
...

Where it is let.<ModuleName>, the ModuleName is opened within it, and that module defines operators (like let (=) a b = ... would probably be popular, as may others) that you can use within chained and's of that let, so you could do something like this:

let.MyThing a <-- something () in
and b = blah(a) in
return b

Which would unfold into the expected things as described earlier in this thread. This moves the symbol to where you expect (the operator) and allows an opened DSEL from that module to appear in the chain, you could even combine multiple modules and styles by just let.MyThing a <=> 4 in let.SomeOtherThing b = bloop(a) in vwoop b opening a new let.<ModuleName> section.

It really seems hairy to have the let*/and* things themselves be overridden instead, easy to miss, etc...

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Dec 14, 2018

@nilsbecker I see. You're thinking of:

let x = ... in

as a stand-alone statement and are thus surprised when that changing the let affects things beyond this statement.

It is more correct to think of let as an expression:

let x = ... in
  ...

and so changing the let naturally affects the body of the binding as well as the definition.

I'll see if I can improve the documentation wording so that things are clear to people who are thinking along those lines.

@Freyr666

This comment has been minimized.

Copy link

Freyr666 commented Dec 14, 2018

@lpw25 I think what people are complaining about is that custom monadic let is way too confusing, especially for the novice.

When I was a complete newbie in Haskell and tried it for the first time, I had a hard time dealing with the do-notation (e.g. why can't I intermix different statements, like ST and IO). And let seems even more confusing than do-notation due to it's syntactic similarity to the usual let.

Usual let expression is (let x : 'a = … in e : 'b) : 'b, sort of sugared lambda application, while let operators impose additional and unobvious restrictions on the result type, adding an implicit function call. What's (let*), is it a map, bind, or a custom function? Syntactically it's like let, though it 1) is very obscure and tells nothing about its semantics and 2) confuses the neophyte making him or her struggle to understand why can't they embed a result-returning-function into their option-monad-let chain. And 3) it uses *+@ operators, which are confusing.

So while I'm dreaming day and night about monadic let instead of m >>= fun x -> abomination, I'm a bit worried about this making OCaml less clear and less novice-friendly. At least something like let+bind x =... or let.bind x = ... or let.opt x = ..., or something more or less explicit may be a better (though more verbose and ugly, and I don't like how my examples looks at all) way of doing it.

Perhaps we could just use one let operator, for example let*, forcing people to define let operators within the submodules, defining their semantics. something like

let open List in 
Map or Applicative.(let* x = list in )

and

let open Option in
Bind or Monad.(let* x = get_opt ... in Some x)
@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Dec 14, 2018

Regarding changing the = symbol. Using <- is definitely a bad idea because <- has a consistent meaning of mutating state in OCaml. Using <= would be possible but is likely to cause confusion with respect to its meaning as less-than-or-equal. Semantically using = is fine, you are binding a name to the given value -- the value happens to be wrapped in a monad but you are still saying that "x equals the result of this computation". It looks a bit odd with things like list where the computation has multiple results, but thinking about such things as computations is always a little strange. To a certain extent the argument against using = would also suggest that we shouldn't allow

let x = print_endline "Hello"; 5

because x is only being bound to the result of the computation not to the computation itself.

@OvermindDL1 I see no good argument for adding another ad-hoc form of local open. That seems likely to cause a lot of confusion for little gain. The other part of your suggestion is to use:

let x =* ... in
and y =* ... in
let z =+ ... in
...

instead of:

let* x = ... in
and* y = ... in
let+ z = ... in
...

This places the operator on the wrong thing. The choice of operator affects the whole let not just the definition part. The distinction between let* and let+ is how it affects the body of the let, moving the distinction onto the = makes this much more confusing -- it essentially reinforces the misunderstanding that @nilsbecker had.

I think people should take a moment to consider what is really happening here. We are replacing the operator >>= with the operator let* and the operator >>| with the operator let+. These operators are, if anything, clearer that what they replace. Any concerns about the need to use open apply just as much now as they will with the new operators, and yet that is not a common complaint about the existing operators. The chosen syntax is based on an existing choice in another language (F#) where the feature has proven popular and has not lead to huge amounts of confusion.

It is also worth considering Stroustup's rule -- essentially that people always demand a loud syntax for something new, and then later they get annoyed with how loud the syntax is for something so established. The syntax here is deliberately not a loud obvious syntax because the aim of monadic syntax is to allow you to work within an ambient monad as if it were simply the ambient monad of the language itself. You obviously need to be able to see clearly which lets are binds, maps and non-monadic, but you do not want that to interrupt the underlying logic of the code -- which is essentially independent of the monad that it is in.

@Freyr666

This comment has been minimized.

Copy link

Freyr666 commented Dec 14, 2018

The chosen syntax is based on an existing choice in another language (F#)

It seems that in F# it's let! only, and they work only within a computational expression, while let{+,*,@} are custom expressions.

@nilsbecker

This comment has been minimized.

Copy link

nilsbecker commented Dec 14, 2018

We are replacing the operator >>= with the operator let* and the operator >>| with the operator let+

I think this is a good point of comparison. The existing options of >>= etc. are definitely not easier to read or to disambiguate than what is proposed. I find that using >>= limits my desire to introduce more than one monad since adding more variations >>=$, >>=% feels more and more like gibberish. How many different letX variations within the same scope are reasonable? If it's no more than three or so, then the explicit module annotation let.Module ... = ... in ... seems overly heavy and I would prefer letXXX .... If there may be many simultaneous monads, let.Module might be easier to parse. But then, one could also resort to opening the respective module locally.

@bluddy

This comment has been minimized.

Copy link

bluddy commented Dec 14, 2018

My opinion is that the resistance to let+ and let* is psychological. When looking over a block of code, it's very easy for the small + and * operators to blend in, particularly because our minds don't expect anything of importance in the area of the let. As ugly as let%bind is, you can't mistake it for a simple let. I think this is the advantage of the ! operator, which attracts the reader's attention -- we've been conditioned by culture to have ! draw our attention to things in general. Perhaps using let!+ and let!* would therefore seem more reasonable to people? Or even let! and let!!, or let! and let!+?

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Dec 14, 2018

I think @bluddy just put his finger on much of what was bothering me.

@OvermindDL1

This comment has been minimized.

Copy link

OvermindDL1 commented Dec 14, 2018

Precisely what @bluddy stated, that combined with you don't know where the new lit+ or whatever is coming from (local open? top-level open? etc...?) and where let.Module ... is perfectly explicit and obvious in both cases while being very simple syntactically.

@bluddy

This comment has been minimized.

Copy link

bluddy commented Dec 14, 2018

you don't know where the new lit+ or whatever is coming from (local open? top-level open? etc...?)

This applies to every single value -- you have no idea where it's coming from, and instead have to find the relevant open. You do have the option of specifying a module for values, and maybe we could allow that option, so we could have let!, let!+ let!.Module and let!+.Module.

@texastoland

This comment has been minimized.

Copy link

texastoland commented Dec 14, 2018

In addition to above let! (nor do notation) doesn't conflate bind with map or both (F# reuses other syntax). In both F# and Haskell (at least for me) I could read and even compose computations without understanding the transformation. I didn't find that with ppx_let and have even less of a mental map for the new symbols (maybe bind is related to products and map to sums in CT?). I want to reread your thoughtful response but superficially =* and =+ convey more intuitively "not talking about equality anymore" vs "not talking about binding names anymore" and feel less alien and more noticeable.

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Dec 18, 2018

I've had a go at improving the documentation in #2206. I didn't change much, but hopefully its a bit clearer. Further suggestions welcome.

@ELLIOTTCABLE

This comment has been minimized.

Copy link

ELLIOTTCABLE commented Dec 23, 2018

So I'm finally playing around with this — pretty cool!

I'm pretty confused as to what is expected of the and operators, here, though:

let (let+) = Lwt.map
let (and+) = Lwt.map
let (let*) = Lwt.bind
let (and*) = Lwt.bind


let () =
   Lwt_main.run begin
      let* line1 = Lwt_io.(read_line stdin)
      and* line2 = Lwt_io.(read_line stdin) in
      Lwt_io.(write_line stdout (line1 ^ line2))
   end

yields:

File "blah.ml", line 21, characters 27-42:
21 |       and* line2 = Lwt_io.(read_line stdin) in
                                ^^^^^^^^^^^^^^^
Error: This expression has type string Lwt.t
       but an expression was expected of type string -> 'a Lwt.t

Coming from JavaScript, I'm pretty excited for something that basically looks like a more-general async/await (if I'm reading this correctly? Forgive me, talk of applicatives and monads sometimes goes over my head 🤣); but I can't quiiiite figure out how to apply this with Lwt for the similar purposes of cleanly interleaving asynchronous and synchronous code …

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Dec 23, 2018

You can use the following for the and operators:

let (and*) a b =
  Lwt.bind a (fun x -> Lwt.bind b (fun y -> (x, y))

although there is not much point using them when they are defined that way.

I would have thought that lwt could provide a more efficient implementation, but I can only see the confusingly named join function and the <&> operator:

val join : unit t list -> unit t
val ( <&> ) : unit t -> unit t -> unit t

for composing multiple threads. What you need is a slightly more general function like <&> that works for non-unit threads. Async provides that as both for Deferred.ts and I'm sure `lwt could provide one as well:

val both : 'a t -> 'b t -> ('a * 'b) t

Note that the lwt ppx just uses binds for supporting let%lwt ... and ..., which I assume means they don't think there is much performance benefit to having a proper and, so you're probably fine to just do without and operators.

@pmetzger

This comment has been minimized.

Copy link
Member

pmetzger commented Dec 23, 2018

@lpw25 Would it be possible for a tutorial to be written on the use of these operators? I suspect they're going to be confusing to a lot of people, especially since monads aren't a common thing (yet) in the OCaml world.

@yallop

This comment has been minimized.

Copy link
Member

yallop commented Dec 24, 2018

What you need is a slightly more general function like <&> that works for non-unit threads. Async provides that as both for Deferred.ts and I'm sure lwt could provide one as well:

val both : 'a t -> 'b t -> ('a * 'b) t

There's an issue open about this:

    More general join and choose operators (#325)

There's also some discussion under the issue of an apparent problem with the Lwt translation of let...and that may be related (but I haven't checked).

314eter added a commit to 314eter/tree-sitter-ocaml that referenced this pull request Jan 15, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment