[clean-list] Monad Type Classes and Uniqueness Typing
Fabien Todescato
f.todescato@larisys.fr
Fri, 28 Jun 2002 13:20:55 +0200
Thank you Arjeen for your most welcome comments.
As you honestly point out, your approach may prove to be a little too
restrictive for my purposes, namely to have a monadic programming framework
with overloaded monadic operators. Whereas you come up with bind :: u:(m .a)
v:(.a -> u:(m .b)) -> u:(m .b), [v <= u], I have class (mBind) infixl 4 m ::
( m a ) ( a -> ( m b ) ) -> m b, which - as I understand the type system -
is applicable to a larger class of monads. From this I hope to build a
monadic programming library where stateful computations with unique state
are integrated in a uniform manner.
Honestly, I am still surprised that the mBind combinator without uniqueness
typing constraints can be overloaded for a state-transformer monad handling
unique states. Unless I build myself a formal proof that indeed such is the
case, I will still suspect a bug in the Clean 2.0 typechecker :)
Now, please, in order to enlighten me about the use of continuations for
concurrent thread implementation, I would be very glad if you could provide
me with some pointers to papers :) I am at the moment reading the beautiful
thesis by Magnus Carlsson and Thomas Hallgren "Fudgets - Purely Functional
Processes with Applications to Graphical User Interfaces" where the use of
continuations seems to be an essential ingredient.
Best regards, Fabien TODESCATO
> -----Message d'origine-----
> De: Arjen van Weelden [SMTP:arjenw@cs.kun.nl]
> Date: vendredi 28 juin 2002 12:22
> À: Clean mailing list (Adresse de messagerie)
> Objet: Re: [clean-list] Monad Type Classes and Uniqueness Typing
>
> 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
> >
> >
> >
> >
>
>
>
> _______________________________________________
> clean-list mailing list
> clean-list@cs.kun.nl
> http://www.cs.kun.nl/mailman/listinfo/clean-list