[stack] Re: Some thoughts on Object Cat

On Sat, Apr 19, 2008 at 11:56 PM, John Nowak <[email protected]> wrote:
>
>
> On Apr 19, 2008, at 10:58 AM, Christopher Diggins wrote:
>
> > One paper caught my eye
> > "http://research.microsoft.com/users/daan/download/papers/hmf-tr.pdf"
> > which talks about impredicative instantiation. This is interesting
> > because it is precisely the problem we talked about previously, and
> > that Colin Hirsch pointed out to me even earlier. I didn't realize
> > that the solution was not so well known. I actually do not use the HM
> > type inference algorithm.
>
> (I assume the problem you're talking about is writing things like the
> 'm' combinator.)

No, I was referring to the "ambiguous impredicativity" problem of
dealing with polymorphism that he refers to. It seems that nested
polymorphism is a tricky kettle of fish for modern type theory.
However my naive approach (which works really well) is to rename
generic variables as I go, and defining forall qualification to be on
the inner-most function that is possible.

I solved the "dup apply" (or "dup i", god I hate using "i" to mean
application) problem by reintroducing "self" types.

> Another solution (or stop-gap solution, depending on how you look at
> it) is to allow definitions to defer type checking. Essentially,
> instead of declaring a function, you declare that some word expands to
> some other words.
>
> For example, rather than defining 'm = dup i' and giving 'm' some
> restrictive equi-recursive type (or requiring a type signature for a
> higher rank type), we can simply make 'm' a macro. If we then did
> '[swap] m', it would expand to '[swap] dup i' before doing type
> inference, and we'd get the type 'A b -> A [C d e -> C e d] b' as a
> result.

That is elegant, but at the same time would cost me the benefit of
being able to split definitions at will.

> Another example is the 'poly' function given on page two of the HMF
> paper. In a concatenative language, we could define 'poly' as '1 True
> rot dup dip dip mk-tuple2'. (There are better ways to write this,
> namely using an 'apply2' combinator, but I'm ignoring that for
> simplicity.) In any case, this will fail to type check without higher
> rank types.

But we've got higher-rank types in Cat.

> However, we if were to say 'poly' is just a macro that
> expands to that same definition, it'll work fine provided that poly is
> used in cases where the type of the function given to poly is knowable
> in the current context.
>
> (Brief note: The definition for 'apply2' is just 'rot dup dip dip'
> which we can easily see by factoring it out of the above definition
> for 'poly'. Note however that 'apply2' must be a macro otherwise it'll
> require both values passed to it to be of the same type!)
>
> There's something else nice about allowing these simple expansion
> macros; you may have already noticed. In Cat, you cannot split any
> definition into two as sometimes the types will get in the way.

This was true in the earlier version, but with the recent
reintroduction of "self" types this is no longer a problem.

> In the
> example below, 'baz' may not type check even though 'foo' does, or
> alternatively 'baz' my type check but in a way that then prevents you
> from writing 'qux' (such as if 'baz' were given an overly-restrictive
> equi-recursive type):
>
>    foo = a b c d e
>    bar = a b c
>    baz = d e
>    qux = bar baz
>
> However, if we have these simple macros, we can make 'baz' a macro and
> be guaranteed that the type of 'qux' will be the same as the type of
> 'foo'. Essentially, these macros let you hand-wave away the problem
> that your type system is not "compositional" by allowing the user to
> do the composition later in the process.
>
> This approach won't let you write possibly infinitely recursive
> definitions with 'm', as you will hit the occurs check when the
> function passed to 'm' tries to duplicate and call itself, but this is
> actually something I depend on in my system for sound termination
> checking. You might seriously consider not allowing things like 'm' to
> be a feature as it allows you to trivially track possible non-
> termination on the type level (no type system extensions are necessary).
>
> - John

I need "m" in order to allow Cat implementation to disallow explicit
recursion if they want, and so that I can perform automated generation
of Cat code from other languages.

You may be interested that coming up real soon is a draft of a brand
new paper describing the Cat type-system and type-inference algorithm
in detail. No more getting rejected from conferences for me, this is
going to be a technical-report! :-)

Cheers,
Christopher