Re: [Haskell-cafe] Actual levity polymorphism

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 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 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 mailto:jaro.reinders@gmail.com> wrote: No, I found it. It is this GHC issue:

https://gitlab.haskell.org/ghc/ghc/-/issues/14917 https://gitlab.haskell.org/ghc/ghc/-/issues/14917

...

On 2 Jan 2023, at 15:07, Tom Ellis mailto:tom-lists-haskell-cafe-2017@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-1030258... https://github.com/ghc-proposals/ghc-proposals/pull/454#issuecomment-1030258... _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.