Lambda the Ultimate

I've been mulling over a language design issue which would be nicely solved if tuples behaved like a monoid. Is anyone aware of a language where tuples can be arbitrarily extended?

For example, if # is the tuple extension operator:

f :: a -> b -> a#b 
f x y = x # y


f 1 "dog" ==> (1,"dog")
f (1,"dog") true ==> (1,"dog",true) 
f () ("dog", true) ==> ("dog", true)

It seems that type inference is still possible here, though I'm not sure exactly how it would work. (ie, how do you unify types a*b*c and d#e?)

IIT Kharagpur

KSHITIJ 2009

THE ANNUAL TECHNO-MANAGEMENT FEST

29th Jan- 1st Feb
THE OVERNITE ACM ICPC 2009 MULTI PROVINCIAL PROGRAMMING CONTEST
( http://overnite.ktj.in )

* C/C++/JAVA to be used as medium of coding.
* An all night coding event.
* Wild card entries to be given through online prelims .
* ONLINE PRELIMS: 29th Nov,2008

OPENSOFT

What would you call a body without soul?
Confused? Yes, this is the same scenario with hardware without
software.

Moreover this event is open source, thus enabling later modifications,
debugging and improving upon the origin software.

JAVAWISE

Open Source Java is the missing piece of the puzzle to enable broader
open source development from desktop to server.

The event challenges the participants to develop an application to be
used on a mobile phone or a PDA.

ìMouse4D

Introduces the latest innovation in the field of Robotics,the
Microsoft Robotics Studio,to tackle one of the best known problems in
the field of Artificial Intellegence,MicroMouse

It requires the competitors to face the challenge in a virtual
world,simulating the task done in the physical realm.

HACKED?...If you have the fire to combat the e-world this is a
platform that we present to you.

FramED9211...Ever wondered how they nab those over-speeding vehicles?

www.ktj.in

Modeling Abstract Types in Modules with Open Existential Types, by Benoît Montagu Didier Rémy:

We propose F^¥, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as done in module systems. The static semantics of F^¥ adapts standard techniques to deal with linearity of typing contexts, its dynamic semantics is a small-step reduction semantics that performs extrusion of type abstraction as needed during reduction, and the two are related by subject reduction and progress lemmas. Applying the Curry-Howard isomorphism, F^¥ can be also read back as a logic with the same expressive power as second-order logic but with more modular ways of assembling partial proofs. We also extend the core calculus to handle the double vision problem as well as type-level and term-level recursion. The resulting language turns out to be a new formalization of (a minor variant of) Dreyer’s internal language for recursive and mixin modules.

This approach to existentials seems to considerably improve their power and simplify their use. It also brings us one step closer to first-class modules!