#+title: CS 3MI3 Tutorial
#+date: November 7

header:
#+BEGIN_SRC agda
module tutorial where

open import Data.Nat
open import Data.Bool
open import Data.List
open import Data.String using (String)
open import Relation.Binary.PropositionalEquality
  renaming (refl to by-definition-chasing)
  hiding ([_])
#+END_SRC

* Being co-dependent

#+BEGIN_SRC agda
-- What is “mutually defined”: Each one depends on the other.

-- example 1

mutual

  data NExpr : Set where
    val : ℕ → NExpr
    ‵if : BExpr → NExpr → NExpr

  data BExpr : Set where
    val : Bool → BExpr
    `≤   : NExpr → NExpr → BExpr

test₀ : BExpr
test₀ = `≤ (val 3) (‵if (val false) (val 0))

-- In constrast, this one depends on the previous but the previous do NOT depend on it.
Vars = String
data Prog : Set where
  _≔_ : Vars → BExpr → Prog

-- example 2

data Nat : Set where
  Zero : Nat
  Succ : Nat → Nat

mutual

  odd : Nat → Bool
  odd Zero     = false
  odd (Succ n) = even n

  even : Nat → Bool
  even Zero     = true
  even (Succ n) = odd n

test : odd (Succ (Succ Zero)) ≡ false
test = by-definition-chasing

#+END_SRC
* Well-typed?

In last tutorial, see Tuesday's code, we showed how “tag” terms by their type --𝓑 and 𝒩--
to avoid type errors; otherwise you can do whatever you like.

English example.

➩ “I am a person.”
  - This has meaning.

➩ “the colourless green liquid slept furiously”.
  - I can write this down; it's well-formed syntax.
  - But it has no meaning!
  - How can you be green and colourless!?

Likewise “x + true” is well-formed but lacks meanings.

Likewise, “1 / 0” lacks meaning.

* Scoping and terms in context

#+BEGIN_SRC agda
data Type : Set where
  ℬ 𝒩 : Type

⟦_⟧ : Type → Set
⟦ ℬ ⟧ = Bool
⟦ 𝒩 ⟧ = ℕ

-- infinitely many variables: 𝓍 0, 𝓍 1, 𝓍 2, …
-- TYPED VARIABLES
data Var (τ : Type) : Set where
  𝓍 : ℕ → Var τ

data Expr : Type → Set where
  ‵_ : ∀ {τ} → ⟦ τ ⟧ → Expr τ
  var : ∀ {τ} → Var τ → Expr τ
  _‵+_ : Expr 𝒩 → Expr 𝒩 → Expr 𝒩

_ : Expr ℬ
_ = ‵ false

_ : Expr 𝒩
_ = ‵ 23

-- crashes = (‵ true)  ‵+ (‵ 23)

-- precedence rules
infix 10 ‵_
infix 5  _‵+_

okay = ‵ 12  ‵+ ‵ 23

-- “terms in context” i.e., well-scoped terms or well-initilised terms, or both.
-- expressions such as “x + 3” don't make sense if “x” has no value.

-- “Γ ⊢ e” says e is a valid expression given ‘context’ Γ.
-- Γ = Pairs of variables and values.
-- If we only use variables ⇒ well-scoped.
-- If we use “Maybe values” ⇒ well-intialised or not; c.f. Data.Maybe

open import Data.Product renaming (_,_ to _↦_)

-- Context = ∀ {τ} → List (Var τ × ⟦ τ ⟧)
-- Wrong since it does not allow us to have differnetly typed variables.
-- Exercise dix me: Use Data.Sum via Σ.

-- For now, this is weak but works: We only cosnider natural numbers.

Context = List (Var 𝒩 × ℕ)

infix 1 _⊢_

data _⊢_ : Context → Expr 𝒩 → Set where
  value    : ∀ {n} → [] ⊢ ‵ n
  var      : ∀ {v n} → ((v ↦ n) ∷ []) ⊢ var v
  plus     : ∀ {Γ₁ Γ₂ e₁ e₂} → Γ₁ ⊢ e₁ → Γ₂ ⊢ e₂ → (Γ₁ ++ Γ₂) ⊢ (e₁ ‵+ e₂)

#+END_SRC