Lambda the Ultimate

Looking to write a language that combines primitive and object types with a prototypic approach ala Self, I am struggling to understand how to implement generic types. I read the GNAT Ada interface implementation document but did not see material directly related to this.

My concerns are:

• Adjust the size of the object to the parameterized type(s)
• Adjust the methods code to the parameterized type(s)
• Compare instantiated generic types for compatibility (eg. two instances of the type with covariant method parameters)

In particular, how do languages that support generic types handle the second point?

I've been having fun recently learning to write programs in Haskell. As a lover of both Scheme and C, its functional semantics and static typing seem like a near perfect combination, and having to re-think certain algorithms that came to me so easily with mutable state has proved to be a fun challenge.

What brought me to Haskell was the fact that I was tired of faking polymorphism in C with void* passing. I just couldn't commit myself to using C++ -- it's just a personal bias -- functions on objects seems much more natural than objects with functions. Plus Haskell is the new hotness (TM).

Of course I thought wouldn't it be great if there was a C (a real C with pointers and all) that also had a ML type system. After a little digging on Google I found this: Towards an ML-style Polymorphic Type System for C; reading through the paper it seems like a very natural evolution of C.

Unfortunately it seems that the idea lives and dies in this paper. I cannot find reference to a compiler implementation anywhere.

Has anyone come across other projects that combine imperative mutable languages (like C) with ML style typing?

Linear Logical Algorithms, Robert J. Simmons and Frank Pfenning, 2008.

Bottom-up logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost semantics that enables reasoning about the running time of algorithms written as inference rules. Previous work with the programming language Lollimon demonstrates the expressive power of logic programming with linear logic in describing algorithms that have imperative elements or that must repeatedly make mutually exclusive choices. In this paper, we identify a bottom-up logic programming language based on linear logic that is amenable to efficient execution and describe a novel cost semantics that can be used for complexity analysis of algorithms expressed in linear logic.

In my last post, I linked to a paper by Ganzinger and McAllester about specifying algorithms as logic programs, and a) admired how concise and natural the programs were, and b) was sad that the logic programs used some "non-logical" operations, such as deletion.

So, what does it mean for an operation to be "non-logical", and why is it a bad thing? Roughly speaking, you can think of the analogy: non-logical operations are to logic programs what impure operations are to functional programs -- they are features which break some parts of the equational theory of the language. Now, the Curry-Howard correspondence for functional programs says that types are propositions, and programs are proofs. It turns out that a different version of this correspondence holds for logic programs: in logic programming, a set of propositions is a program, and the execution of a program corresponds to a process of proof search -- you get a success when execution finds a proof of the goal.

When you have nonlogical operations in your logic programming language, you've introduced operators that don't correspond to valid rules of inference, so even if your logic program succeeds, the success might not correspond to a real proof. Deletion of facts from a database is a good example of a nonlogical operation. Regular intuitionistic and classical logic is monotonic: deduction from premises can only learn new facts, it can never disprove things you already knew to be true. Since deletion removes facts from the set of things you know, it can't have a logical interpretation in classical/intuitionistic logic.

However, it turns out that not all logics are monotonic, and in this paper Simmons and Pfenning show that if you take the language of propositions to be a fragment of linear logic, then all of the operations that Ganzinger and McAllester use actually do have a nice logical interpretation.