RE: Mutually recursive bindings
Tom Pledger writes: Mark P Jones writes: [...] In general, I think you need to know the types to determine what transformation is required ... but you need to know the transformation before you get the types. Unless you break this loop (for example, by supplying explicit type signatures, in which case the transformation isn't needed), then I think you'll be in a catch-22 situation. Why do you need the type to determine the transformation? Here's another example to illustrate the point: h x = (x==x) || h True || h "hello" Before looking at this example, I was gearing up to protest that the transformation was cued simply by scope, but now I see that it was cued by scope *and* not foiled by type. So, I withdraw the transformation idea, [...] But wait! There's life in the transformation idea yet. After dependency analysis but before type checking, we have enough information to transform this: f x = x==x || f True || f (f "hello") which would be illegal without an explicit type signature, into this: f x = f' f1 f2 f3 x where f1 x = f' f1 f2 f3 x f2 x = f' f1 f2 f3 x f3 x = f' f1 f2 f3 x f'f1 f2 f3 x = x==x || f1 True || f2 (f3 "hello") for which Haskell infers the desirable type Eq a = a - Bool. The loop (type checking before transformation, and transformation before type checking) is broken by defining one sacrificial function for each recursive reference, regardless of the possibility that some of them may end up with the the same types (f1 and f2 in the above example both have type Bool - Bool). A keen compiler could detect and coalesce the duplicate decls and parameters after type checking. Regards, Tom ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Mutually recursive bindings
Tom Pledger writes: [...] For example, with FLAMV = free variables which will be lambda-bound, and FLETV = free variables which will be let-bound, and ! marking the alleged innovations: h = \x - (x==x) || h True || h "hello" [...] --- Eq b = (b - Bool; FLETV: h_1st::Bool - Bool, h_2nd::[Char] - Bool) --- (Tentatively give h its quantified type) h :: forall b . Eq b = b - Bool ! (Discharge the h_1st requirement, by unifying Bool - Bool ! with a fresh instance of forall b . Eq b = b - Bool) ! (Discharge the h_2nd requirement, by unifying [Char] - Bool ! with another fresh instance of forall b . Eq b = b - Bool) [...] technique of deferring unification for uses of let-bound variables until after quantification. The quantification over the type variables which are free inside the declaration but not outside it, that is. So, in cases like this (more or less as seen in section 4.5.4 of the Haskell 98 report), we still get the proper behaviour: f x = let g y z = ([x, y], z) in (g True, g 'c') --- g :: forall b . a - b - ([a], b) --- Free vars which will be let-bound: g_1st :: Bool - c g_2nd :: Char - d -- Discharge the g_1st requirement by unifying a - e - ([a], e) with Bool - c Now g :: forall b . Bool - b - ([Bool], b) Fail to discharge the g_2nd requirement, because we can't unify Bool - f - ([Bool], f) with Char - d It seems reasonable that when there is no explicit type signature, we should first infer one from how the parameters are used, and only then check that any recursive uses make sense. I'm not sure whether this is a departure from Hindley-Milner norms. Will someone who knows please comment? Regards, Tom ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Mutually recursive bindings
Hi Tom, Thanks for an interesting example! | For this code (an example from the Combined Binding Groups section of | Mark Jones's "Typing Haskell in Haskell"): | | f :: Eq a = a - Bool | f x = (x == x) || g True | g y = (y = y) || f True | | Haskell infers the type: | g :: Ord a = a - Bool | but if the explicit type signature for f is removed, we get: | f, g :: Bool - Bool Let's take a closer look at this code. Polymorphism, of course, allows us to describe multiple functions with a single piece of code ... which is what you can see here ... there are really two versions of f and g: one pair that takes an argument of type "a" and another that takes an argument of type "Bool". Let's call these functions f_a, g_a, f_Bool, g_Bool. Then the definitions above are morally equivalent to the following expansion: f_a x= (x == x) || g_Bool True g_a y= (y = y) || f_Bool True f_Bool x = (x == x) || g_Bool True g_Bool y = (y = y) || f_Bool True Note here that f_Bool and g_Bool are mutually recursive. We can infer a monomorphic type of Bool - Bool for each of them. The definitions of f_a and g_a, however, are not recursive, and it should be easy to see that we can infer the fully polymorphic types for each one. What we have here is an example of the way that duplicating code can enhance Hindley-Milner style polymorphism, allowing different copies to be assigned different types. | So, why do both GHC and Classic Hugs accept the following program? | ... | fFix g x = (x == x) || g True | gFix f y = (y = y) || f True | | fMono x = fFix gMono x | gMono y = gFix fMono y | | f x = fFix gMono x | g y = gFix fMono y I hope this will be clear by now. You've taken the transformation that I described above one step further, abstracting out the common pattern in the definitions of f_a and f_Bool into fFix, and of g_a and g_Bool into gFix. Your f, fMono are just my f_a and f_Bool, while your g, gMono are just my g_a and g_Bool. Although you've turned the code back into a single, mutually recursive binding group, the same basic argument applies. | Would it be an outright win to have this done automatically? In general, I think you need to know the types to determine what transformation is required ... but you need to know the transformation before you get the types. Unless you break this loop (for example, by supplying explicit type signatures, in which case the transformation isn't needed), then I think you'll be in a catch-22 situation. Why do you need the type to determine the transformation? Here's another example to illustrate the point: h x = (x==x) || h True || h "hello" This time, you need to make three copies of the body of h---one for a generic "a", one for "Bool", and one for "String"---but I don't think you could have known that 3 versions were needed (as opposed to 2 or 4, say) without looking at the types. Incidentally, the transformation can be understood by looking at a version of the program that makes polymorphism explicit by passing types as arguments (a la System F/polymorphic lambda-calculus), and then generating specialized versions for each different argument type. (The basic method parallels something I did quite a few years ago to eliminate dictionaries from an implementation of Haskell-style overloading; see my paper "Dictionary-free Overloading by Partial Evaluation" for more details.) This also throws up another issue; with polymorphic recursion, you might need an *infinite* family of specialized functions. Consider the following example: r x = (x==x) r [x], whose translation to include type parameters would produce: r a x = (x==x) r [a] [x]. (For simplicity, I'm pretending that (==) :: a - a - Bool, making it fully polymorphic. Adding type classes doesn't change anything but obscures the real point.) Now when you ask for r_a you'll get: r_a x = (x==x) r_[a] [x] r_[a] x = (x==x) r_[[a]] [x] r_[[a]] x = (x==x) r_[[[a]]] [x] r_[[[a]]] x = (x==x) r_a [x] ... This reply has been longer than I'd intended; to anyone still reading, I hope you had fun, and I hope this made sense! All the best, Mark ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Mutually recursive bindings
Mark P Jones writes: [...] In general, I think you need to know the types to determine what transformation is required ... but you need to know the transformation before you get the types. Unless you break this loop (for example, by supplying explicit type signatures, in which case the transformation isn't needed), then I think you'll be in a catch-22 situation. Why do you need the type to determine the transformation? Here's another example to illustrate the point: h x = (x==x) || h True || h "hello" Before looking at this example, I was gearing up to protest that the transformation was cued simply by scope, but now I see that it was cued by scope *and* not foiled by type. So, I withdraw the transformation idea, but instead suggest that a similar improvement in inferred polymorphism can be achieved by making the type checker more circumspect (lazy?) about when it performs some unification. For example, with FLAMV = free variables which will be lambda-bound, and FLETV = free variables which will be let-bound, and ! marking the alleged innovations: h = \x - (x==x) || h True || h "hello" - a; FLAMV: x::a -- Eq b = b - b - Bool --- (Substitute b for a) Eq b = (b - Bool; FLAMV: x::b) - ! (Because x will be lambda-bound, go ahead and unify the types of its uses now) Eq b = (b; FLAMV: x::b) Eq b = (Bool; FLAMV: x::b) -- Bool - Bool - Bool Eq b = (Bool - Bool; FLAMV: x::b) _ c; FLETV: h_1st::c Bool -- (Substitute Bool - d for c) d; FLETV: h_1st::Bool - d -- Bool - Bool - Bool - (Substitute Bool for d) Bool - Bool; FLETV: h_1st::Bool - Bool - ! (Because h is let-bound, do not attempt !to unify the types of h_1st and h_2nd) e; FLETV: h_2nd::e --- [Char] - (Substitute [Char] - f for e) f; FLETV: h_2nd::[Char] - f --- (Substitute Bool for f) Bool; FLETV: h_1st::Bool - Bool, h_2nd::[Char] - Bool Eq b = (Bool; FLAMV: x::b; FLETV: h_1st::Bool - Bool, h_2nd::[Char] - Bool) --- Eq b = (b - Bool; FLETV: h_1st::Bool - Bool, h_2nd::[Char] - Bool) --- (Tentatively give h its quantified type) h :: forall b . Eq b = b - Bool ! (Discharge the h_1st requirement, by unifying Bool - Bool ! with a fresh instance of forall b . Eq b = b - Bool) ! (Discharge the h_2nd requirement, by unifying [Char] - Bool ! with another fresh instance of forall b . Eq b = b - Bool) [...] This also throws up another issue; with polymorphic recursion, you might need an *infinite* family of specialized functions. Consider the following example: r x = (x==x) r [x] This also yields to the above technique of deferring unification for uses of let-bound variables until after quantification. Worth using? Regards, Tom ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
