[Agda] (long post) some semantics, some syntax

Conor McBride conor at strictlypositive.org
Tue Nov 11 23:24:08 CET 2008


{-
Friends

This is a long, rambling, complicated message about
an idea I had a few months back and have only just
tried out. The text is this afternoon/evening's
lump of Agda source, and it's hard work. Agda worked
harder than I did, I'm pleased to say. To my amazement
(not to say suspicion), it just about hangs together.

I seem to have cooked up a little dependently typed
syntax, representing only well-typed terms, and with
a straightforward evaluation function. Definitional
equality is inherited from Agda. Questions which
occur to me include

  (1) Has it been done this way before?
  (2) Is it cheating?
  (3) What's the catch?
  (4) Am I right to be in a state of shock?

The trick is to cook up the semantics first, then
index the syntax by the semantics. This seems to be
less troublesome than trying to index syntax by
syntax and postponing the semantics until too late.

It's a well-scoped, well-typed syntax for a dependent
type theory. It relies heavily on generalized indexed
inductive-recursive families, but not on any dodgy
negative definitions or mutual inductive telescopes.
Set1 occurs nowhere in the development.

The whole thing comes in (chat included) at under 350
lines. That's an annoyingly large email, but also an
annoyingly small program. I can only apologize twice.
-}

module SemIx where

{- The idea is to index things by semantic objects,
    rather than syntax.
-}

{- I start by constructing the universe closed under
    Pi, Nat, and Fin.  It's the standard
    inductive-recursive presentation.
-}

{- First, I need Nat and Fin! -}

data Nat : Set where
   zero : Nat
   suc : Nat -> Nat

data Fin : Nat -> Set where
   zero : {n : Nat} -> Fin (suc n)
   suc : {n : Nat} -> Fin n -> Fin (suc n)

{- Now here's the universe, with codes U defined mutually
    with decoder El.
-}

mutual
   data U : Set where
     nat : U
     fin : Nat -> U
     pi : (s : U) -> (El s -> U) -> U

   El : U -> Set
   El nat = Nat
   El (fin n) = Fin n
   El (pi s t) = (x : El s) -> El (t x)

{- a handy abbreviation for non-dependent function spaces -}

_=>_ : U -> U -> U
S => T = pi S \_ -> T

infixr 50 _=>_

{- Next I need an inductive-recursive definition of
    the syntax and semantics of contexts. I learned
    how to do this from Randy.
-}

{- Of course, I need the kit to build the semantics:
    unit and sigma types.
-}

record One : Set where

record Sg (S : Set)(T : S -> Set) : Set where
  field
   fst : S
   snd : T fst

open module Sg' {S : Set}{T : S -> Set} = Sg {S} {T}

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Sg S T
s , t = record {fst = s; snd = t}

{- Now it's easy to represent contexts as
    left-nested records, giving us access to the
    *local* end. Of course, we need to know the
    corresponding notion of environment, in order
    to support dependency. -}

mutual
   data Ctx : Set where
     E : Ctx
     _<_ : (G : Ctx) -> (Env G -> U) -> Ctx

   Env : Ctx -> Set
   Env E = One
   Env (G < S) = Sg (Env G) \g -> El (S g)

infixl 40 _<_

{- Once we know what contexts are, we can say what
    variables are. They're typed de Bruijn indices
    into a context. But what's a type? It's not a
    syntactic type. Rather, it's a function from
    environments to codes in the universe.

    So this is a serious case of general indexing
    by higher-order stuff, in a setting which is
    very intensional. Bad form, but good fun. -}

data Va : (G : Ctx)(T : Env G -> U) -> Set where
     top : {G : Ctx}{T : Env G -> U} ->
           Va (G < T) (\gt -> T (fst gt))
     pop : {G : Ctx}{S T : Env G -> U} ->
           Va G T -> Va (G < S) (\gs -> T (fst gs))

{- What do variables mean? We can evaluate a
    variable to a projection from an environment. -}

vVa : {G : Ctx}{T : Env G -> U} -> Va G T -> (g : Env G) -> El (T g)
vVa top     gt = snd gt
vVa (pop x) gt = vVa x (fst gt)

{- Next comes a big mutual definition, featuring
    inductive definitions of types and terms, with
    a recursive definition of evaluation. -}

mutual

