More on choose_one:
choose_one :: a -> a -> Bool -> a choose_one x y b = if b then x else y f1 :: a => b c => d f1 x = \y z . x +y + z f2 :: a -> b -> c -> d -- I am not sure if this should infer f2 x = \y . \z . x + y + z g = choose_one f1 f2 random_bool inferred type of choose_one: (a => b c => d) U (e -> f -> g -> h) = (a => b c => d) Trying to use g: g x (e -> f) U (a => b c => d) = (a => b c => d) g x y (e -> f -> g) U (a => b c => d) = _|_ g x y z (e -> f -> g -> h) U (a => b c => d) = (a => b c => d) I don't see the problem, can you show me where this doesn't work? Keean. On 31 March 2015 at 21:44, Keean Schupke <[email protected]> wrote: > On 31 March 2015 at 21:28, Jonathan S. Shapiro <[email protected]> wrote: > >> Keean: >> >> You seem to misunderstand the challenge problem. >> > > Its definitely possible, i'm not convinced yet. If there is an issue, I > don't fully understand it. > > >> >> First, f is not imported, so we have no signature for it at all. Assume f >> is a procedure parameter to the current procedure for which no type is >> given. We are left to infer an abstract function type for f based on the >> observed applications in the procedure body. >> > > Just ignore that, it doesn't make any different to my argument, it just > means where I list the possible types of the imported 'f' we would use 'a > -> b -> c -> d' for a local (arity abstract) definition, or if you prefer, > put the concrete calls at the positions you want to infer them from the > lambdas in the definition. > > >> >> The two applications in the example: >> >> f a b >> f a b c d >> >> Occur in the body OF THE SAME PROCEDURE. Thus, the challenge is to infer >> a single abstract function type for f that satisfies *both* uses >> simultaneously. You gave inferred types for the two applications >> independently, but did not account for the need to reconcile them to arrive >> at a single type for f. >> >> Matt and I don't think they reconcile without some ability to remember >> which argument positions must have a call arrow following the argument >> position. In particular the choose_one example can't be handled without >> that. >> > > I think I have demonstrated how it can be handled without. I would > appreciate if you could find the problem with what I have suggested. It > seems to work for me. > > On Tuesday, March 31, 2015, Keean Schupke <[email protected]> wrote: >> >> Because I have a multi-set environment we can happily have {f : a -> b, f >>> : a -> b -> c ->d}, which you could also write using intersection types as >>> f : (a -> b) & (a -> b -> c -> d) >>> >> >> Those signatures are wrong. You'd need something like >> >> F: (a->b->'ret1 ) & (a->b->c->d->'ret2) >> > > Sorry, I just missed one argument so I have a->b and a->b->c->d, I don't > think this changes any of the arguments. > > >> But introducing intersection types seems like a big increase in >> complexity in the type system unless we need them for some other purpose. I >> do agree that this can handle the issue in this example, but there is still >> a need for some form of arity type variable to ensure agreement in the >> choose_one example. >> > > You don't need the intersection types, that was before I worked out the > unification algorithm I posted, which is commutative (IE unifying a and b > then c is the same as a then c then b). > > >> >> That said, intersection types may be a more natural way to think about >> things in a type system that admits subtypes. >> > > True, however they do nasty things to unification, and you have to > introduce expansion types. I've been down this road quite a long way, and I > didn't like it. Top level intersections are fine though, but not necessary. > > The imported type of 'f' must unify with both of these, so valid types >>> would be: >>> >> >> F is not imported. >> > > Again, whether f is imported or not is not relevant to my argument, so you > can ignore that and read 'type inferred from the definition' instead of > 'type defined in the import/export'. > > > Keean. > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
