On Wed, Oct 28, 2015 at 5:05 AM, Simon Peyton Jones <simo...@microsoft.com> wrote: > I'm out of bandwidth at the moment, but let me just remark that this is > swampy territory. It's easy to mess up. > > A particular challenge is polymorphism: > > map :: forall a b. (a->b) -> [a] -> [b] > map f (x:xs) = (f x) : (map f xs) > > In the compiled code for map, is a thunk built for (f x), or is it evaluated > eagerly. Well, if you can instantiate the 'b' with !Int, say, then it should > be evaluated eagerly. But if you instantiate with Int, then build a thunk. > So, we really need two compiled versions of 'map'. Or perhaps four if we > take 'b' into account. In general an exponential number.
You can't insantiate `b` to `!Int` without map quantifying over levity, which is somewhat orthogonal (although it would have interactions). Without that, b has kind *, and !Int has kind Unlifted, so this is a kind error. Or, map is explicitly written having b :: Unlifted, in which case it already has the right calling convention. > That's one reason that GHC doesn't let you instantiate a polymorphic type > variable with an unlifted type, even if it is boxed. It's a reason to not put boxed, unlifted types in *. I don't think it's a reason not to allow quantifying over a separate kind of uniformly represented, unlifted types (i.e. doesn't include Int#, Double#, etc.). > Another big issue is that *any* mixture of subtyping and (Haskell-style) > parametric polymorphism gets very complicated very fast. Especially when you > add higher kinds. (Then you need variance annotations, and before long you > want variance polymorphism.) I'm extremely dubious about adding subtyping to > Haskell. That's one reason Scala is so complicated. I'm not sure how much of this would be required. But how are you saved from this in the impredicativity proposal, which is already attempting to handle more of the induced subtyping of higher-rank types? I would guess it's mostly a matter of, "we're not going to support all that." Which might be fine for the unlifted stuff as well. Richard wrote: > But these do, I think. In running code, if (==) is operating over a lazy > type, it has to check if the pointer points to a thunk. If (==) is operating > over a strict one, it can skip the check. This is not a big difference, but > it *is* a difference. Yeah. It's not that (==) is parametric really. It's that Eq might be able to be parameterized on levity. But this is very useful, since it allows you to instantiate Eq on a bunch of unlifted reference types instead of having to use one-off functions like sameMutableArray#. > A little more thinking about this has led here: The distinction isn't really > forall vs. pi. That is, in the cases where the levity matters, we don't > really need to pi-quantify. Instead, it's exactly like type classes. Yes, I think so, too. It is ad-hoc polymorphism that can be handled by type classes. There is no reason for an explicit value-level witness of levity that can be cased on, which is presumably what pi would allow. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
