On 1 April 2015 at 16:23, Matt Oliveri <[email protected]> wrote: > 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->". >
Okay, I am confused, as I don't see any need for additional variables. Are the 'y', 'n' and '?r' just names. They don't represent numbers or things yet to be substituted do they? > > > 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 "*>"? > +> means "another argument is required to call this function" *> means "this is a call point, you have sufficient arguments to call the function" You are right => and *> can be combined into a single arrow, unless you want to omit this rule: (->) U (*>) = (*>) If you omit this rule you can prevent functions being called with more arguments than they require. But if we are sure we don't ever want to omit this rule they can be combined. > Is it true that > (+>) U (*>) = > (+>) U (=>) = > _|_ > ? > I ask because (-y->) U (-n->) = _|_ Yes this is what I have. Any unifications not listed explicitly are _|_ So: -> = -n-> => = -y-> +> = -?r-> What do 'n', 'y' and '?r' stand for? Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
