On Wed, Feb 25, 2015 at 9:03 AM, Jonathan S. Shapiro <[email protected]> wrote: > On Tue, Feb 24, 2015 at 11:25 PM, Matt Oliveri <[email protected]> wrote: >> >> On Wed, Feb 25, 2015 at 12:28 AM, Jonathan S. Shapiro <[email protected]> >> wrote: ... >> >> There you go with argument positions again. Maybe I'm really missing >> >> something here. Or maybe you're smoking something funny. What's wrong >> >> with this specialization: >> >> >> >> fn 'arity Nat->Nat->Nat->Nat >> >> becomes >> >> fn 1 Nat -> fn 'newArity Nat->Nat->Nat >> >> >> >> Notice that the concreteness of the argument types has not forced the >> >> return type to be concrete. >> > >> > What's wrong with it is subtle. Generalizing your example, the type: >> > >> > fn 1 Nat -> fn 'newArity 'a 'b 'c >> > >> > is syntactically well-formed and semantically sensible, but it is not a >> > type >> > that can feasibly be derived under the typing regime that I have >> > proposed. >> > >> > The universe of derivable-by-inference function types is an inductive >> > construction over compositions of well-formed program fragments. If all >> > global function definitions have a native arity, then it is not possible >> > to >> > compose program fragments in such a way that their types compose to >> > produce >> > the type you propose. >> >> Well I'm not sure exactly what you mean, but I never claimed any of my >> example types were the types of programs. I don't see why you refuse >> to talk about them for that reason. > > Matt: please calm down. I did not "refuse" to talk about them. You asked me > a question, and I am trying to answer. In fact, I said quite clearly above > that the type you gave is syntactically well-formed (provided we replace Nat > with a valid type).
I'm calm. That was careless wording. Sorry. I didn't actually mean to accuse you of refusing to do anything. I was just surprised that when I asked for an explanation of an example, you instead said why the example could not arise. > I also said that it was semantically sensible, but I'm > actually not convinced of that. Well, I don't know if it's semantically sensible in whatever system you're actually thinking of. I'm pretty sure it's sensible in my interpretation of your proposed system, based on what I understand of it. But my interpretation may be wrong. Especially now that it seems so important to you which types can arise from programs. > It is certainly possible to see an expression > > f i j k > > > and infer > > fn 'arity int->int->int->int > > > at an application, and then to partially instantiate that. But there is no > way within the type rules to get from there to: > > fn 1 int -> fn 'newArity int->int->int > > > the reason this is impossible is that this would mean that the function f > has the type > > fn 1 int -> 'a > > > where 'a is unifiable with > > fn 'newArity int->int->int > > > But there are only two ways that we can arrive at a function having type fn > 1 int->'a: > > 1. f is underspecified, in which case the program cannot be run > 2. f returns some global value g which is underspecified, in which case the > program cannot be run. > > I'm not all that interested in the types of non-executable programs. This seems like more explanation of why (fn 1 int -> fn 'newArity int->int->int) should not arise. So you're not be interested in types of non-executable programs. Well I'm not interested in reasons why well-formed, seemingly-meaningful types happen to never arise in some particular inference system. What happens if the user annotates with that type? "Error: Your type would never result from unification of types inferred from valid programs."? We are wandering towards our disagreement about what priority inference should have in language design. Until we started discussing the details of your notation, your proposal did not seem to rely on the type system making use of inference techniques. So if possible, we should talk about it without talking about the details of type inference. >> Indeed, we are interested in >> partially specialized types because they arise by specialization. Are >> you saying it's illegal to specialize the arity of the application in >> (f 2 3 5) + 7 >> ? > > I don't see any problem with that. Yes, I figure now that you don't use arbitrary instances of "good" types. Only those arising from unification with other good types. I think all instances of good types should still be meaningful, even if they aren't good. >> I object anyway! I don't see why that needs to be verified, if >> well-formed types make sense whether or not they arise. > > The types are syntactically well-formed, but not semantically valid. My > claim is that types like fn 1 int -> 'a can only appear in underspecified > programs. Unless you forbid type annotations, I can put (fn 1 int->'a) into any program I want. But maybe I am violating some sacred custom of type inference disciples. In the type systems I'm used to, you wouldn't consider a type meaningless just because it never gets inferred. But actually, what is the type of this function? def countToInfinity n = countToInfinity (n + 1) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
