possibilities for macros in a typed language

[John Nowak]

Recently, I've been thinking about what sort of macro system might be  
suitable for a typed concatenative language. For this discussion, I'll  
assume a language like Cat minus any form of locals/variables. I'll  
call this hypothetical language 'Kitten' from this point on.

Adding macros to Kitten seems fairly easy at first as the syntax is  
easily representable as a list and there are no variables to get in  
the way. Given that adding macros is fairly easy, it seems worth doing  
if they'd be truly useful.

But are they? In Lisp, macros are most commonly used for two reasons.  
The first is a lack of a concise syntax for anonymous functions, but  
this isn't an issue in Kitten. The second is dealing with bindings and  
binding constructs (SET!, etc), but this also isn't an issue. There  
are other uses of macros, but these two probably comprise 90% of the  
use cases.

What other uses then might macros have in Kitten? One use I've come up  
with is allowing a way to write constructs that would otherwise be un-
typeable. For an example, the m combinator 'dup i' cannot be assigned  
a type for the same reason that '\x -> x x' cannot be assigned a type  
in Haskell; it requires the construction of an infinite type. (Cat's  
version of 'i' is called 'apply' I believe.)

Even though 'dup i' isn't typeable, expressions like '[swap] [swap] i'  
and '[dup] [dup] i' are. Accordingly, we could define a macro like  
'[$A] m => [$A] [$A] i' that would work with quote literals. Such a  
macro is writable in a simple declarative system similar to Diggins's  
MetaCat (http://www.cat-language.com/metacat.html), although I believe  
MetaCat isn't currently usable for such things.

Another deficiency of the type system is a lack of number  
parameterized types. As such, you can't write a function like 'ndup'  
that duplicates the top N values on the stack. With an appropriate  
macro system however, you could expand '3 ndup' to a typeable  
construct. You would need something more powerful than MetaCat to do  
so however.

Optimization is another use of macros (as MetaCat shows). Slava Pestov  
recently walked me through some of the more interesting use cases of  
macros for optimization in Factor as well; 'case' is a good example.

There are of course additional, more complex uses. One example would  
be a macro that translates code that uses locals to code that's  
pointfree. Another might be pattern matching. It's not clear if there  
are sufficiently many of such use cases to warrant the addition of a  
macro system as opposed to simply adding a few additional core  
syntactic constructs.

There are obviously downsides to macros as well. Firstly, you  
sacrifice something in terms of concatenativity. For example, 'A B C  
D' might not be decomposable into 'A B' and 'C D' if macros are  
involved. You also lose something in terms of consistency as  
constructors like 'm' would only be usable with function literals and  
not functions passed at runtime. Finally, you lose the "everything is  
a function" aspect of Kitten. In Kitten, even the literal '3' is  
really a function with the type 'A -> A int'. Similarly, '[dup]' is a  
function with the type 'A -> A (B c -> B c c)'. Macros eliminate this  
property, although perhaps some syntactic means of distinguishing  
macros and functions could help.

Macros are a huge design space. It seems to me that there are  
essentially four possibilities for such a system in Kitten:

1. Offer a MetaCat-like system, perhaps with some additional  
expressivity. This covers a fair chunk of the optimization cases very  
simply and it's declarative nature means that you don't need to write  
macros that cooperate with the type system. (Of course the result of  
the rewriting needs to be typeable.) It also allows for 'm' and  
perhaps other more difficult combinators (condnestrec?) to be  
integrated, at least when dealing with literals.

2. Offer a somewhat Lisp-like system where macros are pure functions  
of the type '[parse-entity] -> [parse-entity]'. This allows more  
flexibility than the MetaCat system, although pointfree syntactic  
manipulation is likely to be more complicated in practice. It is also  
likely to be a good deal more verbose as you'll either need to be  
deconstructing and reconstructing parse-entity sums or casting into  
and out of some universal type.

3. Take the Factor approach and offer proper parse words and  
everything derivable from them. Again, this seems like even more  
flexibility at the cost of even more complexity. I'm not too  
interested in this approach for a language like Kitten; it makes a lot  
of sense for Factor though.

4. Offer no macro system whatsoever as the possibilities aren't worth  
the downsides. Something like MetaCat would be integrated directly  
into the system for purposes of optimization only and wouldn't be  
exposed to the user.

Of course, you could always just use Joy and get runtime macros for  
free!

Many thanks if you've managed to keep reading this long. If anyone has  
thoughts on what an ideal macro system for a Kitten-like language  
might be, or even if such a system is useful, they'd be much  
appreciated.

- John

[John Nowak]

Taking this a step further...

Let's start with Kitten (Cat minus locals). Now let's also remove  
recursive definitions. In such a language, any definition is  
equivalent to its finite expansion. In other words, for every place  
the function 'f' is used, replacing 'f' with its definition will not  
alter the meaning of the program.

If we do this, writing a program would consist of writing a series of  
rewrite rules. For example, if we do 'sqr = dup *', then every time  
'sqr' is encountered, we can replace it with 'dup *'. (If the  
implementation actually does this or decides to call 'sqr' instead  
isn't interesting; the results are equivalent.)

But why stop there? What if we allow rewrite rules along the lines of  
MetaCat as normal definitions? Even though we can't define 'm = dup  
i', we could define '$a m = $a $a i'. Optimizations like 'swap swap =  
' could sit aside normal definitions.

I feel like I'm probably reinventing something here. Are there any  
existing languages that work like this?

- John

[Christopher Diggins]

On Fri, Feb 22, 2008 at 3:53 AM, John Nowak <john@...> wrote:
> Recently, I've been thinking about what sort of macro system might be
> suitable for a typed concatenative language. For this discussion, I'll
> assume a language like Cat minus any form of locals/variables. I'll
> call this hypothetical language 'Kitten' from this point on.

I had been calling Cat + locals Kitten at one point, but this is a
minor detail.

> Adding macros to Kitten seems fairly easy at first as the syntax is
> easily representable as a list and there are no variables to get in
> the way. Given that adding macros is fairly easy, it seems worth doing
> if they'd be truly useful.
>
> But are they?

Yes.

> In Lisp, macros are most commonly used for two reasons.
> The first is a lack of a concise syntax for anonymous functions, but
> this isn't an issue in Kitten. The second is dealing with bindings and
> binding constructs (SET!, etc), but this also isn't an issue. There
> are other uses of macros, but these two probably comprise 90% of the
> use cases.
>
> What other uses then might macros have in Kitten? One use I've come up
> with is allowing a way to write constructs that would otherwise be un-
> typeable.
>
> For an example, the m combinator 'dup i' cannot be assigned
> a type

Depends on your type system. In Cat "dup apply" has the type "(A (A (B
-> C) -> D) -> D)"

