Some thoughts on Object Cat

[Christopher Diggins]

In the quest to add objects to Cat I am thinking of doing some rather
strange things.

==

1) Adding a new instruction to create an object:

  object : ( -> object)

2) Adding a new instruction form (any word ending with '+') to
indicate adding a field to an object:

  field+ : ('o 'a -> 'o+field:'a)

This is so that I can support prototype-style object oriented programming.

3) Adding a new instruction form (any word ending with '?') to
indicate a field getter

   field? : ('o -> 'o 'o.field)

4) Adding a new instruction form (any word ending with '!') to
indicate a field setter

  field! : ('o 'o.field -> 'o)

==

So here is how it would look:

  >> object
  stack: ()
  >> 0 x+
  stack: (x=0)
  >> 0 y+
  stack: (x=0,y=0)
  >> 12 x!
  stack: (x=12,y=0);
  >> x? 30 + y!
  stack: (x=12, y=42)

I love to hear any comments or suggestions. I am really not happy with
the syntax of types for adding fields (#2), but it seems like a
neccessary evil.

Christopher Diggins
http://www.cdiggins.com

[LittleDan]

In this system, is there any polymorphism over field names? It looks
like there isn't really. Also, how do you plan to support prototype
OO? In Io, for example, you might do

something := Object clone
something slot := value

But in Cat, or at least the subset I know about, you can only define
procedures, not variables in this way. How do you plan to get around
this?

Dan

On Fri, Apr 18, 2008 at 2:13 PM, Christopher Diggins <cdiggins@...> wrote:

>
>
>
>
>
>
> In the quest to add objects to Cat I am thinking of doing some rather
>  strange things.
>
>  ==
>
>  1) Adding a new instruction to create an object:
>
>  object : ( -> object)
>
>  2) Adding a new instruction form (any word ending with '+') to
>  indicate adding a field to an object:
>
>  field+ : ('o 'a -> 'o+field:'a)
>
>  This is so that I can support prototype-style object oriented programming.
>
>  3) Adding a new instruction form (any word ending with '?') to
>  indicate a field getter
>
>  field? : ('o -> 'o 'o.field)
>
>  4) Adding a new instruction form (any word ending with '!') to
>  indicate a field setter
>
>  field! : ('o 'o.field -> 'o)
>
>  ==
>
>  So here is how it would look:
>
>  >> object
>  stack: ()
>  >> 0 x+
>  stack: (x=0)
>  >> 0 y+
>  stack: (x=0,y=0)
>  >> 12 x!
>  stack: (x=12,y=0);
>  >> x? 30 + y!
>  stack: (x=12, y=42)
>
>  I love to hear any comments or suggestions. I am really not happy with
>  the syntax of types for adding fields (#2), but it seems like a
>  neccessary evil.
>
>  Christopher Diggins
>  http://www.cdiggins.com
>  

[John Cowan]

Christopher Diggins scripsit:

> 1) Adding a new instruction to create an object:
>
>   object : ( -> object)
>
> 2) Adding a new instruction form (any word ending with '+') to
> indicate adding a field to an object:

+1

> 3) Adding a new instruction form (any word ending with '?') to
> indicate a field getter

To me, a "?" suffix indicates a predicate (number? list? string?).  Find some
other character.

> 4) Adding a new instruction form (any word ending with '!') to
> indicate a field setter

+1

--
John Cowan      http://www.ccil.org/~cowan      cowan@...
Be yourself.  Especially do not feign a working knowledge of RDF where
no such knowledge exists.  Neither be cynical about RELAX NG; for in
the face of all aridity and disenchantment in the world of markup,
James Clark is as perennial as the grass.  --DeXiderata, Sean McGrath

[Christopher Diggins]

On Fri, Apr 18, 2008 at 4:42 PM, Daniel Ehrenberg <microdan@...> wrote:

>
>
> In this system, is there any polymorphism over field names? It looks
> like there isn't really. Also, how do you plan to support prototype
> OO? In Io, for example, you might do
>
> something := Object clone
> something slot := value
>
> But in Cat, or at least the subset I know about, you can only define
> procedures, not variables in this way.
>
> How do you plan to get around
> this?

I don't know IO so I have to assume your code translates to the
following ECMAScript

  something = new Object();
  something.slot = value;

I was thinking this would translate to

  object value slot+

Considering something more general

  something = new Object();
  something.slot = 42;
  ...
  something.slot = "hello";

Would become:

  object 42 slot+ ... "hello" slot+

