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

* Set vs Type

  It's an issue of membership.
  + Type ⇒ Syntactically *decidable* membership
  + Sets ⇒ do not; i.e., require semantics, algorithm.

  E.g., ℕ as type whereas  primes are a set
  + ~Succ Succ Zero~ is a member of ℕ by *inspection*
  + 11 is a prime since it has no proper divisors.

* An alternate presentation of iexpr
Op ::= + | - | mod | * | div
iexpr ::= ℕ | Var | Bop Op iexpr expr
* Statement vs Expression?

  + Expression /evaluates/ to a “value” but a statement does not.
  + Statement, for the most part, alters “state” --i.e., “the real world”.

  These are two languages, usually rather distinct.
  It's unfortunate: It makes the programmer have to learn multiple
  incompatible languages.

  ➩ C has ~if⋯then⋯else⋯~ for statements and ~⋯:⋯?⋯~ for values.
  ➩ Lisp, Haskell, Agda, etc don't care to make this distinction.
    - All three use the same conditional for both levels.
    - Lisp-syntax: ~(if (< 1 x) (setq y x) (setq z x))~
      * In C-syntax: ~if (1 < x) y = x; else z = x;~
* simplified Hmwrk2 approach :agda:

#+BEGIN_SRC agda
module tutorial where

open import Data.Nat
open import Data.Bool
open import Data.List

-- Here's a simplified Hmwrk2 approach
-- It will be in AST/Prefix/Lisp style

{- All our variables look like
𝓍 0, 𝓍 1, 𝓍 2, etc
-}
data Variable : Set where
  𝓍 : ℕ → Variable

data Type : Set where
  ℬ 𝒩 : Type
  -- \McB and \McN

-- Interpret the encodes of types.
⟦_⟧ₜ : Type → Set
⟦ ℬ ⟧ₜ = Bool
⟦ 𝒩 ⟧ₜ = ℕ

-- Here are “typed operations”
data BOp : Type → Set where
  ‵+ ‵- ‵* ‵div ‵mod : BOp 𝒩
  -- Likewise for BOp ℬ

-- Here are “typed expressions”
data Expr : Type → Set where
  Var  : ∀ {τ} → Variable → Expr τ

  -- Valᴺ : ℕ → Expr 𝒩
  -- Valᴮ : Bool → Expr ℬ
  -- DRY Principle
  --
  Val : ∀ {τ} → ⟦ τ ⟧ₜ → Expr τ

  Func : ∀ {τ}
       → BOp τ → Expr τ → Expr τ → Expr τ

-- syntactic sugar, by demand
_⟨_⟩_ : ∀ {τ} (left  : Expr τ)
              (op    : BOp τ)
              (right : Expr τ)
      → Expr τ
l ⟨ op ⟩ r = Func op l r

_ : Expr 𝒩
-- _ = Valᴺ 2 ⟨ ‵+ ⟩ Valᴺ 3
_ = Val 2 ⟨ ‵+ ⟩ Val 3
-- Looks like type inference.

{- This crashes: Since ‵+ is TYPED.
_ : Expr 𝒩
_ = Valᴺ 2 ⟨ ‵+ ⟩ Valᴮ true
-}
#+END_SRC