[Haskell-cafe] Actual levity polymorphism

Wed Jan 11 13:13:22 UTC 2023

> On Jan 9, 2023, at 9:52 PM, Jeff Clites <jclites at mac.com> wrote:
> 
> 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. ... So that does seem conceptually possible but practically...perhaps not.

That's a good point about later parameters depending on earlier ones. I had been thinking that we need the information per parameter, but that's definitely wrong. We really need the parameters' representations on the -> in `\ x y z -> ...`, not on the x, y, z. Still doable. But definitely not pleasant.

> 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.

This is a good question, one I share.

> 
> 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)?

Yes. This is a case where the representation would be statically known, and thus specialized away. All good.

> 
> 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?)

This sounds like a case where we can't specialize away. The "cheap and cheerful" version of this simply tries to specialize. If any dictionaries are left after all specialization is complete, we error. This is poor for users, because it makes it very hard / impossible for a user to predict whether their program will be accepted. Put another way, this cheap-and-cheerful approach lacks a declarative specification of what programs are accepted. A more glorious approach, tracking which computations/specializations can be done at compile time, would solve this. That more glory is a large part of what I'll be looking at over the next few months.

> 
> 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!]

These are great points in the conversation. You seem to understand this well.

Thanks,
Richard

> 
> 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
> 
> 
> 