{- The definition of syntactic  types effectively
    gives a predicate saying which semantic types
    can be articulated. -}

   data Ty (G : Ctx) : (Env G -> U) -> Set where
     NAT : Ty G \_ -> nat
     FIN : (n : Tm G \_ -> nat) -> Ty G \g -> fin [ n / g ]
     PI  : {S : Env G -> U}{T : Env (G < S) -> U} ->
           Ty G S -> Ty (G < S) T ->
           Ty G \g -> pi (S g) \s -> T (g , s)

{- Note the way evaluation [ term / environment ]
    is used in constructing the semantics demanded
    of FIN. -}

{- Now, here come the terms. These are indexed by
    contexts and *semantic* types, then evaluated
    recursively, given an environment. -}

   data Tm (G : Ctx) : (T : Env G -> U) -> Set
    where

     -- variables are embedded
     V   : {T : Env G -> U} -> Va G T -> Tm G T

     -- lambda carries a domain and extends context
     LAM : {S : Env G -> U}{T : (g : Env G)(s : El (S g)) -> U} ->
          Ty G S ->
          Tm (G < S) (\gs -> T (fst gs) (snd gs)) ->
          Tm G (\g -> pi (S g) (T g))

     -- application connects the *semantics* of...
     _$_ : {S : Env G -> U}{T : (g : Env G)(s : El (S g)) -> U} ->
          Tm G (\g -> (pi (S g) \s -> T g s)) ->  -- ... function and
          (s : Tm G S) ->                         -- argument, then...
          Tm G \g -> T g [ s / g ] -- evaluates to give return type

     -- zero and successor for natural numbers
     ZZ : Tm G (\_ -> nat)
     SS : Tm G (\_ -> nat => nat)

     -- induction, motive type abstracted over a number
     IND : {p : Env (G < \_ -> nat) -> U} ->
           Ty (G < \_ -> nat) p ->
           Tm G (\g -> p (g , zero) =>
                       (pi nat \x -> p (g , x) => p (g , suc x)) =>
                       pi nat \x -> p (g , x))

     -- zero and successor for finite sets
     FZ : Tm G \_ -> pi nat \n -> fin (suc n)
     FS : Tm G \_ -> pi nat \n -> fin n => fin (suc n)

     -- elimination for the empty set
     MAGIC : {T : Env G -> U} -> Ty G T -> Tm G \g -> fin zero => T g

     -- elimination for non-empty sets
     FORK  : (n : Tm G \_ -> nat) ->
             {p : Env (G < \g -> fin (suc [ n / g ])) -> U} ->
             Ty (G < \g -> fin (suc [ n / g ])) p ->
             Tm G \g -> p (g , zero) =>
                        (pi (fin [ n / g ]) \x -> p (g , suc x)) =>
                        pi (fin (suc [ n / g ])) \x -> p (g , x)

{- Evaluation is just the obvious structural thing! -}

   [_/_] : {G : Ctx}{T : Env G -> U} -> Tm G T -> (g : Env G) -> El  
(T g)
   [ V x / g ] = vVa x g
   [ LAM S t / g ] = \s -> [ t / g , s ]
   [ f $ s / g ] = [ f / g ] [ s / g ]
   [ ZZ / g ] = zero
   [ SS / g ] = suc
   [ IND {p} _ / g ] = ind (\x -> El (p (g , x))) where
     ind : (P : Nat -> Set) -> P zero ->
           ((x : Nat) -> P x -> P (suc x)) -> (x : Nat) -> P x
     ind P z s zero = z
     ind P z s (suc x) = s x (ind P z s x)
   [ FZ / g ] = \n -> zero
   [ FS / g ] = \n -> suc
   [ MAGIC {t} _ / g ] = magic where
     magic : Fin zero -> El (t g)
     magic ()
   [ FORK n {p} _ / g ] = fork (\x -> El (p (g , x))) where
     fork : (P : Fin (suc [ n / g ]) -> Set) ->
            P zero -> ((x : Fin [ n / g ]) -> P (suc x)) ->
            (x : Fin (suc [ n / g ])) -> P x
     fork P z s zero = z
     fork P z s (suc x) = s x

infixl 90 _$_

