[clean-list] Monad Type Classes and Uniqueness Typing
Arjen van Weelden
arjenw@cs.kun.nl
Fri, 28 Jun 2002 12:22:10 +0200
Hello Fabien,
During my experiments with process-combinators and concurrent threads,
I've used more or less the same:
:: StMonad st a = StMonad !.(st -> *(a, st))
returnSt :: u:a -> v:StMonad .st u:a, [v <= u]
returnSt x = StMonad \st -> (x, st)
bindSt :: .(StMonad .st .a) u:(.a -> .StMonad .st .b) -> v:StMonad .st
.b, [v <= u]
bindSt (StMonad l) r = StMonad \st -> let (x, st`) = l st; (StMonad r`)
= r x in r` st`
:: MonadCnt st a = MonadCnt !.(*(a -> *(st -> st)) -> *(st -> st))
returnCnt :: u:a -> v:MonadCnt .st u:a, [v <= u]
returnCnt x = MonadCnt \mc st -> mc x st
bindCnt :: .(MonadCnt .st .a) v:(.a -> .MonadCnt .st .b) -> u:MonadCnt
.st .b, [v <= u]
bindCnt (MonadCnt l) r = MonadCnt \mc st -> l (\x -> let (MonadCnt r`) =
r x in r` mc) st
class Monad m
where
return :: u:a -> v:m u:a, [v <= u]
bind :: u:(m .a) v:(.a -> u:(m .b)) -> u:(m .b), [v <= u]
instance Monad (StMonad .st)
where
return x = returnSt x
bind l r = bindSt l r
instance Monad (MonadCnt .st)
where
return x = returnCnt x
bind l r = bindCnt l r
Notice that the type of bindSt is easier to read than yours and that the
type of bindCnt contains more uniqueness information. Unfortunately, the
type of the overloaded bind is a little more restrictive then the
non-overloaded versions. This is caused by restrictions imposed by the
implementation of the overloading system.
I find the first version easier to understand/use, but the continuation
style allows me to suspend continuations and reschedule them providing
me with a way to build cooperative threads in Clean. Adding exceptions
was also very easy using the continuation style. I have not really used
the overloaded bind, so it might be to restrictive for your purposes.
regards,
Arjen van Weelden
Fabien Todescato wrote:
>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
>
>
>
>_______________________________________________
>clean-list mailing list
>clean-list@cs.kun.nl
>http://www.cs.kun.nl/mailman/listinfo/clean-list
>
>
>
>