Hier Soir, an OTT Hierarchy

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…
Read the rest of this entry »

Problem Types, Dub Types, Type Schemes

November 4th, 2011

Design: Lay(ab)out

August 3rd, 2011

Lexical Structure

August 3rd, 2011

Design: Framing Source Code

August 1st, 2011

Elaborating on the State of the Proof State

July 26th, 2011

Algorithmic Bidirectional Typing and Equality

June 29th, 2011

Algorithmic Rule Systems

June 29th, 2011

Crude but Effective Stratification

June 17th, 2011

Tag, tag, tag

February 16th, 2011

An Environmental Typechecker

December 20th, 2010

I am not a number, I am a classy hack

December 16th, 2010

Lower Taxation Representation?

December 13th, 2010

Insertion Sort

September 10th, 2010

The Art of the Possible

August 20th, 2010

No Representation without Taxation

May 31st, 2010

The Battered Ornaments

May 24th, 2010

EPIG, a journey in Quotation

May 10th, 2010

A bit of infrastructure

April 24th, 2010

Prop?

April 18th, 2010