# possibilities for macros in a typed language

## John Nowak — 2008-02-22 08:53:26

    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 — 2008-02-22 10:29:03

    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 — 2008-02-22 14:41:54

    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 — 2008-02-22 15:12:12

    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 — 2008-02-23 14:14:28

    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 — 2008-02-23 14:26:14

    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 — 2008-02-23 15:32:11

    > > 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@johnnowak.com — 2008-02-23 16:37:30

    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 — 2008-02-23 17:12:45

    > > 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@johnnowak.com — 2008-02-23 18:14:59

    >> 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@johnnowak.com — 2008-02-23 18:15:14

    >> 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 — 2008-02-23 18:33:28

    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@johnnowak.com — 2008-02-23 18:53:20

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