[stack] Re: Some thoughts on Object Cat

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

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.

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