Letting a distributed DSL implementation choose its serialization format (via constraint family)

Question

I'm writing a distributed programming DSL and I'd like to allow implementations to choose their serialization method (if any, as it might not even be needed for a simulated execution).

Trying to solve this by adding a type family led to the problem below for a standard function I have. I imagine that it would work if I could require, and have the type checker understand, that if two values are serializable their pairing is also serializable. However, adding that as a quantified constraint doesn't seem to work. Can this be solved or is there a better solution for the problem?

{-# LANGUAGE TupleSections #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TypeFamilies           #-}

import Data.Kind

class (Monad (DistrM t)) => Distributed (t :: *) where
  type Sendable t :: * -> Constraint
  type DistrM t :: * -> *
  -- ...

data FromSendable t a where
  FromSendable :: (Sendable t b)
               => (b -> DistrM t a)
               -> b
               -> FromSendable t a

pairWith :: ( Sendable t a
            , Distributed t
            , forall a b. (Sendable t a, Sendable t b) => Sendable t (a,b)
            )
         => a
         -> FromSendable t b
         -> FromSendable t (a,b)
pairWith a (FromSendable f b) =
  FromSendable (\(a,b) -> (a,) <$> f b) (a,b)

-- >>> Could not deduce: Sendable t (a1, b1) ...

Edit 1

It type checks if I do

pairWith :: ( Sendable t a
            , Distributed t
            , st ~ Sendable t
            , forall a b. (st a, st b) => st (a,b)
            )
         => ...

It would get cumbersome to have to repeat these types of constraints, so I tried a type synonym but that doesn't work:

type Cs t = forall (st :: * -> Constraint).
  (Sendable t ~ st, forall a b. (st a, st b) => st (a,b))
-- >>> Expected a constraint, but ‘st (a, b)’ has kind ‘*’

Answer 1

This looks weird. I only have a partial answer, but I'll post it anyway. I simplified your code to

class C t where   -- (*)

data T t where
  T :: C t => (a -> t) -> a -> T t

foo ::
   ( C u
   , forall a b . (C a , C b) => C (a, b) )
  => u -> T t -> T (u, t)
foo i (T f x) = T (\(a,b) -> (a, f b)) (i, x)

and, in this version, it compiles fine. However, if we replace

class C t where

with

type instance C :: * -> Constraint

then we get an error telling us that C (a, b) can not be deduced.

I can't completely understand what's going on here, but it looks like quantified constraints do not mix well with type families.

It looks like the above type family is treated like it were

type instance C (t :: *) :: Constraint

and in such case, I can't understand what's wrong. Since C now does not refer to a single type class, it is impossible to implement a quantified constraint like forall a b . (C a , C b) => C (a, b) by (say) passing a pointer to a specific instance, since the three C constraints could be anything at all, in an open world.

I still do not understand why type family C :: * -> Constraint is handled in the same way.

Perhaps GHC should reject quantified constraints involving type families ... -> Constraint in such way? I not sure.

Answer 2

I think you've pushed your code to the edges of GHC's type system here. You can fix the kind error on Cs by writing:

type Cs t = (forall (st :: * -> Constraint).
  (Sendable t ~ st, forall a b. (st a, st b) => st (a,b))) :: Constraint

but then you run up against "GHC doesn't yet support impredicative polymorphism". Until GHC adds support for class families as per issue 14860, you're maybe out of luck with this approach.

However, you did ask about alternative approaches. Doesn't making Sendable t a a multiparameter type class accomplish basically the same thing?

Certainly, the following type-checks:

{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TupleSections          #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE QuantifiedConstraints  #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TypeFamilies           #-}

import Data.Kind

class (Monad (DistrM t)) => Distributed (t :: *) where
  type DistrM t :: * -> *
  -- ...
class Sendable t a where

data FromSendable t a where
  FromSendable :: (Sendable t b)
               => (b -> DistrM t a)
               -> b
               -> FromSendable t a

type Cs t = forall a b. (Sendable t a, Sendable t b) => Sendable t (a,b) :: Constraint
pairWith :: ( Sendable t a
            , Distributed t
            , Cs t
            )
         => a
         -> FromSendable t b
         -> FromSendable t (a,b)
pairWith a (FromSendable f b) =
  FromSendable (\(a,b) -> (a,) <$> f b) (a,b)