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

On Apr 20, 2008, at 3:00 AM, Christopher Diggins wrote:

>> I'm simply suggesting the addition of (concatenative) macros. They
>> don't come at the cost of any existing properties.
>
> Yes, you are correct. They don't cost anything, I mispoke. I meant
> that they don't solve the problem of wanting to cut a program at an
> arbitrary point which is a desirable property for me.

Ah, but they do solve it; you can cut at an arbitrary point provided  
that you're willing to make the right side of the cut a macro if  
necessary. This isn't a wonderful solution of course, but it does at  
least guarantee that you'll be able to do such a thing if it's useful  
and the type system would otherwise prevent it.

Cat, however, does *not* solve this problem. Let me give you an  
example of where Cat falls down. Take this function:

    foo = dup dip dip       // A (A -> A b) -> A b b

Cat gives 'foo' the correct type (although it's a rather unfortunate  
one). Now let's examine another function:

    bar = [id] dup dip dip  // A b c -> A b c

Cat also gives this the correct type. Note that the 'dup dip dip' used  
in 'bar' is the definition of 'foo'. So what would happen if we  
substituted 'foo' into 'bar'?

    baz = [id] foo          // A b b -> A b b b b !?

Cat gives this a completely bogus type. (Fifth correctly rejects this  
function due to an occurs check.) However, if you were to make 'foo' a  
macro instead, 'baz' would yield the same type as 'bar' as the  
expansion would be equivalent.

>>> But we've got higher-rank types in Cat.
>>
>> Really? Where? As far as I can tell, Cat is restricted to rank-1  
>> types.
>
> For example:
>  quote : (A b -> A (C -> C b))
> If we explicitly add forall quantifiers we get:
>  quote : !A.!b.(A b -> A !C.(C -> C b))

How is that, in effect, any different from having all quantifiers at  
the outermost level? The 'quote' function does not require (or even  
benefit from) higher rank types. If Cat truly had higher rank types,  
you'd be able to write something like this:

    qux = "hi" swap dup dip 5 swap apply

However, Cat will give an error about the string and int constraints  
not being compatible. However, if we were to go ahead and supply the  
function directly, there's no problem:

    blort = [id] "hi" swap dup dip 5 swap apply

Cat correctly gives this function the type 'A -> A String Int'. This  
is yet another example of how you cannot arbitrarily split expressions  
in Cat. If you could, 'qux' would be typeable since 'blort' is typeable.

If Cat actually had rank-2 types, it would be able to assign 'qux'  
this type:

    qux :: forall A. A [forall B. B -> B] -> A String Int

- John