solutions

splv23/solutions.gr

@@ -0,0 +1,102 @@
+-- # Section 2
+-- ## Q1
+
+dub : Int → Int
+dub x = 2 * x
+
+-- ## Q2
+
+const : forall {a b : Type} . a -> b [] -> a
+const x [y] = x
+
+ap : forall {a b c : Type}. (c -> a -> b) -> (c -> a) -> (c [] -> b)
+ap f x [ctx] = f ctx (x ctx)
+
+-- ## Q3
+
+import Bool
+
+copyBool : Bool -> (Bool, Bool)
+copyBool False = (False, False);
+copyBool True  = (True, True)
+
+-- ## Q4
+
+andShortCircuit : Bool -> Bool [] -> Bool
+andShortCircuit False [_] = False;
+andShortCircuit True  [x] = x
+
+-- # Section 3
+
+-- ## Q1
+
+twice : forall {a : Type} . (a -> a) [2] -> a -> a
+twice [f] x = f (f x)
+
+example31 : Int
+example31 = twice [\x -> x + 1] 1
+
+-- ## Q2
+
+twiceP : forall {a : Type, r : Semiring} . (a -> a) [(1 + 1):r] -> a -> a
+twiceP [f] x = f (f x)
+
+twice' : forall {a : Type} . (a -> a) [2] -> a -> a
+twice' = twiceP
+
+-- ## Q3
+
+import Cake
+
+mange : forall {n : Nat, m : Nat} . Cake [n + m] -> (Cake [n], Happy [m])
+mange [c] = ([have c], [eat c])
+
+-- ## Q4
+
+data ABVec (a : Type) (b : Type) (n : Nat) (m : Nat) where
+  NilAB   : ABVec a b 0 0;
+  ConsA : a -> ABVec a b n m -> ABVec a b (n+1) m;
+  ConsB : b -> ABVec a b n m -> ABVec a b n (m+1)
+
+abmap : forall {a a' b b' : Type, n m : Nat} . (a -> a') [n] -> (b -> b') [m] -> ABVec a b n m -> ABVec a' b' n m
+abmap [f] [g] NilAB = NilAB;
+abmap [f] [g] (ConsA x xs) = ConsA (f x) (abmap [f] [g] xs);
+abmap [f] [g] (ConsB x xs) = ConsB (g x) (abmap [f] [g] xs)
+
+-- ## Q5
+
+import Vec
+
+data Patient where
+  Patient : (city : String [Public]) -> (name : String [Private]) -> Patient
+
+reducePublic : forall {a : Type, n : Nat}
+              . (String -> a -> a) [n] -> a -> (Vec n Patient) -> a
+reducePublic [f] d Nil = d;
+reducePublic [f] d (Cons (Patient [city] [_]) xs) = f city (reducePublic [f] d xs)
+
+-- # Section 4
+
+-- ## Q1
+
+boolToInt : LChan (Recv Bool (Send Int End)) -> ()
+boolToInt c =
+  let (b, c) = recv c
+  in case b of
+       True  -> close (send c 1);
+       False -> close (send c 0)
+
+-- ## Q2
+
+client : LChan (Send Bool (Recv Int End)) -> Int
+client c =
+  let (i, c) = recv (send c True);
+      ()     = close c
+  in i
+
+-- ## Q3
+
+exampleSession : Int
+exampleSession =
+  let c = forkLinear boolToInt
+  in client c

splv23/solutions2.gr

@@ -0,0 +1,53 @@
+-- Preamble from discussion
+
+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)
+
+-- # Section 5
+
+import Parallel
+import Vec
+
+-- ## Q1
+
+toFloatArray : forall {n : Nat} . Vec n Float -> *FloatArray
+toFloatArray v =
+  let (n', v) = length' v
+  in toFloatArrayAux (newFloatArray (natToInt n')) [0] v
+
+toFloatArrayAux : forall {n : Nat} . *FloatArray -> Int [n] -> Vec n Float -> *FloatArray
+toFloatArrayAux a [n] Nil = a;
+toFloatArrayAux a [n] (Cons x xs) =
+  toFloatArrayAux (writeFloatArray a n x) [n + 1] xs
+
+-- ##
+
+parSum : *FloatArray -> Float
+parSum array =
+ let (n, array) = lengthFloatArray array;
+     [a]         = share array;
+    [n]         = moveInt n;
+     (x, y) = par (\() -> sumFromTo a [0] [div n 2])
+                  (\() -> sumFromTo a [div n 2] [n])
+ in x + y
+
+sumFromTo : FloatArray ->  Int [] -> Int [] -> Float
+sumFromTo array [i] [n] =
+  if i == n
+    then let () = drop @FloatArray array in 0.0
+    else
+      let (x, a) = readFloatArrayI array i
+      in  x + (sumFromTo a [i+1] [n])
+
+main : Float
+main =
+  parSum (toFloatArray (Cons 10.0 (Cons 20.0 (Cons 30.0 (Cons 40.0 Nil)))))