1

我正在编写一个分布式编程 DSL，我希望允许实现选择它们的序列化方法（如果有的话，因为它甚至可能不需要模拟执行）。

尝试通过添加类型族来解决这个问题，导致我拥有的标准函数出现以下问题。我想如果我可以要求它会起作用，并且让类型检查器理解，如果两个值是可序列化的，它们的配对也是可序列化的。但是，将其添加为量化约束似乎不起作用。可以解决这个问题还是有更好的解决方案？

{-# 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) ...

编辑 1

它会检查我是否这样做

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

必须重复这些类型的约束会很麻烦，所以我尝试了一个类型同义词，但这不起作用：

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

2 回答 2

1

这看起来很奇怪。我只有部分答案，但无论如何我都会发布它。我将您的代码简化为

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)

而且，在这个版本中，它编译得很好。但是，如果我们更换

class C t where

和

type instance C :: * -> Constraint

然后我们得到一个错误，告诉我们C (a, b)无法推断。

我无法完全理解这里发生了什么，但看起来量化约束不能很好地与类型族混合。

看起来上述类型的家庭被视为

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

在这种情况下，我不明白出了什么问题。由于Cnow 不引用单个类型类，因此不可能forall a b . (C a , C b) => C (a, b)通过（例如）传递指向特定实例的指针来实现量化约束，因为C在开放世界中，这三个约束可以是任何东西。

我仍然不明白为什么type family C :: * -> Constraint以同样的方式处理。

也许 GHC 应该以这种方式拒绝涉及类型族的量化约束... -> Constraint？我不确定。

于 2020-06-21T07:45:37.773 回答
1

我认为您已经将代码推到了 GHC 类型系统的边缘。Cs您可以通过编写以下内容来修复类型错误：

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

但是你遇到了“GHC 还不支持命令式多态性”。在 GHC 根据issue 14860添加对类族的支持之前，您可能对这种方法不走运。

但是，您确实询问了替代方法。制作Sendable t a多参数类型类不是完成基本相同的事情吗？

当然，以下类型检查：

{-# 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)
于 2020-06-21T19:44:37.917 回答