On Mon, Mar 30, 2015 at 3:29 AM, Matt Oliveri <[email protected]> wrote:
> On Mon, Mar 30, 2015 at 1:14 AM, Jonathan S. Shapiro <[email protected]> > wrote: > > > > More generally: in the scheme that I have been outlining it is > intentionally > > true that specializations from ?r to 'y' occur through a different > mechanism > > than specializations from ?r to 'n'. Basically: applications can cause a > > specialization from ?r to 'y', and specializations to cfns can induce > > specializations from ?r to 'n'. In the ?r to 'y' case, as you note, the > > specialization can always be safely be performed (though it may result > in a > > later type incompatibility). In the ?r to 'n' case, the fact that this > > specialization can only arise from specialization via a cfn means > (because > > cfns always have an explicit return arrow) that the specialization can > only > > occur in contexts where doing so is correct. > > > > This is exactly why I originally described arrows as having only the ?r > and > > 'y' options, and not the 'n' option. Eliminating the 'n' from the arrow > type > > syntax means that it's impossible to introduce an incorrect arrow type > even > > by hand. Allowing them to be specialized by cfns INTO cfns has the effect > > that n-ary calls get introduced in a structured way, without the risk of > 'n' > > appearing in the wrong place. > > Ah. Yes, I think you're right. Another way to say this is that by not > allowing the user to write 'n' arrows, and only instantiating due to > unification, all types that ever arise could've been expressed as > afns. So the system will be sound if the afn version is. It's a sneaky > argument. > Yes. And I agree that this is sneaky, and that it is therefore probably not the best way to do things. I would prefer a cleaner approach, and afn's may be the right thing. > > I think the right thing to do for now is to write using AFN, and then we > can > > go back later and figure out if a notation more similar to ML and Haskell > > conventions is pragmatically tolerable. > > > > In order to discriminate your afns from mine in our discussion, I propose > > that you write the arity type variable as ?r rather than 'r. > > But, to be clear, the ?r is a deep arity variable? > Well, any notation that *has* an arity variable is your notation, so presumably it should mean whatever you say it means. What *I'm* thinking for *my* afn notation (which I'll write as 'safn' to reduce possible confusion) is that safn a b c -> d is equivalent to what I have been writing as: a-?r1->b-?r2->c=>d I guess it's time to explain why (afn (?r1 ++ ?r2) 'a 'b -> 'c) and > (afn ?r1 'a -> afn ?r2 'b -> 'c) are the same type. I think of "afn" > as a type-level computation which ultimately reduces to some type > formed with cfns. While the arity remains abstract, we cannot do the > reduction, so we don't know what the cfns are, but because afn is > "just" a total function producing a type, it must mean something. > I think I agree that they are the same type; what I see here is merely a difference in notation. It seems to me that in your notation it is less visually obvious that a single input argument necessarily reduces to a cfn, but that may just be a matter of getting used to the notation. The one I'm less convinced about is whether (your afn here) afn ?r1 'a 'b -> afn ?r2 'c -> 'd is equivalent to (your afn) afn (?r1 ++ ?r2) 'a 'b 'c -> 'd the thing that has been lost here is where the first arrow appeared in the call chain. The reason it matters is that two distinct applications can cause us to need to preserve that knowledge at unification time. Given the applications: f a b c f d e it is still true that f is an abstract function type, but it is also true that we need a => (a known-returning arrow) after both the second and third arguments to the abstract function type. I'm not sure how this is captured in your approach? > The afn function takes a deep arity (with some obvious constraints), a > list of argument types and a return type. So (afn ?r 'a 'b -> 'c) is > sugar for something like (rawAFN r [a,b] c), where "rawAFN" is the > actual function. As long as the arity is a deep arity, then I agree that it's possible to encode chained afns (your afns) equally well with deep arities. I guess I prefer to encode the affirmatively returning positions using an arrow, but I think that's just a matter of differing aesthetics. > It's defined recursively: > rawAFN [] args rtn = rtn // That weird base case > rawAFN (a :: r) args rtn = rawCFN (firstn a args) (rawAFN r (skipn a args) > rtn) > > Oh yeah, rawCFN takes a list of argument types and a return type. > I *think* I understand what you are saying, but it's not obvious to me how this addresses the unification case I have just described above, where we can't decide how the first two arguments are consumed based on the applications we can see. *Because* we can't decide, I think we're still dealing with an abstraction function where those two arguments are concerned. The consumption of the third argument (c) can be converted to CFN because *all* single argument functions can directly be converted to cfn. The constraints on the deep arity argument of rawAFN are: > - Each element is an integer > 0. > - The sum of the elements is the length of the list of argument types. > Those constraints make sense, but they don't seem to address my unification example. But here's a better example. Suppose we see applications f a b f a b c d then it seems to me that your type will be something like afn (?r1 ++ ?r2) a b c d -> ret but we have lost the information here that ?r1 and ?r2 must each account for two of the arguments. How is that captured in your proposal? > I'm not sure yet if > we'll actually ever need to write "++" or "::" for arity lists either. > Mixed arrow notation suggests that we will not. I'm actually not fond of the mixed arrow notation. It's useful in the present discussion to clarify things, but I think it will introduce surprises. I have a thought about what to do, but it's going to produce an argument here, and I'd like to do *that* argument separately from this argument. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
