Merge pull request #218 from granule-project/dev-minor

v0.9.4.0 release merge

StdLib/Choice.gr

@@ -1,7 +1,6 @@
 ------
 --- Module: Choice
---- Description: A datatype with two elements. The only way to consume it is by either
----   choosing the first or the second element. You must choose exactly one.
+--- Description: A datatype with two elements. The only way to consume it is by either choosing the first or the second element. You must choose exactly one.
 --- Authors: Vilem-Benjamin Liepelt
 --- License: BSD3
 --- Copyright: (c) Authors 2018

StdLib/Coffee.gr

@@ -0,0 +1,23 @@
+------
+--- Module: Coffee
+--- Description: Coffee data type for uniqueness examples
+--- Authors: Daniel Marshall, Dominic Orchard
+--- License: BSD3
+--- Copyright: (c) Authors 2022
+--- Issue-tracking: https://github.com/dorchard/granule/issues
+--- Repository: https://github.com/dorchard/granule
+------
+
+module Coffee hiding (Coffee, Awake) where
+
+data Coffee = Coffee
+data Awake  = Awake
+
+drink : Coffee -> Awake
+drink Coffee = Awake
+
+keep : Coffee -> Coffee
+keep x = x
+
+sip : *Coffee → (Coffee, Awake)
+sip fresh = let !coffee = share fresh in (keep coffee, drink coffee)

StdLib/Either.gr

@@ -12,12 +12,14 @@ module Either where
 
 data Either a b where Left a | Right b
 
+--- Distribute a graded modality inside Either
 -- TODO: latest version can generalise this to `c : k, k : Semiring`
 pushEither : forall {a : Type, b : Type, c : Nat} . {c <= 1} =>
              (Either a b) [c] -> Either (a [c]) (b [c])
 pushEither [Left x]  = Left [x];
 pushEither [Right y] = Right [y]
 
+--- Distrbute a graded modality outside Either
 pullEither : forall {a : Type, b : Type, c : Nat}
         . Either (a [c]) (b [c]) -> (Either a b) [c]
 pullEither (Left [y])  = [Left y];

StdLib/File.gr

@@ -2,7 +2,8 @@ module File where
 
 import Maybe
 
-readMany : Int → Handle R → (Handle R, String) <IO> 
+--- Read a string of a specified length from a file
+readMany : Int → Handle R → (Handle R, String) <IO>
 readMany 0 h = pure (h, "");
 readMany n h =
   let (h, c)  ← readChar h;
@@ -18,6 +19,7 @@ auxiliaryReadFile h rest = let
      False -> let
       (h, c) <- readChar h in auxiliaryReadFile h (stringSnoc rest c)
 
+--- Given a filename, open the file, read it all in, and close it
 readFile : String -> String <{Open, Read, Close, IOExcept}>
 readFile fileName = let
   h <- openHandle ReadMode fileName;
@@ -28,11 +30,12 @@ readFile fileName = let
 auxiliaryWriteFile : Handle W -> String -> (Handle W) <{Write, IOExcept}>
 auxiliaryWriteFile h rest =
   case stringUncons rest of
-    None -> pure h;
-    Some (c, rest) -> let
+    Nothing -> pure h;
+    Just (c, rest) -> let
       h <- writeChar h c
       in auxiliaryWriteFile h rest
 
+--- Given a filename, and a string, open the file, write the string, and close
 writeFile : String -> String -> () <{Open, Write, Close, IOExcept}>
 writeFile fileName fileData = let
   h <- openHandle WriteMode fileName;

StdLib/Fin.gr

@@ -12,20 +12,21 @@ module Fin where
 
 import Nat
 
+--- Representation of a number bounded above by `n`
 data Fin : Nat -> Type where
   FZ : forall {k : Nat} . Fin (k + 1);
   FS : forall {k : Nat} . Fin k -> Fin (k + 1)
 
--- If m < n then (x in Fin m) -> (x in Fin n)
+--- If m < n then (x in Fin m) -> (x in Fin n)
 upcast : forall {n : Nat, m : Nat} . {m .<= n} => Fin m -> Fin n
 upcast FZ = FZ;
 upcast (FS n) = FS (upcast n)
 
--- Map from a natural number into the finite set one bigger than it
+--- Map from a natural number into the finite set one bigger than it
 fromN : forall {n : Nat, m : Nat} . N n -> Fin (n + 1)
 fromN Z = FZ;
 fromN (S n) = FS (fromN n)
 
--- Map from a natural number into a finite set that is arbitrarily bigger than it
+--- Map from a natural number into a finite set that is arbitrarily bigger than it
 fromNInto : forall {n : Nat, m : Nat} . {m >= 1} => N n -> Fin (n + m)
 fromNInto n = upcast (fromN n)

StdLib/List.gr

@@ -16,52 +16,57 @@ import Bool
 
 data List a where Empty; Next a (List a)
 
