#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