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

Hi John,

Great eye for these problems!

I think we should start a list and call them the Nowak type-inference tests. ;-)

> 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.

> 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.

dup dip : (A (A -> B) -> B (A -> B))

Is fine, and exactly what we expect, but when we compose with "dip"

dip : (C d (C -> E) -> E d)

We get the following type:

dup dip dip : (A (A -> B) -> E d)

and the following constraints:

C = A
E = B
A = C d

Notice that C = A = C d is a pardox and should be rejected. It is a
bug in my type checker that I don't catch this.

> 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.

Again, same problem as above. "dup dip dip" is not actually typable.

>  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?

When composing terms it makes a big difference.
http://research.microsoft.com/users/daan/download/papers/hmf-tr.pdf
points out that they are indeed not the same thing.

> The 'quote' function does not require (or even
> benefit from) higher rank types.

Yes it does. Try implementing Cat in haskell without it. Kablooie!

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

> 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.

That is a bug again. The issue is related to the fact that two functions:

(A int b -> A int b)
and
(A string b -> A string b)

was deemed impossible to unify, however there is a set of functions
that would satisfy both constraints which I overlooked, those with
type:

(A b -> A b).

> 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

I'll try to address these issues in the next release ASAP.
Christopher