AGT meet Agda

GradualSTLC.agda

module GradualSTLC where

open import Agda.Primitive
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Maybe

-- the types that we want to represent

data U : Set where
  nat : U
  π : (A B : U) → U -- A → B
  ✠U : U           -- error type
  ?U : U           -- dynamic type

variable
  A A' B B' : U

-- order on the types
-- in some sense we are completing the basic algebra of simple types
-- on nat, _→_ to a poset with smallest (✠U) and greatest (?U) elements

data _≤U_ : Rel U lzero where
  nat≤nat : nat ≤U nat
  nat≤? : nat ≤U ?U
  π≤π : A ≤U A' → B ≤U B' → π A B ≤U π A' B'
  π≤? : A ≤U ?U → B ≤U ?U → -- π A B ≤ π ?U ?U
       π A B ≤U ?U
  ✠≤ : ✠U ≤U A
  ?≤? : ?U ≤U ?U


-- An evidence of being of type A is a pair of a type B and a proof that
-- B refines A
evd : U → Set
evd A = Σ[ B ∈ U ] B ≤U A

-- Since the final language supports the full λ-calculus
-- there is no hope to have a terminating interpretation as-is
-- TODO: investigate what happens when using an indexed datatype
-- (universe levels will probably blow out...)
{-# TERMINATING #-}
El : U → Set
El₀ : U → Set

-- The interpretation of a type is given by any element of a smaller type
-- reminds of an ideal completion
El A = Σ[ e ∈ evd A ] El₀ (e .fst)

El₀ nat = ℕ
El₀ (π A B) = El A → El B
El₀ ✠U = ⊤
El₀ ?U = ⊥


-- properties and operations on ≤U
≤U-refl : Reflexive _≤U_
≤U-refl {x = nat} = nat≤nat
≤U-refl {x = π A B} = π≤π (≤U-refl {x = A}) (≤U-refl {x = B})
≤U-refl {x = ✠U} = ✠≤
≤U-refl {x = ?U} = ?≤?

trans : Transitive _≤U_
trans nat≤nat BC = BC
trans AB@nat≤? ?≤? = AB
trans (π≤π Axy Bxy) (π≤π Ayz Byz) = π≤π (trans Axy Ayz) (trans Bxy Byz)
trans (π≤π Axy Bxy) (π≤? Ayz Byz) = π≤? (trans Axy Ayz) (trans Bxy Byz)
trans AB@(π≤? _ _) ?≤? = AB
trans ✠≤ BC = ✠≤
trans AB@?≤? ?≤? = AB


?U-max : (A : U) → A ≤U ?U
?U-max nat = nat≤?
?U-max (π A B) = π≤? (?U-max A) (?U-max B)
?U-max ✠U = ✠≤
?U-max ?U = ?≤?

substract : {A B C : U} (AC : A ≤U C) (BC : B ≤U C) → Maybe (A ≤U B)
substract nat≤nat nat≤nat = just nat≤nat
substract nat≤nat ✠≤ = nothing
substract nat≤? nat≤? = just nat≤nat
substract nat≤? (π≤? BC BC₁) = nothing
substract nat≤? ✠≤ = nothing
substract nat≤? ?≤? = just nat≤?
substract (π≤π Axz Bxz) (π≤π Ayz Byz) with substract Axz Ayz with substract Bxz Byz
... | just Axy | just Bxy = just (π≤π Axy Bxy)
... | _ | _ = nothing
substract (π≤π Axz Bxz) ✠≤ = nothing
substract (π≤? Axz Bxz) nat≤? = nothing
substract (π≤? Axz Bxz) (π≤? Ayz Byz)with substract Axz Ayz with substract Bxz Byz
... | just Axy | just Bxy = just (π≤π Axy Bxy)
... | _ | _ = nothing
substract (π≤? Axz Bxz) ✠≤ = nothing
substract AB@(π≤? Axz Bxz) ?≤? = just AB
substract ✠≤ BC = just ✠≤
substract ?≤? ?≤? = just ?≤?
substract ?≤? _ = nothing



-- exceptions, upcast, downcast...

raise : {A : U} → El A
raise = (✠U , ✠≤), tt

upcast : A ≤U B → El A → El B
upcast AB ((X , hXA) , x) = ((X , trans hXA AB) , x)

downcast : A ≤U B → El B → El A
downcast AB ((X , XB), x) with substract XB AB
... | just XA = ((X , XA), x)
... | nothing = raise

evd-refl : (A : U) → evd A
evd-refl A = A , ≤U-refl


π??≤? : π ?U ?U ≤U ?U
π??≤? = π≤? ?≤? ?≤?

embedπ : (El ?U → El ?U) → El ?U
embedπ f = (π ?U ?U , π??≤?), f


-- Reconstructing some rules of the gradual simply typed lambda calculus
-- following AGT (fig. 5)

mk-nat : (n : ℕ) → El nat
mk-nat n = (nat , nat≤nat) , n

mk-add : El A → A ≤U nat → El B → B ≤U nat → El nat
mk-add n Anat m Bnat with upcast Anat n with upcast Bnat m
... | ((nat , _), n') | ((nat , _), m') = (nat , nat≤nat), n' + m'
... | _ | _ = raise

mk-lam : (El A → El B) → El (π A B)
mk-lam {A} {B} f = evd-refl (π A B), f

mk-app : {T X : U} → El T → T ≤U π A B → El X → X ≤U A → El B
mk-app t Tπ x XA with upcast Tπ t with upcast XA x
... | ((π A₀ B₀ , π≤π AA BB), f) | a = upcast BB (f (downcast AA a))
... | _ | _ = raise

_on_ : El (π A B) → El A → El B
f on a = mk-app f ≤U-refl a ≤U-refl

mk-case : El A → El (π nat A) → El (π nat A)
mk-case a0 asuc = mk-lam (λ {
  ((nat , _), 0) → a0 ;
  ((nat , _), suc n) → asuc on (mk-nat n) ;
  _ → raise})

-- Embedding of Ω
δ : El (π (π ?U ?U) ?U)
δ = mk-lam (λ x → mk-app x ≤U-refl x π??≤?)

Ω : El ?U
Ω = mk-app δ ≤U-refl δ (π≤π π??≤? ?≤?)


module _ (A : U) (f : El (π A A)) where
  private
    π?A≤? : π ?U A ≤U ?U
    π?A≤? = π≤? ?≤? (?U-max A)

  δf : El (π (π ?U A) A)
  δf = mk-lam (λ x → f on (mk-app x ≤U-refl x π?A≤?))

  fix : El A
  fix = mk-app δf ≤U-refl δf (π≤π π?A≤? ≤U-refl)

-- Awkward definition of multiplication by 2 to test the fixpoint
-- and check that it does not fail

ftwice : El (π (π nat nat) (π nat nat))
ftwice = mk-lam (λ ftwice →
  mk-case (mk-nat 0)
          (mk-lam (λ n → mk-add (mk-nat 2) ≤U-refl (ftwice on n) ≤U-refl)))

twice : El (π nat nat)
twice = fix (π nat nat) ftwice

open import Agda.Builtin.Equality

test-twice0 : twice on (mk-nat 0) ≡ mk-nat 0
test-twice0 = refl

test-twice1 : twice on (mk-nat 1) ≡ mk-nat 2
test-twice1 = refl

test-twice42 : twice on (mk-nat 42) ≡ mk-nat 84
test-twice42 = refl