Static Type Checking of Open Stack Languages 
Author Message
 Static Type Checking of Open Stack Languages

For Forth, the main problems seem to be:

> - 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

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.

> - 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);

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

> - 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.

Fri, 17 May 1996 21:34:09 GMT  
 [ 1 post ] 

 Relevant Pages 

1. Static Type Checking of Open Stack Languages

2. Static Type Checking of Open Stack Languages

3. Dynamic vs. static type checking

4. "like Current" and static type checking

5. agents and static type checking holes

6. Summary of Static vs Dynamic type checking?

7. Static type Checking

8. Argument Type Checking and Static Libraries

9. Type Checking and Assertions: Proposal (was static analysis)

10. static type checking / interface definitions for Python?

11. Smalltalk vs. Static Typed Languages for the Web

12. Types, types: static vs. dynamic -- classification


Powered by phpBB® Forum Software