--- Length function must ignore the elements
+--- Append two lists
+append_list : forall {a : Type} . List a -> List a -> List a
+append_list xs ys = case xs of
+  Empty -> ys;
+  Next x xs -> Next x (append_list xs ys)
+
+--- Make a singleton list
+singleton_list : forall {a : Type} . a -> List a
+singleton_list x = Next x Empty
+
+--- Length function must ignore the elements
 length_list : forall {a : Type} . List (a [0]) -> Int
 length_list xs =
   case xs of
     Empty         -> 0;
     (Next [_] xs) -> 1 + length_list xs
 
--- Map function for lists
+--- Map function for lists
 lmap : forall {a : Type, b : Type}
     . (a -> b) [0..∞] -> List a -> List b
 lmap [f] Empty = Empty;
 lmap [f] (Next x xs) = Next (f x) (lmap [f] xs)
 
--- Lookup function
+--- Lookup function
 lookupBy : forall {a : Type, b : Type}
          . (a -> a -> Bool) [0..∞] -> a [0..∞] -> (List (a, b)) [0..1] -> Maybe b
-lookupBy [p] [k] [Empty] = None;
+lookupBy [p] [k] [Empty] = Nothing;
 lookupBy [p] [k] [Next (k', v) xs] =
-  if p k k' then Some v else lookupBy [p] [k] [xs]
+  if p k k' then Just v else lookupBy [p] [k] [xs]
 
--- Safe head function
+--- Safe head function
 head_list : forall {a : Type} . (List a) [0..1] -> Result a
 head_list xs =
   case xs of
     [Empty]      -> Failed ["Empty list!"];
     [(Next x _)] -> Ok x
 
+--- Foldr on lists
 foldr_list : forall {a : Type, b : Type}
       . (a -> b -> b) [0..∞] -> b -> List a -> b
 foldr_list [f] z xs =
   case xs of
     Empty -> z;
     Next x xs -> f x (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])
 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
-
-append_list : forall {a : Type} . List a -> List a -> List a
-append_list xs ys = case xs of
-  Empty -> ys;
-  Next x xs -> Next x (append_list xs ys)
-
-singleton_list : forall {a : Type} . a -> List a
-singleton_list x = Next x Empty
+pullList = pull @List

StdLib/Maybe.gr

@@ -13,39 +13,40 @@ module Maybe where
 import Bool
 
 --- Type-safe null; wrap a computation that could fail
-data Maybe a = None | Some a
+data Maybe a = Nothing | Just a
 
 --- The maybe function takes a default value, a function, and a Maybe value.
---- If the Maybe value is None, the function returns the default value.
---- Otherwise, it applies the function to the value inside the Some and
--- returns the result.
+--- If the Maybe value is Nothing, the function returns the default value.
+--- Otherwise, it applies the function to the value inside the Just and
+--- returns the result.
 maybe : forall {a : Type, b : Type}
       . b [0..1] -> (a -> b) [0..1] -> Maybe a -> b
-maybe [d] [_] None = d;
-maybe [_] [f] (Some x) = f x
+maybe [d] [_] Nothing = d;
+maybe [_] [f] (Just x) = f x
 
--- Monady interface for Maybe
+--- Monad interface for Maybe
 returnMb : forall {a : Type} . a -> Maybe a
-returnMb = Some
+returnMb = Just
 
+--- Monad interface for Maybe
 bindMb : forall {a : Type, b : Type}
      . Maybe a -> (a -> Maybe b) [0..1] -> Maybe b
-bindMb None [_] = None;
-bindMb (Some x) [k] = k x
+bindMb Nothing [_] = Nothing;
+bindMb (Just x) [k] = k x
 
 --- The fromMaybe function takes a default value and and Maybe value. If the
--- Maybe is None, it returns the default values; otherwise, it returns the value
+-- Maybe is Nothing, it returns the default values; otherwise, it returns the value
 -- contained in the Maybe.
 fromMaybe : forall {a : Type}
           . a [0..1] -> Maybe a -> a
-fromMaybe [d] None = d;
-fromMaybe [_] (Some x) = x
+fromMaybe [d] Nothing = d;
+fromMaybe [_] (Just x) = x
 
---- Whether a `Maybe a` value is `Some a`
-isSome : forall {a : Type} . Maybe (a [0]) -> Bool
-isSome None = False;
-isSome (Some [_]) = True
+--- Whether a `Maybe a` value is `Just a`
+isJust : forall {a : Type} . Maybe (a [0]) -> Bool
+isJust Nothing = False;
+isJust (Just [_]) = True
 
---- Whether a `Maybe a` value is `None`
-isNone : forall {a : Type} . Maybe (a [0]) -> Bool
-isNone m = not (isSome m)
+--- Whether a `Maybe a` value is `Nothing`
+isNothing : forall {a : Type} . Maybe (a [0]) -> Bool
+isNothing m = not (isJust m)

StdLib/Parallel.gr

@@ -12,8 +12,8 @@ module Parallel where
 
 import List
 
--- basic parallel combinator (defined in terms of linear channels)
--- `par` expects two thunks, `f` and `g`, and returns their resulting values in a pair
+--- basic parallel combinator (defined in terms of linear channels)
+--- `par` expects two thunks, `f` and `g`, and returns their resulting values in a pair
 par : forall {a : Type, b : Type} . (() -> a) -> (() -> b) -> (a, b)
 par f g =  let c = forkLinear (\c' -> close (send c' (f ()))); -- compute f in new thread
                b = g (); -- compute g in current thread