{-

I don't know about you, but I'm exhausted!

In the past, we've thought about defining

   Ctx : Set
   Ty : Ctx -> Set
   Tm : (G : Ctx) -> Ty G -> Set

in some strange but probably meaningful inductive way.
The trouble has always been that the types are syntactic
objects, so we have to consider definitional equality
derivations rather explicitly when saying what Tm is.

But what has happened here? I've identified a universe
of the types I want to work with and used its codes to
name the semantic objects corresponding to types in my
language. Instead of modelling the computational
equality on types and terms, I just inherit the
computational equality for their semantics
in the metalanguage. Surely this is some kind of
wickedness!

The nice thing is that I've escaped from the tight
spiral of dependency. I finished setting up the
semantics before I went anywhere near the syntax!
Then, somehow, the syntax works out just so, taking
type as an index (it's a "prior notion") and value
as a decoder (it comes afterwards).

I wonder what happens next.

Thanks, if you've made it this far!

All the best

Conor

-}

{- OK, let's play! -}

[_] : {T : One -> U} -> Tm E T -> El (T _)
[ t ] = [ t / _ ]

{- I built these interactively, and with the benefit
    of too much familiarity with their encodings. -}

{- addition -}

ADD : {G : Ctx} -> Tm G \g -> (nat => (nat => nat))
ADD = LAM NAT (LAM NAT (IND NAT $ V top $ LAM NAT SS $ V (pop top)))

TWO : {G : Ctx} -> Tm G \g -> nat
TWO = SS $ (SS $ ZZ)

{- try [ ADD $ TWO $ TWO ] -}

{- Now some functions on finite sets. Here's the
    weakening functor. It takes a function f on
    finite sets and returns the function on sets one
    bigger which maps zero to zero and (suc x) to
    suc (f x). -}

WEAK : {G : Ctx} -> Tm G \g ->
        pi nat \m -> pi nat \n ->
        (fin m => fin n) => fin (suc m) => fin (suc n)
WEAK = LAM NAT (LAM NAT (LAM (PI (FIN (V (pop top))) (FIN (V (pop  
top))))
         (FORK (V (pop (pop top))) (FIN (SS $ V (pop (pop top))))
          $ (FZ $ V (pop top) )
          $ LAM (FIN (V (pop (pop top))))
             (FS $ V (pop (pop top)) $ (V (pop top) $ V top) )  ) ))

{- try [ WEAK $ (SS $ ZZ) $ (SS $ (SS $ ZZ)) $ (FS $ (SS $ ZZ))
               $ (FZ $ (SS $ ZZ)) ] -}
{- try [ WEAK $ (SS $ ZZ) $ (SS $ (SS $ ZZ)) $ (FS $ (SS $ ZZ))
               $ (FS $ (SS $ ZZ) $ (FZ $ ZZ)) ] -}

{- What's left in the buffer does typecheck, but it overflows
    when I try to run it! -}

{-
THIN : {G : Ctx} -> Tm G \g ->
        pi nat \n -> fin (suc n) => fin n => fin (suc n)
THIN = IND (PI (FIN (SS $ V top))
              (PI (FIN (V (pop top))) (FIN (SS $ V (pop (pop top))))))
        $ LAM (FIN (SS $ ZZ)) (FS $ ZZ)
        $ LAM NAT (LAM (PI (FIN (SS $ V top))
              (PI (FIN (V (pop top))) (FIN (SS $ V (pop (pop top))))) )
          (FORK (SS $ V (pop top))
          (PI (FIN (SS $ V (pop (pop top) )) )
           (FIN (SS $ (SS $ V (pop (pop (pop top)) ))) ))
          $ (FS $ (SS $ V (pop top )) )
          $ LAM (FIN (SS $ V (pop top)))
           (WEAK $ V (pop (pop top)) $ (SS $ V (pop (pop top)))
             $ (V (pop top) $ V top))  ) )

TEST : {G : Ctx} -> Tm G \g -> fin (suc (suc (suc (suc zero))))
TEST = THIN $ (SS $ (SS $ (SS $ ZZ)))
             $ (FS $ (SS $ (SS $ (SS $ ZZ)))
                   $ (FS $ (SS $ (SS $ ZZ))
                         $ (FZ $ (SS $ ZZ))))
             $ (FS $ (SS $ (SS $ ZZ)) $ (FS $ (SS $ ZZ) $ (FZ $ ZZ)))
-}



More information about the Agda mailing list