Lambda the Ultimate

inactiveTopic TinkerType
started 9/30/2002; 2:20:54 AM - last post 10/2/2002; 2:22:36 AM
jon fernquest - TinkerType  blueArrow
9/30/2002; 2:20:54 AM (reads: 1476, responses: 5)
Tinkertype is a framework for compact and modular description of formal systems. A family of related systems is broken into a set of individual inference rules and a set of features controlling the inclusion of rules in particular systems.

The Tinkertype framework is applied to construct a substantial repository of typed lambda calculi including systems with subtyping, polymorphism, type operators and kinding, computational effects, and dependent and recursive types. The repository describes both declarative and algorithmic aspect of the systems and can be used with our tool, the Tinkertype assembler, to generate calculi either in the form of typeset collection of inference rules or executable ML type checkers.

From the author of the textbook Types and Programming Languages. which also has several OCAML implementations of type systems available. [ Presentation]

Posted to LC by jon fernquest on 9/30/02; 2:26:54 AM

jon fernquest - Re: TinkerType  blueArrow
9/30/2002; 2:35:01 AM (reads: 719, responses: 0)
One of the interesting points made in the talk is that although it might be difficult to create the first model or template type system with the toolkit, modifications or variations are not difficult.

A system like this where you could construct executable type checkers for Scheme would be great and would certainly be in the tradition of using Scheme to prototype new programming language ideas and features.

It would also help a powerful language evolve in an incremental new ways, instead of having people abandon it wholesale for the latest new thing (the norm?). Do programming languages really need to have life spans? (Some people cite 8 years as the average.) Evolutionary forking, both growing and shrinking, the more resilient branches thriving and staying alive. Evolution proceeding on several fronts including syntax, semantics, and pragmatics?

Franck Arnaud - Re: TinkerType  blueArrow
9/30/2002; 8:56:59 AM (reads: 697, responses: 0)
Evolutionary forking, both growing and shrinking

Ever seen a language that shrank regularly and significantly, even if only to compensate for new features? It seems virtually impossible to shrink a language with more than one user it seems to me. Entropy is hard to beat.

Incremental forking also does not sound like a good idea (beyond purely experimental code) as the cost of a fork is likely to be more or less constant (loss of interoperability with other branches) and unlikely to be offset by small incremental changes with incremental (small) benefits.

Paul Snively - Re: TinkerType  blueArrow
9/30/2002; 2:45:52 PM (reads: 684, responses: 0)
jon fernquest: Do programming languages really need to have life spans?

Human languages do; why should programming languages be any different?

jon fernquest - Re: TinkerType  blueArrow
10/1/2002; 3:32:55 AM (reads: 653, responses: 0)
>> jon fernquest: Do programming languages really need to have life spans?

>Human languages do; why should programming languages be any different?

Human languages evolve more continuously over longer periods of time.

Computer language evolution is discontinuous.

Programming languages are the materials science of computer science (quote from Benjamin Pierce's lecture notes).

...and as such they should allow programmers to build on and extend the work achieved by previous programs (i.e. re-use) (I'll shortly give an example)

How long did it take for the AI Winter to set in and have people start dumping Lisp as a language for writing applications.

(This was more a function of the hype surrounding AI that resulted ultimately in stigmatizing the very idea of AI. I worked for an AI company in the 1990's where we were instructed not to refer to our company as an AI company, we were CASE, there was also exactly one AI specialist in the whole company.)

...and even before this MacLisp was made extinct with the advent of the Common Lisp standard

...were translators made available from MacLisp into Common Lisp like Microsoft supplies today for Java to C#?

SHRDLU by Winograd is a famous natural language processing system written in MacLisp

You might think that people took this program and built on it but they didn't, it was abandoned and only resurrected recently.

Issues arise in its resurrection that touch on the very definition of computer science as a science.

If you read the link given closely you'll see some people accuse Winograd of claiming things for the program that were never true, which brings up the issue of scientific method and repeatability of an experiment in computer science research.

But apart from this, IMHO *innovative ideas are often implicit in proof of concept or prototype programs* and *programming languages should be a vehicle for preserving and communicating these ideas*.

A prior LTU posting also gives an idea of how many lost programming languages, lost programs and ideas, and reinvented wheels there are:

> It seems virtually impossible to shrink a language with
> more than one user it seems to me.

Several Scheme implementations stripped macros out of Scheme (e.g. Stalin). Ewe, Waba, and Super-Waba strip out all but a tiny kernel of the Java API and add their own API specialized for PDA's, cell phones and other devices. As per the Java 3 discussion you could simplify things by eliminating primitive types and making everything an object. I think there are a lots of ways you could prune back Java to something more minimalistic like Scheme and then regrow it avoiding all the imperfections (e.g. in threads or the class loader) that people don't like and adding things that purists like , like tail recursiveness to the virtual machine. If Java's imperfections ultimately threatened it with extinction, would it behoove Java to remove them?

jon fernquest - Re: TinkerType  blueArrow
10/2/2002; 2:22:36 AM (reads: 612, responses: 0)
Benjamin Pierce has some nice definitions in the first online lecture for his course, [PDF, From resources page]:

"PL is the ''materials science'' of computer science."


'Program meaning' can be approached in many different ways.

# Denotational semantics and domain theory view programs as simple mathematical objects, abstracting away their flow of control and concentrating on their input-output behavior.

# Program logics such as Hoare logic and dependent type theories focus on developing logical rules for reasoning about programs.

# Operational semantics describes program behaviors by means of abstract machines. This approach is somewhat lower-level than the others, but is extremely flexible.

# Process calculi focus on the communication and synchronization behaviors of complex concurrent systems.

# Type systems describe approximations of program behaviors, concentrating on the shapes of the values passed between different parts of the program."