diff options
| author | bringert <bringert@cs.chalmers.se> | 2005-11-30 18:57:23 +0000 |
|---|---|---|
| committer | bringert <bringert@cs.chalmers.se> | 2005-11-30 18:57:23 +0000 |
| commit | d92a26fc9be92fb269888947a8b26aa12883065e (patch) | |
| tree | d74e451a1de42e95db949b0429d96ccb3178acfa /transfer/lib/maybe.tr | |
| parent | 12ca29b32b50fd924c5f69a30d204e4332dff4f9 (diff) | |
Added monad isntances for List and Maybe.
Diffstat (limited to 'transfer/lib/maybe.tr')
| -rw-r--r-- | transfer/lib/maybe.tr | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/transfer/lib/maybe.tr b/transfer/lib/maybe.tr index 02d7fe56d..2b7beee9a 100644 --- a/transfer/lib/maybe.tr +++ b/transfer/lib/maybe.tr @@ -1,3 +1,5 @@ +import prelude + data Maybe : Type -> Type where Nothing : (A : Type) -> Maybe A Just : (A : Type) -> A -> Maybe A @@ -8,4 +10,15 @@ fromMaybe _ _ (Just x) = x maybe : (A : Type) -> (B : Type) -> B -> (A -> B) -> Maybe A -> A maybe _ _ x _ Nothing = x -maybe _ _ _ f (Just x) = f x
\ No newline at end of file +maybe _ _ _ f (Just x) = f x + +-- Instances: + +monad_Maybe : Monad Maybe +monad_Maybe = + rec return = Just + bind = \A -> \B -> \m -> \k -> + case m of + Nothing _ -> Nothing B + Just _ x -> k x + |