Type Theory

Omega

Ωmega is a new programming language by Tim Sheard which is descended from Haskell and adds new facilities for defining static type constraints, such as allowing "users to write functions at the level of types, and then use those functions in the type of functions at value level". It also has "equality qualified types". See also Programming with Static Invariants in Omega and the manual for more information. Mentioned previously (in passing) on LtU.

Barbara Partee: Reflections of a Formal Semanticist as of Feb 2005

What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself.

This essay is a longer version of the introductory essay in (Partee 2004). The introductory essay was first written in this long form in February 2003, but had to be cut down to about half the size to fit in the book...

This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25...

No surprise, really, if you follow the links we give here from time to time about TLGs and such.

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.

XML feed