Constraints on the type argument of a GADT

Learn
#1

I have some code for a RPC-style services, where the calls to a service are represented as a GADT with the result type as a type parameter, alike

data Service a where
  Get :: Service Int
  Set :: Int -> Service ()

Then, I have some code to call said service, a la

call ::
  forall msg.
  (forall res. msg res -> Encoding) ->
  (forall res. msg res -> Decoder RealWorld res) ->
  msg res ->
  m res
call encode mkDecoder msg = _

This Encoding and Decoder comes from the cborg package. Now, a consumer of the library may have Serialise instances for forall res. msg res around, as well as for every possible res. I can use the former easily, but I’m stuck on how to consume the latter.
I can define a function like

callSerialise ::
  (forall res. Serialise (msg res)) =>
  (forall res. msg res -> Decoder RealWorld res) ->
  msg res ->
  m res
callSerialise mkDecoder msg = call encode mkDecoder msg

with encode a class member of Serialise, but this leaves this ugly mkDecoder to be provided by the user, which would be something boilerplate like

myMkDecoder = \case
  Get{} -> decode
  Set{} -> decode

where decode is a class member of Serialise.

Is there a way, in callSerialise, to express

  1. For every possible msg res, there should be an instance Serialise res, and
  2. Given an msg res and the above requirement fulfilled, somehow get the instance (and its decode member) in scope to be used

I looked into the constraints package with its Dict, but that doesn’t seem to suit what I’d like to achieve. Any pointers would be appreciated!

1 Like
#2

It seems like the constraints for callSerialise you want would mean that every type is an instance of Serialise. I’d guess that this can’t be right. It’s very possible I’m misunderstanding something, but here is my reasoning.

In callSerialise, the constraint on msg is forall res. Serialise (msg res). So in order to use callSerialise, there must be some choice of msg that meets this constraint. Let’s call it Msg. Then for any type T, Msg T has Serialise.

You say that you also want to express this constraint:

  1. For every possible msg res, there should be an instance Serialise res

If a "possible msg res" means any msg res that can be used in callSerialise, then Msg T from above is one possible type. So there should be an instance Serialise T. But T was arbitrary, so all types are instances of Serialise.

If all this is correct, wouldn’t just adding the constraint Serialise res be enough? But as I said, I may be confused…

1 Like
#3

Thanks for getting back!

In the case of Service, which is an example of a msg res, the set of types which could be in the res position is well-known: it’s either Int (from the Get constructor in the GADT), or () (from the Set constructor). Hence, what I’d like to express is: if you pass a Service res to callSerialise, then (whichever) res must have a Serialise instance, i.e., Int and () must have a Serialise instance, and I can recover the exact type res represents within callSerialise, because you gave me a Service res.

Of course, if there’d be some SomeRes :: Service a constructor for Service, then the set of possible types in the res position is not fixed, and indeed I’d need to provide a Serialise instance for every possible type res, which is indeed not possible. However, for actual Service-like datatypes in my application, every res in every constructor is fixed.

Hope that clarifies a bit.

2 Likes
#4

Yes, that clarifies a lot! I wasn’t seeing that a GADT can restrict the type of its parameters. Thank you for explaining! Maybe I’m beginning to understand some of this stuff…

I have a feeling we’ve already switched over to you teaching me, instead of me trying to help you, but I have an idea I’d like to share.

My idea is: how about using a class to witness that your msg res type has the necessary instances of Serialise res, like this?

class Decodable msg where
  mkDecoder ::
    forall res. Serialise res => 
    msg res -> 
    Decoder RealWorld res
  mkDecoder _ = decode

instance Decodable Service

callSerialise' ::
  (Decodable msg, forall res. Serialise (msg res)) =>
  msg res ->
  m res
callSerialise' msg = call encode mkDecoder msg

You also have to add a constraint to the type signature of the second parameter to call (although I don’t think this would be a problem):

  (forall res. Serialise res => msg res -> Decoder RealWorld res)
2 Likes
#5

Hmh, I had not considered introducing a new class… That could work indeed, I’ll experiment a bit. Ideally I wish there’d be a way around without a new class, but fair enough. Thanks for the hint!

1 Like