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