> 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. /
_(_)_ -="==="=============='