Lambda the Ultimate

Fixed, thanks. The site works for me, so maybe it's back up. Here's another link to the paper, but it looks it's one page shorter, and the date is a little earlier.

Presumably not, since one can have dependent records that contain types, and this proposal doesn't include anything to do with associated types (it's listed at the end under future work).

The objects proposal can (if I'm reading correctly) be desugared into Haskell functions and datatypes (you probably need GADTs), and you can't really translate everything in a dependent record ala Coq directly into Haskell.

Good point. This proposal does not seem to offer sufficient encapsulation in order to satisfy this requirement. Solving this would seem to require an existential accessible only by the method, and the number of parameters when deconstructing would need to be strictly less than or equal to the number of parameters to the constructor.

Thus, you would only need to modify every point where a Lit is constructed, rather than deconstructed, which seems to be as good as it gets. I don't think this ability is available in functional languages, so I'm curious if there are any better solutions without appealing to extensions.

Glad your are enjoying the paper Martijn.

You are right to complain about this example. We have been lazy in fixing a couple of things in the draft, including to clarify how this example should work. Indeed if you use something like:

t1 = Div (Plus (Lit 3) (Lit 4)) (Lit 0)

then "Nothing" will always be the returned location. What you really want to do here is to add location information at construction time.

To do so, you can use anonymous objects:

t2 = Div (Plus (Lit 3 {loc = Just (1,1)}) (Lit 4 {loc = Just (1,5)})) (Lit 0 {loc = Just (2,1)})

t3 = Div (Plus (Lit 3) (Lit 4)) (Lit 0) {loc = Just (1,2)}

Anonymous objects allow initialization like anonymous classes in Java, but the actual mechanism that allows this is more general in the sense that updating objects is also possible. If you want to put things in terms of Haskell lingo, the mechanism above is providing similar functionality to record updates.

The code in the paper does not change. So our claims are valid.

Like the rest of the proposed features, anonymous objects are nothing but syntactic sugar. So, you can run the example in Haskell today (but not with the clarity nor the advantages of our approach :)). Here is the code:

module Objects where

type Loc = Maybe (Int,Int)

data Exp a where
Lit :: Loc -> Int -> Exp Int
Plus :: Loc -> Exp Int -> Exp Int -> Exp Int
IsZ :: Loc -> Exp Int -> Exp Bool
If :: Loc -> Exp Bool -> Exp a -> Exp a -> Exp a
Div :: Loc -> Exp Int -> Exp Int -> Exp Int

-- loc method accessor

loc :: Exp a -> Loc
loc (Lit l _) = l
loc (Plus l _ _) = l
loc (IsZ l _) = l
loc (If l _ _ _) = l
loc (Div l _ _) = l

-- constructors

lit :: Int -> Exp Int
lit x = Lit Nothing x

plus :: Exp Int -> Exp Int -> Exp Int
plus e1 e2 = Plus (loc e1) e1 e2

isZ :: Exp Int -> Exp Bool
isZ e = IsZ (loc e) e

iff :: Exp Bool -> Exp a -> Exp a -> Exp a
iff e1 e2 e3 = If (loc e1) e1 e2 e3

divv :: Exp Int -> Exp Int -> Exp Int
divv e1 e2 = Div (loc e1) e1 e2

-- evaluation

eval :: Exp a -> a
eval (Lit _ x) = x
eval (Plus _ e1 e2) = eval e1 + eval e2
eval (IsZ _ e) = eval e == 0
eval (If _ p e1 e2) = if eval p then eval e1 else eval e2
eval d@(Div _ e1 e2) =
if eval e2 /= 0 then eval e1 `div` eval e2
else error (show (loc d) ++ ": division by 0")

-- building some expressions

-- location is always Nothing here
t1 = divv (plus (lit 3) (lit 4)) (lit 0)

-- however, you can add the location info:
t2 = divv (plus (Lit (Just (1,1)) 3) (Lit (Just (1,5)) 4)) (Lit (Just (2,1)) 0)

