[Haskell-cafe] Actual levity polymorphism

[Jeff Clites]

Very interesting. A few thoughts about potential rough spots:

> Representation polymorphism can be made to work today via type classes. That is, we have a `class Representation (r :: RuntimeRep)` whose dictionaries have instructions for how to store variables whose types have kind TYPE r, and also to apply functions to such variables. There's no good way to mock this up today because GHC requires a known RuntimeRep in order to bind a variable, but using instructions in a dictionary is possible instead. This would work just fine -- except that it would be very slow, because it means every store or function-apply requires a dictionary access. It would be disastrous.

It would also mean that even to access non-polymorphic function arguments (of a representation-polymorphic function), you would potentially need to consult the dictionaries for all preceding parameters, and that would vary depending on the calling conventions for a particular platform. For example, if a function takes a representation-polymorhpic first parameter and a (non-polymoprhic) unboxed float as its second parameter, then where to find that float would change if the first parameter ends up being an unboxed float. (Or rather, it would probably change for a register-based calling convention and possibly not change for a stack-based calling convention.) That is, assuming the the calling convention for representation-polymorphic function should be the same, once instantiated for a particular representation, as a non-representation-polymorphic function whose arguments have those particular representations. So that means the generated assembly for such a representation-polymorphic function would have to include code to figure all of that out per-invocation. [This is all just about the case of having a single non-specialized implementation as the outcome of compilation.] So that does seem conceptually possible but practically...perhaps not.

> However, GHC *already* has machinery for specializing functions to work with known dictionaries. All you would have to do is to ensure that all Representation dictionaries get specialized away; this could be done with a straightforward check (even implementable in a core plugin). So programmers can be polymorphic over representations, and GHC has to work hard to specialize. What this is missing is a nice mechanism for helping the programmer avoid cases that GHC can't specialize -- but that could be added later. I really think this would just work, quite easily.

At first glance, it seems like these dictionaries would be just like any other typeclass dictionaries in terms of the possibility of specializing them away (right?), so I wonder how much of the time that is possible. That is, I wonder if the programmer would run into forbidden cases commonly, and how limiting that would be.

For instance, could you have a representation-polymorphic `fold` (e.g., which you might call with an unboxed int accumulator value, with a matching accumulator function)?

I assume you couldn't have a rank-2 representation-polymorphic function? (That is, you couldn't have a representation-polymorphic unknown function. Is that right?)

Just sort of thinking out loud. [I've watched your Tweag videos about Levity Polymorphism but I haven't read the paper, so I hope I'm not asking questions that were already covered there. I need to read the paper!]

Thanks,

Jeff

> On Jan 7, 2023, at 10:20 AM, Richard Eisenberg <lists at richarde.dev> wrote:
> 
> For what it's worth, this initiative may get a significant boost soon. My main job at Jane Street these days is designing & implementing unboxed types for OCaml (which has never really had them, unlike their long history within GHC). There is much eagerness to use unboxed types. But we've realized that, to meet these expectations, we'll need the equivalent of levity polymorphism. So I'll be spending some time over the next few months (I think) putting together the design there. Once it starts to come together, I can share it and then work to adapt it to Haskell.
> 
> Though as I'm writing this, I see a really easy way to do this in Haskell. (Sadly for me, it won't work in OCaml.) Representation polymorphism can be made to work today via type classes. That is, we have a `class Representation (r :: RuntimeRep)` whose dictionaries have instructions for how to store variables whose types have kind TYPE r, and also to apply functions to such variables. There's no good way to mock this up today because GHC requires a known RuntimeRep in order to bind a variable, but using instructions in a dictionary is possible instead. This would work just fine -- except that it would be very slow, because it means every store or function-apply requires a dictionary access. It would be disastrous. However, GHC *already* has machinery for specializing functions to work with known dictionaries. All you would have to do is to ensure that all Representation dictionaries get specialized away; this could be done with a straightforward check (even implementable in a core plugin). So programmers can be polymorphic over representations, and GHC has to work hard to specialize. What this is missing is a nice mechanism for helping the programmer avoid cases that GHC can't specialize -- but that could be added later. I really think this would just work, quite easily.
> 
> Well, "easily" from a language-design standpoint. An efficient implementation in GHC would be fiddly, because you'd need to annotate every variable with information about its representation: either it's known (good), or it's not, and then the variable's representation is informed by a specific dictionary. I think this could probably all be tracked efficiently, but it wouldn't surprise me if there's a measurable slowdown in compilation times to track these representations. And infer them.
> 
> Left unaddressed here: how to make datatypes representation-polymorphic, which requires a lower-level understanding of data-constructor representations than I have.
> 
> Richard
> 
>> On Jan 6, 2023, at 11:51 AM, Carter Schonwald <carter.schonwald at gmail.com> wrote:
>> 
>> i've written (more opaquely than i'd like), about this topic a few times , including on that ticket https://gitlab.haskell.org/ghc/ghc/-/issues/14917#note_230433 ! 
>> 
>> ultimately, you want some notion of function types /lambdas that have the equivalent to the C++ Const-Eval / C++ Template arg "compile time instantiation is the only allowed flavor".
>> 
>> for the particulars in the context of runtime rep levity, my intuitions break down, but i've had examples of the sort of "must be resolved at compile time" where for the behavior i'd need isn't expressible using type classes because those can be instantiated abstractly rather than  concretely and still be valid programs. 
>> 
>> granted i'm not terribly current on the state of play in >= ghc 9.4 for this stuff, but i would not be surprised if the architectural hooks needed for a "strict staging lambda" arent there yet. (you can manufacture some of this stuff with typed template haskell, BUT theres no mechanism for expressing the primops that certain uses cases, like SIMD shuffle, would need)
>> 
>> On Mon, Jan 2, 2023 at 9:18 AM J. Reinders <jaro.reinders at gmail.com> wrote:
>> No, I found it. It is this GHC issue: 
>> 
>> https://gitlab.haskell.org/ghc/ghc/-/issues/14917
>> 
>> > On 2 Jan 2023, at 15:07, Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> wrote:
>> > 
>> > On Mon, Jan 02, 2023 at 02:01:56PM +0100, J. Reinders wrote:
>> >> I seem to recall another thread where there were more suggestions
>> >> like a special form of type classes that is always guaranteed to
>> >> monomorphise away
>> > 
>> > Perhaps this?
>> > 
>> > https://github.com/ghc-proposals/ghc-proposals/pull/454#issuecomment-1030258076