exercises.gr

-- # Exercises

-- ## Ex 1 Make the following functions typecheck by addition of
-- graded modalities at the type level only where needed and the
-- relevant unboxing pattern matches at the value level. Give the most
-- precise type.

-- const : forall {a c : Type} . a -> (c -> 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)

-- Consider which particular graded modality to use.  Hint: try a
-- Nat-graded modality first.  Advanced: Can you make it polymorphic
-- in the coeffect grade?

-- ## Ex 2

-- Consider the following definition:

import Bool

copyBool : Bool -> (Bool, Bool)
copyBool False = (False, False);
copyBool True  = (True, True)

-- Why does `copyBool` not violate linearity?

-- ## Ex 3

-- Write a well-typed short-circuiting version of `and` on `Bool`
-- i.e., where `and False x` need not inspect the value of `x`.

-- ## Ex 4  Inductive families and grading

-- Define an indexed data type 'ABList' that has two cons cells for
-- 'a' elements and 'b' elements, i.e., with the header:

-- data ABList (a : Type) (b : Type) : Nat -> Nat -> Type where

-- Define the `map` function for ABList which takes two function
-- parameters for the `a` and `b` elements, with precise usage on
-- each.