Concatenative languages, like Forth, have a convention of annotating word definitions with stack effects. For example, if a word like +== pops two things from the stack as "inputs" and pushes one as an "output," you would write a "type signature" (actually just a comment) such as ==( a a -- a ).
A newcomer to concatenative languages might see this and try to interpret these comments as type signatures that the interpreter can check against existing words every time a word is defined. However, this quickly breaks down for words essential to the DIY character of Forth, and necessary for productivity in most other such languages as well.
How far can such stack effect typechecking go before a language ceases to be concatenative?
What if it pops or puts a variable amount of elements?
>>2
Yes, that is part of the problem. Does a type system have to forbid that, or what?
I tried real hard with that formatting. Still haven't mastered it.
>>3
The types of elements popped by word have to follow some rule. Of course you could probably make a word where the most simple way to describe that rule would be the word itself, and I don't know how a type system would handle that. Checking all possible inputs would quickly break down, so I'd assume it would be similar to proving the theorem that the wrong types could never be passed in given the rest of the program. Maybe someone smarter than me could think of something.
>>4
I thought of something. The compiler should be able to determine a lower bound for how many stack slots will be popped, and how many will be pushed, for any word defined in terms of primitives with known variable stack effects. It could do something as simple as inserting runtime checks before and after these primitives based on the requirements of whatever precedes and follows the variable effect. Not foolproof, but at least it moves a stack underflow error closer to the word that causes it.
>>5
Maybe useful, but does that even count as a type system?
>>6
It needs to be accounted for by any attempt to make a concatenative language that has a type system, especially if the contents of the stack can be said to have types.
It seems to me that a concatenative language could be expressed as a form of function composition f∘g∘h∘... of words, with a recursive stack as their domain; for example + : Num Num [Stack] -> Num [Stack], so that we can match inputs and outputs of adjacent words. Checking the type would be a matter of keeping track of the type of the stack at al times, and to verify that at any point the word in question matches the input.
I don't think variable arguments and dynamic typing could work in this system. Maybe overloaded type signatures, or union types.
Doesn't Factor has some sort of type system?
>>9
Dynamic typing, whereas FORTH is basically untyped
Interesting.
Forth is fantastic. I really need to spend some time learning it.
https://github.com/cesarblum/sectorforth/
Scheme is the Forth of Lisps.
whenever i read the word <forth> i read <fortran>
i do not know why
>>14
Forthtran when
ForthLisp when
>>17
Forth is such a great language!
>>18
Indeed.
>>17
Great. Now we need LispForth.
>>17
Neato.
https://github.com/schani/forthlisp/blob/master/lisp.fs