The HTML version of this document is generated automatically from the corresponding markdown file, don't change it!
This package is based on "The Operational Monad Tutorial" and this documentation describes its extension to a production-quality library. In other words, the "magic" gap between relevant paper and library implementation is documented here.
Take not that this this library is only ~50 lines of code, yet the documentation even includes a proof! :-)
Sources include Chuan-kai Lin's unimo paper, John Hughes 95, and Ryan Ingram's MonadPrompt package.
To understand what's going on, you'll have to read "The Operational Monad Tutorial". Here, I will first and foremost note the changes with respect to the tutorial.
There are several advanced examples as well, you can find them in the ./examples folder.
- Design and Implementation
- Other Design Choices
For efficiency reasons, the type Program representing a list of instructions is now abstract. A function view is used to inspect the first instruction; returning a type
data Prompt instr a where
+ >The HTML version of this document is generated automatically from the corresponding markdown file, don't change it!
This package is based on "The Operational Monad Tutorial" and this documentation describes its extension to a production-quality library. In other words, the "magic" gap between relevant paper and library implementation is documented here.
Take not that this this library is only ~50 lines of code, yet the documentation even includes a proof! :-)
Sources and inspiration for this library include Chuan-kai Lin's unimo paper, John Hughes 95, and Ryan Ingram's MonadPrompt package.
To understand what's going on, you'll have to read "The Operational Monad Tutorial". Here, I will first and foremost note the changes with respect to the tutorial.
Several advanced example monads demonstrate how to put this library to good use. They are located in the ./docs/examples folder.
Program typeFor efficiency reasons, the type Program representing a list of instructions is now abstract. A function view is used to inspect the first instruction; returning a type
data Prompt instr a where
hunk ./docs/Documentation.html 130
- >which is much like the old Program type, except that Then was renamed to (:>>=). The name Prompt was chosen in homage to the MonadPrompt package.
To see an example of the new style, here the interpreter for the stack machine from the tutorial:
interpret :: StackProgram a -> (Stack Int -> a)
+ >which is much like the old Program type, except that Then was renamed to (:>>=). The name Prompt was chosen in homage to the MonadPrompt package.
To see an example of the new style, here the interpreter for the stack machine from the tutorial:
interpret :: StackProgram a -> (Stack Int -> a)
hunk ./docs/Documentation.html 157
- >So-called "view functions" like view are a common way of inspecting data structures that have been made abstract for reasons of efficiency; see for example viewL and viewR in Data.Sequence.
The Program type supports (>>=) in constant time, albeit with the big caveat that this is only the case when not used in a persistent fashion. However, this is much less a restriction with monads than it would be with lists and (++).
More precisely, consider
leftAssociative :: Int -> StackProgram Int
+ >So-called "view functions" like view are a common way of inspecting data structures that have been made abstract for reasons of efficiency; see for example viewL and viewR in Data.Sequence.
The Program type supports (>>=) in constant time, albeit with the big caveat that this is only the case when not used in a persistent fashion. However, this is much less a restriction with monads than it would be with lists and (++).
More precisely, consider
leftAssociative :: Int -> StackProgram Int
hunk ./docs/Documentation.html 192
- >and the expression
interpret (leftAssociative n) []
+ >and the expression
interpret (leftAssociative n) []
hunk ./docs/Documentation.html 199
- >Evaluating this will now take O(n) instead of O(n^2) time for the old Program type from the tutorial. However, persistent use like
let p = leftAssociative n
+ >Evaluating this will now take O(n) instead of O(n^2) time for the old Program type from the tutorial. However, persistent use like
let p = leftAssociative n
hunk ./docs/Documentation.html 212
- >will now take O(n) time for each call of view instead of O(n) the first time and O(1) for the other calls.
Furthermore, Program is actually a type synonym and expressed in terms of a monad transformer ProgramT
type Program instr a = ProgramT instr Identity a
+ >will now take O(n) time for each call of view instead of O(n) the first time and O(1) for the other calls.
Furthermore, Program is actually a type synonym and expressed in terms of a monad transformer ProgramT
type Program instr a = ProgramT instr Identity a
hunk ./docs/Documentation.html 233
- >Likewise, view is a specialization of viewT to the identity monad. This change is transparent (except for error messages on type errors) for users who are happy with just Program but very convenient for those users who want to use it as a monad transformer.
The key point about the transformer version ProgramT is that in addition to the monad laws, it automatically satisfies the lifting laws for monad transformers as well
lift . return = return
+ >Likewise, view is a specialization of viewT to the identity monad. This change is transparent (except for error messages on type errors) for users who are happy with just Program but very convenient for those users who want to use it as a monad transformer.
The key point about the transformer version ProgramT is that in addition to the monad laws, it automatically satisfies the lifting laws for monad transformers as well
lift . return = return
hunk ./docs/Documentation.html 251
- >The corresponding view function viewT now returns the type m (ViewT instr m a). It's not entirely clear why this return type will do, but it's straightforward to work with, like in the following implementation of the list monad transformer:
data PlusI m a where
+ >The corresponding view function viewT now returns the type m (ViewT instr m a). It's not entirely clear why this return type will do, but it's straightforward to work with, like in the following implementation of the list monad transformer:
data PlusI m a where
hunk ./docs/Documentation.html 275
- >By the way, note that monad transformers are not the only way to build larger monads from smaller ones; a similar effect can be achieved with the direct sum of instructions sets. For instance, the monad
Program (StateI s :+: ExceptionI e) a
+ >By the way, note that monad transformers are not the only way to build larger monads from smaller ones; a similar effect can be achieved with the direct sum of instructions sets. For instance, the monad
Program (StateI s :+: ExceptionI e) a
hunk ./docs/Documentation.html 290
- >is a combination of the state monad
type State a = Program (StateI s) a
+ >is a combination of the state monad
type State a = Program (StateI s) a
hunk ./docs/Documentation.html 301
- >and the error monad
type Error e a = Program (ErrorI e) a
+ >and the error monad
type Error e a = Program (ErrorI e) a
hunk ./docs/Documentation.html 312
- >The "sum of signatures" approach and the (:+:) type constructor are advocated in Wouter Swierstra's "Data Types a la carte". Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.
The key point of this library is of course that the view and viewT functions respect the monad laws. While this seems obvious from the definition, the proof is actually not straightforward.
First, we restrict ourselves to view, i.e. the version without monad transformers. In fact, I don't have a full proof for the version with monad transformers, more about that in the next section.
Second, we use a sloppy, but much more suitable notation, namely we write
>>= | instead of Bind |
return | instead of Lift for the identity monad |
i,j,k,... | for primitive instructions |
Then, the view function becomes
The "sum of signatures" approach and the (:+:) type constructor are advocated in Wouter Swierstra's "Data Types a la carte". Time will tell which has more merit; for now I have opted for a seamless interaction with monad transformers.
The key point of this library is of course that the view and viewT functions respect the monad laws. While this seems obvious from the definition, the proof is actually not straightforward.
First, we restrict ourselves to view, i.e. the version without monad transformers. In fact, I don't have a full proof for the version with monad transformers, more about that in the next section.
Second, we use a sloppy, but much more suitable notation, namely we write
>>= | instead of Bind |
return | instead of Lift for the identity monad |
| view (return a) = Return a + >i,j,k,... | for primitive instructions |
Then, the view function becomes
view (return a) = Return a
hunk ./docs/Documentation.html 391
- >Clearly, view uses the monad laws to rewrite it's argument. But we want to show that whenever two expressions
e1,e2 :: Program instr a
+ >Clearly, view uses the monad laws to rewrite it's argument. But we want to show that whenever two expressions
e1,e2 :: Program instr a
hunk ./docs/Documentation.html 400
- >can be transformed into each other by rewriting them with the monad laws in any fashion (remember that >>= and return are constructors), then view will map them to the same result. More formally, we have an equivalence relation
e1 ~ e2 iff e1 and e2 are the same modulo monad laws
+ >can be transformed into each other by rewriting them with the monad laws in any fashion (remember that >>= and return are constructors), then view will map them to the same result. More formally, we have an equivalence relation
e1 ~ e2 iff e1 and e2 are the same modulo monad laws
hunk ./docs/Documentation.html 415
- >and want to show
e1 ~ e2 => view e1 = view e2 (some notion of equality)
+ >and want to show
e1 ~ e2 => view e1 = view e2 (some notion of equality)
hunk ./docs/Documentation.html 422
- >Now, this needs proof because view is like a term rewriting system and there is no guarantee that two equivalent terms will be rewritten to the same normal form.
Trying to attack this problem with term rewriting and critical pairs is probably hopeless and not very enlightening. After all, the theorem should be obvious because two equivalent expressions should have the same first instruction i. Well, we can formalize this with the help of a normal form
data NF instr a where
+ >Now, this needs proof because view is like a term rewriting system and there is no guarantee that two equivalent terms will be rewritten to the same normal form.
Trying to attack this problem with term rewriting and critical pairs is probably hopeless and not very enlightening. After all, the theorem should be obvious because two equivalent expressions should have the same first instruction i. Well, we can formalize this with the help of a normal form
data NF instr a where
hunk ./docs/Documentation.html 441
- >This is the old program type and the key observation is that NF instr is already a monad.
instance Monad (NF inst) where
+ >This is the old program type and the key observation is that NF instr is already a monad.
instance Monad (NF inst) where
hunk ./docs/Documentation.html 452
- >(I'll skip the short calculation and coinduction argument that this really fulfills the monad laws.) We can define a normalization function
normalize :: Program instr a -> NF instr a
+ >(I'll skip the short calculation and coinduction argument that this really fulfills the monad laws.) We can define a normalization function
normalize :: Program instr a -> NF instr a
hunk ./docs/Documentation.html 462
- >which has the now obvious property that
e1 ~ e2 => normalize e1 = normalize e2
+ >which has the now obvious property that
e1 ~ e2 => normalize e1 = normalize e2
hunk ./docs/Documentation.html 469
- >Now, the return type of view is akin to a head normal form, hence
normalize (view e1) = normalize (view e2)
+ >Now, the return type of view is akin to a head normal form, hence
normalize (view e1) = normalize (view e2)
hunk ./docs/Documentation.html 481
- >(for some suitable extension of normalize to the Prompt type.) But since view only uses monad laws to rewrite its argument, we also have
e1 ~ view e1 => normalize e1 = normalize (view e1)
+ >(for some suitable extension of normalize to the Prompt type.) But since view only uses monad laws to rewrite its argument, we also have
e1 ~ view e1 => normalize e1 = normalize (view e1)
hunk ./docs/Documentation.html 494
- >and this concludes the proof, which pretty much only showed that two equivalent expressions have the same instruction list and hence view gives equal results.
The monad transformer case is more hairy, I have no proof here. (If you read this by accident: don't worry, it's still correct. This is for proof nerds only.)
The main difficulty is that the equation
return = lift . return
+ >and this concludes the proof, which pretty much only showed that two equivalent expressions have the same instruction list and hence view gives equal results.
The monad transformer case is more hairy, I have no proof here. (If you read this by accident: don't worry, it's still correct. This is for proof nerds only.)
The main difficulty is that the equation
return = lift . return
hunk ./docs/Documentation.html 513
- >is an equation for the already existing return constructor and the notion of "first instruction" no longer applies. Namely, we have
m = return m >>= id = lift (return m) >>= id
+ >is an equation for the already existing return constructor and the notion of "first instruction" no longer applies. Namely, we have
m = return m >>= id = lift (return m) >>= id
hunk ./docs/Documentation.html 522
- >and it's not longer clear what a suitable normal form might be. It appears that viewT rewrites the term as follows
lift m >>= g
+ >and it's not longer clear what a suitable normal form might be. It appears that viewT rewrites the term as follows
lift m >>= g
hunk ./docs/Documentation.html 534
- >(To be continued.)
ProgramIn the unimo paper, the instructions carry an additional parameter that "unties" recursive type definition. For example, the instructions for MonadPlus are written
data PlusI unimo a where
+ >(To be continued.)
ProgramIn the unimo paper, the instructions carry an additional parameter that "unties" recursive type definition. For example, the instructions for MonadPlus are written
data PlusI unimo a where
hunk ./docs/Documentation.html 563
- >The type constructor variable unimo will be tied to Unimo PlusI.
In this library, I have opted for the conceptually simpler approach that requires the user to tie the recursion himself
data PlusI a where
+ >The type constructor variable unimo will be tied to Unimo PlusI.
In this library, I have opted for the conceptually simpler approach that requires the user to tie the recursion himself
data PlusI a where
hunk ./docs/Documentation.html 578
- >I am not sure whether this has major consequences for composeablity; at the moment I believe that the former style can always be recovered from an implementation in the latter style.
I am not sure whether this has major consequences for composeablity; at the moment I believe that the former style can always be recovered from an implementation in the latter style.