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

[Dan Licata]

Hi Conor,

On Nov11, Conor McBride wrote:
> 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. 

Very cool!

> Questions which occur to me include
> 
>  (1) Has it been done this way before?

This seems related to some Agda code that I'll be talking about at PLPV
in January (linked from here: http://www.cs.cmu.edu/~drl/pubs.html),
which starts to investigate how to account for dependency in the context
of Zeilberger's higher-order focusing.

It turns out that there's a simple way to account for a restricted form
of dependency: dependency only on positive data, but not negative
computation.  This is enough for simple data-indexed things
(vectors...), and combining it with some other work we've done would
allow dependency on LF-style data with binding.  It might also be
economical and feasible to add these positively dependent types to
Haskell---GHC already implements much of the necessary infrastructure.

The language is constructed by defining the syntax of types
simultaneously (via induction-recursion) with the Agda Sets classifying
the patterns for positive types.  The patterns for purely positive types
(those with no negative subformulas) are basically the corresponding
Agda types---e.g., the patterns for nat are the natural numbers.  Then,
through the magic of infinitary syntax, you get to reuse Agda's
dependent pattern matching to do dependent pattern matching in the
object language.  And the bodies of Pi and Sigma are defined by
pattern-matching, so you can do type-level computation as well.  You get
a notion of definitional equality for free from Agda, because
"substituting" into the body of a Pi type is just applying an Agda
function to an argument.

That said, Conor's construction is fancier than mine in one important
way, because it allows dependency on negative computation (functions).
Positively dependent types cut the dependency cycle in an easier way,
because patterns and syntactic types (indexed by "semantic" data) are
defined prior to terms, so indexing Tm by syntactic types is not weirdly
cyclic.  I want to try a fully dependent version of higher-order
focusing using Conor's technique, but I haven't yet.

>  (2) Is it cheating?
>  (3) What's the catch?
> 
> I wonder what happens next.

Me too! This seems great for doing a meta-circular encoding.  But what
if the object language isn't a subset of Agda?

1) What happens if you want the object language to have a coarser notion
of definitional equality than Agda definitional equality for the
corresponding semantic type (e.g., a type indexed by functions, with an
eta rule for them)?

2) What happens if you want effects?  E.g., unencapsulated general
recursion a la Cayenne, or monadically encapsulated state as in Hoare
Type Theory.  HTT has simple but conservative syntactic rules for
definitional equality for the monad; it seems like implementing one of
their models would be harder, and anyway you'd presumably still need an
explicit equality judgement, so this ties back into question 1.

3) Aside from tradition, why bother having the syntactic types at all?
They don't seem to do anything other than rule out some semantic types
(e.g., you don't have large elims in the syntactic types, but you do in
the semantic types).  

-Dan