Re: [stack] Re: Some thoughts on Object Cat

On Apr 20, 2008, at 12:12 AM, Christopher Diggins wrote:

>> (I assume the problem you're talking about is writing things like the
>> 'm' combinator.)
>
> No, I was referring to the "ambiguous impredicativity" problem of
> dealing with polymorphism that he refers to.
> ...
> However my naive approach (which works really well) is to rename
> generic variables as I go,

Does this go beyond the equivalent of let-polymorphism in HM? For  
example, with HM types, this is not allowed (where 'id' is the  
identify function of type 'a -> a'):

    (define (bar f) (cons (f 42) (f "hello")))
    (bar id)

This, however, is:

    (let ((f id)) (cons (f 42) (f "hello")))

Forgive me if I'm telling you what you already know.

> and defining forall qualification to be on the inner-most function  
> that is possible.

Can you please elaborate here? In HM, quantifiers can only appear at  
the outermost level. I'm not sure what you mean by saying Cat's  
quantifiers are for the *innermost* level.

> I solved the "dup apply" (or "dup i", god I hate using "i" to mean
> application) problem by reintroducing "self" types.

I'm not sure I'd say you solved it. For example, in Cat beta 4,  
'[swap] m' is given the type 'A b -> A self b'. This type makes  
absolutely no sense; the second element on the stack after calling  
this is the 'swap' function, and 'swap' does not have type 'A b -> A  
self b'. In fact, this type for 'swap' only requires one element be on  
the stack to call it! If I do '[swap] dup apply' however, I do get the  
correct type (as you would if 'm' were a macro).

Either your 'self' mechanism is bugged or I'm not reading the type  
correctly.

>> Another solution (or stop-gap solution, depending on how you look at
>> it) is to allow definitions to defer type checking. Essentially,
>> instead of declaring a function, you declare that some word expands  
>> to
>> some other words.
>
> That is elegant, but at the same time would cost me the benefit of
> being able to split definitions at will.

I'm simply suggesting the addition of (concatenative) macros. They  
don't come at the cost of any existing properties.

>> Another example is the 'poly' function given on page two of the HMF
>> paper. In a concatenative language, we could define 'poly' as '1 True
>> rot dup dip dip mk-tuple2'. (There are better ways to write this,
>> namely using an 'apply2' combinator, but I'm ignoring that for
>> simplicity.) In any case, this will fail to type check without higher
>> rank types.
>
> But we've got higher-rank types in Cat.

Really? Where? As far as I can tell, Cat is restricted to rank-1 types.

- John