v0.9.5.0

README.md

@@ -184,6 +184,7 @@ the most recent copy of the input file with `.bak` appended.
 | ASCII | Unicode |
 |:---:|:---:|
 | `forall` | `∀` |
+| `exists` | `∃` |
 | `Inf` | `∞` |
 | `->` | `→` |
 | `=>` | `⇒` |

StdLib/List.gr

@@ -63,10 +63,22 @@ foldr_list [f] z xs =
 
 --- Push a graded modality inside a list (defined as `push @List`)
 pushList : forall {s : Semiring, r : s, a : Type}
-         . {(1 : s) <= r} => (List a) [r] -> List (a [r])
+         . {(1 : s) <= r, Pushable r} => (List a) [r] -> List (a [r])
 pushList = push @List
 
 --- Pull a graded modality out of a list (defined as `pull @List`)
 pullList : forall {s : Semiring, r : s, a : Type}
          . List (a [r]) -> (List a) [r]
-pullList = pull @List
+pullList = pull @List
+
+--- # List monad
+
+return_list : forall {a : Type} . a -> List a
+return_list x = Next x Empty
+
+bind_list : forall {a b : Type} . (a -> List b) [] -> List a -> List b
+bind_list [f] Empty = Empty;
+bind_list [f] (Next x xs) = append_list (f x) (bind_list [f] xs)
+
+join_list : forall {a : Type} . List (List a) -> List a
+join_list = bind_list [\x -> x]

StdLib/Prelude.gr

@@ -110,8 +110,8 @@ extract [x] = x
 --- defined: the operation {c ⨱ c} is partial and is only defined if the semiring
 --- `k` permits this behaviour at `c`. (An example of a semiring where this is not true
 --- is for `k = LNL` and `c = 1`).
-pushPair : forall {a : Type, b : Type, k : Coeffect, c : k} . {c ⨱ c} => (a × b) [c] -> a [c] × b [c]
-pushPair [(x, y)] = ([x], [y])
+pushPair : forall {a : Type, b : Type, k : Coeffect, c : k} . {Pushable c} => (a × b) [c] -> a [c] × b [c]
+pushPair = push @(,)
 
 --- Pull coeffects of pair elements outside of the pair
 pullPair : ∀ {a : Type, b : Type, k : Coeffect, n : k} . (a [n], b [n]) → (a, b) [n]

StdLib/Vec.gr

@@ -74,13 +74,19 @@ append
 append Nil ys = ys;
 append (Cons x xs) ys = Cons x (append xs ys)
 
+--- Concatenate a vector of vectors
+concat : forall {a : Type, m n : Nat} .
+        Vec n (Vec m a) -> Vec (n * m) a
+concat Nil = Nil;
+concat (Cons xs xss) = append xs (concat xss)
+
 --- Drop the first `m` elements
-drop
+dropElems
   : forall {a : Type, m n : Nat}
   . N m -> (Vec n a) [0..1] -> Vec (n - m) a
-drop Z [xs] = xs;
-drop (S n) [Nil] = drop n [Nil];
-drop (S n) [Cons _ xs] = drop n [xs]
+dropElems Z [xs] = xs;
+dropElems (S n) [Nil] = dropElems n [Nil];
+dropElems (S n) [Cons _ xs] = dropElems n [xs]
 
 --- Take the first `m` elements
 take
@@ -170,7 +176,7 @@ pullVec : forall {a : Type, s : Semiring, k : s, n : Nat}
 pullVec = pull @Vec
 
 --- pushVec pushes in non linearity of vector into the elements
-pushVec : ∀ {a : Type, s : Semiring, k : s, n : Nat} . {(1 : s) <= k}
+pushVec : ∀ {a : Type, s : Semiring, k : s, n : Nat} . {(1 : s) <= k, Pushable k}
       => (Vec n a) [k] → Vec n (a [k])
 pushVec = push @Vec
 

changelog

