[clean-list] Monad Type Classes and Uniqueness Typing

[Fabien Todescato]

Dear Cleaners,

	The purpose of that somewhat lengthy communication is to present the
definition of a state transformer monad for Clean 2.0. The interest of the
definition proposed here is that the state monad is designed so as to
accomodate the threading of a unique state - such as * World , * ( Array a x
), or * PSt x - as well as the use of overloaded monadic operators. That
latter feature is especially appealling since through the use of so-called
'Monad Transformers', the overloading of monadic operators allows monads
with complex features to be build in a modular manner. For example, it is
shown in [1] how to build  by the composition of monad transformers
backtracking parsers that can handle IO during the very process of parsing.
Such parsers are build by applying a backtracking monad transformer
ultimately to the IO monad. Unfortunately, that paper presents the
constuction for Haskell, where the IO Monad and the relevant overloaded
monadic operators are taken for granted, which is not the case in Clean 2.0.

	It seems intuitively obvious that uniqueness-typing à la Clean is
superior to ad-hoc predefined monads à la Haskell, the former allowing one
to build the latter. However, the definition of an IO monad à la Haskell,
with overloaded monadic operators, based on the uniqueness typing of Clean,
turns out to be a tougher nut to crack than expected. Indeed, we will see in
the following that the standard state-transformer monad definition :

:: STM s x = STM ! .( s -> .( s , x ) )

does not support the definition of an overloaded monadic bind operator,
because of the unfavourable interaction between uniqueness typing and
operator overloading.

However, by using the following continuation-passing style state-transformer
monad :

:: STM s z y = STM ! .( .( y s -> z ) -> .( s -> z ) )

it is possible to circumvent uniqueness-typing problems and define an
overloaded monadic bind operator.

The part A below presents a tentative definition based on the standard
state-transformer monad. The part B below presents the definition based on
the continuation-passing style  state-transformer monad. The part C
concludes. A short bibliography is given at the end.

It is the hope of the author that this work may prove an interesting -
albeit small :) - contribution to the top-notch Clean 2.0 functional
programming system.

Sincerely yours, Fabien TODESCATO

PS.The code fragments presented in the sequel have been submitted to the
Clean 2.0 compiler. Apart from uniqueness typing and type constructor
classes, the code does not rely on special typing construct whatsoever. The
type annotations in the code have been for the most part derived by the
compiler itself. The StdEnv module should be imported in order to get the
standard files and arrays operations used in the examples.

---------------------------------------------------
A.Trying with the standard state-transformer monad.
---------------------------------------------------

The standard definition is - including uniqueness typing - :

:: STM s y = STM ! .( s -> .( s , y ) )

stmReturn :: .a -> .(STM .b .a)
stmReturn y = STM \ s -> ( s , y )

(stmBind) infix 4 :: ! u:(STM v:a w:b) x:(w:b -> y:(STM v:a z:c)) -> u0:(STM
v:a z:c), [y u <= v,y u <= w,y <= x,y <= z,y <= u0]
(stmBind) ( STM stm ) f = STM \ s -> let ( t , y ) = stm s in let ( STM h )
= f y in h t

stmRun :: u:(STM .a .b) .a -> v:(.a,.b), [u <= v]
stmRun ( STM f ) s = f s

Additionaly, we define the following operators that lift functions operating
on a - possibly unique - state to the state-transformer monad :

stmApp :: (.a -> .a) -> .(STM .a (.a -> .a))
stmApp f = STM \ s -> ( f s , f ) // Well, f is returned as the result of
the stateful computation.

stmAcc :: .(.a -> (.b,.a)) -> .(STM .a .b)
stmAcc f = STM \ s -> let ( y , t ) = f s in ( t , y ) // Designed to use
standard clean IO operations.

With the above, it is straightforward to implement monadic IO on a * File,
for example :

putChar :: .Char -> .(STM *File (.File -> .File))
putChar c = stmApp ( fwritec c )

putString :: [.Char] -> .(STM *File [.Char])
putString s = put s
where
  put [       ] = stmReturn s
  put [ h : t ] = putChar h stmBind \ _ -> put t

