Type Systems (was: [stack] Re: tree rewriting)

[Massimo Dentico]

[I send this message as CC to the Tunes mailing-list at the end of
a cross-fertilization. I hope that no one is annoyed by that.]

Mark van Gulik (ghoul6@home.net) on Concatenative mailing-list
(concatenative@egroups.com) wrote:

> 
> First, Mark van Gulik (ghoul6@home.net) 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@tunes.org) 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
> 

[Emphais added by me]

Now, this is for me *extremely* interesting. I think Brian Rice is working
in the same direction but perhaps with another point of view (I don't know
Avail and Slate [1], the Brian's language proposal for the Tunes project [2],
in sufficient details so that I can examine similarities and differences and
in any case these are work in progress). Another language with a Turing-equivalent
type system is Cayenne [3].

In the way you describe we obtain a system in the spirit of Open
Implementation [4], we are *not* stuck with a fix type checker/inferencer.
We have the entire language for constructing domain or application specific
type systems. This means we don't have limitations in expressing invariant.
What about the application to Proof-Carry Code (PCC) [5]? Infact such a system
is more similar to a (semi-)automatic theorem prover (preferable for PCC) than
to "traditional" type checkers/inferencers (even if functional languages have
more and more powerful type systems).

Another interesting connection is between staged computation and type systems.
I think in a language with capabilities like you describe the concept of staged
computation emerges in a natural way. See Lee [6] for an overview, the OGI
Mustang Project [7] and MetaML [8] for an implementation.

However, this is all about meta-programming and reflection [9] (the main goal
of the Tunes project), so you could be interested in that.

References

[1] The Slate Object
    - http://www.tunes.org/~water/slate-home.html

[2] The TUNES Project for a Reflective Computing System
    - http://www.tunes.org/

[3] Cayenne - Hotter than Haskell
    - http://www.md.chalmers.se/~augustss/cayenne/

[4] Open Implementation Home Page
    - http://www.parc.xerox.com/spl/projects/oi/

[5] Proof-Carrying Code (aka Self-Certified Code) (Peter Lee)
    - http://www.cs.cmu.edu/~petel/papers/pcc/pcc.html
    Proof-Carrying Code (George Necula)
    - http://www-nt.cs.berkeley.edu/home/necula/public_html/pcc.html
    
    An excerpt from this page:
    ------------------------------------------------------------------------------
    Overview

    Proof-Carrying Code (PCC) is a technique that can be used for safe
    execution of untrusted code. In a typical instance of PCC, a code
    receiver establishes a set of safety rules that guarantee safe behavior
    of programs, and the code producer creates a formal safety proof
    that proves, for the untrusted code, adherence to the safety rules.
    Then, the receiver is able to use a simple and fast proof validator to
    check, with certainty, that the proof is valid and hence the untrusted
    code is safe to execute.

    PCC has many uses in systems whose trusted computing base is dynamic, either
    because of mobile code or because or regular bug fixes or updates. Examples
    include, but are not limited, to extensible operating systems, Internet
    browsers capable of downloading code, active network nodes and safety-critical
    embedded controllers.
    ------------------------------------------------------------------------------

[6] Peter Lee: Staged Computation
    - http://foxnet.cs.cmu.edu/people/petel/papers/staged/staged.html

[7] The OGI Mustang Project
    - http://www.cse.ogi.edu/PacSoft/projects/Mustang/Overview.html

[8] MetaML Home Page
    - http://www.cse.ogi.edu/PacSoft/projects/metaml/index.html

[9] Review about Computational Reflection
    - http://www.tunes.org/Review/Reflection.html

-- 
Massimo Dentico