Hello Martin,
>> is ( Int -- Int). Very straightforward and simple.
MY> There are a number of message in the concatenative list archives which detail
MY> (or at least imply) a number of different notations for the types of things on
MY> the stack. AFAIK none of them have yet been shown to be completely successful.
Well, I need to be practical, nothing more.
MY> Yours seems to be based on the assumption the words in Joy can be treated in
MY> the same way as lambda functions where the top N items on the stack are taken
MY> to be the formal parameters (of which there are a constant number). A Joy word
MY> may use a variable number of values from the stack, and similarly leave a
MY> variable number.
MY> Consider the word:
MY> unlist == [ dup null not ] [ uncons ] while pop
MY> Which takes a list from the top of the stack leaving each of its items
MY> separately. What's its type? I guess one could express it as:
MY> ( [ x1 .. xN ] -- x1 .. xN )
MY> Taking the type of word + to be ( Int Int -- Int ) then we can use type
MY> inference to say that program unlist + would have type:
MY> ( [ x1 .. Int Int ] -- x1 .. xN-2 Int )
MY> Which may or may be useful, but consider the program:
MY> unlist0 == [ dup first 0 = not ] [ uncons ] while pop
MY> Here, the resultant types on the stack depend on the *values* already on the
MY> stack, not just the program itself.
MY> ISTM that any type system which is intended to describe arbitrary Joy programs
MY> must have at least equal expressive power as Joy itself thus making analysis of
MY> it non-computable. Alternatively we need something which isn't simply an
MY> adaptation of lambda related type systems.
MY> Louis Madon described a mechanism for partitioning the stack into regions based
MY> on analysis of the program, and this may be enough. I suspect not, but who
MY> knows?
Excuse me for big quote, but I should disagree with you.
You take a different approach than my, you think someone should
typecheck any program without any restriction. I think I should
typecheck programs that I seem as typecheckable and has some required
properties. One such property is undestandable stack space consumtion.
Another property is understandable grammar of list
creation/separation.
("If sequence has no structure then it still has grammar, but this
grammar is meaningless." - quote from book I read this time. "Parsing
Techniques - A Practical Approach",
http://www.cs.vu.nl/~dick/PTAPG.html)
I treat "understandable" in wide sense - as everything realizable. If
some genius implement understanding of context-sensitive grammar I
will be more than happy. ;) And if it will be context-sensitive
grammar of stack space consumtion...
>> But when I thought about use of lists I come into interesting problem.
>> What to expect when taking apart head and tail from list?
MY> 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.
MY> Indeed, and I'd suggest that this is ultimately non-computable without forcing
MY> the arity of every Joy word.
This is not bad thing as it may seem in first sight.
I read PhD thesis on Forth systems and author (Piter Knaggs - I can
find this PhD if you're interested) said that variable number of items
on stack is not a good style of programming and often indicate an
error.
Again your first example is meaningless alone - without words before
and after it. It may be rewritten using list reversal - lists are kind
of stacks, from my point of view. This will consume fixed number of
items on stack and code generator (if one will arise) could use
knowledge about list prepresentation to optimize access.
>> How, for example, not to put empty list as splitlist argument? Guard
>> it with checking for emptyness? Then how to (automatically) strip
>> that check?
MY> Good question. How does Haskell optimise away such guards?
Why only Haskell? It is applicable for many languages.
Consider simple filtering problem:
filter (a:as) (b:bs) = a*b+filter as bs
filter [] _ = 0
filter _ [] = 0
If both lists have at least one element then multiply their heads and
add to result of filtering rest of them. If either list is empty -
return 0.
If I construct list A using something like [1..7] and construct
another list using [21..27] then both lists have equal number of
elements (arity? shape?) and at least one check could be stripped.
In case of list representation using arrays it became simple and
straightforward loop. And it will be even more elegant for
architectures like ADSP-21xx where circular buffers supported by
hardware.
Everything we need is the proof that implementation of filter always
get lists of equsl size and structure. Very simple. ;)
Buy!
sz mailto:
sz@...