solutions.gr

-- # 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