On Jun 17, 2008, at 8:03 PM, William Tanksley, Jr wrote:
> John Nowak <john@...> wrote:
>
>> Say I write this definition for a combining form:
>> foo(a, b) = [a, b]
>> If cleave is type-directed, there's no way to give this a type. You'd
>> need to require an annotation in such a case.
>
> I don't get it. Can you provide a specific counterexample where this
> doesn't receive a type?
Ah, I knew I didn't explain that properly (well, at all really). Let
me recap briefly so I can be sure I've covered it.
Factor has a family cleave combinators like bi, tri, etc, which I
assume you're familiar with (otherwise this may not make any sense).
Here is the type of 'bi' in 5th:
bi(A b -> C, C b -> D) => A b -> D
What this says is that bi takes one function of type 'A b -> C' and
one of type 'C b -> D' and yields a function of type 'A b -> D'.
(Remember that 'bi' is a combining form (aka functional) in 5th, so it
takes functions as arguments and yields a function as a result.) The
type of 'tri' is just an extension of the type of 'bi':
tri(A b -> C, C b -> D, D b -> E) => A b -> E
Factor has a combinator named 'cleave' that generalizes these. For
example, instead of writing '[ a ] [ b ] [ c ] tri', you can write
'{ [ a ] [ b ] [ c ] } cleave'. 5th can handle cleave properly. To be
clear on the translation:
bi(a, b) = cleave(a, b) = keep(a) b
tri(a, b, c) = cleave(a, b, c) = keep(a) keep(b) c
Factor also has the combinators '2bi' and '2tri'. These save and push
on the top two elements for each quotation rather than just one. The
types are as follows (forgive me if I'm stating the obvious):
2bi(A b c -> D, D b c -> E) => A b c -> E
2tri(A b c -> D, D b c -> E, E b c -> F) => A b c -> F
And the equalities:
2bi(a, b) = 2cleave(a, b) = 2keep(a) b
2tri(a, b, c) = 2cleave(a, b, c) = 2keep(a) 2keep(b) c
Now, for a brief digression. Factor also has 'bi@' 'tri@' combinators.
Appending the "@" means that the same function is used for all cases:
bi@(a) = cleave(a, a) = keep(a) a
tri@(a) = cleave(a, a, a) = keep(a) (a) a
To type these properly, we need to use intersection types:
bi@(A b -> C /\ C b -> D) => A b -> D
tri@(A b -> C /\ C b -> D /\ D b -> E) => A b -> E
If you want, I can get into the reason this is necessary. For now,
back on track.
An important thing to note about 'cleave' and '2cleave' is that they
don't care at all what the arities of the functions are; they push on
one (or two, in the case of '2cleave') elements for each quotation
regardless. For example, these are all equivalent:
5 cleave(neg, *) = 5 bi(neg, *) = 5 keep(neg) * = 5 neg 5 * = -25
Alright, now onto the "type-directed cleave". Agh, so much to say.
I came up with the idea for a type-directed cleave when trying to
figure out the concatenative equivalent of the functional form of
"construction" from Backus's FP. What construction does is take
several functions and some 'x' and return an array of all of the...
well, I'll just show it:
[neg, sqr, sqrt]:9
[neg:9, sqr:9, sqrt:9]
[-9, 81, 3]
It turns out that construction is the same as the normal 'cleave':
9 cleave(neg, sqr, sqrt)
9 neg 9 sqr 9 sqrt
-9 81 3
In FP, there's no way to have something like '2cleave'. What you need
to do is bundle the two arguments into an array and use a combination
of construction and "insert" (which is the same as 'foldl1' in
Haskell, i.e. a fold with the head of the list as the initializer). To
be clear, the slash denotes the "insert":
[/+, /-, /*]:<5, 3>
[/+:<5, 3>, /-:<5, 3>, /*:<5, 3>]
[5 + 3, 5 - 3, 5 * 3]
[8, 2, 15]
This works, but the downside is the need to explicitly use insert for
each function. The equivalent in 5th using cleave is rather ugly (and
grossly inefficient):
(5, 3) cleave(reduce(+), reduce(-), reduce(*))
(5, 3) reduce(+) (5, 3) reduce(-) (5, 3) reduce(*)
5 3 + 5 3 - 5 3 *
8 2 15
Hence, we have '2cleave', which doesn't require the bundling and
inserting/reducing of the FP and 'cleave' versions:
5 3 2cleave(+, -, *)
5 3 + 5 3 - 5 3 *
8 2 15
Anyway, the point of the "type-directed cleave" was to be able to
write ' 5 3 [+, -, *]' and have it magically work. Of course, in order
to know how many items to copy and push on for each function, you need
to know their arities. There are *three* ways you can go about doing
this.
The first way is to require all functions have the same arity (at
least in terms of what they consume -- the productions don't matter).
This works great for the '[+, -, *]' example, but it's a bit
restrictive.
The second way is to allow each function to have a different arity. In
order to figure out how many items to save, you save as many as
necessary for the function with the greatest arity. For example:
2 3 4 [+, dup, rot]
2 3 4 + 2 3 4 dup 2 3 4 rot
2 7 2 3 4 4 3 4 2
The third way is the most bizarre, but perhaps the most useful. What
you do is save as many items as necessary for the function with the
greatest arity. However, for each function, you only push on as many
items as it directly uses. For example:
2 3 4 [+, dup, rot]
3 4 + 4 dup 2 3 4 rot
7 4 4 4 2 3
Of the three, the third possibility, I think, is the most useful; the
second is awkward to use in many cases and the first is just a special
case of the second and third.
Now, there are a couple things to point out here.
With the normal 'cleave', as shown earlier, we can do things like '5
cleave(neg, *)' to get '-25. This is impossible with any of the type-
directed variants above. This isn't really a big problem however as '5
cleave(neg, *)' is really misusing 'cleave'. It should be written as
'5 keep(neg) *' instead.
The other, and much more important thing thing to note, is that it is
impossible to figure out how many items to save and push on for the
first two type-directed variants unless at least one function is
provided. In other words, you can't give a rewrite rule or any sort of
dynamic semantics for this definition of 'foo':
foo(a, b) = [a, b]
However, with the first two type-directed variants, you could for this
definition of 'bar':
bar(a, b) = [a, b, +]
The rewrite rule here would be 'x y (a, b) = x y a x y b'. Again,
without the additional context given via '+', there's no way to do
this for the first two type-directed variants.
For the third type-directed variant, there's no way to give a dynamic
semantics unless *all* functions are provided. As interesting as this
third variant is, it is just too powerful to include in the language.
Of the three, only the first is really sensible. In that case however,
all it does is save you a character so that you can avoid specifying
the arity of the quotations.
I don't think saving that character is worth the clutter in the
language definition. It would mean you can't look at the type system
as merely a means of restricting the dynamic semantics of the
language. This is the same nasty situation Haskell is in with respect
to type classes. Type classes, however, at least provide some real
expressive powerful.
To very briefly clarify on what I mean about the type system no longer
simply restricting the language, I'll give a brief example. Let's say
we write something like this:
id1 = dup drop
id2 = swap swap
All 'id1' does is ensure one element is on the stack. All 'id2' does
is ensure two elements are on the stack. On a stack with many items,
they're identical. However, when using them in a type-directed cleave,
they have different properties. For example, '1 2 3 type-cleave(id1,
id1)' is not the same as '1 2 3 type-cleave(id2, id2)', even though
they would be with a normal cleave.
It should hopefully be obvious now that, since a type-directed cleave
is essentially meaningless unless sufficient context is given, that we
also can't type it without that same context. I hope it is also clear
why I said in the previous email that they're almost certainly a bad
idea. I apologize for taking the *long* way to get to this conclusion,
but I'm far too tired to write something concise.
- John