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

On Apr 20, 2008, at 1:53 PM, Christopher Diggins wrote:

>> 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.
>
> Still, I'd rather try to construct a type-system that doesn't  
> prevent it.

You can do so quite easily. If you assume all type variables are non- 
free, you will never be able to construct a function that cannot be  
cut at any point. Doing so however implies a loss of generality as  
'[id] dup' yields the type 'A -> A (B -> B) (B -> B)'. In short, this  
sucks.

Doing so in a way that doesn't require this restriction is a real  
problem. I don't believe it will be possible without requiring  
annotations in some cases (as inference for non-finite rank  
polymorphism is undecidable even with intersection types), but I'd be  
very happy to be proven wrong.

>> 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
>
> This is where the bug occurs. Such a thing should be rejected
> straight-away by the type-checker.

That's incorrect. Cat (beta 4) gives 'dup dip dip' the type 'A (A -> A  
b) -> A b b', and Fifth does as well. While this type looks bizarre  
(which is why I said it is unfortunate), as it prevents you from doing  
'[id] foo', it's completely reasonable. For example, the expression  
'[42] foo' will be given the correct type of 'A -> A Int Int'.

It is possible to give 'foo' the type of 'A b b (_ b -> _ b) -> A b  
b', where '_' is an inaccessible portion of the stack (i.e. the  
function passed to 'foo' is *not* row polymorphic), but Fifth will  
require an annotation to do so. This gets back to an issue I've  
brought up before which is that Cat has no way to enforce that a  
function will use no more than N elements of the stack. If you can  
enforce this (restricting N to 1 in this case), you can give 'foo' a  
useful type ('foo' is actually an 'apply2' of sorts).

>> The 'quote' function does not require (or even
>> benefit from) higher rank types.
>
> Yes it does. Try implementing Cat in haskell without it. Kablooie!

One can write 'quote' in Haskell without higher rank types:

    quote :: a -> (() -> a)
    quote x = \u -> x

I realize that's not exactly the same as Cat's 'quote', but it seems  
equivalent. The reason one cannot write Cat in Haskell is a lack of  
row polymorphism. I've challenged quite a few people to implement the  
basics of Cat in Haskell, which they initially thought possible, but  
they eventually agreed that row polymorphism is necessary.

> In simple terms: Cat (given a correct implementation) allows us to
> have polymorphic functions on the stack.

I believe this is just equivalent to let polymorphism. What Cat can't  
do is give a function a type that indicates it *requires* a  
polymorphic function. For example, there's no way to write these  
functions in Cat (be sure to invoke ghci with the -XRank2Types option):

    -- incredibly useless; call with (\x -> head []) or something
    blarg :: (forall a b. a -> b) -> c
    blarg f = const (f 5) (f "hi")

    -- slightly less than incredibly useless; call with 'id'
    yargh :: (forall a. a -> a) -> (Int, String)
    yargh f = (f 5, f "hi")

- John