# Re: tree rewriting

## Mark van Gulik — 2000-05-25 03:34:54

    First, Mark van Gulik (ghoul6@...) wrote:

     >> Well, I would have avoided those special "variables" (dirty word!) like

    >> "2nd" and "1st".  Instead, I would provide a type signature that was itself

    >> applicative.  The allowable operations used in a type signature would be

    >> typeSwap, typeDup, typePop, typeMatchAndPop, and {any type literal}.  Why

    >> have the power of an applicative language if you don't even bother building

    >> the type signature applicatively (just kidding, my syntax wouldn't be as

    >> clear IMO).

     To which Brent Kerby (iepos@...) replied:

     > You say you're kidding, but you bring up a good point. Using things

    > like "typeSwap", "typeDup", "typePop", and "typeMatchAndPop" seems

    > like a good idea, since it avoids the use of the variable-like primitives

    > "2nd" and "1st". However, "swap", "dup", and "pop" by themselves is

    > not complete; for, with just those, how could you construct a

    > combinator that swaps, not the top two items of the stack, but the

    > two items beneath the top one? (in other words, how could you write

    > the type of "[swap] dip"?) ... If you add a typeDip and typeCons,

    > then you'll have completeness, I believe.

    >

    > You'd also need a type "quotation" construct; for, although you

    > can write the type of a binary arithmetic operator as

    >

    >   int typeMatchAndPop int typeMatchAndPop int

    >

    > how could you write the type of a program that pushes such an operator

    > onto the stack? With a quotation construct, you'd write it as just

    >

    >   [int typeMatchAndPop int typeMatchAndPop int]

    >

    > It is interesting that in this style types are written in the exact

    > same syntax as ordinary programs, using concatenation and quotation ...

     That was fully intentional.  The work I did in Avail's type system allowed

    me to add two distinct forms of Currying (both typesafe) to the language,

    without any new primitives.  The basic execution model I chose allowed me to

    implement exceptions, coroutines, and backtracking, also with no extra VM

    support.  The type system, well, that's the gem...

    A method definition (Avail uses multimethods) looks like:

    Method "_copy from_to_" is [t : tuple, start : integer, end : integer |

        .....the actual code.....

    ] : tuple;

    To strengthen the return type to something more meaningful than "tuple", one

    adds a "returns" clause...

    Method "_copy from_to_" is [t : tuple, start : integer, end : integer |

        .....the actual code.....

    ] : tuple

    returns [tT : tupleType, startT : integerType, endT : integerType |

        .....something to calculate the static type at each call site,

             based on the tuple's type, and the ranges of values that

             the starting and ending indices may have.....

    ] : tupleType;

    Similarly, I can introduce a type guard on the arguments.  Consider the

    one-argument closure evaluation operation "_(_)" (each underscore in the

    name is where an argument goes, in this case the first argument is a closure

    and the second argument is the value to invoke it with)...

    Method "_(_)" is [c : [terminates]->void, a : all |

        ..... invoke c somehow with a as the argument .....

    ] : all

    returns [cT : closureType, aT : type |

        cT result;

    ] : type

    requires [cT : closureType, aT : type |

        aT <= cT[1];

    ] : boolean;

    Now consider a call site to "_(_)"...

    bananaPeeler ::= [b : Banana | peel b;] : BananaPeel;

    aBanana ::= new Banana;

    Smoke bananaPeeler(aBanana);

    Note that the "Smoke_" operation expects its argument to be a BananaPeel.

    At this call site the "_(_)" operation is passed two arguments:  The closure

    to invoke, and the argument to pass it.  The closure here is of type

    [Banana]->BananaPeel, which complies with the [terminates]->void due to

    contravariance of the argument and covariance of the result.  Without the

    "returns" clause in the definition of "_(_)", the result from this call

    would have the very weak type "all".  The "returns" clause allows *arbitrary

    code* to run at link-time (a term I use to describe the compile-time of a

    call site).  In this case it simply asks bananaPeeler's type (a closureType)

    what kind of thing it returns (a BananaPeel in this case).  The call site of

    "Smoke_" then gets BananaPeel as its argument type, as expected.

    The "requires" clause also makes sure the closure wull be invoked with the

    right kind of argument.  In this case, it is passed [Banana]->BananaPeel in

    cT and Banana in aT.  It then executes its code, "aT <= cT[1]".  In this

    case the "_<=_" operation on types is invoked (subtype test), passing the

    argument #1 type of cT (which is Banana) and aT (ditto), and answering true,

    indicating the call site is acceptably typed.

    I think by this point (or much sooner) you see the power of allowing the

    type system to be described within the language itself (or in some cases a

    safe subset of it).  You may also want to check out the specific variation

    of tuple types I devised.  The basic gist is that a tuple type has a range

    of possible sizes, the types of the initial N elements (or at least as many

    are actually present in an actual tuple), and the type for the remaining

    elements.  A bit of a compromise between lists and tuples in many functional

    languages, but it really seems to work out well.  The reason I bring up

    tuple types is a possible correspondence with the Joy typing model you

    described, where you assert things about the types of the top N elements of

    the stack.

    Just so you don't have to scan previous posts, the Avail web site is:

        http://www.ericsworld.com/Mark/HTML/Avail.html