Lambda the Ultimate

I've been thinking (and reading) about dependent types and related topics (Calculus of constructions, ML type theory, and so on).

First, I'd like to say how really clear and useful I found the second chapter of ATTAPL ("Dependent Types" by Aspinall and Hofmann). Their presentation of the CoC really clarified things for me. The extra overhead of the Prf type constructor and the distinction it draws between Π-types and ∀ terms was pretty instructive to me (I'd previously seen the CoC with only λ and ∀, as it's presented here). Obviously I've hardly gotten my feet wet, but as an introduction, I highly recommend this article.

But I'm left with a question that I hope someone here can answer. I'm confused by the standard terminology for Π- and Σ-types, "dependent products" and "dependent sums," respectively. For the life of me I can't fathom what these types have to do with anything I've normally thought of as a product or a sum. The product seems to be a function type, and the sum seems (against all common sense) to be a product! And in fact, to make matters even worse, what I generally think of as a "sum" (logical disjunction or variant types) seems to be most easily defined in terms of dependent product.

I guess I'm not alone in finding this confusing. This post on the types list is relevant, but doesn't really help me understand the logic (no pun intended) behind the standard terminology, and the observation that "the dependent product type was in fact a sum type" really highlights my lack of insight.

If we were used to classical logic we would be a bit surprised here: classically, the “existential quantifier” is thought of as a generalisation of “disjunction”.

This might also be relevant (from here), but honestly I'm not even sure anymore! I really hope someone can clarify this for me, even if only from a historical perspective...

