Re: [stack] stackless fixed-arity concatenative languages

On Thu, May 22, 2008 at 2:38 AM, John Nowak <[email protected]> wrote:
>
> On May 22, 2008, at 2:03 AM, John Nowak wrote:
>
>> There are probably others as well. The huge issue here is that none of
>> these types are instances of another! If you believe Cat could
>> eventually type 'dup dip dip' in a satisfactory manner, what type
>> would you want to give it? As far as I can tell, without a system that
>> delays typing as necessary such as the one I've hinted at recently, it
>> isn't possible to give a most general type even with annotations.
>> Maybe a system with intersection types could do it.
>
> Slava has suggested this intersection type for 'bi@':
>
> bi@ :: A b (A -> C /\ C b -> D) -> D
>
> This is a rather interesting type. It only requires one element on the
> stack below the quotation; it applies the quotation to whatever is
> below the top element, then applies it again to whatever the first
> quotation did with 'b' added to the top. When using two (or more)
> elements below the quotation, it is not required that they be of the
> same type. This is a very general type that would cover all uses I can
> think of.
>
> The downside, of course, is that the purpose of 'bi@' is not clear
> from the type. Additionally, many misuses of 'bi@' would not be caught
> until possibly much later. Still, the generality is appealing.
>
> The kind people on #concatenative also pointed out that 'dup dip dip'
> behaves differently than the version of 'bi@' in Factor because it
> applies the quotation to 'y' first, not 'x'. In an impure language,
> these are obviously not equivalent. A definition that matches the
> semantics of 'bi@' in Factor is 'dup [ dip ] dip call', or '[ dip ]
> keep call'.
>

Well, there actually is a difference in semantics in a pure language,
in the arities involved. Your bi@ can be used with a quotation of the
type ( b c -- d ) for an overall type of ( b c b c -- d d ) whereas
Factor's cannot. On the other hand, Factor's bi@ can be used for ( b
-- c d ) for an overall type of  ( b b -- c d c d ) whereas yours
cannot (though it could be used for ( b -- b c ) as ( b b -- b c c ).
The type of dup dup dip might be something more like  A b (A -> C e /\
C -> D) -> D e

Dan