[Haskell-cafe] Backpack: polymorphic instantation?

[Jaro Reinders]

I have now found a way to implement a PrimMonad signature using type 
(constraint) families and equality constraints. It supports IO, ST, and 
ReaderT. The code is here:

https://gist.github.com/noughtmare/3aaef4bce58154f47afe6941ea74ac4f

It still feels like a hack (and maybe even a bug with the GHC implementation of 
Backpack), but it seems to work (it compiles, so it must work :P). I would love 
to know if there is an easier way.

Now, I'll try to see if this is actually practical to use.

Cheers,

Jaro

On 11-09-2021 11:58, Jaro Reinders wrote:
> I'm playing around with backpack, trying to rewrite existing libraries. My end 
> goal is to see if Backpack could improve the primitive library. Right now, the 
> primitive library (in my opinion) relies too heavily on specialization of its 
> type classes, so I think Backpack could help. However, I seem to be running 
> into a limitation. I am wondering if it is a fundamental limitation, if perhaps 
> there is a workaround, or if Backpack could be improved to support this use-case.
> 
> Instead of primitive, I will take the simpler example: semigroup, which also 
> shows this limitation. Let's convert the Semigroup class to a backpack signature:
> 
>      unit indef where
>        signature Semigroup where
>          import Prelude hiding ((<>))
>          data T
>          (<>) :: T -> T -> T
> 
> The problem is how to implement this signature with the type of polymorphic 
> lists. It is easy to implement it for concrete lists like strings:
> 
>      unit string where
>       module Semigroup where
>        import Prelude hiding ((<>))
>        type T = String
>        (<>) :: T -> T -> T
>        (<>) = (++)
> 
> It is also possible to implement it in terms of another signature:
> 
>      unit list where
>        signature Elem where
>          data A
> 
>        module Semigroup where
>          import Prelude hiding ((<>))
>          import Elem
>          type T = [A]
>          (<>) :: T -> T -> T
>          (<>) = (++)
> 
> This is still problematic, because it is annoying that this new type A needs to 
> be instantiated each time you want to use it. However, even more importantly, 
> if I want to translate the 'PrimMonad' class to a Backpack signature then the 
> 'ST s' instance needs a polymorphic type variable 's', which cannot be made 
> concrete.
> 
> And do note that I want the monad to be concrete for performance reasons, but 
> the 's' parameter doesn't have to be concrete, because it is a phantom 
> parameter anyway. And for lists making the 'a' parameter concrete also would 
> not improve performance as far as I know.
> 
> One possible way to fix this is to add a type variable in the 'Semigroup' 
> signature, but then I think it becomes impossible to write the 'String' 
> instance and sometimes you need more than one new type variable such as with 
> the 'ReaderT r (ST s)' instance of 'PrimMonad'.
> 
> In OCaml you can still kind of work around this problem by creating local 
> instances inside functions. That trick still allows you to write a polymorphic 
> concatenation function using a monoid signature (taken from [1]):
> 
>      let concat (type a) xs =
>        let module MU = MonoidUtils (ListMonoid(struct type t = a end)) in
>        MU.concat xs;;
> 
> So, I'm wondering if it would be possible to "generalise" over indefinite 
> Backpack types such as 'A' in the 'Elem' signature above or if we can at least 
> implement something which enables the same trick that you can use in OCaml.
> 
> Thanks,
> 
> Jaro
> 
> [1] https://blog.shaynefletcher.org/2017/05/more-type-classes-in-ocaml.html