Add ExceptT, MonadError, MonadTrans as a test

tests/Compilation/positive/test072/ExceptT.juvix

@@ -0,0 +1,92 @@
+module ExceptT;
+
+import Monad open;
+import Monad open using {module Monad as MMonad};
+import Functor open;
+import Functor open using {module Functor as MFunctor};
+import MonadError open;
+import Stdlib.Data.Pair open;
+
+type Either (a b : Type) :=
+  | left a
+  | right b;
+
+instance
+Either-Functor {err} : Functor (Either err) :=
+  mkFunctor@{
+    <$>
+      {A B : Type} (f : A -> B) : Either err A -> Either err B
+      | (left e) := left e
+      | (right r) := right (f r)
+  };
+
+instance
+Either-Monad {err} : Monad (Either err) :=
+  mkMonad@{
+    functor := Either-Functor;
+    return {A : Type} (a : A) : Either err A := right a;
+    >>=
+      {A B : Type}
+      (x : Either err A)
+      (f : A -> Either err B)
+      : Either err B :=
+      case x of
+        | left e := left e
+        | right r := f r
+  };
+
+type ExceptT (Err : Type) (M : Type → Type) (A : Type) :=
+  mkExceptT {runExceptT : M (Either Err A)};
+
+instance
+ExceptT-Functor
+  {Err : Type}
+  {M : Type -> Type}
+  {{Functor M}}
+  : Functor (ExceptT Err M) :=
+  mkFunctor@{
+    <$>
+      {A B : Type}
+      (f : A -> B)
+      : ExceptT Err M A -> ExceptT Err M B
+      | (mkExceptT x) :=
+        mkExceptT ((Functor.<$>) ((Functor.<$>) f) x)
+  };
+
+instance
+ExceptT-Monad
+  {Err : Type}
+  {M : Type -> Type}
+  {{Monad M}}
+  : Monad (ExceptT Err M) :=
+  mkMonad@{
+    functor := MMonad.functor;
+    return {A} (a : A) : ExceptT Err M A :=
+      mkExceptT (MMonad.return (right a));
+    >>=
+      {A B}
+      (x : ExceptT Err M A)
+      (f : A -> ExceptT Err M B)
+      : ExceptT Err M B :=
+      mkExceptT
+        (ExceptT.runExceptT x
+          MMonad.>>= λ {a :=
+            case a of
+              | left e := MMonad.return (left e)
+              | right r := ExceptT.runExceptT (f r)})
+  };
+
+instance
+ExceptT-MonadError
+  {Err}
+  {M : Type -> Type}
+  {{mon : Monad M}}
+  : MonadError Err (ExceptT Err M) :=
+  mkMonadError@{
+    monad := ExceptT-Monad;
+    throw {A} (err : Err) : ExceptT Err M A :=
+      mkExceptT (MMonad.return (left err))
+  };
+
+runExcept {Err A} {M : Type -> Type} : ExceptT Err M A -> M (Either Err A)
+ | (mkExceptT x) := x;

tests/Compilation/positive/test072/Functor.juvix

@@ -8,3 +8,6 @@ type Functor (f : Type -> Type) :=
     syntax operator <$> fmap;
     <$> : {A B : Type} -> (A -> B) -> f A -> f B
   };
+
+fmap {f : Type -> Type} {{Functor f}} {A B : Type} (fun : A -> B) (x : f A) : f B :=
+  fun Functor.<$> x

tests/Compilation/positive/test072/Monad.juvix

@@ -19,3 +19,5 @@ open Monad public;
 syntax operator >>> bind;
 >>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
   A) (y : M B) : M B := x >>= λ {_ := y};
+
+getFunctor {M : Type -> Type} (_ : Monad M) : Functor M := Monad.functor;

tests/Compilation/positive/test072/MonadError.juvix

@@ -0,0 +1,13 @@
+module MonadError;
+
+import Monad open;
+import Stdlib.Data.Unit open;
+
+trait
+type MonadError (Err : Type) (M : Type -> Type) :=
+  mkMonadError {
+    monad : Monad M;
+    throw : {A : Type} -> Err -> M A;
+  };
+
+open MonadError public;

tests/Compilation/positive/test072/MonadTrans.juvix

@@ -0,0 +1,11 @@
+module MonadTrans;
+
+import Monad open;
+
+trait
+type MonadTrans (T : (Type -> Type) -> Type -> Type) :=
+  mkMonadTrans {lift : {A : Type}
+    -> {M : Type -> Type}
+    -> {{Monad M}}
+    -> M A
+    -> T M A};

tests/Compilation/positive/test072/ReaderT.juvix

@@ -2,22 +2,30 @@ module ReaderT;
 
 import Monad open;
 import Monad open using {module Monad as MMonad};
+import MonadTrans open;
+import MonadTrans open using {module MonadTrans as MMonadTrans};
 import Functor open;
 import Functor open using {module Functor as MFunctor};
 
 type ReaderT (S : Type) (M : Type → Type) (A : Type) :=
   mkReaderT {runReaderT : S → M A};
 
-runReader {S A : Type} {M : Type
-  → Type} (r : S) (m : ReaderT S M A) : M A :=
-  ReaderT.runReaderT m r;
+runReader
+  {S A : Type}
+  {M : Type → Type}
+  (r : S)
+  (m : ReaderT S M A)
+  : M A := ReaderT.runReaderT m r;
 
 instance