The following is a valid program performing IO on a * File using the above
monadic definitions :

Start :: * World -> * World
Start world
  # ( console , world ) = stdio world
//# ( console ,_      ) = stmRun ( putString ['Hello world !\n'] ) console
  # ( console ,_      ) = stmRun ( stmReturn ['Hello world !\n'] stmBind
putString ) console
  # ( _       , world ) = fclose console world
  = world

In the above, I write ( stmReturn ['Hello world !\n'] stmBind putString )
instead of ( putString ['Hello world !\n'] ) only to emphasize the use of
monadic operators.

Now, recall the type of stmBind :

(stmBind) infix 4 :: ! u:(STM v:a w:b) x:(w:b -> y:(STM v:a z:c)) -> u0:(STM
v:a z:c), [y u <= v,y u <= w,y <= x,y <= z,y <= u0]

If we ignore the uniqueness atributes and constraints, we have :

stmBind :: !(STM a b) (b -> STM a c) -> STM a c

That is, with m such that ( m b ) = ( STM a b ) :

stmBind :: ! ( m b ) ( b -> m c ) -> m c

Which is precisely the signature of the bind operator for a monad m.

Now, if we try to capture ( STM a ) as instance of a monad equipped with a
mBind operator, for example :

class (mBind) infixl 4 m :: ( m a ) ( a -> m b ) -> m b

instance
  mBind ( STM a )
where
  (mBind) m f = (stmBind) m f

When we try using as follows the overloaded mBind operator :

Start :: * World -> * World
Start world
  # ( console , world ) = stdio world
  # ( console ,_      ) = stmRun ( stmReturn ['Hello world !\n'] mBind
putString ) console // Uniqueness-typing errors here !
  # ( _       , world ) = fclose console world
  = world

We get the following uniqueness-typing error :

Uniqueness error [moreFTcombinators.icl,63,Start]:"argument 1 of stmRun"
attribute at indicate position could not be coerced ^STM File [u:Char]
Uniqueness error [moreFTcombinators.icl,63,Start]:"argument 1 of mBind"
attribute at indicate position could not be coerced ([Char] -> u:(STM ^File
v:[w:Char]))

One may think that the above comes from uniqueness constraints not properly
taken into account in the definition of the overloaded operator :

class (mBind) infixl 4 m :: ( m a ) ( a -> m b ) -> m b

However, the uniqueness constraints in the stmBind operator involve the type
variable s in ( STM s y ), which cannot occur in the definition of the
overloaded operator mBind, since it is hidden in the unary type constructor
m = ( STM s ) when we write :

instance
  mBind ( STM s ) // The type variable s becomes hidden in a unary type
constructor.
where
  (mBind) m f = (stmBind) m f

Thus, no matter how hard we try equipping the overloaded mBind operator with
suitable uniqueness constraints, it is likely that ( STM s ) cannot be made
an instance of mBind. ( The author did try hard, before seeking another way
out... )

-----------------------------------------------------------
B.Trying with a continuation-based state-transformer monad.
-----------------------------------------------------------

Should we then forget all our hopes about our state-transformer monad ? Not
yet. As surprinsing as it may sounds, a well-known FP trick will prove
handy. Indeed, instead of having ( STM s y ) encapsulate a ( s -> ( s , y )
) value that is a function yielding a pair, we may instead use a
continuation-passing style where we take as argument a continuation taking
two arguments.

To make things short, we apply the transformation ( s -> ( s , y ) ) ~ ( s (
s y -> z ) -> z ). It is now but a short step to notice that in a similar
vein ( s ( s y -> z ) ) ~ ( ( s y -> z ) -> ( s -> z ) ).

>From this we define as follows our continuation-passing state-transformer
monad :

:: STM s z y = STM ! .( .( y s -> z ) -> .( s -> z ) )

With the usual operators as follows :

stmReturn :: a -> STM .b .c a
stmReturn y = STM \ k -> k y

stmApp :: (.a -> .a) -> .(STM .a .b (.a -> .a))
stmApp f = STM \ k -> \ s -> k f ( f s )

stmAcc :: .(.a -> (.b,.a)) -> .(STM .a .c .b)
stmAcc f = STM \ k -> \ s -> let ( y , t ) = f s in k y t

