[GHC] #14917: Allow levity polymorhism in binding position
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple LevityPolymorphism | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The main problem with levity polymorphism in a binding position is that it's impossible to do codegen since the calling convention depending on the instantiation of the runtime representation variable. From the paper, we have the following rejected example code: {{{ bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a }}} However, if you are able to inline the function, this problem disappears. You would need a guarantee stronger than what the `INLINE` pragma provides though since the `INLINE` pragma still allows the function to be fed as an argument to a higher-order function. I'll refer to a hypothetical new pragma as `INLINE MANDATE`. This pragma causes a compile-time error to be admitted if the function is ever used in a way that would cause it to not be inlined. Now `bTwice` would be writeable: {{{ {-# INLINE MANDATE #-} bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a }}} The function definition would be provide in the `.hi` file just as it would be for a function marked as `INLINE`, but unlike the `INLINE` counterpart, there would be no generated code for this function, since generating the code would be impossible. I have several uses for this in mind. I often want a levity-polymorphic variant `ST`. With `INLINE MANDATE`, I still wouldn't get `do` notation, but I could write: {{{ -- This newtype is already allowed today newtype STL s (a :: TYPE r) = STL (State# s -> (# s, a #) #) intA, intB, intC :: STL s Int# wordA, wordB :: Int# -> STL s Word# {-# INLINE MANDATE #-} (>>=.) :: STL s a -> (a -> STL s b) -> STL s b STL a >>=. g = STL (\s0 -> case a s0 of (# s1, v #) -> case g v of STL f -> f s1 myFunc :: STL s Word# myFunc = intA >>=. \a -> intB >>=. \b -> intC >>=. \c -> wordA a >>=. \wa -> wordB b >>=. \wb -> ... -- do something with the data }}} I would appreciate any feedback on this. If there's something that makes this fundamentally impossible, that would be good to know. Or if other people feel like this would be useful, that would be good to know as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm very cautious about this. Sometimes you can't inline. For example a recursive function. And {{{ f :: Int -> Int {-# INLINE f #-} f x = blah g xs = map f xs }}} I can't inline `f` here; or if I do I'll get a `\x`. In our paper we prove that, in our system, you never get a situation where you don't know the runtime reprsentation of a value you have to manipulate. I don't see how to produce a similar proof with weaker restrictions. Runtime code cloining, like .NET, is a good path. But it comes at a price! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by andrewthad): I agree that it isn’t always possible to inline. Higher order functions, like map, don’t allow it. Maybe the most accurate way to describe what I want is for there to be a way to make fully saturated calls to functions with levity polymorphic binders. It seems like it should be possible to perform a check for unsaturated calls. Recursive levity polymorphic functions would not be allowed, but there’s still a lot of useful stuff that could be done. Your point about the proof that the paper offers is good. My suggested addition would mess up that proof, which would be bad. What if (and this is total speculation since I don’t understand type theory) you had two universes that functions could live in. One universe is this one that we currently have. There are no levity polymorphic binders, and in this universe, you have the guarantee that you always know the runtime representation of values that need to be manipulated. In the second universe, levity polymorphism would be unrestricted. Technically, this universe would be a superset of the first one. But it may be helpful to think of them as separate universes since in GHC, codegen could only happen for functions in the first universe. Functions from 1 could be freely used in 2. Functions from 2 could be freely used in 2 as well. But, functions from 2 could not be freely used in 1. They would need to be specialized to satisfy the restrictions around levity polymorphism. In practice, this specialization would take the form of inlining. So, I guess that would mean that the function arrow would have a weird kind, since it could create types belonging to universe 1 or 2. And I have no idea how function application would typecheck. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I actually think this is a good idea. Simon's right in that figuring out exactly when you can inline can be tricky. But this logic is already in the compiler (in the inliner!) and so we can perhaps work it into the desugarer (which is where levity- polymorphism errors are issued). It's possible we'll have a hard time producing sensible error messages, but I think we'll be able to surmount that challenge. As to the proof: I'm not concerned. The proof is about Core. The proposed change wouldn't affect Core at all. Core still wouldn't have levity- polymorphic binders. (Unfoldings might, but not actual Core programs that will be compiled.) We can think of this proposal as suggesting "function templates", where these templates are stand-ins for a (perhaps infinite) family of levity-monomorphic functions. The implementation of this would be fiddly, but I don't see any true obstacles to it. And it does seem very silly that users can't reuse their typing for a function as simple as `twice`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): If something changes in the inliner could working levity-poly definitions fail? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by andrewthad): @Iceland_jack I believe that the inlining phase (or phases) happens after type checking, so this couldn’t even be done during the usual inlining phase. You would need something similar to the inlining phase that happens prior to type checking. The only things allowed to inline during this phase would be fully saturated calls to functions with levity polymorphic binders ( maybe function template, as Richard suggests, is an appropriate name for it). This is why Richard says that it would be hard to produce sensible error messages. So, I don’t think that changes to the inliner could mess this up because this would be a separate and unusual inlining phase. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I am a bit less optimistic than Richard (in comment:3). You imply that all the inlining could be done in the desugarer; but that can only work if you could see all calls. GHC does already have the notion of a "compulsory unfolding" (see `CoreSyn.UnfoldingSource`). Bindings with a compulsory unfolding ''do not have a binding at all'', so they must be inlined at every call site. That fits with the proposal here because we can't implement the levity- polymorphic code, so we can't compile code for it. We'd still somehow need to check that, after the inlining, the levity- polymorphism had vanished, and give a decent error message if not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, I was thinking of compulsory unfoldings without realizing it. I think the existing check for levity-polymorphic arguments in the desugarer (which wouldn't change under this proposal) would catch cases where a levity-polymorphic function wasn't sufficiently specialized. All that would be left to check for is that the compulsory unfolding would actually work (and that the function was sufficiently saturated). If it doesn't, I think we would be able to report a sensible error, because we at least have the name of the thing that didn't unfold. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): You know, this is all very much like unboxed tuples. Unboxed tuples are themselves levity polymorphic, must be levity monomorphic at use sites, and have a compulsory unfolding. So perhaps much of the plumbing is installed already. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
You know, this is all very much like unboxed tuples.
But do we allow `(#,,#) x y` or stuff like that with a possibly- unsaturated use of the data constructor? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Sure we do. I have not explored ''how'' we do, but sure we do. This program compiles and runs: {{{#!hs data List (b :: TYPE (TupleRep [IntRep, DoubleRep, LiftedRep])) = Nil | Cons b (List b) mapUbx :: forall (a :: Type) (b :: TYPE (TupleRep [IntRep, DoubleRep, LiftedRep])). (a -> b) -> [a] -> List b mapUbx _ [] = Nil mapUbx f (x : xs) = Cons (f x) (mapUbx f xs) blargh :: forall a. Int# -> Double# -> a -> (# Int#, Double#, a #) blargh x y = (#,,#) x y strange = mapUbx (blargh 3# 2.78##) [True, False] printList :: Show b => List (# Int#, Double#, b #) -> IO () printList Nil = return () printList (Cons (# n, d, b #) xs) = do print (I# n) print (D# d) print b printList xs main = do printList strange }}} We probably just eta-expand `blargh`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Could we skirt the problem using typeclass machinery? Instead of {{{#!hs bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). Bool → a → (a → a) → a }}} What if we have {{{#!hs bTwice :: ∀ (r :: RuntimeRep) (a :: TYPE r). KnownRep r => Bool → a → (a → a) → a }}} To call this function, we consult the `KnownRep` dictionary to discover its calling conventions. Obviously everything will be terrible if it doesn't specialize, but maybe there's a way to make it work soundly otherwise? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorhism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * cc: dfeuer (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by andrewthad): There was a reddit discussion[1] that reminded me of this, and it got a tangential but related idea going in my mind. I wonder if there's any connection between user-defined functions with a compulsory unfolding and `UNPACK` on polymorphic fields in a data constructor (currently disallowed because they result in code that cannot be compiled). Roughly, the idea was that a compulsory unfolding would be required for functions that target data types with unpacked polymorphic fields. For example: {{{ data Foo a = Foo {-# UNPACK -#} !Int {-# UNPACK #-} !a {-# INLINE MANDATE useFoo #-} useFoo :: Foo a -> a useFoo (Foo _ a) = a }}} This would also lift the restriction on levity-polymorphic fields in a data constructor. There are a bunch of other problems with this that may not be possible to resolve. How does pattern matching actually work with this? How can `Foo Word` be stored inside of another data type? Anyway, I'm not convinced this could actually go anywhere, but I thought I'd jot it down. [1] https://www.reddit.com/r/haskell/comments/8a5w1n/new_package_unpackedcontain... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by josef): I've thought about this problem for some time, but never written down my ideas before. Now seemed like a good time to speak up though :-) Below are some hopefully coherenet notes. I'd introduce a new quantifier (let's call it "V") which provides '''template polymorphism'''. This quantifier can quantify over all kinds, even levity polymorphic things. The idea is that whenever a function of template polymorphic type is called, a new copy of the function will be created, specialized with the instantiated type for its template polymorphic type variables. Example: {{{ id :: V r (a :: TYPE r). a -> a id a = a }}} When we use it like in an expression like this `id #5` or `id "foo"` the typechecker creates new bindings `id_#_Int#` and `id_*_String`. These new bindings are then used as part of elaborating the expressions: `id_#_Int# #5` and `id_*_String "foo"`. {{{ id_#_Int# :: Int# -> Int# id_#_Int# a = a id_*_String :: String -> String id_*_String a = a }}} More formally: A call to a template polymorphic function must instantiate all template polymorphic type parameters. These parameters must be instantiated with either fully ground types without any variables, or variables bound by "V", the template polymorphic quantifier. A trivial point, that I still want to point out: given two (or more) calls to the same template polymorphic function with the same type instantiation only generates one new specialization. Most likely a more sophisticated naming scheme than the one I've used here will be needed to ensure that the names of the new bindings are unique. The quantifier is only allowed to be used on the top-level and must appear before any usual quantifiers. I.e. template polymorphism is rank-1. Quantified template polymorphism, i.e. having class constraints on template polymorphic type variables is not a problem. == Recursion == It is perfectly possible to support monomorphic recursion for template polymorphism. In fact, the elaboration outlined above supports monomorphic recursion out of the box. The recursive call inside of template polymorphic function would generate the same specialization as a call from outside the function, and since we don't generate multiple specializations, the call will simply be specialized to a recursive call in the new specialized function. It is likely possible to support special cases of polymorphic recursion, but it is not clear to me that it is worth the extra work. == Modules == When exporting a template polymorphic function, it's specializations should also be exported, to avoid re-generating them. However, the importing module will have to creating its own new specializations if needed. This can lead to a situation where a module has two imports which exports the same specialization of a function they in turn imported. But there is no real problem here, because it doesn't matter which one we pick since both specializations will be the same. == Extensions == One of the interesting things about this proposal is that generalizes nicely to data types. Example: {{{ data List (V r) (a :: TYPE r) = Cons a (List r a) | Nil }}} This way we get a list data type which can be used at any kind. After type checking and elaboration we will have one list data type for each runtime representation. However, supporting specialization in different modules might require a bit of thought. == Final thoughts == The gist of this proposal is that it gives control over optimization to the library writer, similarly to the RULES pragma. Though it will not help any existing programs go faster. I'd really like to see something like this in GHC. Unfortunately, I don't have the cycles to flesh out this proposal and implement it. But I'd be happy to advice if someone wants to have a go at it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I, too, have pondered template polymorphism for some time, but never fleshed it out even to this level. There are a few problems with this design, however:
More formally: A call to a template polymorphic function must instantiate all template polymorphic type parameters. These parameters must be instantiated with either fully ground types without any variables, or variables bound by "V", the template polymorphic quantifier.
This means that, with your `id` definition, you couldn't have {{{#!hs idList :: [a] -> [a] idList = id }}} even though you could have {{{#!hs idListInt :: [Int] -> [Int] idListInt = id }}} So it seems template polymorphism would be infectious, generally requiring callers of template-polymorphic functions also to be template-polymorphic. I don't think that's a good thing. On the flip side, I don't see concretely why we need the "no variables" restriction.
It is likely possible to support special cases of polymorphic recursion, but it is not clear to me that it is worth the extra work.
This can lead to a situation where a module has two imports which exports the same specialization of a function they in turn imported. But
Generally, these schemes fail on polymorphic recursion, and I think we should do so here, too. there is no real problem here, because it doesn't matter which one we pick since both specializations will be the same. I think there ''is'' a real problem here. First off, it means that the `.o` files that GHC produces won't be able to be linked by, e.g., `ld`: multiple `.o` files might have the same definitions. In the end, I think we'd have to implement some deduplication algorithm during linking, or end up with horrid code bloat.
One of the interesting things about this proposal is that generalizes nicely to data types.
Under your "no variables" rule, this `List` type would have to be specialized at every possible data parameter. I'm worried about bloat.
However, supporting [data] specialization in different modules might require a bit of thought.
This is also a thorny question. Here, we absolutely have to get deduplication correct, as it's a matter of correctness, not just efficiency (in size of the executable). One unaddressed question here is: what restrictions would there be on template-polymorphic levity-polymorphic variables? Presumably, none, but I'm not sure. Also, how is this different from the "compulsory unfoldings" idea earlier in this thread (started in comment:3)? The user declares template polymorphism directly (the compulsory unfoldings idea didn't have any user direction -- but perhaps it should have), and the specializations here happen by creating new bindings instead of inlining, but I'm not sure a user would really see the difference here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by sgraf): Another place where this could be useful is for abstracting the pattern in [https://hackage.haskell.org/package/base-4.11.0.0/docs/src/GHC.Enum.html#efd... efdt{Word,Int}{Up,Dn}FB]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ericson2314): Taking a step back, I think the first thing we need is a notion of a monomorphic term. A closed term is a monomorphic term, but sime open terwm are too. A term whose free variables are all irellevant is also a monomorphic term. This might seem counterintuitive and maybe I need a new name because of that, but it makes sense because we don't actually want to specialize on types: we just want to specialize on relevant things like runtime representations and constraint dictionaries. The second thing to note is that is that substitution preserves monomorphic-term-ness, so in some sense template polymorphism shouldn't be too hard. What I mean by preservation is that it that the body of an abstraction is a monomorphic term other than the free variable being replaced, and the substituted term is monomorphic, then the beta-reduced term is monnomorphic. The issue with polymorphic recursion is not that we can't make progress unlining, but that the partial evaluation may not terminate. For template polymorphism, I think annotations are sufficient. We want be able to force otherwise-optional specialization "deeply", and control where that request is undecidable vs where it is guaranteed to succeed or prevented from trying. The new quanitifers would be, as said, to require specialization, with the "infection" @goldfire points out that entails. Besides runtime reps, this is also needed for CLaSH, and intrinsics taking immediate values (as @carter told me about). Variables bound with such quantifiers would not penalize monnomorphic terms. That means the final definition of a monnomorphic term is one whose free variables are all irellevant or "monomorphizable". Lastly, I welcome the object file problems. As we said to @goldfire and @nomeata at an NYC Meetup, it's annoying that module organization, a convenience for humans, ends up affecting performance. We desperately want to cache compilation on as fine a granularity as possible, too. I hope tackling this inlining issue forces that caching one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Richard says ''This means that, with your id definition, you couldn't have'' {{{ idList :: forall a. [a] -> [a] idList = id }}} Yes you could! `idList` is parameterised over a normal always-boxed type variable, so all its calls will be at boxed types. So `idList` can call the boxed-a version of `id`. Easy! Template polymorphism is not infectious. On the contrary, you have to keep specifying it for each enclosing function. It's a bit tiresome to have to do this -- it'd be easier for the programmer to say that ''all'' polymorphism can be specialised in this way, as .NET does -- but I think that's out of reach for us.
Generally, these schemes fail on polymorphic recursion, and I think we should do so here, too.
I don't think so. For `f :: V r. forall (a :: TYPE r). blah` we need one version of `f` per instantation of `r`. And there are only a finite number of possiblities for `r` (boxed pointer, unboxed-32-bit, unboxed-64-bit, etc). If a function is template-polymorphic in N `RuntimeRep` parameters, then you could get a number of versions exponential in N, but that's very pathological.
Under your "no variables" rule, this List type would have to be specialized at every possible data parameter. I'm worried about bloat.
I agree. I don't understand this no-variable business. Just one specialisation per variant of the `RuntimeRep` parameter(s).
In the end, I think we'd have to implement some deduplication algorithm during linking
We already have this problem with specialisation. Suppose you say {{{ module Lib where f = bah f :: Num a => a -> a {-# INLINABLE f #-} module A where { import Lib; foo = f :: Int -> Int } module B where { import Lib; bar = f :: Int -> Int } module C where { import Lib; import A; bax = f :: Int -> Int } }}} Then A and B will independently generate a duplicate version of `f` specialised for `Int -> Int`. But C will not, because it can use the specialised version it "sees" from A. So far no one has reported unacceptable bloat. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
It's a bit tiresome to have to do this -- it'd be easier for the
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ericson2314): programmer to say that all polymorphism can be specialised in this way, as .NET does -- but I think that's out of reach for us. Once we have the monomorphizing quantifiers, I would advocate for a language proposal to infer runtime rep parameters and {{{TYPE r}}} where where {{{Type}}} is inferred today. (Someday, I want to rewrite the RTS in Haskell...without getting RSI from wrist typing boilerplate :D)
And there are only a finite number of possiblities for {{{r}}}
Well, we'd also like to use this to statically prevent dictionary passing, and constraints are in generate infinitely inhabited. Also it would be nice to unbox aggregates in collections, maybe reusing the unboxed tuple and sum representations. That also creates infinite choices for {{{r}}} in principle. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by bgamari):
Someday, I want to rewrite the RTS in Haskell...without getting RSI from wrist typing boilerplate
You are not the only one ;) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14917: Allow levity polymorphism in binding position -------------------------------------+------------------------------------- Reporter: andrewthad | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Ericson2314): * cc: Ericson2314 (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14917#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC