module STLC where

-- This is a self-contained implementation of a formally proved
-- type-checker for the STLC.


-- * Kit
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- First of all, we need to define a few general-purposes data-types
-- and operations on them. 

-- ** Nat
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- Here goes natural numbers, Peano-style. 

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- Coming with the addition:

_+_ : ℕ → ℕ → ℕ
x + zero = x
x + suc y = suc (x + y)

-- ** Fin
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- Then, Finite Sets. For n : ℕ, the elements of Fin n are "fz"
-- (ie. 0), "fs fz" (ie. 1), ..., up to "fs^(n-1) fz" (ie. n-1). That
-- is, given i : Fin ℕ, we *know* that i is between 0 and n-1.

data Fin : ℕ → Set where
  fz : {n : ℕ} → Fin (suc n)
  fs : {n : ℕ} → Fin n → Fin (suc n)

-- This "fs^(n-1)" operation I have written above will be useful
-- later. So let us define it formally:

_^_ : {n : ℕ} → ({n : ℕ} → Fin n → Fin (suc n)) → (m : ℕ) → Fin n → Fin (n + m)
f ^ zero = \ x → x
f ^ suc y = \ x → f ((f ^ y) x) 


-- * Types
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- All right, we define the Simply TYPED Lambda Calculus. So, let us
-- start with Types.

-- ** Data-type definition
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- Well, no need to get into complicated things: we consider a system
-- based on a base type "∘" plus a function space "⇒". Just as we
-- define and manipulate ∘, we could as well support natural number,
-- booleans, etc.

data Type : Set where
  ∘ : Type
  _⇒_ : (S T : Type) → Type


-- ** "Diff" of Type
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- During type-checking, we have to compare types. When two types are
-- not equal, there are 4 possibilities. We exhaustively represent
-- these possibilites by the following data-type. 

-- Note that this data-type is not just saying "they are different",
-- it gives an "diff" of one Type wrt. to another.

