# Re: [stack] While we're not moved

## Martin Young — 2000-09-01 15:35:52

    > Hello Concatenative,

     Hello.

     > I thought on static typechecker for Joy.

     Which is interesting...

     > Then it is easy to define type patterns for some kinds of operators:

    > dup ( x -- x x)

    > +   ( x x -- x) because we can add integers and floats (and chars)

    > eq0 ( x -- Bool) also we may take float, char and integer.

    > 1   ( -- Int)

    > 1.0 ( -- Float)

    > '1  -- gues what type has '1 ;)

    >

    > Then I tried to infer type for +1:

    >

    > +1 == 1 + ;

    > + has type ( x x -- x) where one of x is set by literal 1 to Int. Then

    > all x's set to Int. And one x come from input stack. Then type of +1

    > is ( Int -- Int). Very straightforward and simple.

     There are a number of message in the concatenative list archives which detail

    (or at least imply) a number of different notations for the types of things on

    the stack.  AFAIK none of them have yet been shown to be completely successful.

    Yours seems to be based on the assumption the words in Joy can be treated in

    the same way as lambda functions where the top N items on the stack are taken

    to be the formal parameters (of which there are a constant number).  A Joy word

    may use a variable number of values from the stack, and similarly leave a

    variable number.

    Consider the word:

    unlist == [ dup null not ] [ uncons ] while pop

    Which takes a list from the top of the stack leaving each of its items

    separately.  What's its type?  I guess one could express it as:

    ( [ x1 .. xN ] -- x1 .. xN )

    Taking the type of word + to be ( Int Int -- Int ) then we can use type

    inference to say that program unlist + would have type:

    ( [ x1 .. Int Int ] -- x1 .. xN-2 Int )

    Which may or may be useful, but consider the program:

    unlist0 == [ dup first 0 = not ] [ uncons ] while pop

    Here, the resultant types on the stack depend on the *values* already on the

    stack, not just the program itself.

    ISTM that any type system which is intended to describe arbitrary Joy programs

    must have at least equal expressive power as Joy itself thus making analysis of

    it non-computable.  Alternatively we need something which isn't simply an

    adaptation of lambda related type systems.

    Louis Madon described a mechanism for partitioning the stack into regions based

    on analysis of the program, and this may be enough.  I suspect not, but who

    knows?

     > If we use type pattern to distinguish between different primitives

    > with the same name (as in StrongForth) then it is possible to develop

    > version of +1 for floats and characters.

     ...but only if you can statically determine the types on the stack, otherwise

    it's a runtime choice.

     > But when I thought about use of lists I come into interesting problem.

    > What to expect when taking apart head and tail from list?

     I believe this is another example of the problem described above.

     > It was not a problem. Problem (or a task or a food for thought) is the

    > following: we construct some list using some grammar hidden inside Joy

    > definitions and static typechecker should know about that grammar (or

    > more precisely -- reversed grammar) to know what to expect when taking

    > list apart.

     Indeed, and I'd suggest that this is ultimately non-computable without forcing

    the arity of every Joy word.

     > How, for example, not to put empty list as splitlist argument? Guard

    > it with checking for emptyness? Then how to (automatically) strip

    > that check?

     Good question.  How does Haskell optimise away such guards?

    --

    Martin Young  working for  STMicroelectronics at     `(o)_(o)' The fat wise /

    1000 Aztec West, Almondsbury, Bristol, BS32 4SQ.      (  V  ) owl eats only >

    +44 1454 462 523    `v'      Martin.Young@...      `.___,' clean mice.  /

                       _(_)_                             -="==="=============='