Created
January 13, 2022 10:29
-
-
Save dorchard/4b0df8e3369e8b7a04fbf4097f0d23ec to your computer and use it in GitHub Desktop.
Examples from the paper 'Linearity and Uniqueness: An Entente Cordiale'
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- # 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 = () |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment