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

On Sun, Apr 20, 2008 at 12:45 AM, John Nowak <[email protected]> wrote:
>
>
> 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)

In Cat:

\f.[42 f apply "hello" f apply pair]

Or without:

dup 42 swap apply swap "hello" swap apply pair

This is typable.

However this problem of a straightforward application of HM to Cat
occurs even in

[1] dup

as we discussed previously.

The problem is outlined in detail in my most recent technical report:
http://www.cat-language.com/Cat-TR-2008-001.pdf

> This, however, is:
>
>    (let ((f id)) (cons (f 42) (f "hello")))
>
> Forgive me if I'm telling you what you already know.

Yep. No worries though.

> > 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'll refer you again to the technical report for this.

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

Thank you for finding that. The problem is a bug in the unification of
self types with type variables. I should be able to solve this by
simply choosing type variables over "self" types.

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

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.

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

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

This was never explained properly until the new technical report.

Cheers,
Christopher