Examples from the paper 'Linearity and Uniqueness: An Entente Cordiale'

examples.gr

-- # Examples from the paper 'Linearity and Uniqueness: An Entente Cordiale'

-- ## Linearity (see Section 2, Key ideas)

-- Linearity (with cake)

data Cake  = Cake
data Happy = Happy

eat : Cake -> Happy
eat Cake = Happy

have : Cake -> Cake
have Cake = Cake

-- You cannot have your cake and eat it...

-- impossible : Cake → (Happy, Cake)
-- impossible cake = (eat cake, have cake)

-- ...unless you have infinite cake (p.5)
possible : !Cake → (Happy, Cake)
possible lots =
  let !cake = lots in (eat cake, have cake)

-- e.g.
-- Granule> possible [Cake]
-- (Happy, Cake)

 -- ...or there is a more precise way (a specialisation of this appears on p.23)
accurate : ∀ {n : Nat} . Cake [n+1] → (Happy, Cake [n])
accurate lots =
  let [cake] = lots in (eat cake, [have cake])

-- e.g.
-- Granule> accurate [Cake]
-- (Happy, [Cake])

--  File handles and side effects (p.5)
firstChar : Char <IO>
firstChar = let
  h <- openHandle ReadMode "README.md";
  (h, c) <- readChar h;
  () <- closeHandle h
  in pure c

twoChars : (Char, Char) <IO>
twoChars = let
  h <- openHandle ReadMode "README.md";
  (h, c1) <- readChar h;
  (h, c2) <- readChar h;
  () <- closeHandle h
  in pure (c1, c2)

-- e.g.
-- Granule> firstChar
-- '#'
-- Granule> twoChars
-- ('#', ' ')

-- ## Uniquness (see Section 2 and Section 4)

-- Uniqueness (with coffee)

data Coffee = Coffee
data Awake  = Awake

drink : Coffee -> Awake
drink Coffee = Awake

keep : Coffee -> Coffee
keep Coffee = Coffee

-- impossible : *Coffee -> (Awake, *Coffee)
-- impossible Coffee = (drink coffee, keep coffee)

-- Akin to `possible` from Clean on p.6
-- also appears on p.19

sip : *Coffee -> (Coffee, Awake)
sip fresh = let !coffee = &fresh in (keep coffee, drink coffee)

-- e.g.
-- Granule> sip #Coffee
-- (Coffee, Awake)

-- Arrays and mutability examples

fill' : *FloatArray -> !Int -> *FloatArray
fill' arr [0] = arr;
fill' arr [i] =
  let f = intToFloat i;
      arr' = writeFloatArray arr i f
  in fill' arr' [i - 1]

dotp' : *FloatArray -> *FloatArray -> !Int -> Float -> (Float, (*FloatArray,* FloatArray))
dotp' arr1 arr2 [0] v = (v, (arr1, arr2));
dotp' arr1 arr2 [i] v =
  let (e1, arr1') = (readFloatArray arr1 i);
      (e2, arr2') = (readFloatArray arr2 i)
  in dotp' arr1' arr2' [i - 1] (v + (e1 * e2))

-- ## Relative monad properties

-- Copying a non-linear value as unique and then borrowing it gives you the
-- original value
unitR : forall {a : Type} . !a -> !a
unitR t = clone t as x in &x

-- Borrowing a unique value and copying it to apply a function is the same as
-- just applying the function
unitL : forall {a b : Type} . *a -> (!a -> !b) -> !b
unitL t f = clone &t as x in f &x

-- Nesting copies works as you would expect (and obeys associativity)
assoc : forall {a b c : Type} . !a -> (*a -> !b) -> (*b -> !c) -> !c
assoc t f g = clone t as x in
                clone f x as y in g y

-- (p.20) example
cloneExample : (Float, FloatArray)
cloneExample =
  let x = newFloatArray 10 in
  let [y] = &x in
  let [()] = clone [y] as y' in (let () = deleteFloatArray y' in [()])
  in readFloatArray' y 1

-- A main stub, provides the default entry-point for Granule
main : ()
main = ()