Lambda the Ultimate

Another cool demonstration from Oleg:

I'd like to point out a different take on Djinn:

http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/type-inference.scm

http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/logic.scm

The first defines the Hindley-Milner typechecking relation for a
language with polymorphic let, sums and products. We use the Scheme
notation for the source language (as explained at the beginning of the
first file); ML or Haskell-like notations are straightforward. The
notation for type terms is infix, with the right-associative arrow.

The typechecking relation relates a term and its type: given a term we
obtain its type. The relation is pure and so it can work in reverse: given a type, we can obtain terms that have this type. Or, we can give a term with blanks and a type with blanks, and ask the relation to fill in the blanks.

As an example, the end of the file type-inference.scm shows the derivation for the terms call/cc, shift and reset from their types in the continuation monad. Given the type

(((a -> . ,(cont 'b 'r)) -> . ,(cont 'b 'b)) -> . ,(cont 'a 'b))

we get the expression for shift:

   (lambda (_.0) (lambda (_.1)
	((_.0 (lambda (_.2) (lambda (_.3) (_.3 (_.1 _.2)))))
	 (lambda (_.4) _.4))))

It took only 2 milli-seconds.

More interesting is using the typechecker for proving theorems in
intuitionistic logic: see logic.scm. We formulate the proposition in types, for example:

  (,(neg '(a * b)) -> . ,(neg (neg `(,(neg 'a) + ,(neg 'b)))))

This is one direction of the deMorgan law. In intuitionistic logic,
deMorgan law is more involved:

	NOT (A & B) == NOTNOT (NOT A | NOT B)

The system gives us the corresponding term, the proof:

(lambda (_.0)
      (lambda (_.1) 
	(_.1 (inl (lambda (_.2) 
		    (_.1 (inr (lambda (_.3) (_.0 (cons _.2 _.3))))))))))

The de-typechecker can also prove theorems in classical logic,
via double-negation (aka CPS) translation. The second part of
logic.scm demonstrates that. We can formulate a proposition:

(neg (neg `(,(neg 'a) + ,(neg (neg 'a)))))

and get a (non-trivial) term

	(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))

It took only 403 ms. The proposition is the statement of the Law of
Excluded Middle, in the double-negative translation.

So, programming languages can help in the study of logic.

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.