[Ehud, I'm not really sure if this kind of thing is appropriate for the front page... Any guidance?]

This page has a few interesting looking papers. I stumbled here because of the paper titled "A universal characterization of the closed Euclidean interval" (PDF)*. It contains a simple categorical definition of a notion of closed
interval that has computational content.

[edit]
I want to point out the paper "Synthetic topology for data types and classical spaces" (PDF) on the above page. It describes itself roughly as "topology for computer scientists and computer science for topologists".

* The google search term I was using was actually "essential geometric morphism" which I was looking up with regards to topos theory and synthetic differential geometry.

I like STL’s containers. However, no matter how hard I try, I can’t enjoy using STL’s algorithms (by which I don’t mean sort, but for_each, transform, etc.) They require excess baggage, forcing me to invent weird structs to act like functors or to declare redundant variables (with very verbose types) to collect the results, etc. I desire the Haskell version that I see in my head, but the C++ version that pours from my fingers into the buffer looks ugly and rigid.

Disappointed, I end up converting them into explicit loops because they somehow look cleaner. I wondered if this ever happened to somebody else, and I found this thread started by Scott Meyers in comp.lang.c++.moderated. It’s a gigantic thread, but from some of the (both pro & con) arguments I’ve read, I realized that it is just not fair to discuss these concepts in a C++ setting just like it’s not fair to discuss static typing in a C++ setting.

So, I wonder if (non-FP) people’s experience with STL is bad PR for FP…

LtU readers know I tend to stress the importance of language communities and their impact on language success as well as language evolution. Thus, I feel I am allowed to point you to this sociology paper.

Aside from the humour, you might want to reflect on the applicability of the ideas presented in the paper to the notion of language expressiveness (think of the community of language constructs), and to the interaction between programmers and language constructs.

Beware: If you are new to this sort of thing, sections five and six are likely to infuriate you (or simply to sound incredibly stupid)...

GADTs are obviously currently a hot topic in functional programming research. Most of the papers focus only on the GADT mechanism (how type checking works etc.). The only example that one usually sees is the "typed evaluator".

I am not an expert on this topic, and I'd like to know more about how they would actually be useful in practical programming.

For example, I wonder how a parser would look like if it is impossible to construct "wrong" ASTs. Would type checking then effectively take place during parsing? How would a type error in the parsed program be detected and thrown?

What other interesting applications exist? In general, how do GADTs change the programming model?

I have a (somewhat) hypothetical question: would you be willing to move into the middle of nowhere, Arkansas, and get paid a little over 30k/yr to get a job programming in O'Caml? What about Erlang?

I’m currently working on open source project that has 
a goal to create a language definition framework
that can be used as textual DSL construction kit. 
The framework is currently named Extensible Term 
Language (ETL). This language definition framework 
is very similar by architecture to XML. The framework 
has just reached its first public version.

* There is language definition language that is defined using
  framework itself (this aspect is more like XML Schema or
  Relax NG rather than DTD). This is a basic dog-food test for
  such framework.

* It works with plain text.
   - Non ETL-aware editors can work with languages defined using
     ETL
   - There is no special hidden markup.
   - It is possible to have and edit incorrect text. Even if
     syntax changes (for example some keyword is renamed).
     It is possible to fix source using normal text manipulation
     tools.

* It allows for agile definition of underlying model, language,
  and instance sources.

* The syntax has underlying document object model.

* There may be a lot of different implementation of parsers and many
  models of parser like AST, DOM, push, or pull parsers.

* The language definition framework specifies syntax and mapping to
  model rather than semantics of the language. It is possible to
  build semantic aware tools, but they should live above the language
  like it is now with XML.

* There are no build-in transformation facilities, but it is possible
  to define facilities using means above the framework. Such facilities
  might work on AST level or on more detailed levels (for example there
  is a tool that transforms source file to html basing on grammar
  definition).

* The language defines common lexical layer and common phrase level.

* Like XML it allows creating reusable language modules. These
  language modules can be exchanged between tools. There are few
  samples of such reuse in the package.

However there are also differences from XML:

* ETL syntax is believed (by me) to be much more usable than XML.
  It is possible to define traditionally looking programming
  languages using it. See samples in the referenced package (for
  example there is a grammar for Java-like language named EJ).

* One must have a grammar to derive underlying object model from
  source code. However such grammar may be created independently
  (in that case object model will be different from original
  intention of author). In XML the grammar is used mostly for
  validation and specifying syntax of text values, and object
  model is self-evident from source.

The project is still in pre-alpha stage. There is a working grammar
definition language and few extensions are planned for it.

There is a ready-to-use parser that can be used in situations when
grammar is static, like command line tools (extensions to parser
to make it more suitable to dynamic environment like Eclipse are
already planned and it is more or less known what to do). The parser
is of pull kind. And it is possible to build AST or DOM parsers
above it. For example there are ready-to-use AST parsers that
build tree of JavaBeans and AST models that have been generated
using Eclipse Modeling Framework. The parser itself uses EMF AST
during compilation of grammar to executable form.

The current version could be downloaded from http://sourceforge.net/project/showfiles.php?group_id=153075&package_id=178546&release_id=391153

Please look at the file doc/readme.html for more details about
the package. The file gives references and some explanations
for examples. There is also a document that describes motivation
for the language.

The work of Peyton Jones and Eber on specifying financial contracts with combinators (How to write a financial contract) has often cropped up here, but hasn't, I think, ever had its own story.

Since Yale has a vistor, Christian Stefenson, presenting a talk on Enterprise Resource Planning ( A Declarative Framework for Enterprise Systems), which based on the work of Peyton Jones & Eber, I thought it might be timely to raise this very interesting idea.

Some links

• DSL for financial contracts
• Paul Snively's comments about virtual world money'

It has been discussed recently somewhat in The new old..
and Revisiting AWK, but I am finding more and more treatments of Unix shell scripting (actually, not quite "shell scripting", but the combination of all of the Unix mini-languages) as a means to perform complex tasks usually reserved for real monolithic programming languages.

Here is an interesting (intro level) computational linguistics paper (original postscript) (verbatim pdf) about counting trigrams on a decent size corpus using just standard Unix utilities.

Type Refinements for Programming Languages is the web page for a graduate course at CMU. It is full to the brim of great papers about PL theory, including some things we talk about here, like Soft Type Systems, Dependent Types, and Polymorphic Type Inference.