data Type− : Type → Set where
  neq∘ : (S T : Type) → Type− ∘
  neq⇒ : {S T : Type} → Type− (S ⇒ T)
  neqT : {S T : Type} → (T' : Type− T) → Type− (S ⇒ T)
  neqS : {S T : Type} → (S' : Type− S)(T' : Type) → Type− (S ⇒ T)

-- As I said, Type− really is a "diff". Therefore, given the original
-- type and its diff, we can compute the type it differs from:

_−_ : (S : Type) → Type− S → Type
∘       − neq∘ S T    = S ⇒ T
(S ⇒ T) − neq⇒        = ∘
(S ⇒ T) − neqT T'     = S ⇒ (T − T')
(S ⇒ T) − neqS S' T'  = (S − S') ⇒ T'


-- ** Equality
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- Finally, let us define the notion of equality of Types. However, as
-- usual, when comparing things for equality, we are not just
-- expecting as "yes/no" answer: if the two types are different, we
-- need to know why, ie. get the diff.  
-- 
-- This is for a simple reason: we are building a *proof*, therefore
-- we must have evidences that justify our conclusion. Hence, we
-- define the following equality predicate.

data TypeEq? : (S T : Type) → Set where
  type= : (S : Type) → TypeEq? S S
  type≠ : {S : Type} → (S' : Type− S) → TypeEq? S (S − S')


-- The equality test takes two types and fulfils this predicate:

typeEq? : (S T : Type) → TypeEq? S T

-- *** <1>1. Case: both types are ∘

typeEq? ∘ ∘                       = type= ∘

-- *** <1>2. Case: ∘ and (* ⇒ *) are necessarily distinct

typeEq? ∘ (S ⇒ T)                 = type≠ (neq∘ S T)

-- *** <1>3. Case: (* ⇒ *) and ∘ are necessarily distinct

typeEq? (S ⇒ T) ∘                 = type≠ neq⇒

-- *** <1>4. Case: both types are * ⇒ *: S ⇒ T and S' ⇒ T'

typeEq? (S ⇒ T) (S' ⇒ T') with typeEq? S S'

-- **** <2>1. Case: S and S' are equal

typeEq? (.S ⇒ T) (S ⇒ T') 
    | type= .S with typeEq? T T' 

-- ***** <3>1. Case: T and T' are equal

typeEq? (.S ⇒ .T) (S ⇒ T) 
    | type= .S 
    | type= .T                    = type= (S ⇒ T)

-- ***** <3>1. Case: T and T' are distinct

typeEq? (.S ⇒ T)  (S ⇒ .(T − T')) 
    | type= .S 
    | type≠ T'                    = type≠ (neqT T')

-- **** <2>1. Case: S and S' are distinct

typeEq? (S ⇒ T) (.(S − S') ⇒ T') 
    | type≠ S'                    = type≠ (neqS S' T')


-- ** Context of types
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


-- Now that we have defined Types, let us define a Context,
-- conventionally denoted Γ. A context is list of Type of size
-- n. Variable will index into this context with an element of Fin n.

infixr 5 _,_
infixr 5 _++_

data Context : ℕ → Set where
  ε   : Context zero
  _,_ : {n : ℕ}(xs : Context n)(x : Type) → Context (suc n)

-- Here is concatenation of Contexts:

_++_ : {n m : ℕ} → Context m → Context n → Context (m + n)
x ++ ε = x
x ++ (ys , y) = (x ++ ys) , y


-- *** Accessing the Context
--%%%%%%%%%%%%%%%%%%%%

-- As mentioned above, we are going to index into a Context of size n
-- by the mean of an element of Fin n. Let us define the function
-- extracting the type at position i. 

-- Again, we are not just interested in getting the data: we also keep
-- proof of the fact that it is the *correct* type we are getting out,
-- we are not making it out of nowhere.

data _!_ : {n : ℕ} → Fin n → Context n → Set1 where
  chunks : {m n : ℕ} → 
           (Γ : Context n)(T : Type)(Δ : Context m) →  ((fs ^ m) fz) ! ((Γ , T) ++ Δ)


_‼_ : {n : ℕ}(i : Fin n)(Γ : Context n) → i ! Γ
() ‼ ε
fz ‼ (Γ , T)                   = chunks Γ T ε
(fs i) ‼ (Γ , T)  with i ‼ Γ
(fs .((fs ^ m) fz)) ‼ (.((Γ , S) ++ Δ) , T)
    | chunks  {m} Γ S Δ        = chunks Γ S (Δ , T)


-- * Well-scoped, untyped lambda terms
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- This data-type lets us describe well-scoped, untyped lambda
-- terms. Not that it is *impossible* to write down an ill-scoped
-- lambda term with this representation, by definition.

data Term : ℕ -> Set where
  var : {n : ℕ} → (v : Fin n) → Term n
  app : {n : ℕ} → (f : Term n)(x : Term n) → Term n
  lam : {n : ℕ} → (S : Type)(b : Term (suc n)) → Term n

-- * Well-typed terms in a context
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- ** Data-type
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- This data-type lets us describe (well-scoped-) well-typed lambda
-- terms of type T in a typing context Γ. Note again that is
-- *impossible* to write down an ill-typed term with this
-- data-type. The idea of the type-checker is then, if possible, to
-- turn an untyped Term into the corresponding well-typed term.

-- Let x be an element of T ⊣ Γ. This reads as "x is of type T in the
-- context Γ". On paper, one usually writes "Γ ⊢ x : T", so it is just
-- a matter of reading it backward.

data _⊣_ : {n : ℕ} → Type → Context n → Set where
  gVar : {m n : ℕ} → 

             (Γ : Context n)(T : Type)(Δ : Context m) → 
             --------------------------------------------
             T ⊣ ((Γ , T) ++ Δ)

  gApp : {n : ℕ}{Γ : Context n}{S T : Type} → 

             (f : (S ⇒ T) ⊣ Γ)
             (x : S ⊣ Γ) → 
             -----------------
             T ⊣ Γ

  gLam : {n : ℕ}{Γ : Context n}(S : Type){T : Type} →

             (b : T ⊣ (Γ , S)) → 
             -------------------
             (S ⇒ T) ⊣ Γ

-- Note that the definition of the 3 constructors correspond directly
-- to the typing rules!

-- ** Forgetful map to terms
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- Given a well-scoped term, we can "forget" the proof that it is
-- well-typed, hence giving back an untyped Term.

_∋_ : {n : ℕ}{Γ : Context n} → 
      (T : Type) → (t : T ⊣ Γ) → Term n
.T      ∋ (gVar {m} {n} Γ T Δ)   = var ((fs ^ m) fz)
T       ∋ (gApp f x)             = app (_ ∋ f) (_ ∋ x)
(S ⇒ T) ∋ (gLam .S b)            = lam S (T ∋ b)

-- * Ill-typed terms
--%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

-- Now, if type-checking fails, we would like to know "why". Just as
-- the _⊣_ judgement represents a proof of "why the term type-checks",
-- we define the data-type not⊣ to justify "why the term doesn't
-- type-check". This is also in the same spirit that Type−, explaining
-- why two types are not equal.

data not⊣ : {n : ℕ} → Context n → Set where
  notNonFun : {n : ℕ}{Γ : Context n} →

                  (t : ∘ ⊣ Γ)
                  (x : Term n) → 
                  --------------
                  not⊣ Γ

  notMismatch : {n : ℕ}{Γ : Context n}{S S' T : Type} →

                    (f : (S ⇒ T) ⊣ Γ)
                    (s : S' ⊣ Γ) →
                    -----------------
                    not⊣ Γ

  notArg : {n : ℕ}{Γ : Context n}{S T : Type} →

               (f : (S ⇒ T) ⊣ Γ)
               (t : not⊣ Γ) →
               -----------------
               not⊣ Γ

  notFun : {n : ℕ}{Γ : Context n} →
        
               (f : not⊣ Γ)
               (t : Term n) →
               ---------------
               not⊣ Γ

  notLam : {n : ℕ}{Γ : Context n} →

               (S : Type)
               (b : not⊣ (Γ , S)) →
               ---------------------
               not⊣ Γ

-- ** Forgetful map
--********************************           

-- Same as for well-typed terms, we can forget the fact that a term is
-- ill-typed, getting back the original term we started with:

∌ : {n : ℕ}{Γ : Context n} → (t : not⊣ Γ) → Term n
∌ (notNonFun t s) = app (∘ ∋ t) s
∌ (notMismatch f s) = app (_ ∋ f) (_ ∋ s)
∌ (notArg f t) = app (_ ∋ f) (∌ t)
∌ (notFun f t) = app (∌ f) t
∌ (notLam S b) = lam S (∌ b)



-- * Type-checker
--****************************************************************

-- All right! Now, we just have to implement this damned type-checker!

-- There are two issues to a type-checking problem: either the term
-- type-checks, obtaining its type T (denoted ⊢ T ∋), or it doesn't
-- type-check (denoted ⊬).

-- In both cases, we have to give evidences justifying the success or
-- failure of the operation. These evidences build the correctness
-- proof.

data TypeCheck? : {n : ℕ} → Context n → Term n → Set where
  ⊢_∋ : {n : ℕ}{Γ : Context n} → 
         (T : Type)(t : T ⊣ Γ) → TypeCheck? Γ (T ∋ t)
  ⊬ : {n : ℕ}{Γ : Context n} → 
      (t : not⊣ Γ) → TypeCheck? Γ (∌ t)
 

-- So, here comes the type-checker:


typeCheck? : {n : ℕ} → (Γ : Context n)(t : Term n) → TypeCheck? Γ t

-- ** <1>1. Case: Variable: v

typeCheck? Γ (var v) with v ‼ Γ
typeCheck? .((Γ , T) ++ Δ) (var .((fs ^ m) fz)) 
    | chunks {m} Γ T Δ                  = ⊢ T ∋ (gVar Γ T Δ)

-- ** <1>2. Case: Application: f x

typeCheck? Γ (app f x) with typeCheck? Γ f 

-- *** <2>1. Case: f has a function type S ⇒ T

typeCheck? Γ (app .((S ⇒ T) ∋ f) x) 
    | ⊢ (S ⇒ T) ∋ f with typeCheck? Γ x 

-- *** <3>1. Case: s type-checks

typeCheck? _ (app .((S ⇒ T) ∋ f) .(S' ∋ s)) 
    | ⊢ (S ⇒ T) ∋ f 
    | ⊢ S' ∋ s with typeEq? S S' 

-- **** <4>1. Case: s has type S

typeCheck? _ (app .((S ⇒ T) ∋ f) .(S ∋ s)) 
    | ⊢ (S ⇒ T) ∋ f 
    | ⊢ .S ∋ s
    | type= .S                          = ⊢ T ∋ (gApp f s)

-- **** <4>2. Case: s has type S' ≠ S

typeCheck? _ (app .((S ⇒ T) ∋ f) .(_ ∋ s)) 
    | ⊢ (S ⇒ T) ∋ f 
    | ⊢ .(S − S') ∋ s 
    | type≠ S'                          = ⊬ (notMismatch f s)

-- *** <3>2. Case: s doesn't type-check

typeCheck? _ (app .((S ⇒ T) ∋ f) .(∌ s)) 
    | ⊢ (S ⇒ T) ∋ f 
    | ⊬ s                               = ⊬ (notArg f s)

-- *** <2>2. Case: f doesn't have a function type

typeCheck? _ (app .(∘ ∋ f) x) 
    | ⊢ ∘ ∋ f                           = ⊬ (notNonFun f x)

-- *** <2>3. Case: f doesn't type-check

typeCheck? _ (app .(∌ t) x) 
    | ⊬ t                               = ⊬ (notFun t x)

-- ** <1>3. Case: Lambda abstraction

typeCheck? Γ (lam S b) with typeCheck? (Γ , S) b 

-- *** <2>1. Case: the body type-checks

typeCheck? Γ (lam S .(T ∋ t)) 
    | ⊢ T ∋ t                           = ⊢ (S ⇒ T) ∋ (gLam S t)

-- *** <2>2. Case: the body doesn't type-check

typeCheck? Γ (lam S .(∌ t)) 
    | ⊬ t                               = ⊬ (notLam S t)


-- * What have we done? What have we proved?

-- We have defined well-scoped terms, Term, and well-typed, _⊣_. We have
-- then implemented a function mapping untyped Terms to well-typed
-- terms. Such function is a type-checker.

-- Agda being a total language, we have therefore proved that our
-- type-checker always terminates (otherwise, it would not have been
-- possible to write it in a first place).

-- We claim to have proved the correctness of this type-checker,
-- provided that one agrees with our definition of a well-typed term,
-- _⊣_. The definition of _⊣_ being simple and self-explanatory gives
-- us strong confidence in this. For more safety, one could come up
-- with an alternative definition and prove their equivalence.

-- * Outro

-- Local Variables:
-- eval: (outline-minor-mode)
-- outline-regexp: "-- [*\f]+"
-- outline-level: outline-level
-- End: