Monads in Qi
It is hard to even begin to learn the cutting edge of functional language theory these days without talking about monads. In languages running in a purely functional manner, monads offer a way of dealing with the outside environment in a safe and controlled manner. In a pure environment, monads provide us a way to carry data computations via pure functional composition and still have computations that happen "on the side." A lot of research into functional languages requires a solid understanding of monads and thus to apply their results to the Qi programming language, I'll define a few monad operations here and define a type theory that can handle the list monadSince you can find a wide variety of monads for the language Haskell, I will start by describing monads in Haskell and use that to define representations inside of the Qi language. Basically, a monad is a type that defines two operations. The operations are "lift" and "pipe". In Haskell, they are often called "return" and "bind" respectively. As long at the two functions hold the following identities, we can consider the type to be a monad.
Here is a definition of the rules a monad must follow in a pure version of scheme.
(pipe (lift x) f) = (f x)
(pipe m lift) = m
(pipe (pipe m f) g) = (pipe m (lambda (x) (pipe (f x) g)))
In Haskell, the Monad m class is defined by
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
We can see that return "lifts" a value of type a into the monad class m a. Bind takes in a monad of type "a" and a function that takes in a value of type "a" and gives a monad of type "b". Bind then returns to us a monad of type "b" where the monad "a" has been transformed by the function into a monad of type "b". Once we have these two functions working as defined, we have a monad. Notice that we have not defined these functions yet. Haskell allows us to define a higher order type that we promise that all implementations of the type will have the listed functions and they will match the given type signatures. These sorts of definitions are not as easy in Qi, yet.
One of the basic monad types in Haskell is the list monad. We define list monads as having type Monad [] and we can make a set of functions that follow the monad laws over Monad []'s.
instance Monad [ ] where
(x:xs) >>= f = f x ++ (xs >>= f)
[] >>= f = []
return x = [x]
Let us rewrite these rules in Qi.
(define bind
[] _ -> []
[X | Xs] F -> (append (F X) (bind Xs F)))
(define return
X -> [X] )
Well that was easy! Let us try out this new monad... We'll take a list of [10 20 30] and a function that takes an X and returns [X X+1] and give it to bind to see what it does with it.
(2-) (bind [10 20 30] (/. X [ X (+ X 1) ] ) )
[10 11 20 21 30 31]
So far, so good. Let us check the monad laws to see if this version follows those laws. Law 1 says that (bind (return X) F) == (F X)
(5-) (define f X -> [ X (+ X 1) ] )
f
(6-) (bind (return 2) f)
[2 3]
(7-) (f 2)
[2 3]
Law 2 says (bind Monad return) == Monad
(8-) (bind [ 4 5 6] return)
[4 5 6]
Law 3 says that (bind (bind Monad F) G) = (bind Monad (/. X (pipe (F X) G)))
(9-) (define g X -> [ (+ X 33) (+ X 44) ] )
g
(10-) (bind (bind [10 20 30] f) g)
[43 54 44 55 53 64 54 65 63 74 64 75]
(11-) (bind [10 20 30] (/. X (bind (f X) g)))
[43 54 44 55 53 64 54 65 63 74 64 75]
So we have proven that our monad list does in fact honor the monad laws. However, we are not running the type checker in Qi on this problem, so the monad we get is the same one that we can get in any functional language. We have to wait until runtime to see the error of the following attempt at using a monad.
(14-) (bind [10 20 a] (/. X (bind (f X) g)))
1+: a is not a NUMBER
So now the question becomes, can we get a monad into the TYPED version of Qi. Firstly, we must note that Qi has no notion of polymorphic type overloading. Hence we cannot easily make a general purpose "bind" operator that all monads can use. We also should note that the type checker treats a polymorphic list as a special case, and thus we cannot perform a direct translation like the one from Haskell. In some way, we will have to contain our lists in another type.
Let us take the simplest translation. If something is of type (list A) then we can make a monadic list type of (monad list A) via the following sequent rules.
(datatype monad
X : (list A);
=====
[X] : (monad list A);
)
Monadic lists are simply lists inside of a container list and any list in a container can be a monad list of that type. We should read this as saying, "We can construct monads from lists by adding a list around it and we can construct lists from monads." We note that Qi allows you to go back from a monadic representation to the list based one as long as you properly use the type. Unfortunately, Qi has no notion of modules so we cannot seal off this behaviour from other functions in our code.
Continuing, we will define some helper functions to allow us to manipulate the monad data structure inside the instance functions. Of course, Qi has no notion of either class or instance and allows us to pull lists from monads. But if we ignore these quirks for the moment, we can define a reasonable monad list type that works. I include a constructor function "list_monad" and a few internal data access helpers.
(define list_monad
{ (list A) --> (monad list A) }
X -> [X] )
(define m_head
{ (monad list A) --> A }
X -> (head (get_list X)))
(define m_tail
{ (monad list A) --> (monad list A) }
X -> [ (tail (get_list X))] )
(define m_cons
{ A --> (monad list A) --> (monad list A) }
X [Xs]-> [(cons X Xs)])
(define join
{ (monad list (monad list A)) --> (monad list A)}
Xs -> (join-help [[]] Xs))
(define join-help
{ (monad list A) --> (monad list (monad list A)) --> (monad list A) }
Final [[]] -> [ (reverse (get_list Final)) ]
Final ML -> (let XRest (m_tail (m_head ML))
(if (= XRest [[]])
(join-help (m_cons (m_head (m_head ML)) Final)
(m_tail ML))
(join-help (m_cons (m_head (m_head ML)) Final)
(m_cons (m_tail (m_head ML)) (m_tail ML))) )))
Our m_ functions and join properly deal with getting (list A)'s from their containers and putting them back in. Join has to take the job of flatten and check for the end of a list and if we find it, drop it from the "Final" list. This accounts for the if statement in the function. It obviously makes heavy use of the data manipulation functions which lowers legability. We can read it as saying, "Take the first element head of the list (remember that we have a monad list of a monad lists here) and put it on the final list. Then take the rest of that head list and put it back on the processing queue. The Final output list is built in reverse order so we are forced to reverse the computation at the end of the join. Not pretty, but it works for the purpose of monad construction.
Now we are in a position to define "bind" and "return" as before.
(define bind
{ (monad list A) --> ( A --> (monad list B)) --> (monad list B) }
XS F -> (join [(map F (get_list XS)) ]))
(define return
{ A --> (monad list A) }
X -> [[X]]
)
Note that we basically take the list out of the monad container and apply normal list functions to it, wrapping it up back in the monad container when we return.
Testing it out gives:
(14+) (bind (list_monad [10 20 30]) (/. X (list_monad [X (+ X 1)]) ))
[[10 11 20 21 30 31]] : (monad list number)
And our monad type is certainly not a list
(31+) (head (bind (list_monad [4 5 6]) return))
error: type error
Now let us assure ourselves that our monad list is polymorphic to type A. We now define a fractal symbol function f.
(36+) (define f
{ symbol --> (monad list symbol) }
X -> (list_monad [ x o x]) where (= X x)
_ -> (list_monad [ o o o]))
And let us use it with our monad functions
(37+) (bind (return x) f)
[[x o x]] : (monad list symbol)
(38+) (bind (bind (return x) f) f)
[[x o x o o o x o x]] : (monad list symbol)
(39+) (bind (bind (bind (return x) f) f) f)
[[x o x o o o x o x o o o o o o o o o x o x o o o x o x]] : (monad list symbol)
So there you have it, a very simple, poorly performing basic list monad of polymorphic type A in the Qi Programming Language. Feel free to offer any questions or criticism that you have. Thanks for reading.
9 Comments:
When you say respectively, I take it you made a mistake. Your 'lift' is more akin to 'return and your 'pipe' is more akin to 'bind.
By 
Christophe Poucet, at
11:52 AM
Thank you for the heads up, Christophe!
I did write that backwards. I've changed the sentence in the main article now. I usually only use "respectively" when I've double checked everything to make sure the indicated names match up logically. I guess I needed one more proofread. *grin*
Thanks for your comments. Feel free to leave more. *smile*
By EntropyFails, at
1:03 PM
I realize this is a tangent; but I can find nowhere else to discuss (QILang is moderated). . . . .
What happened to www.lambdassociates.org?
Perhaps it may be time to get an unmoderated list going for the Qi Language. =)
Lambda Associates is back up and running. They just had a couple server issues.
Don't feel bad about posting here, I'll take any blog comments I can get! (minus spam of course)
By EntropyFails, at
10:24 AM
Well, lambdassociates.org is back.
I'd like to get QI running on LispWorks first; but when I get into it seriously your "primes" example will be my QI starting point.
(I'm hoping to use QI to explore type concepts without having to divert into haskell).
I really like the type system in Qi as well. I find it easier to define types in Qi than in Haskell because it has no restrictions on types. I feel that this brings the type theory closer to the fundamentals than in Haskell where you are forced out of FOL types by the language design choices.
Let me know if you have any questions by either posting here or on the Qi Lang group!
By EntropyFails, at
3:21 PM
You freely use "lift" synonymously for "return", and "pipe" synonymously for"bind." This occasionally causes confusion.
For example, you write:
>Law 3 says that (bind (bind Monad F) G) = (bind Monad (/. X (pipe (F X) G)))
However, since you have already defined "pipe" to be synonymous with "bind," this actually means the following:
>Law 3 says that (bind (bind Monad F) G) = (bind Monad (/. X (bind (F X) G)))
In addition, after first defining the monad rules in pure Scheme as follows:
>(pipe (lift x) f) = (f x)
>(pipe m lift) = m
>(pipe (pipe m f) g) = (pipe m (lambda (x) (pipe (f x) g)))
you then check whether the following monad:
>(define bind
>[] _ -> []
>[X | Xs] F -> (append (F X) (bind Xs F)))
>
>(define return
>X -> [X] )
follows the monad laws using "bind" instead of "pipe."
Instead, it would seem better to redefine the monad laws in the first place using "bind" instead of "pipe," and "return" instead of "lift," as follows:
>(bind (return x) f) = (f x)
>(bind m return) = m
>(bind (bind m f) g) = (bind m (lambda (x) (bind (f x) g)))
That would eliminate naming inconsisties between the monad laws and the monad law checks for monads.
By Benjamin L. Russell, at
2:30 AM
I haven't found get_list funcion implementation.
Here is my variant:
(define get_list
{ (monad list A) --> (list A)}
[[X]] -> [X])
does it fit right?
Nevertheless
this application does not work:
(mbind (list_monad [10 20 30]) (/. X (list_monad [X (+ X 1)]) ))
partial function get_list;
aborted
Is that because i improperly defined get_list function?
