From 01d1715994d2e7c58ef97fdd81dd7015a9118b17 Mon Sep 17 00:00:00 2001 From: bringert Date: Wed, 30 Nov 2005 18:40:29 +0000 Subject: [PATCH] Transfer: added monad class. fixed Compos class types. --- transfer/lib/prelude.tr | 31 +++++++++++++++++++++++-------- 1 file changed, 23 insertions(+), 8 deletions(-) diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr index 409647a26..97336c47f 100644 --- a/transfer/lib/prelude.tr +++ b/transfer/lib/prelude.tr @@ -299,17 +299,32 @@ Monoid = sig mzero : A -- The Compos class -- -Compos : Type -> Type -Compos T = sig - C : Type +Compos : (C : Type) -> (C -> Type) -> Type +Compos C T = sig composOp : (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c composFold : (B : Type) -> Monoid B -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b -composOp : (T : Type) -> (d : Compos T) - -> (c : d.C) -> ((a : d.C) -> T a -> T a) -> T c -> T c -composOp _ d = d.composOp +composOp : (C : Type) -> (T : C -> Type) -> (d : Compos C T) + -> (c : C) -> ((a : C) -> T a -> T a) -> T c -> T c +composOp _ _ d = d.composOp -composFold : (T : Type) -> (d : Compos T) -> (B : Type) -> Monoid B - -> (c : d.C) -> ((a : d.C) -> T a -> b) -> T c -> b +composFold : (C : Type) -> (T : C -> Type) -> (d : Compos C T) -> (B : Type) -> Monoid B + -> (c : C) -> ((a : C) -> T a -> b) -> T c -> b composFold _ _ d = d.composFold + +-- +-- The Monad class +-- + +Monad : (Type -> Type) -> Type +Monad M = sig return : (A : Type) -> M A + bind : (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B + +return : (M : Type -> Type) -> Monad M -> M A +return _ d = d.return + +bind : (M : Type -> Type) -> Monad M + -> (A : Type) -> (B : Type) -> M A -> (A -> M B) -> M B +bind _ d = d.bind +