State monad with explicit lambda functions in Prova

State monad is perhaps the most widely known monad. The current literature on the State monad and monads in general seems to require a proliferation of syntactic constructs that the likes of the Haskell language use to represent these concepts. It is clear that there is unity (the category theory) behind all this and yet it does not seem to be as clear as it should be. Just consider this syntax from http://www.haskell.org/all_about_monads/html/statemonad.html

newtype State s a = State { runState :: (s -> (a,s)) } 
instance Monad (State s) where 
    return a        = State $ \s -> (a,s)
    (State x) >>= f = State $ \s -> let (v,s') = x s in runState (f v) s' 

makeRandomValueST :: StdGen -> (MyType, StdGen)
makeRandomValueST = runState (do n <- getOne (1,100)
                                 b <- getAny
                                 c <- getOne ('a','z')
                                 m <- getOne (-n,n)
                                 return (MT n b c m))

My question is, can we at least try to simplify this? In fact, even explanations differ widely, with discussions about monads as computations, vs. monads as containers, vs. monads as constructors. I would prefer it all to look and behave the same syntactically and semantically. In Prova, a sequence of bind functions is expressed via function composition and as you'll see below, lambda expressions in the Haskell do-style are available as easily.

Let's start with the new example func_007.prova. The first part shown below is just the test goals plus the functions used in the tests. Reminder, in Prova, [x,y,...] is the same as x(y,...).

% Demonstrate
%    the State monad defined in terms of map and join,
%    the use of monadic computations instead of monadic instances as inputs to bind,
%    the use of explicit lambda functions in the bind pipelines
%
% In all next 5 examples, internal results are not exposed explicitly, there is no lambda variables. 
% Use state generator with an initial state as input
% getState 1 =>> (\x -> putState x)
% this returns: X=[state,[1,1]]
:- solve(
	derive(
		[[join,map(putState)],[[getState(1)]],X]
	)
).

% getState 1 =>> (\x -> incValue x)
% this returns: X=[state,[2,2]]
:- solve(
	derive(
		[[join,map(incValue)],[[getState(1)]],X]
	)
).

% state([1,1]) =>> (\x -> incValue x)
% this returns: X=[state,[2,2]]
:- solve(
	derive(
		[[join,map(incValue)],[state([1,1])],X]
	)
).

% state([true,'a']) =>> (\x -> flipcase x)
% this returns: X=[state,[false,'A']]
:- solve(
	derive(
		[[join,map(flipcase)],[state([true,'a'])],X]
	)
).

% getState 1 =>> (\x -> putState . add 1 x) =>> (\x -> putState . add 1 x)
% this returns: X=[state,[3,3]]
:- solve(
	derive(
		[[join,map([putState,add(1)]),join,map([putState,add(1)])],[[getState(1)]],X]
	)
).

% The examples below use explicit lambda functions on the state contents.
% The full state pair (state,result) is passed transparently between stages.
% getState 1 =>> (\x -> incValue x)
% this returns: A=1, X=[state,[2,2]]
:- solve(
	derive(
		[[join,map(lambda(A,[incValue,A]))],[[getState(1)]],X]
	)
).

% getState 1 =>> (\A -> incValue A) =>> (\B -> incValue B)
% this returns: B=2, A=1, X=[state,[3,3]]
:- solve(
	derive(
		[[join,map(lambda(B,[incValue(B)])),join,map(lambda(A,[incValue(A)]))],[[getState(1)]],X]
	)
).

% Use function composition in lambda functions.
% Note, we must put the list of functions in a list.
% getState 1 =>> (\A -> (incValue A =>> (\B -> (putState . add(A,B))))
% this returns: B=2, A=1, X=[state,[3,3]]
:- solve(
	derive(
		[[join,map(lambda(B,[[putState,add(A,B)]])),join,map(lambda(A,incValue(A)))],[[getState(1)]],X]
	)
).

%%% state transformers %%%
% Needs to take and ignore the extra state variable 
add([D,V,S],[VM,S]) :-
	VM=V+D.	

getState([S],state([S,S])).

% Note that putState(V) is still a function (\S -> (V,V))
putState([V,S],state([V,V])).

% Note that the initial state is actually ignored in this example
incValue([V,S],state([VM,VM])) :-
	VM=V+1.

flipcase([C,true],state([CM,false])) :-
	CM=C.toUpperCase().
flipcase([C,false],state([CM,true])) :-
	CM=C.toLowerCase().

There are plenty of examples here. The first five show that the State monad is no different from the List or the Maybe monads. It requires a map function and a join function. There is no need for fmap, mapM, or fmapM, everything is done the same way. There is no need for type definitions, we just use a special term state([S,V]) that encapsulates the actual state variable and the result value. Each monadic function like incValue operates on raw data, the actual pair [S,V] under state(), and produces a wrapped monadic state. This monadic state is automatically shipped between the stages, provided we use join (as always) to unwrap the state that is wrapped twice.

Note that we can also use functions that do not produce state inside the state transformation pipeline. The function add is an example of that. It takes the value variable that is the first operand number to be added and then the second operand that comes from the monadic state passed around, plus the state variable that is not used but required. This function add does not produce the actual wrapped state, so there needs to be a state updater for add to work in the pipeline, so putState is used for that purpose.

Now for lambda functions. This adds the final ingredient to the whole puzzle. How do we keep intermediate result values and pass them to later stages, not just as part of the implicit value V passed in a wrapped state([S,V]) between the immediately connected stages? - The answer is: use lambda functions. The lambdas also solve the problem of using arbitrary expressions that assemble such intertmediate results in some combined whole. In the last three tests, we use the term lambda(Vars,Expression) that allows us to do this. The Expression can be either one (possibly partially applied) function with arguments, like incValue(V), or a function composition that then has to be a list containing a list of (possibly partially applied) functions, like [[putState,add(B,A)]]. Note that all the lambda variables are instantiated dynamically by unwrapping the value from the state passed from the previous stage. However, you can obviously pass the values between non-adjacent stages by reusing the same variable symbol from the earlier result appearing to the right in the functional composition sequence, at a later stage, appearing to the left in the composition.

An important point to observe in the last test repeated again below: the Prova function composition pipeline under 'derive' is totally flat while the comparable Haskell function requires nesting.

% Use function composition in lambda functions.
% Note, we must put the list of functions in a list.
% getState 1 =>> (\A -> (incValue A =>> (\B -> (putState . add(A,B))))
% this returns: B=2, A=1, X=[state,[3,3]]
:- solve(
	derive(
		[[join,map(lambda(B,[[putState,add(A,B)]])),join,map(lambda(A,incValue(A)))],[[getState(1)]],X]
	)
).

Now to the implementation, do you think that will be difficult?

%%% map definition for the State monad
map([lambda(V,Fun),state([S,V])],state([SM,VM])) :-
	!,
	derive([[Fun],S,[SM,VM]]).
map([Fun,state([S,V])],state([SM,VM])) :-
	!,
	derive([[Fun(V)],S,[SM,VM]]).

% an extra rule for using a monadic computation (a generator) as input
map([Fun,Gen],B) :-
	derive(Gen([],G)),
	map([Fun,G],B).

% a catch-all, map Fun on a non-monad (a datum): often called from the map rule for lists
% this is related to the discussion here on shape: http://www-staff.it.uts.edu.au/~cbj/Publications/shapes.html
map([Fun,A],B) :-
	derive(Fun(A,B)).

%%% join definition for the State monad
join(state(X),[X]).

And that is all. In fact, only the definition of map for the state(...) input had to be defined and the lambda case processed separately.