2

我正在使用 Dominic Orchard 的type-level-sets库，该库非常接近他的论文。

我正在构建一个 DSL，用于在同步并发程序期间表达各方之间的通信。我需要的一件事是能够表达涉及原始社区子集的“子程序”；这将与fromUniversal.

这是我的代码的简化版本：

module Lib () where

import Data.Type.Nat (Nat)
import Data.Type.Set (IsSet, Subset)
import Polysemy (Sem, makeSem, reinterpret)

data Located (parties :: [Nat]) v = Located v

data Com (parties :: [Nat]) m a where
  SendInt :: forall recipients senders parties m.
             (Subset recipients parties,
              Subset senders parties) =>
             Located senders Int -> Com parties m (Located recipients Int)
  FromUniversal :: forall parties m a.
               Located parties a -> Com parties m a

-- Polysemy uses template haskell:
makeSem ''Com
--sendInt :: Member...=> (Located senders Int) -> Sem r (Located recipients Int)
--fromUniversal :: Member (Com parties) r => (Located parties a) -> Sem r a
--We can manually write them out instead of using makeSem;
--that helps make Located's type argument explicit.

-- Lift a program in a small community (clique) into a larger community's monad. 
runClique :: forall parties clq s r a.
          (IsSet parties,
           IsSet clq,
           Subset clq parties) =>
          Sem (Com clq ': r) a -> Sem (Com parties ': r) (Located clq a)
