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 ‘*’

The type error is because you've mixed up `b`s - the value level `b` you pull out of the `FromSendable f b` isn't of type `b`. This compiles: `pairWith a (FromSendable f b) = FromSendable (\b -> (a,) <$> f b) b`. It only needs the `Distributed t` constraint, but this is equivalent to realizing `FromSendable t` is a functor, and writing `deriving instance (Distributed t) => Functor (FromSendable t); pairWith a = fmap (a,)`. (In fact, we can even weaken `Distributed t` to `Functor (DistrM t)`). But I don't really understand what you're trying to do / whether this really solves your problem. — moonGoose, Jun 21 '20 at 01:55
Thanks for your comment. I neglected to convey this properly but it's really essential to keep `(a,b)` since that's what's going to be sent over the wire. The library ensures that `f` is always the same wherever it's used. — æons, Jun 21 '20 at 13:30

chi · Answer 1 · 2020-06-21T15:49:53.107

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.

Thanks for simplifying the problem for me! Your comment led me to find [this issue](https://gitlab.haskell.org/ghc/ghc/issues/14860) on the GHC issue tracker which helped me make some progress. I'll update the original question. — æons, Jun 21 '20 at 15:17

score 1 · Answer 2 · answered Jun 21 '20 at 19:44

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)

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

Edit 1

2 Answers2