Re: [stack] possibilities for macros in a typed language

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