Merge pull request #979 from stefan-hoeck/remove-eithert-contrib

Remove Control.Monad.Trans.Either from contrib

libs/contrib/Control/Monad/Trans/Either.idr

@@ -1,55 +0,0 @@
-module Control.Monad.Trans.Either
-
-%default total
-
-
-public export
-record EitherT m a b where
-    constructor MkEitherT
-    runEitherT : m (Either a b)
-
-export
-Functor m => Functor (EitherT m a) where
-    map f (MkEitherT runEitherT) = MkEitherT (map (map f) runEitherT)
-
-export
-Monad m => Applicative (EitherT m a) where
-    pure = MkEitherT . pure . Right
-    (MkEitherT left) <*> (MkEitherT right) = MkEitherT $ do
-        l <- left
-        r <- right
-        pure (l <*> r)
-
-export
-Monad m => Monad (EitherT m a) where
-    join (MkEitherT runEitherT) = MkEitherT $ do
-        case !runEitherT of
-            Left l => pure (Left l)
-            Right (MkEitherT inner) => inner
-
-
-export
-eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT m a b -> m c
-eitherT f g (MkEitherT runEitherT) = case !runEitherT of
-    Left l => f l
-    Right r => g r
-
-export
-bimapEitherT : Functor m => (a -> c) -> (b -> d) -> EitherT m a b -> EitherT m c d
-bimapEitherT f g (MkEitherT runEitherT) = MkEitherT (map m runEitherT)
-    where
-    m : Either a b -> Either c d
-    m (Left l) = Left (f l)
-    m (Right r) = Right (g r)
-
-export
-mapEitherT : (m (Either a b) -> n (Either c d)) -> EitherT m a b -> EitherT n c d
-mapEitherT f (MkEitherT runEitherT) = MkEitherT $ f runEitherT
-
-export
-hoist : Applicative m => Either a b -> EitherT m a b
-hoist e = MkEitherT $ pure e
-
-export
-fail : Applicative m => a -> EitherT m a b
-fail = MkEitherT . pure . Left

libs/contrib/Control/Validation.idr

@@ -12,7 +12,7 @@ module Control.Validation
 
 import Control.Monad.Identity
 import Control.Monad.Syntax
-import Control.Monad.Trans.Either
+import Control.Monad.Error.Either
 import Data.Nat
 import Data.Strings
 import Data.Vect
@@ -23,7 +23,7 @@ import Decidable.Equality
 
 public export
 Result : (Type -> Type) -> Type -> Type
-Result m = EitherT m String
+Result m = EitherT String m
 
 ||| Validators in this module come in two flavours: Structural Validators and
 ||| Property Validators. They are both wrappers around functions which take
@@ -95,7 +95,7 @@ withError e (MkValidator f) = MkValidator (replaceError e . f)
 ||| A validator which always fails with a given message.
 export
 fail : Applicative m => String -> ValidatorT m a b
-fail s = MkValidator $ \_ => fail s
+fail s = MkValidator $ \_ => left s
 
 infixl 2 >>>
 
@@ -125,14 +125,14 @@ export
 decide : Monad m => (t -> String) -> ((x : t) -> Dec (p x)) -> PropValidator m t p
 decide msg dec = MkPropValidator \x => case dec x of
     Yes prf => pure prf
-    No _ => fail (msg x)
+    No _ => left (msg x)
 
 ||| Given a function converting a into Maybe b, build a Validator of a
 ||| converting it into b.
 export
 fromMaybe : Monad m => (a -> String) -> (a -> Maybe b) -> ValidatorT m a b
 fromMaybe e f = MkValidator \a => case f a of
-    Nothing => fail $ e a
+    Nothing => left $ e a
     Just b => pure b
 
 ||| Verify whether a String represents a natural number.
@@ -167,8 +167,8 @@ length l = MkValidator (validateVector l)
     where
     validateVector : (l : Nat) -> List a -> Result m (Vect l a)
     validateVector Z [] = pure []
-    validateVector (S _) [] = fail "Missing list element."
-    validateVector Z (_ :: _) = fail "Excessive list element."
+    validateVector (S _) [] = left "Missing list element."
+    validateVector Z (_ :: _) = left "Excessive list element."
     validateVector (S k) (x :: xs) = do
         ys <- validateVector k xs
         pure (x :: ys)
@@ -178,7 +178,7 @@ export
 equal : (DecEq t, Monad m) => (a : t) -> PropValidator m t (\b => a = b)
 equal a = MkPropValidator \b => case decEq a b of
     Yes prf => pure prf
-    No _ => fail "Values are not equal."
+    No _ => left "Values are not equal."
 
 ||| Verify that a Nat is less than or equal to  certain bound.
 export

libs/contrib/contrib.ipkg

@@ -10,7 +10,6 @@ modules = Control.ANSI,
 
           Control.Monad.Algebra,
           Control.Monad.Syntax,
-          Control.Monad.Trans.Either,
 
           Control.Algebra,
           Control.Algebra.Laws,