@@ -22,8 +22,8 @@ par f g =  let c = forkLinear (\c' -> close (send c' (f ()))); -- compute f in n
                _ = close c'
            in (a, b)
 
--- parallel combinator for lists of computations
--- `parList` expects a list of thunks, and returns a list of values (computed in parallel)
+--- parallel combinator for lists of computations
+--- `parList` expects a list of thunks, and returns a list of values (computed in parallel)
 parList : forall {a : Type} . List (() -> a) -> List a
 parList lst =
   case lst of

StdLib/Prelude.gr

@@ -51,18 +51,18 @@ if0 g [x] [y] =
 
 --- # Numeric functions and constants
 
--- Given some n, return
--- + 1 iff n is positive
--- + -1 iff n is negative
--- + 0 otherwise
+--- Given some n, return
+--- + 1 iff n is positive
+--- + -1 iff n is negative
+--- + 0 otherwise
 sign : Int [1..2] -> Int
 sign [x] = if x > 0 then 1 else if x < 0 then -1 else 0
 
 --- An approximation of pi
 pi : Float
 pi = 3.141592653589793
 
--- An approximation of Euler's number
+--- An approximation of Euler's number
 e : Float
 e = 2.718281828459045
 
@@ -86,33 +86,38 @@ uncurry : forall {a : Type, b : Type, c : Type} .
           (a -> b -> c) -> (a × b -> c)
 uncurry f (x, y) = f x y
 
---- # Coeffect-polymorphic combinators
+--- # Semiring-polymorphic combinators
 
 --- Coeffectful composition
 comp : forall {k : Coeffect, n : k, m : k, a : Type, b : Type, c : Type} .
        (b [n] -> c) -> (a [m] -> b) [n] -> a [n * m] -> c
 comp g [f] = \[x] -> g [f [x]]
 
+--- Graded necessity is an applicative functor
 boxmap : forall {a b : Type, s : Semiring, r : s} . (a -> b) [r] -> a [r] -> b [r]
 boxmap [f] [x] = [f x]
 
-unbox : forall {a : Type, k : Semiring} . a [1 : k] -> a
-unbox [x] = x
-
+--- 'Comultiplication' operation showing that graded necessity is a graded comonad
 disject : forall {a : Type, k : Semiring, n : k, m : k} . a [m * n] -> (a [n]) [m]
 disject [x] = [[x]]
 
+--- 'Counit' operation showing that graded necessity is a graded comonad
 extract : forall {a : Type, s : Semiring, r : s} . {(1 : s) <= r} => a [r] -> a
 extract [x] = x
 
---- Push coeffects on a pair into the left and right elements
--- pushPair : forall {a : Type, b : Type, k : Coeffect, c : k} . {(Hsup c c) == c} => (a × b) [c] -> a [c] × b [c]
--- pushPair [(x, y)] = ([x], [y])
+--- Push coeffects on a pair into the left and right elements. A distributive
+--- law of graded necessity over products. Note however that this is not always
+--- 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])
 
---- Pull coeffects of pair elements up to the pair
-pullPair : ∀ {a : Type, b : Type, k : Coeffect, n : k, m : k} . (a [n], b [m]) → (a, b) [n ∧ m]
+--- 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]
 pullPair = pull @(,)
 
+--- Generic copying of a value into a pair
 copy : forall {a : Type, s : Semiring} . a [(1 + 1):s] -> (a, a)
 copy [x] = (x, x)
 

StdLib/Result.gr

@@ -22,10 +22,11 @@ fromResult [default] result =
       (Failed [_]) -> default;
       (Ok x) -> x
 
--- Monady interface for Result
+--- Monady interface for Result
 return_res : forall {a : Type} . a -> Result a
 return_res = Ok
 
+--- Monady interface for Result
 bind_res : forall {a : Type, b : Type}
          . Result a -> (a -> Result b) [0..1] -> Result b
 bind_res m [k] =

StdLib/Stack.gr

@@ -3,12 +3,16 @@ module Stack where
 -- Use vectors to implement stacks
 import Vec
 
+
+--- Pop most recently added item from the stack
 pop : forall {n : Nat, a : Type} . Vec (n+1) a -> (a, Vec n a)
 pop = uncons
 
+--- Push item onto the stack
 push : forall {n : Nat, a : Type} . a -> Vec n a -> Vec (n+1) a
 push = Cons
 
+--- Pop the most recent item from the stack without removing it
 peek : forall {n : Nat, a : Type} . (Vec (n+1) a) [1..2] -> (a, Vec (n+1) a)
 peek [Cons x xs] = (x, Cons x xs)