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

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