Opened 19 months ago

Last modified 13 months ago

#14917 new feature request

Allow levity polymorphism in binding position

Reported by: andrewthad Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.2
Keywords: LevityPolymorphism Cc: dfeuer, Ericson2314
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (22)

comment:1 Changed 19 months ago 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!

comment:2 Changed 19 months ago 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.

comment:3 Changed 19 months ago 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.

comment:4 Changed 19 months ago by Iceland_jack

If something changes in the inliner could working levity-poly definitions fail?

comment:5 Changed 19 months ago 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.

comment:6 Changed 19 months ago 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.

comment:7 Changed 19 months ago 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.

comment:8 Changed 19 months ago 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.

comment:9 Changed 18 months ago 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?

comment:10 Changed 18 months ago by goldfire

Sure we do. I have not explored how we do, but sure we do. This program compiles and runs:

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.

comment:11 Changed 18 months ago by dfeuer

Could we skirt the problem using typeclass machinery? Instead of

bTwice ::  (r :: RuntimeRep) (a :: TYPE r). Bool  a  (a  a)  a

What if we have

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?

comment:12 Changed 18 months ago by dfeuer

Cc: dfeuer added

comment:13 Changed 18 months ago by dfeuer

Summary: Allow levity polymorhism in binding positionAllow levity polymorphism in binding position

comment:14 Changed 18 months ago 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_unpackedcontainers/

comment:15 Changed 18 months ago 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.

comment:16 Changed 18 months ago 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

idList :: [a] -> [a]
idList = id

even though you could have

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.

Generally, these schemes fail on polymorphic recursion, and I think we should do so here, too.

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.

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.

comment:17 Changed 18 months ago by sgraf

Another place where this could be useful is for abstracting the pattern in efdt{Word,Int}{Up,Dn}FB.

comment:18 Changed 13 months ago 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 some open terms are too. A term whose free variables are all irrelevant is also a monomorphic term. This might seem counterintuitive--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 run-time 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 quantifiers 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 irrelevant 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.

Last edited 13 months ago by Ericson2314 (previous) (diff)

comment:19 Changed 13 months ago 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.

comment:20 Changed 13 months ago by Ericson2314

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.

Once we have the monomorphizing quantifiers, I would advocate for / draft a language extension 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.

Last edited 13 months ago by Ericson2314 (previous) (diff)

comment:21 Changed 13 months ago by bgamari

Someday, I want to rewrite the RTS in Haskell...without getting RSI from wrist typing boilerplate

You are not the only one ;)

comment:22 Changed 13 months ago by Ericson2314

Cc: Ericson2314 added
Note: See TracTickets for help on using tickets.