Some thoughts on Object Cat
Christopher Diggins — 2008-04-18 19:13:18
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
Daniel Ehrenberg — 2008-04-18 20:42:43
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 — 2008-04-18 21:23:01
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 — 2008-04-18 22:01:59
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 — 2008-04-18 22:12:05
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 — 2008-04-18 22:23:13
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 — 2008-04-18 23:05:56
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 — 2008-04-19 06:21:01
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 — 2008-04-19 06:34:08
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 — 2008-04-19 15:00:07
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 — 2008-04-20 03:56:43
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 — 2008-04-20 04:12:20
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 — 2008-04-20 04:45:09
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 — 2008-04-20 07:00:01
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 — 2008-04-20 09:02:45
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 — 2008-04-20 16:06:09
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
Christopher Diggins — 2008-04-20 17:53:32
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
John Nowak — 2008-04-20 22:29:48
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
Manfred Von Thun — 2008-04-23 09:10:10
On 20/4/08 2:12 PM, "Christopher Diggins" <
cdiggins@...> wrote:
>
>
>
> On Sat, Apr 19, 2008 at 11:56 PM, John Nowak <john@...
> <mailto:john%40johnnowak.com> > 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.
In Joy at least, the i combinator does not mean application. Joy is a
concatenative language, not an applicative language. The applicative
languages are the lambda calculus and the combinatory calculus,
together with their descendents just about all programming languages
descend from the lambda calculus. All applicative languages have an
apply operation: apply this function to those arguments, but mostly there
is no explicit symbol for that operation. Joy does not have such an
operation
neither explicit nor implicit.
The i combinator in Joy is pretty much the same as the eval function in
Lisp. It undoes what the the (pseudo-) function quote does. In Lisp this
is true about expressions X (which denote objects):
> (eval(quote(X)) = X
And in Joy this is true about expressions X (which denote
stack-to-stack functions)
> [X] i = X
so the i combinator undoes what the quotation brackets do. Lisp¹s eval
and Joy¹s i are sometimes called dequotation operators. But they are
quite different from application. (Many books on Lisp have an example
program which is a Lisp interpreter written in Lisp. The two principal
parts are eval and apply and they are very different.)
All other Joy combinators are variations on the eval-theme. Some
enterprising Lisp programmer might write variations on the eval-theme
in Lisp at least for those combinators that do not depend on Joy¹s
stack semantics. One example would be a map-eval, quite different
from the (second order) map function which many books will give as
examples.
- Manfred
[Non-text portions of this message have been removed]
Christopher Diggins — 2008-04-23 15:40:42
Hi Manfrred,
> > I solved the "dup apply" (or "dup i", god I hate using "i" to mean
> > application) problem by reintroducing "self" types.
>
> In Joy at least, the i combinator does not mean application. Joy is a
> concatenative language, not an applicative language.
>
> The applicative
> languages are the lambda calculus and the combinatory calculus,
> together with their descendents just about all programming languages
> descend from the lambda calculus. All applicative languages have an
> apply operation: apply this function to those arguments, but mostly there
> is no explicit symbol for that operation. Joy does not have such an
> operation neither explicit nor implicit.
Joy does not have an "implicit" apply operation, but "i" most
definitely is the explicit "apply" operation, if we are to consider
expressions as functions from stacks to stacks. This is because "i"
takes a stack-to-stack function off of the stack and applies it to the
rest of the stack.
> The i combinator in Joy is pretty much the same as the eval function in
> Lisp. It undoes what the the (pseudo-) function quote does.
That's not quote correct. (eval (quote (1 2 3))) is meaningless in Lisp
Anyway, this is where the confusion slips in, you are using the model
of quotes are expressions, and then quotes are functions. Depending on
what model you want to use to explain the semantics of Joy, it makes a
big difference. If you continued throughout with the understanding
that a quote is a function I think it would be quite clear, that
"dequoting" is really applying the function to the stack.
> In Lisp this
> is true about expressions X (which denote objects):
>
> > (eval(quote(X)) = X
>
> And in Joy this is true about expressions X (which denote
> stack-to-stack functions)
>
> > [X] i = X
>
> so the i combinator undoes what the quotation brackets do.
Another way of understanding what is happening is that you are
applying the stack-to-stack transform function to the stack.
> Lisp¹s eval
> and Joy¹s i are sometimes called dequotation operators.
This is the jargon of the Lisp programmer though, and is not
represenative of the actual mathematics being performed. Using the
term "dequotation" is distracting, because it implies something that
is happening differently than function application. My point is that
you can't say "X is a function from a stack to stack", but then say we
"eval it". This is because "eval" has no well-defined sense in
mathematics when it comes to functions.
> But they are
> quite different from application. (Many books on Lisp have an example
> program which is a Lisp interpreter written in Lisp. The two principal
> parts are eval and apply ‹ and they are very different.)
>
> All other Joy combinators are variations on the eval-theme. Some
> enterprising Lisp programmer might write variations on the eval-theme
> in Lisp at least for those combinators that do not depend on Joy¹s
> stack semantics. One example would be a map-eval, quite different
> from the (second order) map function which many books will give as
> examples.
>
> - Manfred
- Christopher Diggins
John Nowak — 2008-04-23 18:00:16
On Apr 23, 2008, at 5:10 AM, Manfred Von Thun wrote:
> In Joy at least, the i combinator does not mean application. Joy is a
> concatenative language, not an applicative language. The applicative
> languages are the lambda calculus and the combinatory calculus,
> together with their descendents – just about all programming languages
> descend from the lambda calculus. All applicative languages have an
> apply operation: apply this function to those arguments, but mostly
> there
> is no explicit symbol for that operation. Joy does not have such an
> operation neither explicit nor implicit.
Are concatenative languages not just a particular kind of applicative
language? It seems to me that there's no real difference between this:
foo = 1 2 + *
And this (where '1' and '2' are functions of type 'A -> A Num' as
above):
foo stack = * (+ (2 (1 stack)))
Of course, because Joy is a restricted form of applicative language,
you can reason about things in ways you can't in the general case.
Perhaps there's something more fundamental I'm missing here that makes
Joy non-applicative.
- John
William Tanksley, Jr — 2008-04-23 18:38:59
John Nowak <
john@...> wrote:
> Manfred Von Thun wrote:
> > In Joy at least, the i combinator does not mean application. Joy is a
> > concatenative language, not an applicative language. The applicative
> > languages are the lambda calculus and the combinatory calculus,
> > together with their descendents – just about all programming languages
> > descend from the lambda calculus. All applicative languages have an
> > apply operation: apply this function to those arguments, but mostly
> > there
> > is no explicit symbol for that operation. Joy does not have such an
> > operation neither explicit nor implicit.
> Are concatenative languages not just a particular kind of applicative
> language? It seems to me that there's no real difference between this:
> foo = 1 2 + *
> And this (where '1' and '2' are functions of type 'A -> A Num' as
> above):
> foo stack = * (+ (2 (1 stack)))
I suppose the key word in "no real difference" is "real". See
http://en.wikipedia.org/wiki/No_true_Scotsman. Clearly there's a
difference -- trivially, the two are reverses; less trivially, one of
them includes grouping operators that aren't present in the other; and
critically, those grouping operators happen to serve to distinguish
between an operator and its operands.
> Of course, because Joy is a restricted form of applicative language,
> you can reason about things in ways you can't in the general case.
> Perhaps there's something more fundamental I'm missing here that makes
> Joy non-applicative.
I think your example serves well enough, even though it doesn't
actually include an example of an operand which is not ALSO an
operator.
> - John
-Wm
zallambo — 2008-04-23 20:29:36
--- In
concatenative@yahoogroups.com, "Christopher Diggins"
<cdiggins@...> wrote:
>
> Hi Manfrred,
>
> > > I solved the "dup apply" (or "dup i", god I hate using "i" to mean
> > > application) problem by reintroducing "self" types.
> >
> > In Joy at least, the i combinator does not mean application. Joy is a
> > concatenative language, not an applicative language.
> >
> > The applicative
> > languages are the lambda calculus and the combinatory calculus,
> > together with their descendents just about all programming languages
> > descend from the lambda calculus. All applicative languages have an
> > apply operation: apply this function to those arguments, but
mostly there
> > is no explicit symbol for that operation. Joy does not have such an
> > operation neither explicit nor implicit.
>
> Joy does not have an "implicit" apply operation, but "i" most
> definitely is the explicit "apply" operation, if we are to consider
> expressions as functions from stacks to stacks. This is because "i"
> takes a stack-to-stack function off of the stack and applies it to the
> rest of the stack.
>
> > The i combinator in Joy is pretty much the same as the eval
function in
> > Lisp. It undoes what the the (pseudo-) function quote does.
>
> That's not quote correct. (eval (quote (1 2 3))) is meaningless in Lisp
Evaluating (eval (quote (1 2 3))) gives precisely the same result as
evaluating (1 2 3) - an error. Consider instead (eval (quote (+ 2 3))),
which yields 5, as expected. In general, evaluating (eval (quote X))
always
gives the same result as evaluating X.
> Anyway, this is where the confusion slips in, you are using the model
> of quotes are expressions, and then quotes are functions. Depending on
> what model you want to use to explain the semantics of Joy, it makes a
> big difference. If you continued throughout with the understanding
> that a quote is a function I think it would be quite clear, that
> "dequoting" is really applying the function to the stack.
>
> > In Lisp this
> > is true about expressions X (which denote objects):
> >
> > > (eval(quote(X)) = X
> >
> > And in Joy this is true about expressions X (which denote
> > stack-to-stack functions)
> >
> > > [X] i = X
> >
> > so the i combinator undoes what the quotation brackets do.
>
> Another way of understanding what is happening is that you are
> applying the stack-to-stack transform function to the stack.
Well said. I think Joy can be viewed as purely concatenative - as the
composition of functions, or as applicative - a series of unary functions
from stacks to stacks that will be applied in order. The former is
probably
preferable when reasoning about the language. But realistically it is
implemented as an applicative language.
> > Lisp¹s eval
> > and Joy¹s i are sometimes called dequotation operators.
>
> This is the jargon of the Lisp programmer though, and is not
> represenative of the actual mathematics being performed. Using the
> term "dequotation" is distracting, because it implies something that
> is happening differently than function application. My point is that
> you can't say "X is a function from a stack to stack", but then say we
> "eval it". This is because "eval" has no well-defined sense in
> mathematics when it comes to functions.
Here are my thoughts about "apply" vs "eval". Consider just operands and
operators. In lisp, eval and apply behave like this:
(eval operand) -> operand
(eval (f a1 a2)) -> (apply f '(a1 a2))
(apply f '(a1 a2)) -> (f (eval a1) (eval a2))
But with a global stack instead of parameters and everything being a
function, we get:
(eval f) -> (apply f stack)
(apply f) -> (f stack)
Since everything is a function, eval always invokes apply and apply always
applies the function to the global stack. There is no longer any real
difference between their roles. Instead, evaluating a sequence of
expressions becomes much more important.
In lisp, you can "compose" functions by concatenating them in a global
scope
or within a 'begin' expression. This does compose the side effects of the
functions, but it is not very useful in lisp because the result that the
sequence produces is just the result of the last expression. But if
instead
functions only produced side-effects on a stack and did not return
results,
this would become true composition.
So I would say that, describing concatenative languages in terms of lisp,
'eval' and 'apply' are unified, but the procedure that 'i' corresponds
to is really an improved version of 'eval-sequence' (as SICP calls it)
that
applies a sequence of functions onto a stack.
> > But they are
> > quite different from application. (Many books on Lisp have an example
> > program which is a Lisp interpreter written in Lisp. The two principal
> > parts are eval and apply and they are very different.)
> >
> > All other Joy combinators are variations on the eval-theme. Some
> > enterprising Lisp programmer might write variations on the eval-theme
> > in Lisp at least for those combinators that do not depend on Joy¹s
> > stack semantics. One example would be a map-eval, quite different
> > from the (second order) map function which many books will give as
> > examples.
> >
> > - Manfred
>
> - Christopher Diggins
>
Justin
John Cowan — 2008-04-23 20:45:56
zallambo scripsit:
> Evaluating (eval (quote (1 2 3))) gives precisely the same result as
> evaluating (1 2 3) - an error. Consider instead (eval (quote (+ 2 3))),
> which yields 5, as expected. In general, evaluating (eval (quote X))
> always gives the same result as evaluating X.
In the top-level lexical environment that is. Eval does not have access
to the lexical environment from which it is invoked.
I think the confusion arises because Christopher thinks of [foo] as a
function, whereas in Joy it is a list of functions, and only a function
because everything in Joy can be treated as a function. So the effect
of applying the function [foo] to stack S is that we get S [foo] as the
new stack. The i function does not apply a function to the rest of
the stack, but evaluates in turn all the functions in the list at the
top of the stack, thus implicitly composing them.
--
John Cowan
cowan@...
I amar prestar aen, han mathon ne nen,
http://www.ccil.org/~cowan
han mathon ne chae, a han noston ne 'wilith. --Galadriel, LOTR:FOTR
Christopher Diggins — 2008-04-23 22:14:13
Emphasis mine:
> ... So the effect of *applying* the function [foo] to stack S is that we get S [foo] as the
> new stack.
And the effect of calling "i" afterward is the same as applying the
function "foo" to the stack S.
> The i function does not apply a function to the rest of the stack, but evaluates in turn all the functions in the list at the top of the stack, thus implicitly composing them.
These two approaches are not incompatible. There are two equally valid
semantic views of a Joy program: compose all functions then apply the
resulting function to the empty stack, or apply each of the functions
to the stack in sequence.
// My approach
S x0 [x1 x2] i == (x2.x1)(x0(S))
// Your approach
S x0 [x1 x2] i == ((x2.x1).x0)(S)
It is important to note that evaluating a Joy program ultimately
requires an application at the top level. This is because the output
of a Joy program is a stack, not a function.
- Christopher
John Cowan — 2008-04-24 16:29:20
Christopher Diggins scripsit:
> These two approaches are not incompatible. There are two equally valid
> semantic views of a Joy program: compose all functions then apply the
> resulting function to the empty stack, or apply each of the functions
> to the stack in sequence.
Indeed. It's the mark of a concatenative language that eval is compose
followed by apply, but that doesn't mean that eval *is* apply except in
the degenerate case where there is only one function to compose.
--
A poetical purist named Cowan [that's me:
cowan@...]
Once put the rest of us dowan. [on xml-dev]
"Your verse would be sweeter
http://www.ccil.org/~cowan
If it only had metre
And rhymes that didn't force me to frowan." [overpacked line!] --Michael Kay
Christopher Diggins — 2008-04-24 17:31:45
On Thu, Apr 24, 2008 at 12:29 PM, John Cowan <
cowan@...> wrote:
> Christopher Diggins scripsit:
> > These two approaches are not incompatible. There are two equally valid
> > semantic views of a Joy program: compose all functions then apply the
> > resulting function to the empty stack, or apply each of the functions
> > to the stack in sequence.
>
> Indeed. It's the mark of a concatenative language that eval is compose
> followed by apply, but that doesn't mean that eval *is* apply except in
> the degenerate case where there is only one function to compose.
I am talking about "i" in terms of what it does as a stack
transformation function, where whitespace denotes composition (an
important detail is that it denotes composition within brackets as
well as outside), and "[...]" is an abstraction operation (i.e. a
lambda, and not some kind of informal notion of "quotation"). You
appear to be focusing on the particular implementation details in a
Lisp style language. Here is what I understand that you have in mind
for an evaluator in pseudo-code:
S x = (apply x S)
S [x0 x1 ... xN] = (cons (quote (x0 x1 ... xN)) S)
S i = (eval (car x) (cdr s))
That is of course a valid implementation of Joy.
However it obscures what is happening from a mathematical standpoint
when Joy expressions are expressed as functions on stacks. This is why
so far people keep switching between formal mathematical concepts like
"application" and "composition" and then jumping into a completely
different notions of "eval", "quote", "dequote" within the same
paragraph.
The following semantics more accurately represent what happens from a
pure mathematical standpoint and demonstrate the meaning of "i" that I
am trying to explain:
S x = (apply x S)
S [x0 x1 ... xN] = (cons (compose (x0 ... xN)) S)
S i = (apply (car x) (cdr s))
Where:
(define (compose x . xs)
(if (null? xs)
x
(lambda (S) (apply (compose (car xs) (cdr xs)) (apply x S)))))
Finally I will point out that the following are both valid
interpretation of "S x y"
S x y = (apply x (apply y S))
S x y = (apply (compose x y) S)
My apologies, but this has to be my last post on the subject. This
discussion has already consumed too much of my time, and I sense a
strong unwillingness to understand what I am patiently trying to
explain.
- Christopher