(stmBind) infixl 4 :: ! .(STM .a .b c) (c -> .(STM .a .b .d)) -> STM .a .b
.d
(stmBind) ( STM stm ) f = STM \ k -> stm ( \ y s -> let ( STM g ) = f y in g
k s )

stmRun :: !.(STM .a u:(.a,b) b) .a -> v:(.a,b), [u <= v]
stmRun ( STM f ) s = f ( \ y s -> ( s , y ) ) s

We can check the working of the above by trying some monadic IO with a *
File, as follows - same example as in part A - :

putChar :: .Char -> .(STM *File .a (*File -> .File))
putChar c = stmApp ( fwritec c )

putString :: ![.Char] -> STM *File .a [Char]
putString s = put s
where
  put [       ] = stmReturn s
  put [ h : t ] = putChar h stmBind \ _ -> put t

Start :: * World -> * World
Start world
  # ( console , world ) = stdio world
  # ( console ,_      ) = stmRun ( stmReturn ['Hello world !\n'] stmBind
putString ) console
  # ( _       , world ) = fclose console world
  = world

Now, contrary with what we had in part A., we see that the type of the
stmBind operator does not involve complex uniqueness typing constraints :

(stmBind) infixl 4 :: ! .(STM .a .b c) (c -> .(STM .a .b .d)) -> STM .a .b
.d

We can now try again to capture ( STM .a .b ) as instance of a monad, by
defining :

class (mBind) infixl 4 m :: ( m a ) ( a -> ( m b ) ) -> m b

instance
  mBind ( STM .a .b )
where
  (mBind) m f = (stmBind) m f

And we can check that the overloaded operator does now work in presence of
uniqueness typing and allow us to do monadic IO :

putChar :: .Char -> .(STM *File .a (*File -> .File))
putChar c = stmApp ( fwritec c )

putString :: ![.Char] -> STM *File .a [Char]
putString s = put s
where
  put [       ] = stmReturn s
  put [ h : t ] = putChar h mBind \ _ -> put t // NOTE THE USE OF THE
OVERLOADED mBind HERE.

Start :: * World -> * World
Start world
  # ( console , world ) = stdio world
  # ( console ,_      ) = stmRun ( stmReturn ['Hello world !\n'] mBind
putString ) console  // NOTE THE USE OF THE OVERLOADED mBind HERE.
  # ( _       , world ) = fclose console world
  = world

Similarly, we can check that destructive array operations can be performed
in a monadic manner using the mBind overloaded operator :

updateArray :: .Int a -> .(STM *(b a) .c (*(b a) -> *(b a))) | Array b a
updateArray i x = stmApp \ a -> update a i x

updateListArray :: ![(.Int,a)] -> STM *(b a) .c [(Int,a)] | Array b a
updateListArray l
  = update l
where
  update [               ] = stmReturn l
  update [ ( i , y ) : l ] = updateArray i y mBind \ _ -> update l  // NOTE
THE USE OF THE OVERLOADED mBind HERE.

Start :: * {# Int }
Start = fst ( stmRun ( stmReturn [(0,8),(4,2),(1,3)] mBind updateListArray )
( createArray 8 0 ) )

----------------------
C.Conclusion and Plans
----------------------

By using a continuation-passing style to implement the state-transformer
monad, we have succeeded in equipping Clean 2.0 with monadic IO or monadic
array operations, similar to the ones provided in Haskell. Furthermore, the
continuation-passing state-transformer monad so built can be used in a
generic monadic framework by providing instances of overloaded monadic
operators.

The author plans to use the continuation-passing state-transformer monad
presented here in order to build efficient and IO-capable parsers in the
manner presented in [1]. More generally, it is hoped that this work may help
Clean functional programmers benefit from the wealth of monadic programming
techniques usually presented in a Haskell setting.

--------------------
(Short) Bibliography
--------------------

[1] Monadic-style Backtracking  - Ralf Hinze
[2] Systematic Design of Monads - John Hughes & Magnus Carlsson
[3] Monadic Parser Combinators  - Graham Hutton, Erik Meijer