Christopher Diggins — 2006-11-08 17:15:46

Cat version 0.9.7 has been posted to http://www.cat-language.com/downloads.html

The latest Cat version introduces a significant new change: stack
state descriptors now describe the stack reading left to right, where
the left most element is the top of the stack. The documentation
doesn't reflect this yet, except for the documentation on primitives
(http://www.cat-language.com/primitives.html).

A subtle but important new addition is the inclusion of linear
recursion combinator, which allows you to write recursive functions.
The Cat type inference algorithm currently can't handle
self-referential functions, but you implement recursive algorithms
using "rec".

Here is an example of the factorial program:

>> define f { [dup 1 <=] [*] [pop 1] [dup --] rec }

inferred type for program 'f' as ( int ) -> ( int )
main stack: _empty_

>> 5 f

main stack: 120

>> 6 f

main stack: 120 720

The type of the rec combinator is interesting (at least I thought so):

(
(A:any*)->(A A) // argument relation
(A)->(B:any*) // on termination
(A B)->(B) // result relation
(A)->(bool A) // termination condition
A // input
)->(B)

That's it for now, more to come soon.
Christopher

William Tanksley, Jr — 2006-11-09 00:54:23

Christopher Diggins <cdiggins@...> wrote:

> The latest Cat version introduces a significant new change: stack
> state descriptors now describe the stack reading left to right, where
> the left most element is the top of the stack. The documentation
> doesn't reflect this yet, except for the documentation on primitives
> (http://www.cat-language.com/primitives.html).

Why was this done? It's your language and your right, but this is
backwards from how most other notations show the stack (and backwards
from how things would be pushed on the stack). Is it more efficient to
implement? I could see that being the case...

Anyhow, very nice.

> Christopher

-Billy

Christopher Diggins — 2006-11-09 01:30:04

Hi Billy,

Thanks for the compliment and the feedback. Efficiency wasn't a concern of
mine, the issue I encountered was while working on a paper to describe the
type system that the stack state descriptor (i.e. everything between two
parantheses) mapped directly to the concept of a tuple in the ML based
languages. I found myself having to explain that Cat types were tuples
written backwards, but didn't feel I had a strong justification for such a
break from convention (at least from the POV of type theory).

There is also the issue of when you introduce type variables into the mix.
In the old way type variable declarations would have to appear in the
rightmost position. For example previously the type of dup was:

dup : (A A:any) -> (A)

Now it is:

dup : (A:any A) -> (A)

Which I find easier to explain to people when talking about type variables.

However, I have my doubts. I have trouble peering into the minds of other
programmers.
Do you think I made things more or less muddled, by changing the order of
types?

Anyone else have feedback?

Thanks again,
Christopher

[Non-text portions of this message have been removed]

William Tanksley, Jr — 2006-11-09 03:22:51

Christopher Diggins <cdiggins@...> wrote:

> Thanks for the compliment and the feedback. Efficiency wasn't a concern of
> mine, the issue I encountered was while working on a paper to describe the
> type system that the stack state descriptor (i.e. everything between two
> parantheses) mapped directly to the concept of a tuple in the ML based
> languages. I found myself having to explain that Cat types were tuples
> written backwards, but didn't feel I had a strong justification for such a
> break from convention (at least from the POV of type theory).

I'm a little confused -- ML isn't stack-based, so the choice of
ordering for stack notation can't be related to ML's tuple notation.
If an ML person asks, tell them that the stack grows and tuples don't,
so the notation is different.

HOWEVER, I do think that the community you're working for does matter.
If you're hoping to profit from the experience of ML programmers (a
worthy goal), and they truly do need to see the stack written the
other way, then I'm all for that. I'm just not seeing the reason why
they'd want the stack the other way. Is it possibly related to how you
explained it?

> There is also the issue of when you introduce type variables into the mix.
> In the old way type variable declarations would have to appear in the
> rightmost position. For example previously the type of dup was:

> dup : (A A:any) -> (A)
> Now it is:
> dup : (A:any A) -> (A)
> Which I find easier to explain to people when talking about type variables.

*This* I certainly agree with; the first one is much clearer. However,
it's different from what I recall about ML. Doesn't ML allow the
programmer to place type annotations almost anywhere in the
definition? If Cat had that capability, the direction of the notation
wouldn't matter at all.

It's also interesting to me that the notation appears *all* backwards.
I expect to see the input on the left and the output on the right. I
would expect dup's stack effect to look like "(A:any) -> (A A)", and I
find the direction of the arrow a little surprising as well. I
*suspect* that the other notation is more convenient for a reader
expecting the parameters for a function to appear after the function.
In postfix and concatenative languages, things flip around... And
maybe the notation should as well.

> However, I have my doubts. I have trouble peering into the minds of other
> programmers.
> Do you think I made things more or less muddled, by changing the order of
> types?
> Anyone else have feedback?

I'll stand back now and let someone else speak up... :-)

> Christopher

-Billy

Christopher Diggins — 2006-11-09 04:43:55

On 11/8/06, William Tanksley, Jr <wtanksleyjr@...> wrote:

> Christopher Diggins <cdiggins@...> wrote:
> > Thanks for the compliment and the feedback. Efficiency wasn't a concern of
> > mine, the issue I encountered was while working on a paper to describe the
> > type system that the stack state descriptor (i.e. everything between two
> > parantheses) mapped directly to the concept of a tuple in the ML based
> > languages. I found myself having to explain that Cat types were tuples
> > written backwards, but didn't feel I had a strong justification for such a
> > break from convention (at least from the POV of type theory).
>
> I'm a little confused -- ML isn't stack-based, so the choice of
> ordering for stack notation can't be related to ML's tuple notation.

But to relate the Cat type system to the ML type system, I do so by
explaining that a function is a mapping from a pair of tuples to a
pair of tuples.

> If an ML person asks, tell them that the stack grows and tuples don't,
> so the notation is different.

The functional view of Cat is that it doesn't actually cause stacks to
grow or shrink, but each function maps to a new pair of stacks. The
fact that most implementations do in fact have two global stacks which
grow and shrink is an implementation detail. I believe one of
Manfred's papers discusses this. So semantically a stack is in fact a
tuple.

> HOWEVER, I do think that the community you're working for does matter.
> If you're hoping to profit from the experience of ML programmers (a
> worthy goal), and they truly do need to see the stack written the
> other way, then I'm all for that.
>
> I'm just not seeing the reason why
> they'd want the stack the other way. Is it possibly related to how you
> explained it?

