summaryrefslogtreecommitdiff
path: root/lib/ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-08-19 15:23:01 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-08-19 15:23:01 -0400
commit0156bf0da091dd2a773c08c2917c121bc86643bb (patch)
tree49a42ce8909e7f3df3a9fe122d4da57b21f67108 /lib/ur
parent2babe3938c1d97e46be24e033d9cb575f746d80b (diff)
Basis.mkMonad
Diffstat (limited to 'lib/ur')
-rw-r--r--lib/ur/basis.urs5
-rw-r--r--lib/ur/option.ur6
-rw-r--r--lib/ur/option.urs2
3 files changed, 13 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs
index ece4bfef..494eaa4b 100644
--- a/lib/ur/basis.urs
+++ b/lib/ur/basis.urs
@@ -126,6 +126,11 @@ val bind : m ::: (Type -> Type) -> t1 ::: Type -> t2 ::: Type
-> m t1 -> (t1 -> m t2)
-> m t2
+val mkMonad : m ::: (Type -> Type)
+ -> {Return : t ::: Type -> t -> m t,
+ Bind : t1 ::: Type -> t2 ::: Type -> m t1 -> (t1 -> m t2) -> m t2}
+ -> monad m
+
con transaction :: Type -> Type
val transaction_monad : monad transaction
diff --git a/lib/ur/option.ur b/lib/ur/option.ur
index 0aa07a2d..5c89fc9d 100644
--- a/lib/ur/option.ur
+++ b/lib/ur/option.ur
@@ -1,5 +1,11 @@
datatype t = datatype Basis.option
+val monad = mkMonad {Return = @@Some,
+ Bind = fn [a] [b] (m1 : t a) (m2 : a -> t b) =>
+ case m1 of
+ None => None
+ | Some v => m2 v}
+
fun eq [a] (_ : eq a) =
mkEq (fn x y =>
case (x, y) of
diff --git a/lib/ur/option.urs b/lib/ur/option.urs
index 62687963..ba43613f 100644
--- a/lib/ur/option.urs
+++ b/lib/ur/option.urs
@@ -1,5 +1,7 @@
datatype t = datatype Basis.option
+val monad : monad t
+
val eq : a ::: Type -> eq a -> eq (t a)
val ord : a ::: Type -> ord a -> ord (t a)