[Haskell-cafe] Backpack: polymorphic instantation?

[Jaro Reinders]

Nevermind. The PrimReaderT module doesn't actually implement the signature.

On 12-09-2021 12:13, Jaro Reinders wrote:
> 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