[PRL] IOP and disjoint unions

[Mitchell Wand]

>>>>> On Thu, 28 Apr 2005 21:34:58 -0400, Richard Cobbe <cobbe at ccs.neu.edu> said:

RC> On Thu, Apr 28, 2005 at 08:37:14PM -0400, William D Clinger wrote:
>> Returning to the running example, let's add selection notation
>> (e.g. x.f) to the sum type:
>> 
>> LambdaTerm = (LambdaTerm x LambdaTerm)        // Application
>> + String
>> + double
>> + (String x LambdaTerm)            // Abstraction
>> + (LambdaTerm x LambdaTerm)        // Selection
>> 
>> Is this really going to save you from writing a lot of code?

RC> I'm sorry, I'm not following.  Is which going to save me writing a lot
RC> of code: adding the record selection form, or the implicit subtyping?

I stopped following a while ago.  In my very bad pidgin Java, I'd write
something like

abstract class LambdaTerm
   {SetOfString freeVars (),
    expval eval(),
    void printit()}

class ApplicationTerm extends LambdaTerm {
   LambdaTerm rator;
   LambdaTerm rand;
   ApplicationTerm (LambdaTerm _rator, LambdaTerm _rand)
     {rator = _rator; rand = _rand}
   SetOfString freeVars() 
     {return SetOfString.union(rator.freeVars(), rand.freeVars());}
   // etc }

and if you have a value known to be of type LambdaTerm, then the only
methods you can call on it are freeVars, eval, and printit.  Good old
dynamic dispatch does just what you want.

Or maybe it's

interface LambdaTerm ...

and

class ApplicationTerm implements LambdaTerm ...

but it's the same deal either way, at least so far as this example goes.

Or are you thinking about the situation in which sometimes you know
you've got an ApplicationTerm and sometimes you only know that you've
got a LambdaTerm?  

Obviously I've been thinking in category theory too long. There a sum
type can always be represented by its polymorphic _case_ function:

A+B ~=~ (all C)([A->C]x[B->C])

where ~=~ means "at least iso, and maybe equals"

--Mitch