> for the same reason that '\x -> x x' cannot be assigned a type
> in Haskell; it requires the construction of an infinite type. (Cat's
> version of 'i' is called 'apply' I believe.)

The problem with Haskell is the lack of inference for inner forall
polymorphism.

> Even though 'dup i' isn't typeable, expressions like '[swap] [swap] i'
> and '[dup] [dup] i' are. Accordingly, we could define a macro like
> '[$A] m => [$A] [$A] i' that would work with quote literals. Such a
> macro is writable in a simple declarative system similar to Diggins's
> MetaCat (http://www.cat-language.com/metacat.html), although I believe
> MetaCat isn't currently usable for such things.

Currently the only thing preventing this is that "m" has to already be
predefined, a MetaCat macro can't define new instructions. I think I
may abolish that rule however.

> Another deficiency of the type system is a lack of number
> parameterized types. As such, you can't write a function like 'ndup'
> that duplicates the top N values on the stack. With an appropriate
> macro system however, you could expand '3 ndup' to a typeable
> construct. You would need something more powerful than MetaCat to do
> so however.

That is true, but it would be a very minor hack to improve the MetaCat
system to fix this. This is a very interesting idea!
The lack of parameterized types in Cat is a huge thorn in its paw.
Using macros we can side-step the issue by generating code.

The only problem I forsee is that programmers might type things like
"250 ndup" which would possibly bring the type-system to its knees,
because of the inherent complexity of typing massive stacks. The other
solution is to introduce fixed size type vectors.

> Optimization is another use of macros (as MetaCat shows). Slava Pestov
> recently walked me through some of the more interesting use cases of
> macros for optimization in Factor as well; 'case' is a good example.
>
> There are of course additional, more complex uses. One example would
> be a macro that translates code that uses locals to code that's
> pointfree. Another might be pattern matching. It's not clear if there
> are sufficiently many of such use cases to warrant the addition of a
> macro system as opposed to simply adding a few additional core
> syntactic constructs.
>
> There are obviously downsides to macros as well. Firstly, you
> sacrifice something in terms of concatenativity. For example, 'A B C
> D' might not be decomposable into 'A B' and 'C D' if macros are
> involved.

Type-checking is usually done after macro expansion.

> You also lose something in terms of consistency as
> constructors like 'm' would only be usable with function literals and
> not functions passed at runtime.
>
> Finally, you lose the "everything is
> a function" aspect of Kitten. In Kitten, even the literal '3' is
> really a function with the type 'A -> A int'. Similarly, '[dup]' is a
> function with the type 'A -> A (B c -> B c c)'.
> Macros eliminate this property,
>
> Macros are a huge design space. It seems to me that there are
> essentially four possibilities for such a system in Kitten:
>
> 1. Offer a MetaCat-like system, perhaps with some additional
> expressivity. This covers a fair chunk of the optimization cases very
> simply and it's declarative nature means that you don't need to write
> macros that cooperate with the type system. (Of course the result of
> the rewriting needs to be typeable.) It also allows for 'm' and
> perhaps other more difficult combinators (condnestrec?) to be
> integrated, at least when dealing with literals.
>
> 2. Offer a somewhat Lisp-like system where macros are pure functions
> of the type '[parse-entity] -> [parse-entity]'. This allows more
> flexibility than the MetaCat system, although pointfree syntactic
> manipulation is likely to be more complicated in practice. It is also
> likely to be a good deal more verbose as you'll either need to be
> deconstructing and reconstructing parse-entity sums or casting into
> and out of some universal type.
>
> 3. Take the Factor approach and offer proper parse words and
> everything derivable from them. Again, this seems like even more
> flexibility at the cost of even more complexity. I'm not too
> interested in this approach for a language like Kitten; it makes a lot
> of sense for Factor though.
>
> 4. Offer no macro system whatsoever as the possibilities aren't worth
> the downsides. Something like MetaCat would be integrated directly
> into the system for purposes of optimization only and wouldn't be
> exposed to the user.
>
> Of course, you could always just use Joy and get runtime macros for
> free!

If it is available at runtime then "macro" is the wrong term. You are
then describing a reflection facility.

> Many thanks if you've managed to keep reading this long. If anyone has
> thoughts on what an ideal macro system for a Kitten-like language
> might be, or even if such a system is useful, they'd be much
> appreciated.
>
> - John

Cheers,
Christopher

[John Cowan]

John Nowak scripsit:

> But why stop there? What if we allow rewrite rules along the lines of  
> MetaCat as normal definitions? Even though we can't define 'm = dup  
> i', we could define '$a m = $a $a i'. Optimizations like 'swap swap =  
> ' could sit aside normal definitions.
>
> I feel like I'm probably reinventing something here. Are there any  
> existing languages that work like this?

You are getting very close to Q <http://q-lang.sourceforge.net>.
Q is a functional programming language based directly on equational
reasoning, rather than using it as sugar for lambda expressions only.
(It is eager and dynamically typed.)  Here's my favorite toy example,
for putting Boolean expressions, possibly including variables, into
disjunctive normal form (constants are lowercase, variables uppercase,
"and" and "or" have already been declared infix):

// eliminate double negations:
not not A               = A;

// push negations inward (de Morgan's laws):
not (A or B)            = not A and not B;
not (A and B)           = not A or not B;

// distributivity laws:
A and (B or C)          = A and B or A and C;
(A or B) and C          = A and C or B and C;

// associativity laws:
A and (B and C)         = (A and B) and C;
A or (B or C)           = (A or B) or C;

Note that there is nothing resembling constructor discipline!

--
Where the wombat has walked,            John Cowan <cowan@...>
it will inevitably walk again.          http://www.ccil.org/~cowan

[John Nowak]

On Feb 22, 2008, at 9:41 AM, Christopher Diggins wrote:

>> Adding macros to Kitten seems fairly easy at first as the syntax is
>> easily representable as a list and there are no variables to get in
>> the way. Given that adding macros is fairly easy, it seems worth  
>> doing
>> if they'd be truly useful.
>>
>> But are they?
>
> Yes.

I suppose this was more rhetorical.

>> For an example, the m combinator 'dup i' cannot be assigned
>> a type
>
> Depends on your type system.

Of course. A system with rank-N polymorphism can handle 'dup i'  
properly. Unfortunately (perhaps?), we don't have such a system for a  
compositional/concatenative language yet.

> In Cat "dup apply" has the type "(A (A (B -> C) -> D) -> D)"

I'm not convinced this is useful. As a trivial example, it assigns  
'[swap] dup apply' the type 'A b -> A (C -> D) b'. Your system then  
rejects this type because (C -> D) is unknowable. Perhaps you have  
examples of where 'A (A (B -> C) -> D) -> D' can be composed to yield  
useful types?

Such a system also disallows the use of "unknowable" types for non-
terminating functions like 'error'. My system gives 'error' the type  
'A -> B' which is quite useful as it allows one conditional branch to  
terminate a program without having to balance the error-causing branch  
with the successful branch for the sake of placating the type system.  
For example, 'true [dup] [error] if' is legal (and safe). If error did  
not have the type 'A -> B', something like 'true [dup] [error dup] if'  
would be needed instead. (Or alternatively, you could rewrite it as  
'true [] [error] if dup'.) Disallowing 'A -> B' also disallows unsafe  
coercion functions which may or may not be desirable.

I'm also not sure that 'A (A (B -> C) -> D) -> D' won't occasionally  
yield knowable types that are bogus, so some proof of its soundness  
would be desirable here.

>> for the same reason that '\x -> x x' cannot be assigned a type
>> in Haskell; it requires the construction of an infinite type. (Cat's
>> version of 'i' is called 'apply' I believe.)
>
> The problem with Haskell is the lack of inference for inner forall
> polymorphism.

Aye. Rank-N types are needed to handle this properly.

> That is true, but it would be a very minor hack to improve the MetaCat
> system to fix this. This is a very interesting idea!
> The lack of parameterized types in Cat is a huge thorn in its paw.
> Using macros we can side-step the issue by generating code.

Surely the correct solution is to offer parameterized types!

>> There are obviously downsides to macros as well. Firstly, you
>> sacrifice something in terms of concatenativity. For example, 'A B C
>> D' might not be decomposable into 'A B' and 'C D' if macros are
>> involved.
>
> Type-checking is usually done after macro expansion.

I was speaking here primarily from a pedagogical standpoint. With  
macros, you can no longer state that every space-delineated token is a  
function. The fact that you can do this without the presence of macros  
is a result of languages like Cat not needing any special forms. This  
is a very nice property that macros destroy, as macros are obviously a  
way of introducing special forms.

- John

[John Nowak]

On Feb 22, 2008, at 10:12 AM, John Cowan wrote:

> John Nowak scripsit:
>
>> But why stop there? What if we allow rewrite rules along the lines of
>> MetaCat as normal definitions? Even though we can't define 'm = dup
>> i', we could define '$a m = $a $a i'. Optimizations like 'swap swap =
>> ' could sit aside normal definitions.
>>
>> I feel like I'm probably reinventing something here. Are there any
>> existing languages that work like this?
>
> You are getting very close to Q <http://q-lang.sourceforge.net>.
> Q is a functional programming language based directly on equational
> reasoning, rather than using it as sugar for lambda expressions only.

Very interesting. Unfortunately, I think the system I proposed would  
not actually bring me so close to Q. In particular, all of the  
rewriting would need be done before execution begins. This would mean  
that doing things like 'X sqr = X X *' would work, but only when 'X'  
is known at compile time because it is a literal or perhaps due to  
some partial evaluation phase. Something like '5 sqr' would translate  
to '5 5 *', but '2 3 + sqr' wouldn't work. Well, perhaps it could  
actually, as the stack effect of '2 3 +' is known at compile time. Hm.

Alternatively, it would be interesting to allow such things to happen  
at runtime, but I'm not yet sure how to go about integrating that with  
the type system. I'll have to think more about this. Perhaps it is  
just as simple as translating the rewrite rule to a function with  
locals which is then translated to a normal pointfree function. Think  
*very* quickly here as I head out the door to work...

Thanks John.

- Other John

[Christopher Diggins]

> > In Cat "dup apply" has the type "(A (A (B -> C) -> D) -> D)"
>
> I'm not convinced this is useful. As a trivial example, it assigns
> '[swap] dup apply' the type 'A b -> A (C -> D) b'. Your system then
> rejects this type because (C -> D) is unknowable.

You are incorrect.
Cat infers the type as: ('a -> ('b 'c -> 'c 'b) 'a)
Why would you claim otherwise?

> > Type-checking is usually done after macro expansion.
>
> I was speaking here primarily from a pedagogical standpoint. With
> macros, you can no longer state that every space-delineated token is a
> function.

This is already not the case in Joy or Cat. (e.g. in Cat "define",
"[", "]", "{", "}").

- Christopher

[John Nowak]

Apologies if this is formatted strangely... replying via broken webmail.

>> > In Cat "dup apply" has the type "(A (A (B -> C) -> D) -> D)"
>>
>> I'm not convinced this is useful. As a trivial example, it assigns
>> '[swap] dup apply' the type 'A b -> A (C -> D) b'. Your system then
>> rejects this type because (C -> D) is unknowable.
>
> You are incorrect.
> Cat infers the type as: ('a -> ('b 'c -> 'c 'b) 'a)
> Why would you claim otherwise?

My derivation is at the end of the email. I've yet to actually use the Cat
interpreter so perhaps I made an incorrect assumption.

Out of curiosity, what type does Cat give '[swap] dup'? Is it not 'A -> A
(B c d -> B d c) (B c d -> B d c)'? If not, why?

>> I was speaking here primarily from a pedagogical standpoint. With
>> macros, you can no longer state that every space-delineated token is a
>> function.
>
> This is already not the case in Joy or Cat. (e.g. in Cat "define",
> "[", "]", "{", "}").

Yes, yes. I meant that '3' is a function, '[1 2 3]' is a function, et
cetera. Replace "token" with "valid syntactic entity" or some such.

- John

;; (initial composition)
E -> E (F g h        -> F h g)        ;; [swap]
     A (A   (B -> C) -> D    ) -> D   ;; dup apply

;; D -> F h g
E -> E (F g h        -> F h g)
     A (A   (B -> C) -> F h g) -> F h g

;; h -> (B -> C)
E -> E (F g (B -> C) -> F (B -> C) g)
     A (A   (B -> C) -> F (B -> C) g) -> F (B -> C) g

;; A -> F g
E -> E   (F g (B -> C) -> F (B -> C) g)
     F g (F g (B -> C) -> F (B -> C) g) -> F (B -> C) g

;; E -> F g
F g -> F g (F g (B -> C) -> F (B -> C) g)
       F g (F g (B -> C) -> F (B -> C) g) -> F (B -> C) g

F g -> F (B -> C) g

[Christopher Diggins]

> > You are incorrect.
> > Cat infers the type as: ('a -> ('b 'c -> 'c 'b) 'a)
> > Why would you claim otherwise?
>
> My derivation is at the end of the email. I've yet to actually use the Cat
> interpreter so perhaps I made an incorrect assumption.
>
> Out of curiosity, what type does Cat give '[swap] dup'? Is it not 'A -> A
> (B c d -> B d c) (B c d -> B d c)'? If not, why?

[swap] dup : ( -> ('a 'b -> 'b 'a) ('c 'd -> 'd 'c))

Notice that you are not generating new type variables for the
duplicated version of swap on the stack.

I looked at your derivation and it seems correct, but we get a
different result if we compose "[swap] dup" with "apply", rather than
"[swap]" with "dup apply". This is a very interesting result, because
it says that if a type derivation fails there may exist another legal
type derivation.

This is a real problem though. Consider the following case:

define f1 { [swap] }
define g1 { dup apply }
define f2 { [swap] dup }
define g2 { apply }

For example: "f1 g1" is rejected whereas "f2 g2" is accepted.

I wonder if this implies that equirecursive types need to be reintroduced.

- Christopher


Christopher

[John Nowak]

>> Out of curiosity, what type does Cat give '[swap] dup'? Is it not 'A ->
>> A
>> (B c d -> B d c) (B c d -> B d c)'? If not, why?
>
> [swap] dup : ( -> ('a 'b -> 'b 'a) ('c 'd -> 'd 'c))
>
> Notice that you are not generating new type variables for the
> duplicated version of swap on the stack.

I thought this was only done in Cat when an occurs check fails. What
exactly are the rules for when to generate new variables? What is the type
of 'quote dup'? If it is 'a -> ( -> a) ( -> a)', then why isn't it 'a -> (
-> a) ( -> b)'? The later is obviously unsound, so I'm curious what the
rule is for (not) generating new types.

> I looked at your derivation and it seems correct, but we get a
> different result if we compose "[swap] dup" with "apply", rather than
> "[swap]" with "dup apply". This is a very interesting result, because
> it says that if a type derivation fails there may exist another legal
> type derivation.

It also unfortunately (and perhaps obviously) means your type system is
not compositional.

- John

[John Nowak]

>> Out of curiosity, what type does Cat give '[swap] dup'? Is it not 'A ->
>> A
>> (B c d -> B d c) (B c d -> B d c)'? If not, why?
>
> [swap] dup : ( -> ('a 'b -> 'b 'a) ('c 'd -> 'd 'c))
>
> Notice that you are not generating new type variables for the
> duplicated version of swap on the stack.

I thought this was only done in Cat when an occurs check fails. What
exactly are the rules for when to generate new variables? What is the type
of 'quote dup'? If it is 'a -> ( -> a) ( -> a)', then why isn't it 'a -> (
-> a) ( -> b)'? The later is obviously unsound, so I'm curious what the
rule is for (not) generating new types.

> I looked at your derivation and it seems correct, but we get a
> different result if we compose "[swap] dup" with "apply", rather than
> "[swap]" with "dup apply". This is a very interesting result, because
> it says that if a type derivation fails there may exist another legal
> type derivation.

It also unfortunately (and perhaps obviously) means your type system is
not compositional.

- John

[Christopher Diggins]

On Sat, Feb 23, 2008 at 1:14 PM,  <john@...> wrote:

>
> >> Out of curiosity, what type does Cat give '[swap] dup'? Is it not 'A ->
> >> A
> >> (B c d -> B d c) (B c d -> B d c)'? If not, why?
> >
> > [swap] dup : ( -> ('a 'b -> 'b 'a) ('c 'd -> 'd 'c))
> >
> > Notice that you are not generating new type variables for the
> > duplicated version of swap on the stack.
>
> I thought this was only done in Cat when an occurs check fails. What
> exactly are the rules for when to generate new variables?

When you unify a polymorphic function type (e.g. one that has generic
type-variables) on the left side of the arrow with a type variable,
every instantiation of the polymorphic function variable should have
new copies generated of its generic type-variables. Non-generic
type-variables are left alone.

> What is the type
> of 'quote dup'? If it is 'a -> ( -> a) ( -> a)', then why isn't it 'a -> (
> -> a) ( -> b)'? The later is obviously unsound, so I'm curious what the
> rule is for (not) generating new types.

The answer is: ('a -> ( -> 'a) ( -> 'a). The type of quote is ('a -> (
-> 'a)). The generated function is not actually polymorphic: it has a
type-variable that is bound to an outer scope. In
http://research.microsoft.com/users/luca/Papers/BasicTypechecking.pdf
this is called a "non-generic" type variable. I have to point out that
genericity is a relative concept. A type variable is generic or
non-generic relative to a particular function.

Does this help?

> > I looked at your derivation and it seems correct, but we get a
> > different result if we compose "[swap] dup" with "apply", rather than
> > "[swap]" with "dup apply". This is a very interesting result, because
> > it says that if a type derivation fails there may exist another legal
> > type derivation.
>
> It also unfortunately (and perhaps obviously) means your type system is
> not compositional.

Yes. Personally I find this disappointing, but acceptable. One way to
recover compositionality of the type system may be to reintroduce
equirecursive types.

- Christopher

[John Nowak]

>> I thought this was only done in Cat when an occurs check fails. What
>> exactly are the rules for when to generate new variables?
>
> When you unify a polymorphic function type (e.g. one that has generic
> type-variables) on the left side of the arrow with a type variable,
> every instantiation of the polymorphic function variable should have
> new copies generated of its generic type-variables.

Makes sense. I figured this would probably have to be the case if quote
were handled properly (which it is). Thank you for explaining.

>> It also unfortunately (and perhaps obviously) means your type system is
>> not compositional.
>
> Yes. Personally I find this disappointing, but acceptable.

Agreed.

> One way to recover compositionality of the type system may
> be to reintroduce equirecursive types.

Oi. I'll have to take a good look at this.

- John