What is a little weird is that "slot+" can allow us to override
"slots" at run-time which is what we in a prototype-based language.

The "slot!" syntax would be used when we are sure the slot already
exists. (e.g. converting to Cat from Java) and want a type error, when
the slot can't be found statically.

What I am lacking is to distinguish between a getter that always works
(returning "undefined" when not found) and another that causes a type
error.

- Christopher

[Christopher Diggins]

An alternative syntax is:

slot.get // gets the slot, throws type error if unrecognized
slot.set // sets the slot, throws type error if unrecognized
slot.exists // queries if the slot exists
slot.add // adds a new slot of the given type, overwriting existing slots

- Christopher

> Christopher Diggins scripsit:
>
>
> > 1) Adding a new instruction to create an object:
> >
> > object : ( -> object)
> >
> > 2) Adding a new instruction form (any word ending with '+') to
> > indicate adding a field to an object:
>
> +1
>
> > 3) Adding a new instruction form (any word ending with '?') to
> > indicate a field getter
>
> To me, a "?" suffix indicates a predicate (number? list? string?). Find some
> other character.
>
>
> > 4) Adding a new instruction form (any word ending with '!') to
> > indicate a field setter
>
> +1
>
> --
> John Cowan http://www.ccil.org/~cowan cowan@...
> Be yourself. Especially do not feign a working knowledge of RDF where
> no such knowledge exists. Neither be cynical about RELAX NG; for in
> the face of all aridity and disenchantment in the world of markup,
> James Clark is as perennial as the grass. --DeXiderata, Sean McGrath
>
>
>
> Messages in this topic (3) Reply (via web post) | Start a new topic
> Messages | Files | Photos | Links | Database | Polls | Members | Calendar
>
> Change settings via the Web (Yahoo! ID required)
> Change settings via email: Switch delivery to Daily Digest | Switch format
> to Traditional
> Visit Your Group | Yahoo! Groups Terms of Use | Unsubscribe
>
>
> Recent Activity
>
>  1
> New MembersVisit Your Group
>
> Yahoo! Finance
>
> It's Now Personal
>
> Guides, news,
>
> advice & more.
> Change your life
>
> with Yahoo! Groups
>
> balance nutrition,
>
> activity & well-being.
> Cat Fanatics
>
> on Yahoo! Groups
> Find people who are
> crazy about cats.

[Christopher Diggins]

On Fri, Apr 18, 2008 at 4:42 PM, Daniel Ehrenberg <microdan@...> wrote:
>
> In this system, is there any polymorphism over field names? It looks
> like there isn't really.

I forgot to respond to this question. What do you mean exactly?

In Cat we use the bottom type "any" for dynamic polymorphism.

As for other kinds of polymorphism, we can write:

define new_pair { object swap dup first+ second+ }

In which case the type is:

new_pair : ('a -> object(x:'a y:'a))

Sorry for switching type syntax mid-conversation, but it occured to me
that this new syntax would be a lot easier to understand.

Does this answer your question about polymorphism over names?

- Christopher

[William Tanksley, Jr]

John Cowan <cowan@...> wrote:
> Christopher Diggins scripsit:
>  > 3) Adding a new instruction form (any word ending with '?') to
>  > indicate a field getter
> To me, a "?" suffix indicates a predicate (number? list? string?).  Find some
>  other character.

Forth uses @ as a suffix for getting. So does J (the APL derivative), IIRC.

