slightly tweak algebraic effects interface

granule-project · Mar 7, 2024 · 2d180a5 · 2d180a5
1 parent 38c1c18
commit 2d180a5
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 20 deletions.
diff --git a/examples/effects_nondet.gr b/examples/effects_nondet.gr
@@ -11,18 +11,18 @@ import List
 data Labels = Toss | Drop
 
 -- Operations
-data GameOps (r : Type) : Set Labels -> Type where
-  FlipCoin : () -> (Bool -> r) [2] -> GameOps r {Toss};
-  Fumble   : () -> (Void -> r) [0] -> GameOps r {Drop}
+data GameOps : Set Labels -> Type -> Type where
+  FlipCoin : forall {r : Type} . () -> (Bool -> r) [2] -> GameOps {Toss} r;
+  Fumble   : forall {r : Type} . () -> (Void -> r) [0] -> GameOps {Drop} r
 
 -- -- Functoriality of operations
 fmap_gameops : forall {a b : Type, l : Set Labels}
-             . (a -> b) [0..Inf] -> GameOps a l -> GameOps b l
+             . (a -> b) [0..Inf] -> GameOps l a -> GameOps l b
 fmap_gameops [f] (FlipCoin () [k]) = FlipCoin () [f . k];
 fmap_gameops [f] (Fumble () [k]) = Fumble () [f . k]
 
 -- -- Handler to list monad
-handler : forall {a : Type, l : Set Labels} . GameOps (List a) l -> List a
+handler : forall {a : Type, l : Set Labels} . GameOps l (List a) -> List a
 handler (FlipCoin () [k]) = join_list (Next (k True) (Next (k False) Empty));
 handler (Fumble ()   [k]) = Empty
 

diff --git a/examples/effects_state.gr b/examples/effects_state.gr
@@ -11,19 +11,19 @@ import State
 data Labels = Get | Put
 
 -- Operations
-data StateOps (s : Type) (r : Type) : Set Labels -> Type where
- GetOp : ()         -> (s  -> r) [1] -> StateOps s r {Get};
- PutOp : s [0..Inf] -> (() -> r) [1] -> StateOps s r {Put}
+data StateOps (s : Type) : (Set Labels) -> Type -> Type where
+ GetOp : forall {r : Type} . ()         -> (s  -> r) [1] -> StateOps s {Get} r;
+ PutOp : forall {r : Type} . s [0..Inf] -> (() -> r) [1] -> StateOps s {Put} r
 
  -- Functoriality of operations
 fmap_stateops : forall {s a b : Type, l : Set Labels}
-              . (a -> b) [0..Inf] -> StateOps s a l -> StateOps s b l
+              . (a -> b) [0..Inf] -> StateOps s l a -> StateOps s l b
 fmap_stateops [f] (GetOp () [k]) = GetOp () [f . k];
 fmap_stateops [f] (PutOp [s] [k]) = PutOp [s] [f . k]
 
 -- Handler to state monad
 stateHandler : forall {s r : Type, l : Set Labels}
-             . StateOps s (State s r) l -> State s r
+             . StateOps s l (State s r) -> State s r
 stateHandler (GetOp () [k]) = join_state (State (\([s] : s [0..Inf]) -> (k s, [s])));
 stateHandler (PutOp s [k])  = join_state (State (\([_] : s [0..Inf]) -> (k (), s)))
 

diff --git a/frontend/src/Language/Granule/Checker/Primitives.hs b/frontend/src/Language/Granule/Checker/Primitives.hs
@@ -140,10 +140,10 @@ typeConstructors =
 
      -- Free : (e : Type) -> Effect
     , (mkId "GradedFree", (FunTy (Just $ mkId "eff") Nothing keffect
-                       (FunTy Nothing Nothing (funTy (Type 0) (funTy (tyVar "eff") (Type 0))) keffect), [], [0]))
+                       (FunTy Nothing Nothing (funTy (tyVar "eff") (funTy (Type 0) (Type 0))) keffect), [], [0]))
     , (mkId "Eff",
          (FunTy (Just $ mkId "eff") Nothing keffect
-            (FunTy (Just $ mkId "sig") Nothing (funTy (Type 0) (funTy (tyVar "eff") (Type 0)))
+            (FunTy (Just $ mkId "sig") Nothing (funTy (tyVar "eff") (funTy (Type 0) (Type 0)))
               (funTy (tyVar "eff") (TyApp (TyApp (tyCon "GradedFree") (tyVar "eff")) (tyVar "sig")))), [], [0,1]))
 
     -- Arrays
@@ -324,26 +324,26 @@ fromPure = BUILTIN
 --------------------------------------
 
 --- Lift a CPS-style effect operation to direct-style, also called the "generic effect" operation
-call : forall {eff : Effect, s : Semiring, grd : s, i : Type, o : Type, r : Type, sigs : Type -> eff -> Type, e : eff}
-     . (i -> (o -> r) [grd] -> sigs r e) -> i -> o <Eff eff sigs e>
+call : forall {eff : Effect, s : Semiring, grd : s, i : Type, o : Type, r : Type, sigs : eff -> Type -> Type, e : eff}
+     . (i -> (o -> r) [grd] -> sigs e r) -> i -> o <Eff eff sigs e>
 call = BUILTIN
 
 --- Deploy an effect handler on a computation tree
-handle : forall {eff : Effect, sig : Type -> eff -> Type, a b : Type, e : eff}
-       . (fmap : (forall {a : Type} . (forall {b : Type} . (forall {l : eff} . (a -> b) [0..Inf] -> sig a l -> sig b l))) [0..Inf])
+handle : forall {eff : Effect, sig : eff -> Type -> Type, a b : Type, e : eff}
+       . (fmap : (forall {a : Type} . (forall {b : Type} . (forall {l : eff} . (a -> b) [0..Inf] -> sig l a -> sig l b))) [0..Inf])
        --- ^ functoriality of sig
-       -> (forall {l : eff} . sig b l -> b) [0..Inf]
+       -> (forall {l : eff} . sig l b -> b) [0..Inf]
        -> (a -> b)
        --- ^ (a * sig) - algebra
        -> a <Eff eff sig e>
        -> b
 handle = BUILTIN
 
 --- Deploy an effect handler on a computation tree for a graded algebra
-handleGr : forall {eff : Effect, sig : Type -> eff -> Type, a : Type, b : eff -> Type, e : eff}
-       . (fmap : (forall {a : Type} . (forall {b : Type} . (forall {l : eff} . (a -> b) [0..Inf] -> sig a l -> sig b l))) [0..Inf])
+handleGr : forall {eff : Effect, sig : eff -> Type -> Type, a : Type, b : eff -> Type, e : eff}
+       . (fmap : (forall {a : Type} . (forall {b : Type} . (forall {l : eff} . (a -> b) [0..Inf] -> sig l a -> sig l b))) [0..Inf])
        --- ^ functoriality of sig
-       -> (forall {l : eff} . (forall {j : eff} . sig (b j) l -> b (l * j)) [0..Inf])
+       -> (forall {l : eff} . (forall {j : eff} . sig l (b j) -> b (l * j)) [0..Inf])
        -> (a -> b (1 : eff))
        --- ^ (a * sig) - graded algebra
        -> a <Eff eff sig e>