Type Theory

The Church Project

http://types.bu.edu or http://www.church-project.org

The Church Project investigates the foundations, design principles and implementation techniques of programming languages and related systems. The overall goal is the development of software technology that performs better and is more reliable. The project is named in honor of Alonzo Church, the inventor of the lambda calculus.

Four major research efforts (supported by various funding bodies including EC, EPSRC, and NSF) are presently undertaken by project participants:

  • Compiling with Flow Types
  • Compositional Analysis
  • Programming with Dependent Types (DML) (Xanadu)
  • Linear Naming and Computation

We previously linked to a document on this site, but not the site itself.

A Type System Equivalent to Flow Analysis

A Type System Equivalent to Flow Analysis
Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis. In this paper we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.

I believe it's instructive to see type systems in this light. Did we discuss something like this recently?

Poly* type inference tool

Poly* is a novel retargetable meta type system for various process and mobility calculi. Poly* is a direct descendant of PolyA, a type system for Mobile Ambients by Amtoft, Makholm, and Wells. Meta* is a generic process calculus that can be instantiated to specific process calculi like the Pi-calculus and Mobile Ambients by supplying reduction rules.

A web interface is available for experimentation after you can read the technical report and ESOP 2005 paper.

The list of common questions and answers about Poly* may be a good place to start if you are merely curious.

Python "Monkey Typing"

I guess the record wouldn't be complete without mentioning this proposal,

This PEP proposes an extension to "duck typing" called "monkey typing", that preserves most of the benefits of duck typing, while adding new features to enhance inter-library and inter-framework compatibility. The name comes from the saying, "Monkey see, monkey do", because monkey typing works by stating how one object type may mimic specific behaviors of another object type.

More here and here (from Guido).

Guido: Adding Optional Static Typing to Python -- Part II

Part II (see Part I discussion on LtU).

Among the notions discussed: Interfaces and Design By Contract, Parameterized Types and Types vs. Classes.

Adding Optional Static Typing to Python

Link: Guido van Rossum broaches the subject of type tagging for Python.

Optional static typing has long been requested as a Python feature. It's been studied in depth before (e.g. on the type-sig) but has proven too hard for even a PEP to appear. In this post I'm putting together my latest thoughts on some issues, without necessarily hoping to solve all problems.

Static vs. dynamic is a never-ending thread in most PL discussions these days. But designing a type system is a *hard* task, one which I'm not sure doesn't require from a ground on up approach. But it would be nice if you could choose to work your way into, though most of the Smalltalk crowd will inform us that Strongtalk never did quite catch on.


(accompanying discussion forum)

Combining lazy and eager evaluation of terms

In an attempt to combine some of the benefits of lazy and eager evaluation, I have implemented a language with an evaluation strategy which is strict with respect to divergence, but performs lazy evaluation on certain intermediate subterms to allow a more expressive use of recursion.

Does anybody have any references to work on similar evaluation schemes?

Tim Sweeney started this interesting Types-list thread. A summary of the responses he receieved is here.

Higher-order module system of ML is actually possible in Haskell

A nice post from Oleg on the Haskell mailing list shows how to implement high order modules, and more specifically translucent applicative functors in idiomatic Haskell.

Thus different instantiations of the functor with respect to type-compatible arguments are type-compatible; and yet the functor hides the representation details behind the unbreakable abstraction barrier.

The work is inspired by (our own) Ken Shan's work that can be found here.

Oleg concludes,

The example illustrates that Haskell already has a higher-order module language integrated with the core language and with the module checking being a part of the regular typechecking.

Eliminating Array Bound Checking through Non-dependent types

Oleg posted this pertinent message on the Haskell mailing list. It's always nice to see cool examples such as this.

Having saiod that, I must also say that I agree with Conor McBride who wrote that anyone who would argue (and I'm not saying you do) that work to try to make more advanced type systems and stronger static guarantees more convenient and well-supported is not necessary because it happens to be possible to bang out this or that example in Haskell as it stands if you think about it hard enough, is adopting the position of the ostrich.

Making type systems more expressive is a worthy goal. You want them to remain decidable (i.e., static), of course. Can we at least agree on that? ;-)

TyPiCal: Type-based static analyzer for the Pi-Calculus

TyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, and information flow analysis.

Type system is an ordinary type system extended so that channel types carry precise information about how each channel is used. This allows a type inferencer to obtain information about the behavior of a process.

XML feed