UTLC.idr

module UTLC

-- This is a terrible implementation of the Untyped Lambda Calculus,
-- using the semantics from Fig 5-3 in TAPL, amended using the changes
-- proposed in Chapter 6 of TAPL, associated with the deBruijn
-- indices.

-- This gives us the `Fin n` datatype, which is the numbers from 0 up
-- to (but not including) n. So, `Fin 0` has no inhabitants; `Fin 1`
-- has one inhabitant, namely 0; and `Fin 2` has two inhabitants,
-- namely 0 and 1; and so on and so forth.
import Data.Fin

%default total


-- Terms are indexed by the number of free variables
data Term : (n : Nat) -> Type where

  -- Variables : A natural number less than n
  Var : (k : Fin n) -> Term n

  -- Lambdas : They bind one of the variables of the inner term
  Abs : (t1 : Term (S n)) -> Term n

  -- Application
  App : (t1, t2 : Term n) -> Term n

%name Term t1,t2,t3,t4,t5

-- Values are lambdas without any free variables
data Value : Term 0 -> Type where
  VAbs : Value (Abs t1)

instance Uninhabited (Value (App t1 t2)) where
  uninhabited VAbs impossible
instance Uninhabited (Value (Var k)) where
  uninhabited VAbs impossible


-- This function does all of substitution!
sub : (a : Nat) -> Term 0 -> Term (a `plus` S b) -> Term (a `plus` b)


-- Single-step Evaluation
data Eval1 : Term 0 -> Term 0 -> Type where
  EAppAbs : {auto vprf : Value t2}
            -> Eval1 (App (Abs t12) t2) (sub 0 t2 t12)

  EApp1 :   Eval1 t1 t1'
            -> Eval1 (App t1 t2) (App t1' t2)

  EApp2 :   {auto vprf : Value t1}
            -> Eval1 t2 t2'
            -> Eval1 (App t1 t2) (App t1 t2')

instance Uninhabited (Eval1 (Abs t1) t') where
  uninhabited EAppAbs   impossible
  uninhabited (EApp1 e) impossible
  uninhabited (EApp2 e) impossible

instance Uninhabited (Eval1 (Var k) t') where
  uninhabited EAppAbs   impossible
  uninhabited (EApp1 e) impossible
  uninhabited (EApp2 e) impossible

-- Strong Progress: This is a proof that either you have a value, or you have an
-- evaluation rule you can use.
total
val_or_eval1 : (t : Term 0) -> Either (Value t) (Exists (\t' => Eval1 t t'))
val_or_eval1 (Var k)  = absurd k
val_or_eval1 (Abs t1) = Left VAbs
val_or_eval1 (App t1 t2) with (val_or_eval1 t1, val_or_eval1 t2)
  val_or_eval1 (App t1 t2) | (Left vprf1, Left _)
               = case t1 of (Abs t12) => Right (Evidence (sub 0 t2 t12) EAppAbs)
                            (Var _)   => absurd vprf1
                            (App _ _) => absurd vprf1
  val_or_eval1 (App t1 t2) | (Left vprf, Right (Evidence t2' estp2))
               = Right (Evidence (App t1 t2') (EApp2 estp2))
  val_or_eval1 (App t1 t2) | (Right (Evidence t1' estp1), _)
               = Right (Evidence (App t1' t2) (EApp1 estp1))


namespace ExistsExtras
  instance ({x : a} -> Uninhabited (p x)) => Uninhabited (Exists p) where
    uninhabited (Evidence x prf) = uninhabited prf

-- A Normal Form is something that evaluates to itself
--
-- For the moment this is single-step evaluation, there's nothing that
-- stops this being multi-step evaluation except that I don't think I
-- need it with these evaluation rules.
data NF1 : Term 0 -> Type where
  NoEval1 : Not (Exists (\t' => Eval1 t t'))
            -> NF1 t

instance Uninhabited (NF1 (Var k)) where
  uninhabited (NoEval1 f) {k} = absurd k

total
value_is_nf : (t : Term 0) -> Value t -> NF1 t
value_is_nf (Var k)  vprf    = absurd vprf
value_is_nf (Abs t1) vprf    = NoEval1 absurd
value_is_nf (App t1 t2) vprf = absurd vprf

-- Multi-step evaluation
--
-- These are defined in terms of Nil and (::) (Cons), because the
-- intuition is that they're a list of single-step evaluation
-- steps. Using Nil and Cons allows us to use (overloaded) List
-- Syntax.
data Eval : Term 0 -> Term 0 -> Type where
  -- Either a term evaluates to itself
  Nil : Eval t t

  -- Or It makes a single step closer to a normal form
  (::) : Eval1 t1 t2
          -> Eval t2 t3
          -> Eval t1 t3

namespace EvalPrfs
  eval1_in_eval : Eval1 t t' -> Eval t t'
  eval1_in_eval eprf = [eprf]


  (++) : Eval t t' -> Eval t' t'' -> Eval t t''
  (++) Nil e            = e
  (++) (step :: e1) e2  = step :: e1 ++ e2


data NFOf : Term 0 -> Term 0 -> Type where
  IsNFOf : Eval t t' -> NF1 t' -> NFOf t t'

value_is_nf_of_self : (t : Term 0) -> Value t -> NFOf t t
value_is_nf_of_self t vprf = IsNFOf [] (value_is_nf t vprf)


namespace Examples

  namespace ID
    -- \x.x
    ut_id : Term 0
    ut_id = Abs (Var 0)

    ut_id_v : Value ut_id
    ut_id_v = VAbs

    ut_id_norm : val_or_eval1 ut_id = Left (ut_id_v)
    ut_id_norm = Refl

    -- (\x.x)(\x.x)
    ut_id_id : Term 0
    ut_id_id = App ut_id ut_id

    ut_id_id_v : Not (Value ut_id_id)
    ut_id_id_v = absurd

    ut_id_id_e_id : Eval1 ut_id_id ut_id
    ut_id_id_e_id = ?prf1 -- EAppAbs

    ut_id_id_norm : val_or_eval1 ut_id_id = Right (Evidence ut_id EAppAbs)
    ut_id_id_norm = ?prf2 -- Refl

  namespace Omega
    -- \x.xx
    ut_omega : Term 0
    ut_omega = Abs (App (Var 0) (Var 0))

    ut_omega_v : Value ut_omega
    ut_omega_v = VAbs

    ut_omega_norm : val_or_eval1 ut_omega = Left (ut_omega_v)
    ut_omega_norm = Refl

    -- (\x.xx)(\x.xx)
    ut_omega_omega : Term 0
    ut_omega_omega = App ut_omega ut_omega

    ut_omega_omega_v : Not (Value ut_omega_omega)
    ut_omega_omega_v = absurd

    ut_omega_omega_e_omega_omega : Eval1 ut_omega_omega ut_omega_omega
    ut_omega_omega_e_omega_omega = ?prf3 -- EAppAbs

    ut_omega_omega_norm : val_or_eval1 ut_omega_omega = Right (Evidence ut_omega_omega EAppAbs)
    ut_omega_omega_norm = ?prf4 -- Refl