From d92a26fc9be92fb269888947a8b26aa12883065e Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 30 Nov 2005 18:57:23 +0000 Subject: Added monad isntances for List and Maybe. --- transfer/lib/maybe.tr | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'transfer/lib/maybe.tr') 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 + -- cgit v1.2.3