Some thoughts on Object Cat
Christopher Diggins
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 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
latte
I'm only a newbie, but that syntax looks good! I think it's simple
and intuitive - the "field?" and "field!" approach immediately
reminded me of Ruby (not that I've done a lot of coding in that
either...).
The creating of an object is good too, as is adding a field. The one
thing I'd mention as a small change is maybe renaming "field" to
"method". That seems a little more OO-ish, and is what Ruby uses
iirc.
Christopher Diggins
Thanks for the pointer.
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.
Thanks everyone for their help and suggestions!
Christopher Diggins
Hi Andy,
Thanks for the encouragement.
The "field?" is actually a general form of instruction, where "field"
is the literal name of the field.
For example:
"object 12 x+ 13 y+ x?" would leave the value "12" on the stack. The
"x?" queries an object for a particular field (or method) in pushes it
on the stack.
However, and this may be what you are actually pointing out and I am
simply misunderstanding, there is indeed a problem with the term
"field", because I can add both functions and non-function values to
an object in this way. The more correct term would probably be "slot".
Cheers,
Christopher
latte
On Apr 20, 3:05 am, "Christopher Diggins" <cdigg...@gmail.com> wrote:
Ahh... ok, that's interesting - thanks for that!
I have to admit that in mentioning the term "method", I was only
thinking of the name. I hadn't actually thought further ( of the "use-
case" of adding both functions and non-function values to the
object... ). "Slot" sounds like a good name though.
- Andy
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 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 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 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
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
Colin
>
> (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).
(A string b -> A string b) require at least two elements on the stack,
but (A b -> A b) is the type of a function that can be called with
just one element on the stack?
Ciao, Colin
John Nowak
>> 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
Christopher Diggins
> > 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.
Just to be fair, I made an incorrect analysis. I'm currently examining
the problem in more depth.
Moved conversation off of concatenative, since I don't think the
concatenative group cares that much about the type system of Cat.
- Christopher
Trans
language will support object polymorphism, and if it supports that
then you should be able to use per-object operations --of course these
operands should be "reserved", sure. But still why all the special
syntax? Just have two commands, one for set and one for get. I don;t
think you need a "create" command --is there any reason for 'set' not
to create the field if it doesn't already exist? So...
>> object 0 "x" !
>> object "x" ?
T.
Christopher Diggins
> language will support object polymorphism, and if it supports that
> then you should be able to use per-object operations --of course these
> operands should be "reserved", sure. But still why all the special
> syntax? Just have two commands, one for set and one for get. I don;t
> think you need a "create" command --is there any reason for 'set' not
> to create the field if it doesn't already exist? So...
>
> >> object 0 "x" !
> >> object "x" ?
>
> T.
Hi Trans,
You are correct that we could do just what you specify. The problem is
that object polymorphism, also called ad-hoc polymorphism, can not be
verified at compile-time. The goal is to have a core type system that
is polymorphic and fully verifiable at compile-time, that we can also
extend later with dynamic object-oriented features.
Concerning the syntax, the goal was to express the fact that in
languages where there is no dynamic field lookup (e.g. C++) then
object "x" ! would not be legal, because "x" could be any string
generated at run-time, preventing us from verifying the types
statically. A similar issue arises when distinguishing between "set"
and "add", because I want "set" to fail at compile-time, in the cases
where we are dealing with a more restricted object model.
I hope this clear it up a bit?
- Christopher
Trans
T.
Trans
> In the quest to add objects to Cat I am thinking of doing some rather
> strange things.
want to add objects to Cat?
In large part objects are sort of an illusion. With the exception of
creating isolated scopes, there's nothing much to be gained. In an
object system, the actual operation applied depends on the class of
the receiver-object. In a functional system one can just view the
initial argument to a function as that receiver -- so (as per my
previous thread) if we could make multi-dispatch definitions we would
in effect have the same thing, and then some.
Also, is there more to this then what you suggesting here. From the
looks of it it seems like a static hash lookup type, rather than OOP.
Where does 'self' come in, and inheritance, etc.?
I just get the feeling that adding honest to goodness OOP to Cat will
only serve to harm the current elegance of the language. I'd mcuh
rather see multi-dispatch, and protected scopes instead --which cover
all the important basis of OOP w/o all the additional complexity.
T.
John Nowak
On Apr 23, 2008, at 12:24 PM, Trans wrote:
> I just get the feeling that adding honest to goodness OOP to Cat will
> only serve to harm the current elegance of the language. I'd mcuh
> rather see multi-dispatch, and protected scopes instead --which cover
> all the important basis of OOP w/o all the additional complexity.
It depends how flexible the object system is. Ad hoc polymorphism with
multiple dispatch is implemented in Haskell via type classes.
Unfortunately, type classes have a huge design space and several
(unsolved) problems. A single-dispatch mechanism of comparable
dynamism would be much simpler.
A good paper to look at here is Wadler's "A Section Look at
Overloading" that describes a restricted form of type classes that
avoids many of the issues present in Haskell (albeit by restricting
what type classes are able to do):
http://homepages.inf.ed.ac.uk/wadler/topics/type-classes.html
- John