------------------------------------------------------------------------
-- One minute papers
------------------------------------------------------------------------

-- | Type system

-- We are going to see more and more of it throughout the
-- lectures. It's normal to still be a bit lost.



-- | Difference between functions and proofs

-- They are the same thing from the point of view of the
-- system. It is more of a judgement *you* make based on
-- how you *feel* about the program.
--
-- Is the computational content interesting?
-- e.g. `ℕ → ℕ → ℕ` is a boring statement to prove but
-- implementing _+_ or _*_ is definitely interesting.
-- Then it's probably a function
--
-- Are all of the solutions the same?
-- e.g. `m + n ≡ n + m` is an interesting statement to prove
-- but this does not contain any interesting computation.
--
-- But then again: `A → A` is a boring statement with no
-- interesting computational content... and yet the identity
-- function is a very useful piece of kit to have!


-- | Subst, lhs ≡ lhs
-- Let us reconstruct equality and substitution from the ground
-- up

-- First the type of booleans with two constructors
data Bool : Set where
  true : Bool
  false : Bool

variable b c : Bool

-- * `IsTrue` is the predicate that takes an index and insists
-- it is the constructor `true`, as witnessed by the return
-- type of its unique constructor `isTrue`
data IsTrue : Bool → Set where
  isTrue : IsTrue true

-- How can we use such proofs?
-- Knowing how to prove `P true`
-- Knowing that `b` satisfies `IsTrue`
-- We can prove `P b`
-- thanks to dependent pattern matching:
-- when matching on the proof of `IsTrue b`, we reveal
-- the constructor `isTrue` which can only be used if
-- `b` happens to be `true` and so Agda substitues `true`
-- for `b`. And so we are able to return the proof `ptrue`.
substTrue : (P : Bool → Set) → P true → IsTrue b → P b
substTrue P ptrue isTrue = ptrue

-- * We can play the same game with `false` instead of `true`
-- and obtain `IsFalse` and `substFalse`.
-- (this is literally generated by search & replace)
data IsFalse : Bool → Set where
  isFalse : IsFalse false

substFalse : (P : Bool → Set) → P false → IsFalse b → P b
substFalse P pfalse isFalse = pfalse

-- * Rather than doing the work twice, we can introduce the
-- `Is` family which takes
-- 1. a parameter `b` that is fixed and decides whether we want
-- to have the behaviour of `IsTrue` or `IsFalse`
-- 2. an index of type `Bool` which we will constrain
--
-- The only constructor `is` insists that the index is equal
-- to the parameter.
data Is (b : Bool) : Bool → Set where
  is : Is b b

-- And you could indeed recover something equivalent to `IsTrue`
-- by partially applying `Is` to `true`.
IsTrue' : Bool → Set
IsTrue' = Is true

-- The elimination principle for `Is` is now more general:
-- Knowing that `P b` holds
-- Knowing that `c` satisfies `Is b`
-- We can prove `P c`.
-- using dependent pattern matching:
-- matching on `is` only leads to a valid equation if `Agda` is
-- able to make `b` and `c` the same thing. It does so by picking
-- either one and substituting it for the other.
substIs : (P : Bool → Set) → P b → Is b c → P c
substIs P pb is = pb

-- * The last generalisation step is to abstract away from `Bool`
-- and define a generic type of equality. It takes
-- 1. an implicit parameter `A` corresponding to the type of elements
-- we happen to be considering
-- 2. a parameter `a` of type `A`
-- 3. an index of type `A` that we want to constraint to being equal
-- to the parameter `a`.
--
-- As in the `Is` example we have a second constructor
-- demanding that the index is the same as the parameter.
-- We call it `refl` for `reflexivity`.

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

variable A : Set
variable x y : A