@@ -1,3 +1,18 @@
+  # 0.9.5.0
+   - Rank N typing (see https://github.com/granule-project/granule/blob/dev-minor/examples/rankN.gr)
+   - Algebraic effects and handlers. See e.g.,
+     * https://github.com/granule-project/granule/blob/dev-minor/examples/effects_nondet.gr
+     * https://github.com/granule-project/granule/blob/dev-minor/examples/effects_state.gr
+   - Updated standard docs
+   - Fixes to deriving copyShape and drop combinators
+   - push deriving combinators now have Pushable constraint, e.g.
+
+             pushList : forall {s : Semiring, r : s, a : Type}
+                       . {(1 : s) <= r, Pushable r} => (List a) [r] -> List (a [r])
+             pushList = push @List
+
+   - Minor tweaks to the Granule Language Server to improve vscode interaction (no longer complains on the entire file about 'Premature end of file' whilst typing).
+
   # 0.9.4.0
   - Advanced synthesis algorithm for `language GradeBase` mode.
   - Better standard library documentation

compiler/app/Language/Granule/Compiler.hs

@@ -23,7 +23,6 @@ import Language.Granule.Checker.Checker
 import Language.Granule.Syntax.Def (extendASTWith)
 import Language.Granule.Syntax.Preprocessor
 import Language.Granule.Syntax.Parser
-import Language.Granule.Syntax.Preprocessor.Ascii
 import Language.Granule.Syntax.Pretty
 import Language.Granule.Utils
 import Paths_granule_compiler (version)
@@ -112,14 +111,14 @@ parseGrFlags
   <=< getParseResult . execParserPure (prefs disambiguate) parseGrConfig . words
 
 data GrConfig = GrConfig
-  { grRewriter        :: Maybe (String -> String)
+  { grRewriter        :: Maybe Rewriter
   , grKeepBackup      :: Maybe Bool
   , grLiterateEnvName :: Maybe String
   , grShowVersion     :: Bool
   , grGlobals         :: Globals
   }
 
-rewriter :: GrConfig -> Maybe (String -> String)
+rewriter :: GrConfig -> Maybe Rewriter
 rewriter c = grRewriter c <|> Nothing
 
 keepBackup :: GrConfig -> Bool
@@ -334,10 +333,10 @@ parseGrConfig = info (go <**> helper) $ briefDesc
 
         grRewriter
           <- flag'
-            (Just asciiToUnicode)
+            (Just AsciiToUnicode)
             (long "ascii-to-unicode" <> help "WARNING: Destructively overwrite ascii characters to multi-byte unicode.")
           <|> flag Nothing
-            (Just unicodeToAscii)
+            (Just UnicodeToAscii)
             (long "unicode-to-ascii" <> help "WARNING: Destructively overwrite multi-byte unicode to ascii.")
 
         grKeepBackup <-

compiler/src/Language/Granule/Compiler/HSCodegen.hs

@@ -88,7 +88,7 @@ cgTypeScheme :: Compiler m => TypeScheme -> m (Hs.Type ())
 cgTypeScheme (Forall _ binders constraints typ) = do
   typ' <- cgType typ
   let tyVars = map (UnkindedVar () . mkName . fst) binders
-  return $ TyForall () (Just tyVars) Nothing typ'
+  return $ Hs.TyForall () (Just tyVars) Nothing typ'
 
 cgPats :: Compiler m => [CPat] -> m [Pat ()]
 cgPats = mapM cgPat
@@ -104,7 +104,7 @@ cgPat (GrPat.PInt _ _ _ n) =
   return $ PLit () (Signless ()) $ Int () (fromIntegral n) (show n)
 cgPat (GrPat.PFloat _ _ _ n) =
   return $ PLit () (Signless ()) $ Frac () (toRational n) (show n)
-cgPat (GrPat.PConstr _ _ _ i l_pt)
+cgPat (GrPat.PConstr _ _ _ i _ l_pt)
   | i == Id "," ","  = do
       pts <- mapM cgPat l_pt
       return $ pTuple pts
@@ -142,6 +142,7 @@ cgType (GrType.TySet p l_t) = return mkUnit
 cgType (GrType.TyCase t l_p_tt) = unsupported "cgType: tycase not implemented"
 cgType (GrType.TySig t t2) = unsupported "cgType: tysig not implemented"
 cgType (GrType.TyExists _ _ _) = unsupported "cgType: tyexists not implemented"
+cgType (GrType.TyForall _ _ _) = unsupported "cgType: tyforall not implemented"
 
 isTupleType :: GrType.Type -> Bool
 isTupleType (GrType.TyApp (GrType.TyCon id) _) = id == Id "," ","
@@ -220,6 +221,7 @@ cgVal (Abs _ p _ ex) = do
   return $ lamE [p'] ex'
 cgVal Pack{} = error "Existentials unsupported in code gen"
 cgVal Ext{} = unexpected "cgVal: unexpected Ext"
+cgVal TyAbs{} = error "Rank-N quantifiaction unsupported in code gen"
 
 
 cgBinop :: Compiler m => Operator -> Exp () -> Exp () -> m (Exp ())

docs/style.css

@@ -11,6 +11,14 @@ body {
   border-bottom: solid 3px #ccc;
 }
 
+.code pre {
+  white-space: pre-wrap;       /* css-3 */
+  white-space: -moz-pre-wrap;  /* Mozilla, since 1999 */
+  white-space: -pre-wrap;      /* Opera 4-6 */
+  white-space: -o-pre-wrap;    /* Opera 7 */
+  word-wrap: break-word;       /* Internet Explorer 5.5+ */
+}
+
 .inline {
   font-family: monospace;
   background: rgb(250, 250, 250);
@@ -96,4 +104,8 @@ a.toplink {
   font-size: 10pt;
   margin-right: 2em;
   color: #c9c9c9;
+}
+
+strong {
+  color: rgb(194, 20, 200);
 }

examples/cost.gr

@@ -10,8 +10,7 @@ two =
 -- Prove (map f) in O(|f|n)
 
 mapLinear : forall {a b : Type, n : Nat, f : Nat}
-          . (a -> b <f>) [] -> Vec n a -> (Vec n b) <n*f>
-
+          . (a -> b <f>) [n] -> Vec n a -> (Vec n b) <n*f>
 mapLinear [_] Nil = pure Nil;
 mapLinear [f] (Cons x xs) =
  let y <- f x;

examples/effects_nondet.gr

@@ -0,0 +1,54 @@
+-- Example of using algebraic effects and handlers in Granule to capture
+-- non-determinism effects
+
+-- Uses the builtin `call` and `handle` operations.
+-- See https://granule-project.github.io/docs/modules/Primitives.html#algebraiceffectsandhandlers
+
+import List
+
+-- # Coin toss game effect operations
+
+data Labels = Toss | Drop
+
+-- Operations
+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 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 l (List a) -> List a
+handler (FlipCoin () [k]) = join_list (Next (k True) (Next (k False) Empty));
+handler (Fumble ()   [k]) = Empty
+
+-- # Examples
+
+foo : Bool <Eff (Set Labels) GameOps {Toss}>
+foo = call FlipCoin ()
+
+-- Two coin flips, all good
+example1 : (Bool, Bool) <Eff (Set Labels) GameOps {Toss}>
+example1 = let
+  x <- call FlipCoin ();
+  y <- call FlipCoin ()
+  in pure (x, y)
+
+-- -- Two coin flips, attempt, but fumble in the middle
+example2 : (Bool, Bool) <Eff (Set Labels) GameOps {Toss,Drop}>
+example2 = let
+  x <- call FlipCoin ();
+  a <- call Fumble ();
+  y <- call FlipCoin ()
+  in let () = drop @Void a in pure (x, y)
+
+-- -- Easy runner
+go : forall {e : Set Labels, a : Type} . a <Eff (Set Labels) GameOps e> -> List a
+go = handle [/\{a,b,l}.fmap_gameops] [/\{l}.handler] (return_list)
+
+main : List (Bool, Bool)
+main = go example1

examples/effects_state.gr

@@ -0,0 +1,46 @@
+-- Example of using algebraic effects and handlers in Granule to capture
+-- state effects
+
+-- Uses the builtin `call` and `handle` operations.
+-- See https://granule-project.github.io/docs/modules/Primitives.html#algebraiceffectsandhandlers
+
+import State
+
+-- # State operations
+
+data Labels = Get | Put
+
+-- Operations
+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 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 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)))
+
+-- # Examples
+
+incr : Int <Eff (Set Labels) (StateOps Int) {Get, Put}>
+incr = let
+  y   <- call GetOp ();
+  [z] <- pure (moveInt y);
+  ()  <- call PutOp [z + 1] in
+  pure z
+
+-- Handle state wrapped
+handleState : forall {a b : Type, e : Set Labels, s : Type}
+            . a <Eff (Set Labels) (StateOps s) e>
+           -> State s a
+handleState = handle [/\{a,b,l}.fmap_stateops] [/\{l}.stateHandler] (return_state)
+
+main : (Int, Int [])
+main = runState (handleState incr) [42]

examples/listToVec.gr

@@ -1,15 +1,15 @@
 import Vec
 import List
 
-listToVec : ∀ {a : Type} . List a → exists {n : Nat} . Vec n a
-listToVec Empty = pack < 0 , Nil > as exists {n : Nat} . Vec n a;
+listToVec : ∀ {a : Type} . List a → ∃ {n : Nat} . Vec n a
+listToVec Empty = pack < 0 , Nil > as ∃ {n : Nat} . Vec n a;
 listToVec (Next x xs) =
   unpack < m , v > = listToVec xs
-  in pack < m + 1 , (Cons x v) > as exists {n : Nat} . Vec n a
+  in pack < m + 1 , (Cons x v) > as ∃ {n : Nat} . Vec n a
 
 vecToList : ∀ {a : Type, n : Nat} . Vec n a → List a
 vecToList Nil = Empty;
 vecToList (Cons x xs) = Next x (vecToList xs)
 
-iso : forall {a : Type} . List a -> List a
+iso : ∀ {a : Type} . List a -> List a
 iso x = unpack < n , list > = listToVec x in vecToList list

examples/pad_left.gr

@@ -1,5 +1,13 @@
 import Vec
 
+monus
+  : forall {m n : Nat}
+  . N m -> N n -> N (m - n)
+monus m Z = m;
+monus Z (S n') = monus Z n';
+monus (S m') (S n') = monus m' n'
+
+
 pad_left
   : ∀ {a : Type, m : Nat, n : Nat}
   . a [n - m]

examples/rankN.gr

@@ -0,0 +1,14 @@
+-- A function expecting a rank-1 polymorphic function which it reuses at
+-- two different types (`Char` and `()`)
+foo : (forall {b : Type} . b -> (Int, b)) [2] -> ((Int, Char), (Int, ()))
+foo [k] = ((k @ Char) 'a', (k @ ()) ())
+
+-- Application of `foo` with a reusable type abstraction function
+main : ((Int, Char), (Int, ()))
+main = foo [(/\(t : Type) -> \(x : t) -> (42, x))]
+
+-- Mixing existentials and rankN forall
+unpacker : forall {f : Type → Type, a : Type} .
+            (exists {a : Type} . f a) → (forall {t : Type} . f t → a) → a
+unpacker e f =
+  unpack < b , e' > = e in (f @ b) e'

frontend/package.yaml

@@ -1,5 +1,5 @@
 name: granule-frontend
-version: '0.9.4.0'
+version: '0.9.5.0'
 synopsis: The Granule abstract-syntax-tree, parser and type checker libraries
 author: Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III, Jack Hughes, Preston Keel, Daniel Marshall, Michael Vollmer
 copyright: 2018-22 authors