I've tried my type-checker on Forth... 
Author Message
 I've tried my type-checker on Forth...

(This I posted on comp.lang.forth)

I have recently posted an article in comp.lang.pop describing a static
type-checker for POP-11. It deals with the problem of inferring what happens
to the stack by using -grammars- to describe the stack, function arguments and
function results. Essentially a function is regarded as -parsing- the stack
to obtain its arguments and -generating- its results. Thus the stack-grammar
has to be divided by the argument grammar and then multiplied by the result
grammar.

I don't know if the capabilities of the checker are a good match to serious
FORTH programs. It does require that dynamic stack usage be characterisable
as regular grammars, which is a good model for POP-11, so that I have been
able to check a chunk of serious program in that language. Neither is it clear
that the model for data-structures is appropriate for FORTH, resembling as
it does that for SML. But, I did cobble up a demo using examples given in a
FAQ file:

On making the declaration:

    declare SUM_OF_SQUARES:Int*Int -> Int;

and compiling the FORTH sequence:

    : SUM_OF_SQUARES (a b -- c) DUP * SWAP DUP * + ;

(using a 1-page partial implementation in POP-11), the type checker produced
the following analysis (it uses the comment as a hint for variable names)

Defining procedure: SUM_OF_SQUARES
  Initial Type:        SUM_OF_SQUARES  :  (Int*Int -> Int)

    CODE                 Type of STACK                     Val

                       Int*Int                         a, b
1   callw(DUP)         (Int)*(Int)*(Int)               a, b, b
2   callw(*)           (Int)*(Int)                     a, b * b
3   callw(SWAP)        (Int)*(Int)                     b * b, a
4   callw(DUP)         (Int)*(Int)*(Int)               b * b, a, a
5   callw(*)           (Int)*(Int)                     b * b, a * a
6   callw(+)           Int                             b * b + a * a
  Variable declarations in procedure  - None -
  Residual constraints in procedure  - None -

The type of some functions can be inferred:

   : LIN (a b x -- a+b*x) * +;

Defining procedure: LIN
  Initial Type:        LIN  :  (<_1>*<_2>*<_3> -> r.21)

    CODE                 Type of STACK                     Val

                       <_1>*<_2>*<_3>                   a, b, x
1   callw(*)            <_1>*(Int)                       a, b * x
2   callw(+)            Int                              a + b * x
  Variable declarations in procedure  - None -
  Residual constraints in procedure  - None -

Type -- LIN           : (Int)*(Int)*(Int) -> Int

Robin Popplestone.



Mon, 13 May 1996 23:07:37 GMT  
 
 [ 1 post ] 

 Relevant Pages 

1. I've tried Smalltalk Express, any others??

2. I've tried Smalltalk Express, any others??

3. forth type checkers

4. forth type checker

5. JED: the FORTH EMACS you've been waiting for

6. opacity and static typing (Re: Type checkers for scheme)

7. We've been /.'ed!

8. OT: (Humor/Humour) - Signs That You've Had Too Much Of The 90's:

9. i've been close to python's cradle :)

10. try gfdg try kuiou try gsdfas try

11. The Smalltalk Store: Why we've been slow, and why we're getting better

 

 
Powered by phpBB® Forum Software