-ReaderT-Functor {S : Type} {M : Type
-  → Type} {{func : Functor M}} : Functor (ReaderT S M) :=
+ReaderT-Functor
+  {S : Type}
+  {M : Type → Type}
+  {{func : Functor M}}
+  : Functor (ReaderT S M) :=
   mkFunctor@{
-    <$> {A B : Type} (f : A → B)
-      : ReaderT S M A → ReaderT S M B
+    <$>
+      {A B : Type} (f : A → B) : ReaderT S M A → ReaderT S M B
       | (mkReaderT g) :=
         -- NOTE we cannot use unqualified <$> or the scoper gets confused
         let
@@ -26,7 +34,10 @@ ReaderT-Functor {S : Type} {M : Type
   };
 
 instance
-ReaderT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
+ReaderT-Monad
+  {S : Type}
+  {M : Type → Type}
+  {{mon : Monad M}}
   : Monad (ReaderT S M) :=
   mkMonad@{
     functor :=
@@ -35,18 +46,28 @@ ReaderT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
       };
     return {A : Type} (a : A) : ReaderT S M A :=
       mkReaderT λ {s := MMonad.return a};
-    >>= {A B : Type} (x : ReaderT S M A) (f : A → ReaderT S M B)
+    >>=
+      {A B : Type}
+      (x : ReaderT S M A)
+      (f : A → ReaderT S M B)
       : ReaderT S M B :=
       mkReaderT
         λ {s := runReader s x MMonad.>>= λ {a := runReader s (f a)}}
   };
 
 import MonadReader open;
+import MonadError open;
+import MonadError open using {module MonadError as MMonadError};
+import ExceptT open;
+import MonadReader open using {module MonadReader as MMonadReader};
 import Stdlib.Data.Unit open;
 import Stdlib.Function open;
 
 instance
-ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}}
+ReaderT-MonadReader
+  {S : Type}
+  {M : Type → Type}
+  {{Monad M}}
   : MonadReader S (ReaderT S M) :=
   mkMonadReader@{
     monad := ReaderT-Monad;
@@ -60,14 +81,40 @@ import StateT open;
 import Identity open;
 import Stdlib.Data.Pair open;
 
-liftReaderT {R A : Type} {M : Type → Type} (m : M A)
+liftReaderT
+  {R A : Type}
+  {M : Type → Type}
+  (m : M A)
   : ReaderT R M A := mkReaderT (const m);
 
-liftStateT {S A : Type} {M : Type → Type} {{Monad M}} (m : M
-  A) : StateT S M A :=
+instance
+ReaderT-MonadTrans {R : Type} : MonadTrans (ReaderT R) :=
+  mkMonadTrans@{
+    lift
+      {A : Type}
+      {M : Type -> Type}
+      {{Monad M}}
+      (x : M A)
+      : ReaderT R M A := liftReaderT x
+  };
+
+liftStateT
+  {S A : Type}
+  {M : Type → Type}
+  {{Monad M}}
+  (m : M A)
+  : StateT S M A :=
   mkStateT
     λ {s := m MMonad.>>= λ {a := MMonad.return (a, s)}};
 
+liftExceptT
+  {Err A : Type}
+  {M : Type → Type}
+  {{mon : Monad M}}
+  (m : M A)
+  : ExceptT Err M A :=
+  mkExceptT (fmap {{Monad.getFunctor mon}} right m);
+
 import Stdlib.Data.Nat open;
 
 askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat :=
@@ -81,12 +128,37 @@ monadic : ReaderT Nat (StateT Nat Identity) Nat :=
 main : Nat :=
   runIdentity (evalState 2 (runReader 5 monadic));
 
+example : ExceptT Nat (StateT Nat Identity) Nat :=
+  liftExceptT get
+    >>= λ {x :=
+      if
+        | x == 0 := throw 999
+        | else := return 333};
+
+exampleClassy
+  {M : Type -> Type}
+  {{monErrM : MonadError Nat M}}
+  {{MonadState Nat M}}
+  : M Nat :=
+  let
+    mon : Monad M := MMonadError.monad {{monErrM}};
+  in (>>=)
+    {{mon}}
+    get
+    λ {x :=
+      if
+        | x == 0 := throw 999
+        | else := return {{mon}} 333};
+
+-- runClassy : Either Nat Nat := runIdentity (evalState 0 (runExcept exampleClassy))
+
 -- FIXME fails instance termination
 -- instance
--- StateT-MonadReader {R S : Type} {M : Type
---   → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) :=
+-- StateT-MonadReader {R S : Type}
+--   {M : Type → Type}
+--   {{mreader : MonadReader R M}} : MonadReader R (StateT S M) :=
 --   mkMonadReader@{
---     monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}};
---     reader {A : Type} : (R → A) → StateT S M A := liftStateT << MonadReader.reader;
---     ask : StateT S M R := liftStateT MonadReader.ask;
+--     monad := StateT-Monad@{mon := MMonadReader.monad {{mreader}}};
+--     reader {A : Type} : (R → A) → StateT S M A := liftStateT << MMonadReader.reader;
+--     ask : StateT S M R := liftStateT MMonadReader.ask;
 --   };