Archive for the ‘Observational Type Theory’ Category

Hier Soir, an OTT Hierarchy

Sunday, November 13th, 2011

I’m still waiting for my computer to typecheck this file, which I concocted yesterday evening. I’m told by someone with a better computer (thanks, Darin) that it does typecheck, and moreover, satisfy the termination checker. It relies unexcitingly on the size-change principle and is easily rendered entirely structural.

What I’ve managed to do (at last!) is to implement an Agda model of Observational Type Theory for a hierarchy of universes, in this case Nat-indexed, but that’s probably not crucial. It’s a reasonably good fit with what we envisage for Epigram 2, once stratified. However, the real thing will not suffer all of the turd-transportation I just did to simulate cumulativity (the embedding of types from one universe into the next). Ouch, that hurt! It’s not pretty, but previously I didn’t know how to do it at all.

Let me try to explain what’s going on…

Coinduction, observationally

Monday, March 22nd, 2010

I thought I might report a bit about what I’ve been up to with coinduction. Headline: we can set up propositional equality so that every coprogram equals its unfolding, even though that had jolly well better not hold definitionally if we want decidable anything.

What I’ve got is an Agda universe with inductive and coinductive Petersson-Synek trees (also known as Hancock-Setzer interaction structures). Actually, it’s a pair of universes—PROP and SET. Equality is a proposition computed recursively over the structure of sets and elements.

W-types: good news and bad news

Sunday, March 7th, 2010

I thought I’d just collect together some disparate observations about W-types, and their use in encoding other recursive datatypes. My motivation, bluntly, is to point out the inevitable unsuitability of W-types as the basis for recursive datatypes in an implementation of decidable type theories. I don’t want to downplay the conceptual importance of W-types as a uniform basis for recursive structures in an extensional setting. I’m just saying that computers aren’t clever enough to cope all that well with W-type encodings: if we want to make our understanding go, we need to refine it. This is a long post, so if you want the bad news first, skip to the end.

What are W-types?

Martin-Löf identified a general notion of well-ordering — data with a well-founded notion of ‘structurally smaller’. The power of dependent types enabled him to express this parametrically, once for all, rather than by fiddling about with syntactic criteria for acceptable recursive definitions. Here goes (informal notation)

W (S : Set) (P : S → Set) : Set
(s : S) ⊲ (f : P s → W S P) : W S P


Monday, February 8th, 2010

I’ve had an enquiry for more details on quotients in the new Epigram setup, so I’ll take that as a cue to blog a bit.

First, I’d better sketch some basics about propositions and equality. It’s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible thus far in a decidable type theory. The headlines:

  • quotients given by a ‘carrier’ set, equivalence relation
  • definitional equality on equivalence classes inherited from carrier on representatives
  • propositional equality on equivalence classes is equivalence of representatives
  • propositional equality is substitutive

The tabloid headline is STUFF YOUR SETOIDS.

OTT by reflecting telescopes

Monday, May 16th, 2005

Starting point: TT with some proper dependency, e.g.

b : Bool
T b : *

T false = Null
T true = One

we assume at least Pi, Sigma, Empty, Null, One, Bool. We also use Prop < = *,
for propositional types.

We introduce telescopes G |- D Tel , e.g.

G |- () Tel

G |- D Tel G.D |- S : *
G |- D.S Tel


G.() = G
G.(D.S) = (G.D).S

We inhabit telescopes with substitutions, given G |- D Tel