#+Title: Agda demo
#+Author: Mark Armstrong
#+Description: A quick demo of Agda

* About this file

This is a /literate Agda/ file; hence, the file ending being
~.lagda~, rather than ~.agda~.

Agda supports literate programming in ~.lagda~ files,
with the code in between either
LaTeX style blocks (~\begin{code}~, ~\end{code}~)
or, in more recent versions,
Org style source blocks (~#+begin_src agda2~, ~#+end_src~).

If you use an older version of Agda, this file may not
work for you by default; you can find/replace the Org style
block delimiters with LaTeX style ones, and it should work.

To switch from ~org-mode~ to ~agda2-mode~ when using this file,
use ~M-x agda2-mode~; to go back, ~M-x org-mode~.

Musa has developed a (somewhat alternate) solution to working
with Agda in Org mode, called
[[https://github.com/alhassy/org-agda-mode][~org-agda~ mode]];
you may find it useful if you want to write Agda in Org mode.

* Standard library inclusions

Agda includes very few types and constructs as built-in;
therefore, we must either
- include a fair amount from the standard library, or
- define everything ourselves.

In this instance, I choose to import from the standard library,
but apply some heavy renaming to make the connection between types
and propositions much clearer.

By qualifying the import with ~using ()~, nothing is imported
except what we list in the ~renaming (…)~ qualifier.
#+begin_src agda2
-- The module name for the file must be the same as the filename
module agda-demo where

-- Types used for “propositions”
open import Level
  using ()
  renaming (zero to lzero)
open import Data.Empty
  using ()
  renaming (⊥ to Falsehood ; ⊥-elim to ex-falso)
open import Data.Unit
  using ()
  renaming (⊤ to Truth ; tt to witness)
open import Data.Product
  using ()
  renaming (_×_ to _∧_ ; _,_ to ∧-intro)
open import Data.Sum
  using ()
  renaming (_⊎_ to _∨_ ; inj₁ to ∨-intro-left ; inj₂ to ∨-intro-right)
open import Relation.Nullary using (¬_)
open import Relation.Unary using (Pred)
open import Relation.Binary.PropositionalEquality
  using (_≡_)
  renaming (refl to ByReflexivity)

-- Types used for “data”
open import Data.Bool using (Bool ; true ; false ; if_then_else_)
open import Data.Nat
  using (ℕ ; suc ; zero ; _+_ ; _*_ ; _∸_ ; _^_)
open import Data.Maybe using (Maybe ; just ; nothing)
#+end_src

The type former ~Pred~ creates a predicate on a given type;
for instance, ~Pred ℕ~ is the type of unary predicates on the natural numbers
(examples of this type would include ~even~, ~odd~, ~prime~, ~greater-than-10~).
However, ~Pred~ actually takes one additional argument of type ~Level~
(which has to do with the “hierarchy of universes”).
We will usually work at level “zero”, so we define ~Predicate~ as a shorthand.
#+begin_src agda2
_Predicate : Set → Set₁
A Predicate = Pred A lzero
#+end_src

* Recreating numerical expression with prefix operators in Agda

Let's revisit assignment 1, but see how we would do it in Agda.

#+begin_src agda2
module Assignment1 where
#+end_src

First, we form a type of integer expressions;
this is largely the same as what we did in F#, except I choose
to work only with natural numbers
(which are far simpler than the standard library's integer type),
so negative and absolute value are excluded.
#+begin_src agda2
  data IExpr : Set where
    -- Naming the arguments of a constructor (n here)
    -- sometimes makes Agda use better names when case splitting.
    Const : (n : ℕ) → IExpr
    -- Constructors of the same arity can be declared together.
    Plus Times Monus Exp : (e : IExpr) → (f : IExpr) → IExpr
#+end_src

Defining an interpret function over such an inductive datatype
is quite easy; in fact, it's easier in Agda as 
#+begin_src agda2
  -- Again, naming the argument here (e) sometimes makes Agda choose better names.
  interpret : (e : IExpr) → ℕ
  interpret (Const n) = n
  interpret (Plus e e₁) = interpret e + interpret e₁
  interpret (Times e e₁) = interpret e * interpret e₁
  interpret (Monus e e₁) = interpret e ∸ interpret e₁
  interpret (Exp e e₁) = interpret e ^ interpret e₁
#+end_src

* Expressions with variables and substitutions

With the basic expressions, we don't get too much use out of type checking;
there's just not that much that can “go wrong”.

We get a bit more if we consider expressions with variables and substitutions,
because here we may have “illegal” expressions that should not be interpreted.

First, let us solve the problem as we would in a non-dependently typed language.
Rather than use exceptions, though, we'll use the ~Maybe~ type,
which models partial values.
#+begin_src agda2
module Substitution where

  Variable : Set
  Variable = ℕ

  data IExpr : Set where
    Var   : Variable → IExpr
    Subst : Variable → IExpr → IExpr → IExpr
    Const : ℕ → IExpr
    Plus  : IExpr → IExpr → IExpr
    Times : IExpr → IExpr → IExpr
    Monus : IExpr → IExpr → IExpr
    Exp   : IExpr → IExpr → IExpr

  -- There is not a boolean valued equality check easily available for ℕ,
  -- so we define one.
  _==_ : (m n : ℕ) → Bool
  zero == zero    =  true
  suc m == suc n  =  m == n
  zero == suc _   =  false
  suc _ == zero   =  false

  -- substitute x e f  ≈  f[x ≔ e]
  substitute : (x : Variable) → (e f : IExpr) → IExpr
  substitute x e (Var y) = if x == y then e else Var y
  substitute x e (Subst y f₁ f₂) =
    if x == y
      then Subst y (substitute x e f₁) f₂
      else Subst y (substitute x e f₁) (substitute x e f₂)
  substitute x e (Const f) = Const f
  substitute x e (Plus f₁ f₂) = Plus (substitute x e f₁) (substitute x e f₂)
  substitute x e (Times f₁ f₂) = Times (substitute x e f₁) (substitute x e f₂)
  substitute x e (Monus f₁ f₂) = Monus (substitute x e f₁) (substitute x e f₂)
  substitute x e (Exp f₁ f₂) = Exp (substitute x e f₁) (substitute x e f₂)

  {-# TERMINATING #-}
  interpret? : (e : IExpr) → Maybe ℕ
  interpret? (Var x) = nothing
  interpret? (Subst x e e₁) = interpret? (substitute x e e₁)
  interpret? (Const n) = just n
  interpret? (Plus e e₁) with interpret? e | interpret? e₁
  interpret? (Plus e e₁) | just v₁ | just v₂ = just (v₁ + v₂)
  interpret? (Plus e e₁) | just _ | nothing = nothing
  interpret? (Plus e e₁) | nothing | just _ = nothing
  interpret? (Plus e e₁) | nothing | nothing = nothing
  interpret? (Times e e₁) with interpret? e | interpret? e₁
  interpret? (Times e e₁) | just v₁ | just v₂ = just (v₁ * v₂)
  interpret? (Times e e₁) | just _ | nothing = nothing
  interpret? (Times e e₁) | nothing | just _ = nothing
  interpret? (Times e e₁) | nothing | nothing = nothing
  interpret? (Monus e e₁) with interpret? e | interpret? e₁
  interpret? (Monus e e₁) | just v₁ | just v₂ = just (v₁ ∸ v₂)
  interpret? (Monus e e₁) | just _ | nothing = nothing
  interpret? (Monus e e₁) | nothing | just _ = nothing
  interpret? (Monus e e₁) | nothing | nothing = nothing
  interpret? (Exp e e₁) with interpret? e | interpret? e₁
  interpret? (Exp e e₁) | just v₁ | just v₂ = just (v₁ ^ v₂)
  interpret? (Exp e e₁) | just _ | nothing = nothing
  interpret? (Exp e e₁) | nothing | just _ = nothing
  interpret? (Exp e e₁) | nothing | nothing = nothing
#+end_src

But we can do better with dependent types.
We can restrict our attention to only expressions which do not have open variables,
hence avoiding the need for the ~Maybe~ type.

To accomplish this here, we will define a /predicate/ on integer expressions,
~Closed~.
#+begin_src agda2
  {-# TERMINATING #-}
  Closed : IExpr Predicate  -- ≈ IExpr → Set
  Closed (Var x) = Falsehood  -- Empty type, ⊥
  Closed (Subst x e₁ e₂) = Closed (substitute x e₁ e₂)
  Closed (Const x) = Truth  -- Unit type, ⊤
  Closed (Plus x x₁)  = Closed x ∧ Closed x₁  -- Product type, _×_
  Closed (Times x x₁) = Closed x ∧ Closed x₁
  Closed (Monus x x₁) = Closed x ∧ Closed x₁
  Closed (Exp x x₁)   = Closed x ∧ Closed x₁
#+end_src

Now, we can define an alternate version of ~interpret?~
which returns a natural number; no ~Maybe~.
It takes as arguments an expression /and a proof that that expression is closed/.
#+begin_src agda2
  {-# TERMINATING  #-}
  interpret : (e : IExpr) → Closed e → ℕ
  interpret (Subst x e e₁) closed = interpret (substitute x e e₁) {!!}
  interpret (Const n)     closed = n
  interpret (Plus e e₁)   (∧-intro e-closed e₁-closed) =
    interpret e e-closed + interpret e₁ e₁-closed
  interpret (Times e e₁)  (∧-intro e-closed e₁-closed) =
    interpret e e-closed * interpret e₁ e₁-closed
  interpret (Monus e e₁)  (∧-intro e-closed e₁-closed) =
    interpret e e-closed ∸ interpret e₁ e₁-closed
  interpret (Exp e e₁)    (∧-intro e-closed e₁-closed) =
    interpret e e-closed ^ interpret e₁ e₁-closed
#+end_src