Working within the constraints given :-) Yes, I have realised the fully abstract arrow types don't work, and are not necessary.
> Well, that's the answer that *I* gave, but I don't understand how that relates to your fully abstract arrow types. Given the description that you gave of your fully abstract arrow types, I don't understand how to express what you wrote above (which uses call arrows) in your notation. So now for any application: f a b c The last arrow is concrete. f : a -> b -> c => d and unification rules are (->) U (->) = (->) (=>) U (->) = (=>) (=>) U (=>) = (=>) The problem this represents merging of applications (ie requirements). I realise now this is your "afn". When we provide a definition we need something slightly different: k x y = \z . x + y + z k :: a +> b *> c *> d with unification rules: (+>) U (+>) = (+>) (*>) U (*>) = (*>) and rules for combining: (->) U (+>) = (+>) (->) U (*>) = (*>) -- omitting this rule prevents calling with more arguments (=>) U (*>) = (*>) The first set of arrows accumulate call points in applications (abstract). The second set of arrows record call points in definitions (concrete). Apologies for the proliferation of arrow types, I want to keep the operators binary to keep unification simple to think about. That seems to work to me. Have I missed anything? Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
