[Haskell-cafe] Actual levity polymorphism

[J. Reinders]

I think theoretically a type class is indeed all you need even for representation polymorphism. I believe that is what the Sixten language [1] does.

Currently GHC rejects any levity polymorphic function arguments and local binders. Issue #15532 [2] tracks the possibility of relaxing these restrictions. The type class approach is mentioned in that thread. 

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 and another suggestion that functions that are always guaranteed to inline can also be allowed to be representation polymorphic. But I can’t find this thread again.

Also, I think the identity function is so simple that you don’t even need the KnownLevity class for levity polymorphism. The implementation can just copy the pointer from the input to the output.

Cheers, 
Jaro

[1] https://github.com/ollef/sixten
[2] https://gitlab.haskell.org/ghc/ghc/-/issues/15532

> On 2 Jan 2023, at 13:02, Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> wrote:
> 
> I'm investigating unboxed types in GHC 9.2.  Levity polymorphism seems
> to be severely limited in a way that makes it hard to envisage a
> Haskell ecosystem which comfortably combines lifted and unlifted
> types.  Am I missing something?
> 
> Understandably, the following attempt at defining a
> RuntimeRep-polymorphic identity does not work:
> 
>    myId1 :: forall (r :: RuntimeRep) (t :: TYPE r). t -> t
>    myId1 x = x
> 
> The GHC Users Guide explains why[1].  It's impossible to generate code
> for myId1 because there is no way of determining the machine
> representation of the argument x.
> 
> But worse, it's not even possible to define a *Levity*-polymorphic
> identity:
> 
>    myId2 :: forall (lev :: Levity) (t :: TYPE (BoxedRep lev)). t -> t
>    myId2 x = x
> 
> In this case the argument can only have kind TYPE LiftedRep or TYPE
> UnliftedRep.  The machine representation is the same in each case.
> The problem this time is that the code generator doesn't know whether
> it should emit code to evaluate the argument (UnliftedRep case) or not
> (LiftedRep case). But this seems like a solvable problem.  Surely a
> KnownLevity type class (possibly magical) could solve the problem.
> This seems like it should work
> 
>    myId3 :: forall (lev :: Levity) (t :: TYPE (BoxedRep lev)).
>             KnownLevity lev =>
> 	     t -> t
>    myId3 x = x
> 
> and in fact I wouldn't be surprised if this could be made to work:
> 
>    myId4 :: forall (r :: RuntimeRep) (t :: TYPE r).
>             KnownRuntimeRep r =>
> 	     t -> t
>    myId4 x = x
> 
> So what is the situation here?
> 
> 1. myId3 already works (then where is KnownLevity made available and
>   why isn't it mentioned in the Users Guide?)
> 
> 2. myId3 can never work (then why not?)
> 
> 3. myId3 might be able to work but it's an open research problem (then
>   who is working on it, if anyone?)
> 
> 4. myId3 would work and it would be useful but no one's proposed or
>   implemented it (then who would be the best person to collaborate
>   with on that?)
> 
> 5. myId3 would work but it would not actually be useful (then what
>   have I misunderstood?)
> 
> I suspect the answer is 1 (or maybe 4) based on the following passage
> in the Levity Polymorphism[2] paper by RE & SPJ[2]:
> 
>> users can use a runtime type check (though GHC’s Typeable feature)
>> to determine the memory representation of an as-yet- unbound
>> argument to a function
> 
> (and the same questions for myId4).
> 
> Thanks,
> 
> Tom
> 
> [1] https://downloads.haskell.org/~ghc/9.4.4/docs/users_guide/exts/representation_polymorphism.html#no-representation-polymorphic-variables-or-arguments
> 
> [2] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/levity-pldi17.pdf
> _______________________________________________
> 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.