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

On Sat, Feb 23, 2008 at 1:14 PM,  <[email protected]> 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