Some of the dependent types we discussed today in Agda

FpAtLunch.agda

module FpAtLunch where

open import Data.Nat
open import Data.Bool

---------------------------------
-- Lists of length n (Vectors) --
---------------------------------

-- In Agda `Set` is used to denote the type of types (rather than `Type` or `*`)
data Vec (A : Set) : ℕ → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (1 + n)

-- The curly braces just mean implicit argument (so we don't specify it here)
safeHead : ∀ {A n} → Vec A (1 + n) → A
safeHead (x ∷ xs) = x


--------------------
-- Even predicate --
--------------------

data Even : (n : ℕ) → Set where
  zero : Even 0
  ss   : ∀ {n} → Even n → Even (2 + n)

-- Adding two even numbers produces an even number, or "Gianlo's theorem"
even-+ : ∀ {n m} → Even n → Even m → Even (n + m)
even-+ zero    em = em
even-+ (ss en) em = ss (even-+ en em)


---------------
-- Typed DSL --
---------------

-- We'll pick two types for our DSL, natural numbers and booleans
data Type : Set where
  nat  : Type
  bool : Type

-- And some simple programs on these types
-- Note we're overloading the symbol `false` and `true`
data Prog : Type → Set where
  zero   : Prog nat
  succ   : Prog nat → Prog nat
  true   : Prog bool
  false  : Prog bool
  ifelse : ∀ {a} → Prog bool → Prog a → Prog a → Prog a

-- How our DSL types map to Agda
⟦_⟧ : Type → Set
⟦ nat  ⟧ = ℕ
⟦ bool ⟧ = Bool

eval : ∀ {t} → Prog t → ⟦ t ⟧
eval zero     = 0
eval (succ p) = 1 + eval p
eval true     = true
eval false    = false
eval (ifelse b p q) with eval b
... | true = eval p
... | false = eval q