Yes it is. When I finish the paper, my rationale should make more sense.

> > There is also the issue of when you introduce type variables into the mix.
> > In the old way type variable declarations would have to appear in the
> > rightmost position. For example previously the type of dup was:
>
> > dup : (A A:any) -> (A)
> > Now it is:
> > dup : (A:any A) -> (A)
> > Which I find easier to explain to people when talking about type variables.
>
> *This* I certainly agree with; the first one is much clearer. However,
> it's different from what I recall about ML. Doesn't ML allow the
> programmer to place type annotations almost anywhere in the
> definition?

I am not sure, but the Cat annotations differ from any other language
I know of in their behaviour.

> If Cat had that capability, the direction of the notation
> wouldn't matter at all.
>
> It's also interesting to me that the notation appears *all* backwards.
> I expect to see the input on the left and the output on the right. I
> would expect dup's stack effect to look like "(A:any) -> (A A)", and I

What a silly mistake I made! Sorry about that.

The type of dup in Cat is in fact:

dup: (A:any)->(A A)

The type of eval (roughly Joy's i operator) should be more illustrative:

eval: ((A:any*)->(B:any*) A)->(B)

Thanks for your contributions to the discussion!
Christopher

William Tanksley, Jr — 2006-11-09 18:12:11

Christopher Diggins <cdiggins@...> wrote:

> William Tanksley, Jr <wtanksleyjr@...> wrote:
> > Christopher Diggins <cdiggins@...> wrote:
> > > languages. I found myself having to explain that Cat types were tuples
> > > written backwards, but didn't feel I had a strong justification for such a
> > > break from convention (at least from the POV of type theory).

> > I'm a little confused -- ML isn't stack-based, so the choice of
> > ordering for stack notation can't be related to ML's tuple notation.

> But to relate the Cat type system to the ML type system, I do so by
> explaining that a function is a mapping from a pair of tuples to a
> pair of tuples.

Okay.

> > If an ML person asks, tell them that the stack grows and tuples don't,
> > so the notation is different.

> The functional view of Cat is that it doesn't actually cause stacks to
> grow or shrink, but each function maps to a new pair of stacks. The
> fact that most implementations do in fact have two global stacks which
> grow and shrink is an implementation detail. I believe one of
> Manfred's papers discusses this. So semantically a stack is in fact a
> tuple.

Good point, and I agree, but the type notation doesn't show the entire
stack; it only shows the top few items. Therefore, the *way* in which
you show the items _must_ be independant of how you think about the
stack. Given that, it seems to me that it would be wiser to describe
it to users as what it is, a stack effect notation, rather than as
what its underlying data structure might be (a tuple).

And listing the items with the final top-of-stack on the right makes
sense, because that's the order you'd have to write literals of the
given type in order to fulfill that stack effect notation. I can't
think of *any* interpretation of writing it the other way around; I
still don't understand why ML programmers would expect to see it that
way.

> > I'm just not seeing the reason why
> > they'd want the stack the other way. Is it possibly related to how you
> > explained it?

> Yes it is. When I finish the paper, my rationale should make more sense.

After I finish this reply, then, I'll fall silent and wait for your paper.

> > It's also interesting to me that the notation appears *all* backwards.
> > I expect to see the input on the left and the output on the right. I
> > would expect dup's stack effect to look like "(A:any) -> (A A)", and I

> What a silly mistake I made! Sorry about that.

Oh! Okay, that makes sense.

> The type of dup in Cat is in fact:
> dup: (A:any)->(A A)

Makes sense (but I see why you did it that way -- it's a rather boring
operator :-).

> The type of eval (roughly Joy's i operator) should be more illustrative:
> eval: ((A:any*)->(B:any*) A)->(B)

Yes, it is. Thank you. In fact I see that it's a great example of some
problems you've no doubt run into -- if that function were to be
written (using your notation) as:

eval: (A:any* (A)->(B:any*))->(B)

It's clear that it would be ambiguous, since the stack has an
unbounded number of items before you get to the function, whose type
tells you how many items are acceptable (and one of those items might
well be another function whose types happen to match the types above
it!).

Now, if we switch to my notation we get:

eval: (A (A:any*)->(B:any*))->(B)

...which has the disadvantage of requiring a complete parse of the
type in order to determine what types A can acquire (but that might
make ML users happier, since it allows them to place the type
annotations anywhere they want, as they're used to doing with ML).

Either that, or the variable initializer can scan the stack notation
from right to left when it's looking for variable type
initializations, and you'd therefore be requiring the type annotation
to appear in the element closest to the top of stack (just as your
notation requires now). It would be a little more complex to implement
than your current solution, though (but not as complex as allowing the
programmer to place annotations just anywhere).

> Thanks for your contributions to the discussion!

I'm learning from you. Thank you.

> Christopher

-Billy