While I'm responding, I might as well ask: have you studied Io, Self,
Darwin, and ECMAScript for ideas and guidance on this? Darwin
(http://javalab.cs.uni-bonn.de/research/darwin/project.html) would
seem especially useful for someone concerned with type safety, and its
site also includes an _excellent_ warning against a common mistake
that many people fall into when dealing with prototypes (people often
confuse _delegation_ and _consultation_; see
http://javalab.cs.uni-bonn.de/research/darwin/delegation.html.

-Wm

[John Nowak]

On Apr 18, 2008, at 3:13 PM, Christopher Diggins wrote:

> In the quest to add objects to Cat I am thinking of doing some rather
> strange things.
> ...
> This is so that I can support prototype-style object oriented  
> programming.

You want extensible polymorphic records with first class labels; that  
will get you very close to prototype-based OO in the style of a  
language like Io.

There are quite a few good papers out there if you search google and  
citeseer. I particularly like the work by Daan Leijen (http://research.microsoft.com/users/daan/pubs.html 
). The types themselves aren't hard to manage, but efficient  
compilation generally is.

- John

P.S. Any reason we're all ignoring the reply-to header?

[John Nowak]

On Apr 18, 2008, at 6:01 PM, Christopher Diggins wrote:

> On Fri, Apr 18, 2008 at 4:42 PM, Daniel Ehrenberg  
> <microdan@...> wrote:
>>
>
>> In Io, for example, you might do
>
> I don't know IO

You must learn Io before tackling a new prototype system. In  
particular, you must be aware of all of the problems inherent in Io's  
system. You must look at Self as well if you've not already.

There's also another very interesting prototype language that's quite  
different from Io and Self called Kevo. There's very little  
information about it available, but what's there is worth looking at.  
In short, it does away with delegation. All objects are self-
sufficient and new objects are created through the composition of  
existing objects. Objects have creation-time sharing, not lifetime  
sharing. It's very much in line with Wittgenstein's writings on  
prototypes.

I did a fair bit of work (all evaporated) on prototype-based languages  
before working on Fifth. It does seem that we tend to be attracted to  
similar approaches.

- John

[Christopher Diggins]

On Sat, Apr 19, 2008 at 2:34 AM, John Nowak <john@...> wrote:

>
> On Apr 18, 2008, at 6:01 PM, Christopher Diggins wrote:
>
> > On Fri, Apr 18, 2008 at 4:42 PM, Daniel Ehrenberg
> > <microdan@...> wrote:
> >>
> >
> >> In Io, for example, you might do
> >
> > I don't know IO
>
> You must learn Io before tackling a new prototype system. In
> particular, you must be aware of all of the problems inherent in Io's
> system. You must look at Self as well if you've not already.

I should be clear that I am not trying to design an entire prototype
system but simply introduce the minimal building blocks of one. The
very narrow problem I have is converting JavaScript into Cat, and I
want to do this with minimal changes.

> There's also another very interesting prototype language that's quite
> different from Io and Self called Kevo. There's very little
> information about it available, but what's there is worth looking at.
> In short, it does away with delegation. All objects are self-
> sufficient and new objects are created through the composition of
> existing objects. Objects have creation-time sharing, not lifetime
> sharing. It's very much in line with Wittgenstein's writings on
> prototypes.
>
> I did a fair bit of work (all evaporated) on prototype-based languages
> before working on Fifth. It does seem that we tend to be attracted to
> similar approaches.

Thank you for all the suggestions, I will look at those languages.

Cheers,
Christopher

[John Nowak]

On Apr 19, 2008, at 10:58 AM, Christopher Diggins wrote:

> One paper caught my eye
> "http://research.microsoft.com/users/daan/download/papers/hmf-tr.pdf"
> which talks about impredicative instantiation. This is interesting
> because it is precisely the problem we talked about previously, and
> that Colin Hirsch pointed out to me even earlier. I didn't realize
> that the solution was not so well known. I actually do not use the HM
> type inference algorithm.

(I assume the problem you're talking about is writing things like the  
'm' combinator.)

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.

For example, rather than defining 'm = dup i' and giving 'm' some  
restrictive equi-recursive type (or requiring a type signature for a  
higher rank type), we can simply make 'm' a macro. If we then did  
'[swap] m', it would expand to '[swap] dup i' before doing type  
inference, and we'd get the type 'A b -> A [C d e -> C e d] b' as a  
result.

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. However, we if were to say 'poly' is just a macro that  
expands to that same definition, it'll work fine provided that poly is  
used in cases where the type of the function given to poly is knowable  
in the current context.

(Brief note: The definition for 'apply2' is just 'rot dup dip dip'  
which we can easily see by factoring it out of the above definition  
for 'poly'. Note however that 'apply2' must be a macro otherwise it'll  
require both values passed to it to be of the same type!)

There's something else nice about allowing these simple expansion  
macros; you may have already noticed. In Cat, you cannot split any  
definition into two as sometimes the types will get in the way. In the  
example below, 'baz' may not type check even though 'foo' does, or  
alternatively 'baz' my type check but in a way that then prevents you  
from writing 'qux' (such as if 'baz' were given an overly-restrictive  
equi-recursive type):

    foo = a b c d e
    bar = a b c
    baz = d e
    qux = bar baz

However, if we have these simple macros, we can make 'baz' a macro and  
be guaranteed that the type of 'qux' will be the same as the type of  
'foo'. Essentially, these macros let you hand-wave away the problem  
that your type system is not "compositional" by allowing the user to  
do the composition later in the process.

This approach won't let you write possibly infinitely recursive  
definitions with 'm', as you will hit the occurs check when the  
function passed to 'm' tries to duplicate and call itself, but this is  
actually something I depend on in my system for sound termination  
checking. You might seriously consider not allowing things like 'm' to  
be a feature as it allows you to trivially track possible non-
termination on the type level (no type system extensions are necessary).

- John

[Christopher Diggins]

On Sat, Apr 19, 2008 at 11:56 PM, John Nowak <john@...> wrote:

>
>
> On Apr 19, 2008, at 10:58 AM, Christopher Diggins wrote:
>
> > One paper caught my eye
> > "http://research.microsoft.com/users/daan/download/papers/hmf-tr.pdf"
> > which talks about impredicative instantiation. This is interesting
> > because it is precisely the problem we talked about previously, and
> > that Colin Hirsch pointed out to me even earlier. I didn't realize
> > that the solution was not so well known. I actually do not use the HM
> > type inference algorithm.
>
> (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. It seems that nested
polymorphism is a tricky kettle of fish for modern type theory.
However my naive approach (which works really well) is to rename
generic variables as I go, and defining forall qualification to be on
the inner-most function that is possible.

I solved the "dup apply" (or "dup i", god I hate using "i" to mean
application) problem by reintroducing "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.
>
> For example, rather than defining 'm = dup i' and giving 'm' some
> restrictive equi-recursive type (or requiring a type signature for a
> higher rank type), we can simply make 'm' a macro. If we then did
> '[swap] m', it would expand to '[swap] dup i' before doing type
> inference, and we'd get the type 'A b -> A [C d e -> C e d] b' as a
> result.

That is elegant, but at the same time would cost me the benefit of
being able to split definitions at will.

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

> However, we if were to say 'poly' is just a macro that
> expands to that same definition, it'll work fine provided that poly is
> used in cases where the type of the function given to poly is knowable
> in the current context.
>
> (Brief note: The definition for 'apply2' is just 'rot dup dip dip'
> which we can easily see by factoring it out of the above definition
> for 'poly'. Note however that 'apply2' must be a macro otherwise it'll
> require both values passed to it to be of the same type!)
>
> There's something else nice about allowing these simple expansion
> macros; you may have already noticed. In Cat, you cannot split any
> definition into two as sometimes the types will get in the way.

This was true in the earlier version, but with the recent
reintroduction of "self" types this is no longer a problem.

> In the
> example below, 'baz' may not type check even though 'foo' does, or
> alternatively 'baz' my type check but in a way that then prevents you
> from writing 'qux' (such as if 'baz' were given an overly-restrictive
> equi-recursive type):
>
>    foo = a b c d e
>    bar = a b c
>    baz = d e
>    qux = bar baz
>
> However, if we have these simple macros, we can make 'baz' a macro and
> be guaranteed that the type of 'qux' will be the same as the type of
> 'foo'. Essentially, these macros let you hand-wave away the problem
> that your type system is not "compositional" by allowing the user to
> do the composition later in the process.
>
> This approach won't let you write possibly infinitely recursive
> definitions with 'm', as you will hit the occurs check when the
> function passed to 'm' tries to duplicate and call itself, but this is
> actually something I depend on in my system for sound termination
> checking. You might seriously consider not allowing things like 'm' to
> be a feature as it allows you to trivially track possible non-
> termination on the type level (no type system extensions are necessary).
>
> - John

I need "m" in order to allow Cat implementation to disallow explicit
recursion if they want, and so that I can perform automated generation
of Cat code from other languages.

You may be interested that coming up real soon is a draft of a brand
new paper describing the Cat type-system and type-inference algorithm
in detail. No more getting rejected from conferences for me, this is
going to be a technical-report! :-)

Cheers,
Christopher

[John Nowak]

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)

This, however, is:

    (let ((f id)) (cons (f 42) (f "hello")))

Forgive me if I'm telling you what you already know.

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

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

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

- John

[Christopher Diggins]

On Sun, Apr 20, 2008 at 12:45 AM, John Nowak <john@...> 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

[John Nowak]

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

[Christopher Diggins]

On Sun, Apr 20, 2008 at 5:02 AM, John Nowak <john@...> wrote:

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

Thank you very much for identifying these problems John. I believe
they all can be tracked down to implementation bugs, and I will
attempt to fix them straight away!

- Christopher Diggins