do blocks within functions

[weaversa]

Why does one work and one fail?

sawscript> let f1 a b = (a, b)
sawscript> f1 1 2
(1,2)
sawscript> let f2 a b = do { return (a, b); }
sawscript> f2 1 2

user error (Not a monomorphic type: {a.4} a.4 (Int, Int))

[TomMD]

Much like Haskell monads, return isn't simply a way to return from imperative code:

sawscript> :type return
{a.0, a.1} a.1 -> a.0 a.1

If you'd like to remove the ambiguity caused by that first type constructor (a.0 in the above) then you can add a type signature. Notice you can never return foo and get a value of type (Int,Int).

For example:

sawscript> f2 1 2 : TopLevel (Int,Int)
(1,2)

[weaversa]

Are there other monads besides TopLevel?

If not, and there's only one monad, would it be possible to automatically promote (demote?) non-monadic to monadic?

[brianhuffman]

The other monads are the ones for function specs (CrucibleSetup, JavaSetup, etc.) and the ProofScript monad.

It might be useful to have a kind of defaulting to TopLevel, which would help with your example.

[weaversa]

Defaulting would be lovely?

Would that somehow facilitate merging let x and x <- into one thing?

[brianhuffman]

No, defaulting would not let you merge let x and x <-. It would only apply in the (rare) situation where you've written a do block that doesn't use any monadic operations other than return. So the implementation effort would yield a pretty small reward.

Another feature we could consider is to allow the do syntax to be used with non-monadic types, so we could write definitions like

sawscript> let f3 a b = do { let c = b; (a, c); }

[brianhuffman]

Another idea is that maybe we should change the types of most TopLevel operations to have non-monadic types instead, e.g. change a -> TopLevel b to just a -> b.

[brianhuffman]

A third idea is to ditch the monadic types completely in favor of some kind of effect annotations on function types.

[atomb]

Using Python to control SAW should provide a more familiar notion of function definitions. That's probably easier than changing SAWScript, so I'm going to close this.