I think you are converging on the right track, but I'm puzzled by the number of distinct arrows here.
First, I *think* I understand what the -> and => arrows are, but I'm really puzzled by +> vs *>. Can you take a moment to define each of the arrows here? If I'm understanding this correctly, I suspect that *> and => are actually the same sort of arrow, but I can understand why you want to distinguish them notationally. Also, I think the -> requires a variable on the arrow, because we need to keep them correlated in the choose_one example after term substitution, or equivalently, we need to keep them correlated in id. On Wed, Apr 1, 2015 at 7:47 AM, Keean Schupke <[email protected]> wrote: > 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 > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
