module Palmse.Combinators.Lam* where
-- open import Data.List
-- A bracket abstraction algorithm for typed combinatory logic. It differs
-- from the usual bracket abstraction algorithm given in the lectures. Its
-- dependent type expresses that it preserves (object) types. Because of the
-- Curry-Howard identification of formulas and types this can also
-- be read as a translation from a Hilbert system for implicational logic to
-- a natural deduction system.
infixr 10 _=>_
infixl 3 _´_
-- Define types = formulas:
data Ty : Set where
N : Ty
_=>_ : Ty -> Ty -> Ty
-- Here N is an uninterpreted base type. We leave it as an exercise to extend
-- the algorithm to full system T as presented in the lectures.
-- Define "contexts" = lists of types = lists of formulas:
data Cxt : Set where
[] : Cxt
_#_ : Cxt -> Ty -> Cxt
-- The contexts represents the assignment of
-- types to variables. We will here use de Bruijn indices. The last type in the
-- context is the type of variable 0, the next last is the type of variable 1,
-- etc.
-- Define sets of variables indexed by the type and the context of the variable.
data Va : Cxt -> Ty -> Set where
z : {Γ : Cxt} -> {a : Ty} -> Va (Γ # a) a
s : {Γ : Cxt} -> {a b : Ty} -> Va Γ a -> Va (Γ # b) a
-- "z" is the de Bruijn variable 0. "s" increases the de Bruijn variable by 1.
-- Note also that by Curry-Howard this can be read as the definition of the
-- assumption rule in logic, that is, that a context contains a certain type.
-- "z" means assuming the last formula in the context.
-- "s" looks for the formula one step further into the context.
-- Define the set of combinatory terms with free variables. There are no bound variables.
data Tm : Cxt -> Ty -> Set where
K : {Γ : Cxt} -> {a b : Ty} -> Tm Γ (a => b => a)
S : {Γ : Cxt} -> {a b c : Ty} -> Tm Γ ((a => b => c) => (a => b) => a => c)
_´_ : {Γ : Cxt} -> {a b : Ty} -> Tm Γ (a => b) -> Tm Γ a -> Tm Γ b
v : {Γ : Cxt} -> {a : Ty} -> Va Γ a -> Tm Γ a
-- "V i" represents de Bruijn variable "i". As Curry discovered this can be read as a definition
-- of the inference rules of implicational logic.
-- The identity combinator I is definable in terms of S and K:
I : {Γ : Cxt} -> {a : Ty} -> Tm Γ (a => a)
I {a = a} = S ´ K ´ K {b = a}
-- Note that we need to specify the type of the second argument "b" of the second instance of K.
-- The key step of bracket abstraction is to define an analogue of lambda abstraction
-- (see further down the page). This is done by induction on the form of a combinator expression.
-- All cases are easy except the variable, and to solve this case we need to know how to do
-- weakening:
weak : {Γ : Cxt} -> {a b : Ty} -> Tm Γ a -> Tm (Γ # b) a
weak K = K
weak S = S
weak (e ´ e') = (weak e) ´ (weak e')
weak (v i) = v (s i)
-- This is an auxiliary function which weakens ("lifts") a combinator
-- term. All variables are increased by 1.
--
-- We are now ready for the main part of the algorithm.
-- The general idea is that we define an operation lam (below)
-- which performs the operation of lambda abstraction of combinator terms.
-- We first consider the case of variables:
lamvar : (Γ : Cxt) -> (a b : Ty) -> Va (Γ # a) b -> Tm Γ (a => b)
lamvar Γ .b b z = I
lamvar .(Γ # b) a b (s (z {Γ})) = K ´ v z
lamvar .(Γ # b') a b (s (s {Γ} {.b} {b'} i))
= weak {Γ} {a => b} {b'} (lamvar Γ a b (s i))
-- Having done the variables, the rest is easy,
-- applying K to the base cases K and S,
-- and using S for the case of application.
lam : {Γ : Cxt} -> {a b : Ty} -> Tm (Γ # a) b -> Tm Γ (a => b)
lam K = K ´ K
lam S = K ´ S
lam (e ´ e') = S ´ lam e ´ lam e'
lam {Γ} {a} {b} (v i) = lamvar Γ a b i
-- The proofs would be clearer if the implicit arguments were filled out (exercise!)