-- `subst` follows the same principle as `substIs` albeit for
-- a generic type `A`.
subst : (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

------------------------------------------------------------------------
-- Today's lecture: exploring the design space
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Happy design path
-- Lookup, n ways
------------------------------------------------------------------------

-- Forward lists
data List (A : Set) : Set where
  [] : List A
  _,-_ : A → List A → List A

-- Natural numbers
data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

variable
  n : ℕ
  xs : List A

------------------------------------------------------------------------
-- Oops

-- Given a list of values of type `A` and an index,
-- return the value at that position in the list.
-- e.g. lookup ["a","b","c"] 2 should return "b"
lookup : List A → ℕ → A

-- If the list is non-empty then we inspect the index:
-- if it's zero    then we want the first element
--   and so we return the head
-- if it's (suc n) then we want the nth element in the tail
--   and so we perform a recursive call
lookup (x ,- xs) zero = x
lookup (x ,- xs) (suc n) = lookup xs n

-- If the list is empty however, we cannot proceed.
-- The type `A` is arbitrary and so there is no way
-- for us to construct an inhabitant for it.
-- In Haskell we would have the opportunity to lie
-- and pretend this case does not exist at the risk
-- of ending up with a runtime error.

lookup [] n = {!!} -- oops


------------------------------------------------------------------------
-- Partiality

-- The simplest solution is to have a more honest type:
-- rather than claiming we will be able to return a value
-- of type `A` no matter what, we can claim we may or may
-- not return one.

-- The Maybe type is just like in Haskell
data Maybe (A : Set) : Set where
  just : A → Maybe A
  nothing : Maybe A

-- This time lookup acknowledges it may fail.
lookupM : List A → ℕ → Maybe A

-- If the list is non-empty, we can play the same game we played
-- in the above version: if the index is zero then return the
-- answer and otherwise perform a recursive call.

lookupM (x ,- xs) zero = just x
lookupM (x ,- xs) (suc n) = lookupM xs n

-- In the empty case it is now possible for us to produce a value:
-- we can simply return `nothing`!

lookupM [] n = nothing

-- Note however that the type of `lookupM` offers no guarantee
-- whatsoever on whether or not we are actually implementing
-- the appropriate function.
-- For all we know we may be returning `nothing` uniformly
-- because we were too lazy to write a proper implementation!

------------------------------------------------------------------------
-- Tightening the input type

-- We saw that if the index happened to be out of bounds then
-- we could not possibly return a value. If only we could ensure
-- that the index is *in* bounds!

-- The main idea here is that the index, a natural number, should
-- be smaller than the list's length, another natural number.
-- A possible solution is to define a type of lists whose lenghts
-- is known together with a type of indices whose upper bound is known.


-- A `Vect n A` is a `List A` whose length is enforced to
-- be exactly `n`. Correspondingly it has two constructors
-- (the same as lists but with more precise types):
-- `[]` is the constructor for the empty vector (it has size `zero`)
-- `_,-_` combines a head and a tail of size `n` to obtain a vector
--   of size `suc n`.
data Vect (A : Set) : ℕ -> Set where
  [] : Vect A zero
  _,-_ : A -> Vect A n -> Vect A (suc n)

variable vs : Vect A n

-- A `Fin n` is a `ℕ` that is guaranteed to be strictly smaller
-- than `n`. It has two constructors (the same as `ℕ` but with
-- more precise types):
-- `zero` is the constructor for the number `0`. It is strictly
--   smaller than anything that is non-zero. Hence the constraint.
-- `suc` takes a number (strictly smaller than some `n`) and
--   returns its successor. If `k < n` then `1+k < 1+n` hence
--   the `suc n` return type of `suc`.

data Fin : ℕ → Set where
  zero : Fin (suc n)
  suc : Fin n → Fin (suc n)

variable k : Fin n

-- We can now write `vlookup` which
-- provided a vector of type `A` whose size is `n`
-- and a number strictly smaller than `n\
-- returns a value of type `A`
vlookup : Vect A n → Fin n → A

-- In the non-empty case, we can use the same call patterns as before.
-- Everything typechecks

vlookup (x ,- xs) zero = x
vlookup (x ,- xs) (suc k) = vlookup xs k

-- The empty case is now impossible. We can leave it out entirely if
-- we want. Here I write it down to show the absurd pattern `()`
-- dismissing an impossible value:
-- the pattern [] checked at type `Vect A n` implies that `n` equals `zero`
-- that means that the `Fin n` argument is actually a `Fin zero` argument
-- but all the `Fin` constructors return a `Fin (suc m)` value for some `m`
-- and so `Fin zero` is an empty family.

vlookup [] ()


-- Challenge: see how `Vect` allows us to give functions such as
-- `zip` or `replicate` a more precise type than their list counterparts.


------------------------------------------------------------------------
-- Strengthening the output type

-- The type we gave to `vlookup` could still have led us to a different
-- implementation:

vhead : Vect A n → Fin n → A
vhead (x ,- _) _ = x

-- We can be more precise by giving an inductive specification explicitly
-- stating what it means for a value to be at a given position in a vector.

infix 0 _[_]≈_
data _[_]≈_ {A : Set} : Vect A n → Fin n → A → Set where
  zero : x ,- vs [ zero ]≈ x
  suc : vs [ k ]≈ y → x ,- vs [ suc k ]≈ y

-- Here the zero constructor states that the zeroth value is the head of
-- a non-empty vector
-- While the suc constructor turns a proof that `y` is the `k`th value in
-- `vs` into one that it is the `suc k`th value in `x ,- vs`.

-- We can then have a certified lookup function that returns not only
-- a value but also a proof that it is the one we are looking for.
-- To do so we use a dependent pair (aka Sigma type)

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

-- This function allows us to remember where the value we obtained came
-- from by retaining a proof it is at index `k` in `xs`.
clookup : (xs : Vect A n) (k : Fin n) → Σ A (λ v → xs [ k ]≈ v)
clookup (x ,- xs) zero = x , zero
clookup (x ,- xs) (suc k)
  = let (v , prf) = clookup xs k in
    v , suc prf


------------------------------------------------------------------------
-- The dead ends we did not show you

-- We showed you the happy path but the design space is a lot bigger.
-- You could for instance have defined _[_]≈_ to operate on lists and
-- natural numbers and then implemented functions like


-- A lookup that can still fail but if it does not then returns a very
-- precise proof. This could still just be constantly `nothing`!
-- lookup : (xs : List A) (k : ℕ) → Maybe (Σ A (λ v → xs [ k ]≈ v))

-- A lookup that either succeeds or returns an "error message" that is
-- a proof that the index was too big. This gives you more structure
-- to exploit for error reporting.
-- lookup : (xs : List A) (k : ℕ) → length xs ≤ k ⊎ (Σ A (λ v → xs [ k ]≈ v))


-- But this last function still has the drawback of mixing the checking that
-- the index is valid with the action of looking up the associated value.
-- As library writers, we should strive to offer interfaces that are based
-- on a separation of concerns.
-- For instance users can achieve a similar error-reporting result by combining
--
-- isFin : (n : ℕ) (k : ℕ) → n ≤ k ⊎ Fin n
-- lookup : (xs : Vect A n) (k : Fin n) → A
--
-- with the advantage that `lookup` is now guaranteed to be error-free if we
-- have access to indices that have already been validated.

-- This approach is summarised by rules 1 & 2 of the Unix philosophy:
-- ✔ 1. Write programs that do one thing and do it well.
-- ✔ 2. Write programs to work together.
-- ❌ 3. Write programs to handle text streams, because that is a universal interface.
-- We disregard rule 3 as we are concerned with writing libraries, not small
-- command line utilities and so can instead rely on structure-rich formats.
