The notion of equality gives rise to one of the slipperier tar-pits in which type theorists can get stuck, but it is central to dependently typed programming, as presented in Epigram (McBride & McKinna, 2004). I shall attempt to explain the issues involved, before introducing work in progress with Thorsten Altenkirch on a type theory with yet another variation of equality: Observational Type Theory. OTT attempts to combine the virtues of intensional type theory (decidable typechecking, closed expressions compute canonical values) with those of extensional type theory (propositional equality reflects behaviour, rather than construction). OTT owes its ancestry to Martin Hofmann's doctoral research. More directly, it amounts to syntactic presentation of Thorsten's model construction (from his LICS 1999 paper), simplified by adopting my heterogeneous (John Major) approach to equality. With care, we think we can arrange things to support all the reasoning power of the extensional theory and all the computational power of the intensional theory.

OTT is the basis for the type theory underpinning Epigram 2, the new version of our dependently typed functional programming language, currently under development in Nottingham and St Andrews. I shall indicate the potential benefits of going OTT.