runClique program = do
    a <- (reinterpret _clique) program
    return (Located a)
  where _clique :: forall rInitial x.
                   Com clq (Sem rInitial) x -> Sem (Com parties ': r) x
        _clique (SendInt l) = sendInt l

在_clique中，有提供Subset recipients clq和的上下文Subset csl parties；我需要 GHC 以某种方式理解这意味着Subset recipients parties. 但是没有这样的实例可用。

为了类型级别集的目的，我如何表示“子集”的传递性？

这是错误消息：

~/.../src/Lib.hs:35:31: error:
    • Could not deduce (Subset recipients parties)
        arising from a use of ‘sendInt’
      from the context: (IsSet parties, IsSet clq, Subset clq parties)
        bound by the type signature for:
                   runClique :: forall k (parties :: [Nat]) (clq :: [Nat]) (s :: k)
                                       (r :: [(* -> *) -> * -> *]) a.
                                (IsSet parties, IsSet clq, Subset clq parties) =>
                                Sem (Com clq : r) a -> Sem (Com parties : r) (Located clq a)
        at src/Lib.hs:(25,1)-(29,72)
      or from: (x ~ Located recipients Int, Subset recipients clq,
                Subset senders clq)
        bound by a pattern with constructor:
                   SendInt :: forall k (recipients :: [Nat]) (senders :: [Nat])
                                     (parties :: [Nat]) (m :: k).
                              (Subset recipients parties, Subset senders parties) =>
                              Located senders Int -> Com parties m (Located recipients Int),
                 in an equation for ‘_clique’
        at src/Lib.hs:35:18-26
    • In the expression: sendInt l
      In an equation for ‘_clique’: _clique (SendInt l) = sendInt l
      In an equation for ‘runClique’:
          runClique program
            = do a <- (reinterpret _clique) program
                 return (Located a)
            where
                _clique ::
                  forall rInitial x.
                  Com clq (Sem rInitial) x -> Sem (Com parties : r) x
                _clique (SendInt l) = sendInt l
   |
35 |         _clique (SendInt l) = sendInt l
   |                               ^^^^^^^^^

我试着简单地添加

instance {-# OVERLAPS #-} (Subset s t, Subset t v) => Subset s v where
  subset xs = subset (subset xs :: Set t)

to Lib.hs (apparently Subset isn't closed-world; I think); this gives a variety of different error messages depending what compiler options I use, or if I swap out OVERLAPS for INCOHERENT. The jist of it seems to be that GHC can't pick an instance to use, even if I promise it'll be ok.

I tried making the recipient type explicit in _clique (so I can just add the needed Subset recipients parties to the context), but it seems like no matter what I do reinterpret always introduces/requires a "fresh" x and/or recipients; I haven't found a way of providing the context for the type-variable that's actually used.

It seems unlikely that this is impossible, but I've been stuck on it for a day and I'm out of my depth.

Edit

我一直在使用以下解决方案进行该项目；这显然是平庸的。具体来说，除了传递性之外，还有很多属性很好，比如两个集合都是第三个集合的子集，那么它们的并集也是第三个集合的子集。对于 Haskell 的类型系统来说，“免费”获得这样的属性可能太过分了……

4

2 回答 2

1

GHC Haskell 仅真正支持两种类型的约束的传递性：

  1. （名义）等式约束

    (a ~ b, b ~ c) => a ~ c

  2. 表示等式约束

    (Coercible a b, Coercible b c) => Coercible a c

这些规则（非常小心地）被纳入完全神奇~和Coercible约束的约束求解过程中；约束语言中没有其他传递性。基本问题是，如果你有一堂课

class C a b

你写

instance (C a b, C b c) => C a c

然后b是模棱两可的。当 GHC 试图解决C a c时，它不知道你 b想要什么。目前，用户没有任何方法可以指示b在需要约束的地方使用哪个，因此该实例确实无法使用。

输入的Subset类型Data.Type.Set看起来不像相等或Coercible约束，所以你不能这样做。

是否有其他方法可以表达列表是 GHC可以识别为传递的另一个列表的子集的想法？我不确定。假设我们有类似的东西

class Subset' a b
transitive :: (Subset' a b, Subset' b c) => SomeProof a b -> SomeProof b c -> Dict (Subset' a c)

transitive如果可以在不使用其证明论据的情况下进行定义，我会感到惊讶。此外，实际使用这样的 aSubset'可能会很困难，甚至是不可能的。

Subset'约束可能看起来像以下之一：

type Subset' a b = Union a b ~ Nub (Sort b)
type Subset' a b = Intersection a b ~ Nub (Sort a)

您可能会或可能无法使用提供的 , 和 的定义，Union并且您必须想出自己的. 我毫不怀疑任何这样的项目都会很复杂。您必须使用所提供证据的结构来构建必要的平等。然后毕竟......你真的到哪里去了？这看起来像一个死胡同。SortNubIntersection

于 2021-11-10T23:56:29.847 回答
0

到目前为止，我能想到的最好的解决方案是Ghosts of Departed Proofs，我可以用它来将子集的逻辑移出类型系统。它有点笨拙，我完全不确定我是否正确使用它。

子集.hs

module Subset (
  immediateSubset,
  Subset,
  SubsetProof,
  transitiveSubset,
  unionOfSubsets
) where

import Data.Type.Set (Subset, Union)
import Logic.Classes (Transitive, transitive)
import Logic.Proof (axiom, Proof, sorry)

data Subset' s t where {}
instance Transitive Subset' where {}
type SubsetProof s t = Proof (Subset' s t)

immediateSubset :: (Subset s t) =>
                   SubsetProof s t
immediateSubset = axiom
transitiveSubset :: forall k (s :: [k]) (t :: [k]) (v :: [k]).
                    SubsetProof s t -> SubsetProof t v -> SubsetProof s v
transitiveSubset = transitive
unionOfSubsets :: forall k (s1 :: [k]) (s2 :: [k]) (t :: [k]).
                  SubsetProof s1 t -> SubsetProof s2 t -> SubsetProof (Union s1 s2) t
unionOfSubsets s1t s2t = sorry

在这个版本unionOfSubsets中没有被使用；在实践中，为这个和其他类似属性提供真实/更好的证明会很好。

库文件

module Lib {-()-} where

import Data.Type.Nat (Nat)
import Data.Type.Set (IsSet)
import Polysemy (Sem, makeSem, reinterpret)

import Subset (immediateSubset, Subset, SubsetProof, transitiveSubset)


data Located (parties :: [Nat]) v = Located v

data Com (parties :: [Nat]) m a where
  SendInt :: forall recipients senders parties m.
             SubsetProof recipients parties 
             -> SubsetProof senders parties
             -> Located senders Int
             -> Com parties m (Located recipients Int)
  FromUniversal :: forall parties m a.
                   Located parties a -> Com parties m a

-- Polysemy uses template haskell:
makeSem ''Com
--sendInt :: Member (Com parties) r => (Located senders Int) -> Sem r (Located recipients Int)
--fromUniversal :: Member (Com parties) r => (Located parties a) -> Sem r a
--we can manually write out the functions instead of useing makeSem;
--that might help make Located's type artument explicit, but I don't think it matters here.

-- "lift" a program in a small community (clique) into a larger community's monad. 
runClique :: forall parties clq r a.
          (IsSet parties,
           IsSet clq,
           Subset clq parties) =>
          Sem (Com clq ': r) a
          -> Sem (Com parties ': r) (Located clq a)
runClique = (Located <$>) . (reinterpret _clique)
  where cp = immediateSubset :: SubsetProof clq parties
        _clique :: forall rInitial x.
                   Com clq (Sem rInitial) x -> Sem (Com parties ': r) x
        _clique (SendInt rc sc x) = sendInt (transitiveSubset rc cp) (transitiveSubset sc cp) x
        _clique (FromUniversal (Located v)) = return v
于 2021-11-08T14:10:12.920 回答