Do syntax can't handle wrapped let forms

[Izaakwltn]

Here's an example:

(defpackage #:let-do-bug
  (:use #:coalton
        #:coalton-prelude)
  (:local-nicknames (#:state #:coalton-library/monad/state)))

(in-package #:let-do-bug)

Without let:

(coalton-toplevel

  (declare add-to-state-twice (Integer -> (state:ST Integer Unit)))
  (define (add-to-state-twice x)
    "Adds x twice to the current state."
    (do
     (target <- state:get)
     (state:put (+ target x))
      (target <- state:get)
      (state:put (+ target x))))

  (define (add-twice x y)
    (fst (state:run (add-to-state-twice x) y))))

It also works with a standalone, non-wrapped let:

(coalton-toplevel
  (declare add-to-state-twice2 (Integer -> (state:ST Integer Unit)))
  (define (add-to-state-twice2 x)
    "Adds x twice to the current state."
    (do
     (target <- state:get)
     (state:put (+ target x))
      (let x1 = x)
      (target1 <- state:get)
      (state:put (+ target1 x1))))

  (define (add-twice2 x y)
    (fst (state:run (add-to-state-twice2 x) y))))

However it doesn't compile with a wrapped let:

(coalton-toplevel
  (declare add-to-state-twice3 (Integer -> (state:ST Integer Unit)))
  (define (add-to-state-twice3 x)
    "Adds x twice to the current state."
    (do
     (target <- state:get)
     (state:put (+ target x))
      (let ((x1 x))
        (target1 <- state:get)
        (state:put (+ target1 x1)))))

  (define (add-twice3 x y)
    (fst (state:run (add-to-state-twice3 x) y))))

Compiling add-to-state-twice3 returns the error:

(TARGET1 <- STATE:GET)
 ^^^^^^^ unknown variable

[stylewarning]

I don't think this is a "bug", but it's something we could opt to support.

DO syntax has relatively tight allowance for what's allowed, and same for LET syntax. LET syntax itself doesn't allow fragments of DO to be used within its syntax.

[eliaslfox]

I consider this a bug. Do should support the full expression syntax.

[stylewarning]

How much syntax? Is this OK?

(do
  (x <- (fn () (y <- ...))
  ...)

I don't believe Haskell supports what you're suggesting. let in a Haskell do is statement syntax of the do itself, which gets desugared to a normal let expression. See this BNF-ish grammar here. The relevant part:

exp    -> ...
       |	do { stmts }	(do expression)
       ...

stmts	  ->	stmt1 ... stmtn exp [;]	(n>=0)

stmt   ->	exp ;
       |	pat <- exp ;
       |	let decls ;
       |	;	(empty statement)

Same thing with Rust's do_notation crate.

For these reasons I don't agree.

[eliaslfox]

How much syntax? Is this OK?

no

See this BNF-ish grammar here. The relevant part:

From the grammar it looks like all expressions are valid statements. The following compiles on ghc 9.6.4:

main = do
  let x = "hello" in putStrLn x
  putStrLn "world"

[stylewarning]

@eliaslfox I might have read into your suggestion too much, thinking you were saying statements should be allowed anywhere within expressions (which is the last example of this issue).

I agree then that expressions should be allowed, but statements (as they're called in the grammar) should only be in the syntax of do.

Apologies for the misunderstanding.

[eliaslfox]

No worries. I missed that detail when reading the last example.

The following compiles in Coalton currently:

COALTON-USER> (coalton-toplevel
                (define (f x)
                  (do
                   (y <- (pure x))
                   (let ((z y))
                     (pure z)))))
; No value
COALTON-USER> (type-of 'f)
∀ :A :B. MONAD :B ⇒ (:A → (:B :A))

It looks like the correct behavior is implemented.