Lambda the Ultimate

An article (draft) titled "ΠΣ: A Core Language for Dependently Typed Programming", an online demo and a Hackage repository with source code for a type checker.

To my big surprise I haven't found it on LtU.

This is a proposal for a language that could serve the role the Haskell Core serves for Haskell - a small in list of features, verbose language in which we can translate higher-level concepts.

This is interesting as PiSigma contains minimum features and one can play with implementation.

Hello LtU,

Please excuse me if I get my terms wrong, not a type system expert in any way. Since I don't really know what I'm talking about and what details are relevant I'll try to keep this short. I think it's best to discuss this and I'll come up with the details during the discussion.

I want to "map" different "type classes" into a unified system. I understand there is no such thing as a universal type system, so I'm looking for something pragmatic.

For example,

I could write a Map<String, -type- > view (or call it record, named tuple, etc) of a Java Class.

class Person {
   String name;
   int age;
}

Would become something like:

{ "name": String, "age", int }

Similarly, I could combine an XML document

<person age="23" name="Meh"/>

with a list of named & typed XPath expressions

("age", int, /person/@age)
("name", String, /person/@name)

and view that as a similar Map.

Another example would be a query on a database of similar form.

I'd then like to have operations such as:

• trimming the Map to a new Map with a subset of it's fields
• projecting a field of the map to the type of it's value
• taking the union of some maps into a new Map

It's important that I can dynamically walk (incrementally) the structure of a type and build a user interface on that.

Finally I'd like to (structurally) check equality of two types.

Currently I'm trying to write this myself but there are lots of details that make this rather complex. For example, efficiently dealing with values from derived types (obtained from slice/combine operations), etc.

Is there any (Java) library that does what I'm looking for? Does this sort of thing have a name?

Thanks a lot for your input!

Jelle.

Marc Feeley and Danny Dubé, PICBIT: A Scheme System for the PIC Microcontroller, Fourth Workshop on Scheme and Functional Programming. November 7, 2003.

This paper explains the design of the PICBIT R4RS Scheme system which specifically targets the PIC microcontroller family. The PIC is a popular inexpensive single-chip microcontroller for very compact embedded systems that has a ROM on the chip and a very small RAM. The main challenge is fitting the Scheme heap in only 2 kilobytes of RAM while still allowing useful applications to be run. PICBIT uses a novel compact (24 bit) object representation suited for such an environment and an optimizing compiler and byte-code interpreter that uses RAM frugally. Some experimental measurements are provided to assess the performance of the system.

A very interesting perspective on language implementation, found via @dhess and previous discussion.