[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