t3 = Div (Just (1,2)) (plus (lit 3) (lit 4)) (lit 0)

Adding anonymous objects to the core language is fairly trivial. I've been postponing this for quite a while now, but I hope that I can restart work on this topic in the next few months.

Hi Marco,

Not entirely sure if I understand your point, but what we mean by "classes as types" is something like what is on page 5 of the slides or Figure 1 in the paper. So type classes like "Eq" cannot be used on positions where types should occurs; and types cannot occur in positions where type classes should occur.

For another example, consider this:

p1 :: [a] => Eq a -> Int

This is not a valid Haskell type, right?

Does this help to clarify our point?

.. but I was reading the sheets and I thought a 'container' class such as Set can be specified as, pardon me Haskell, it's been a while,

class Set (S a) where
insert: a -> S a -> S a
union: S a -> S a -> S a

I.e. you can specify type classes over parameterized types, which makes some of the claims moot, although no doubt it's still an excellent paper.

I think what you mean is:

class Set s where
insert :: a -> s a -> s a
union :: s a -> s a -> s a

Indeed this is perfectly valid Haskell code. Let's call this solution A.

One of the things that are going on about in the paper (among others) is that the following is not valid Haskell code:

class Set a where
insert :: a -> Set a
union :: Set a -> Set a

Let's call this solution B.

In section 2.3 of the paper we discuss both solutions, so we do acknowledge that it is possible to work with container types based on Haskell type classes. We call (variants of) solution A bulk types (if you look at Peyton Jones paper, you'll see your proposed solution there). We refer to solution B as ADT.

We wrote the current draft a while ago, and I must say that the terminology used there is wrong. William Cook makes a very nice argument to what the difference between solution A and B are. If you haven't read:

On Understanding Data Abstraction, Revisited

I strongly suggest you to do so. This explains the difference between solution A and B, and settles the terminology in a much nicer way than we have done in the current text. In his terminology solution A is essentially just a (signature of an) ADT, while solution B is just the interface of an object. Those things are quite different beasts, an this essay explains nicely why this is the case.

In any case, I think the confusion that you mentioned regarding 'container' types comes from our related work, where we claim that with some of the Haskell extensions:

"we cannot, in general, define datatypes/container types such as our Graph, Set , Format and Exp examples in those approaches"

Perhaps, less ambiguously, we should have wrote:

"we cannot still have class definitions for object interfaces
like our Graph, Set , Format and Exp examples"

Or, in other words, in those extensions, classes are still not types (just like in current Haskell).

In any case, thanks for the comment, I think the original text may me a bit misleading in that respect.

Nah, I got it. It was a case of sloppy reading, and being used by my some convention on my own language now. Great paper.

Neither the system proposed in this paper nor Scala implicits (credits due to Martin Odersky, not me :)) do constraint simplification. This also means that we do not lose any late binding ability.

In Scala it doesn't even make sense to talk about constraints, because there is no actual notion of a constraints (only implicit parameters). This is also true to an extent in our system, because we really interpret constraints as implicit parameters. This is related to the semantics of constraints: set semantics for Haskell; tuple semantics for our system.

The issue that you mention has been debated in essentially all the proposals extending or inspired by type classes. Namely "Named instances for haskell type classes", "Making implicit parameters explicit" and our paper. You can find a summary in Section 5, under the paragraph "Named Instances and Explicit Implicit Parameters".

The paper "Named instances for haskell type classes" may be interesting to look at if you'd like to see a system where you can still perform constraint simplification and yet support explicitly passed instances. Of course you cannot get both at the same time :).

Hope this helps!

That certainly is helpful. My concern about the user-perceived complexities of composition with named instances is probably still relevant. The problem there isn't so much a matter of early vs. late binding as it seems to be a matter of inherent ambiguity arising from the presence of multiple possible instance resolutions. I probably need to catch up on the paper you pointed me at before I can talk about this sensibly.

The rest of my comment is mainly driven by trying to understand how to apply these ideas effectively given the differing language design objectives between BitC and Scala.