Lambda the Ultimate

The Left Hand of Equals, by James Noble, Andrew P. Black, Kim B. Bruce, Michael Homer, Mark S. Miller:

When is one object equal to another object? While object identity is fundamental to object-oriented systems, object equality, although tightly intertwined with identity, is harder to pin down. The distinction between identity and equality is reflected in object-oriented languages, almost all of which provide two variants of “equality”, while some provide many more. Programmers can usually override at least one of these forms of equality, and can always define their own methods to distinguish their own objects.

This essay takes a reflexive journey through fifty years of identity and equality in object-oriented languages, and ends somewhere we did not expect: a “left-handed” equality relying on trust and grace.

This covers a lot of ground, not only historical, but conceptual, like the meaning of equality and objects. For instance, they consider Ralph Johnson on what object oriented programming means:

I explain three views of OO programming. The Scandinavian view is that an OO system is one whose creators realise that programming is modelling. The mystical view is that an OO system is one that is built out of objects that communicate by sending messages to each other, and computation is the messages flying from object to object. The software engineering view is that an OO system is one that supports data abstraction, polymorphism by late-binding of function calls, and inheritance.

And constrast with William Cook's autognosis/procedural-abstraction view, which we've discussed here before.

The paper's goal then becomes clear: "What can we do to provide an equality operator for a pure, autognostic object-oriented language?" They answer this question in the context of the Grace programming language. As you might expect from some of the authors, security and trust are important considerations.

Is there some reason Haskell didn't expose GADTs as guards?

    -- Haskell
    data Term t
        Lit Int :: Term Int
        App (Term (a -> b)) Term a :: Term b
        ...

    -- Guards
    data Term t 
        Lit Int where t = Int 
        App (Term (a -> b)) Term a where t = b 
        ...

It seems equivalent and semantically simpler.