Static Type Checking of Open Stack Languages
For Forth, the main problems seem to be:
Quote:
> - some words, such as ?DUP, return a variable number of values. The
> cases usually are distinguished by flags rather than stack markers or
> counts. (But PICK and ROLL aren't a fit subject for polite conversation...)
> Some programmers define their own words with such behavior, too. It
> would be nice if the checker can somehow handle this, most of the time,
> if only so it can check the words that use the aberrant words.
The apparatus in my checker to support such things is the grammar. Thus a
function -fred- might have type
fred:Int -> Int*String + Int
the problem is, what do you do with the answer? And this depends on whether
you use exact division of grammars or ordinary (Hopcroft and Ullman [H&U])
division. Consider the POP-11:
5 + fred(23)
or Forth:
5 23 fred +
Now + : Int*Int->Int, so that we are trying to form the grammatical quotient
(Int*(Int*String + Int)) / (Int*Int)
Now this is the identity grammar (what I call Unit) according to H&U. But the
quotient is not exact. Taking H&U division corresponds to saying "this
person knows what (s)he is doing", and is supposing -fred- will return an
integer in this case. Taking -exact- division is being more particular (which
is what a type-checker should be). Thus one would have an error or at least a
warning.
Some of the complications of my type-checker serve to ensure that divisions
are exact by inferring things about the result of a test. Typically these
apply to variables, which figure significantly in POP-11. E.g.
if isnumber(x) then ...
after -then- the type-checker knows that -x- is a number. In principle the
stack-grammar could be modified after a test. The POP-11 sequence, written
Forth-style with "." meaning "do it":
5 if 23.fred.dup.isstring then .erase endif .+ ;
would then type-check.
Incidentally, if fred has the (overloaded) type
fred: (Int -> Int*String) + (String -> Int)
there is no problem.
Quote:
> - Vectored execution, which is like C's function pointers. Since Forth
> has no way (that I know of) to restrict the scope of the function-pointer
> variables, it must assume anything might be put there. In practice, it
> could assume that system-provided words, such as . , have some standard
> signature. ("Making a wrong program worse is no sin.") For user-defined
> words you may want a way to declare the signature yourself.
One can try to modify (or some would say mangle) the Hindley-Milner approach
for the purpose. Unfortunately there is no concept of principal type. For
instance, if we define the POP-11 function applist, which iterates through a
list applying a function to each member of the list
define applist(L,f);
unless null(L) then
f(hd(L)); applist(tl(L),f);
endunless;
enddefine;
It will type-check with 2 signatures (remembering that <a> is a -monolog-.)
applist : All a,b; List of {<a>} * (<a> ->b) -> {b};
applist : All a,b; <a> * List of {<b>} * (<a> * <b> -> <b>) -> <b>;
The first one says "take a list of <a>, apply a function from <a> to b
and you will obtain a stacked sequence of b", and describes behaviour like:
applist([1 2 3], dup) =>
** 1 1 2 2 3 3
[dup has the type-signature dup:All a; a -> a*a; ]
The second one says, "take an <a>, and a list of <b> and a function which
takes an <a> and a <b> and gives you a <b>, and you will obtain a <b>, and
thus does a kind of -reduction-.
applist(0,[1 2 3], nonop +) =>
** 6
Quote:
> - Games with the return stack. Apparently ANS Forth doesn't require you
> to support these.
POP-11, being derived from POP-2 which had totally secure dynamic typing,
only allows people to play very structured games with the return stack.
I have not in fact even treated these.
