[Prev][Next][Index][Thread]
Re: Type names vs type structure
I've pondered upon building a scripting language with an
orthogonal design much like the one Andrew Kennedy proposes.
1. Functions
2. Labeled sums and products, with row types (a la Wand et al)
3. Full polymorphism (a la Odersky/Laufer or Mark Jones)
4. Recursion, allowing any rational tree to describe a type
Examples:
type list(a) = [nil:() | cons:(head:a, tail:list(a))]
type fix(f) = f(fix(f))
type list2(a) = fix(typefun(l:*)[nil:() | cons:(head:a, tail:list(a))])
type monad m = (unit:all(a:*)a->m(a), bind:all(a:*,b:*)m(a)->(a->m(b))->m(b))
Most of this is standard, but I cannot recall seeing 4 combined with
1, 2, and 3. Indeed, I cannot bring to mind any paper that neatly
describes 4 alone. For instance, I know of no paper that describes
extending Hindley-Milner with unification on rational trees, although
the idea seems to have been kicking around for a while. (A rational
tree is any infinite tree that can be finitely represented by a cyclic
structure.) Relevant references would be appreciated!
I know there are a lot of languages out there close to this, such as
Mark Jones latest Hugs variant and Lennart Augustsson's Cayenne.
Again, I'd be grateful for additional references.
Cheers, -- P
-----------------------------------------------------------------------
Philip Wadler wadler@research.bell-labs.com
Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler
600 Mountain Ave, room 2T-402 office: +1 908 582 4004
Murray Hill, NJ 07974-0636 fax: +1 908 582 5857
USA home: +1 908 626 9252
-----------------------------------------------------------------------
``There may, indeed, be other applications of the system
than its use as a logic.'' -- A. Church, 1932
-----------------------------------------------------------------------