On Wed, Apr 1, 2015 at 10:47 AM, Keean Schupke <[email protected]> wrote: > 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".
No this is mixed arrow notation. Pretty much exactly. We just switched from "=>" to "-y->" later on. There's also "-n->". "->" is abstract, and has an elided callvar. An explicit callvar is written like "-?r->". > 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? Mainly, you forgot to tell us what "+>" and "*>" mean. XD >From the k example, it looks like maybe "+>" is "-n->" and "*>" is another name for "-y->". Why do you need both "=>" and "*>"? Is it true that (+>) U (*>) = (+>) U (=>) = _|_ ? I ask because (-y->) U (-n->) = _|_. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
