該賞金過期2天。這個問題的答案有資格獲得 50聲望獎勵。 ShapeOfMatter想引起更多人對這個問題的關注：
據我所知，這個問題的關鍵是如何class在 Haskell 中進行傳遞。這顯然很有用，目前尚不清楚是否可能。
我正在使用 Dominic Orchard 的型別級別集庫，它非常接近他的論文。
我正在構建一個 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
I've been proceeding with the project using the below solution; it's distinctly mediocre. Specifically, there are a lot of properties besides just transitivity that would be nice to have, like two sets are both subsets of a third set, then their union is a also a subset of the third set. Getting properties like that "for free" may be too much to ask of Haskell's type system...
uj5u.com熱心網友回復：
到目前為止，我能想出的最佳解決方案是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
uj5u.com熱心網友回復：
GHC Haskell 只真正支持兩種型別的約束的傳遞性：
（名義）等式約束
(a ~ b, b ~ c) => a ~ c表征等式約束
(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不使用其證明引數的情況下進行定義，我會感到驚訝。此外，實際使用這種Subset'方法可能很困難，甚至不可能。
Subset' 約束可能看起來像以下之一：
type Subset' a b = Union a b ~ Nub (Sort b)
type Subset' a b = Intersection a b ~ Nub (Sort a)
在這里你可能會或可能無法使用所提供的定義Union，Sort以及Nub，你就得拿出你自己的Intersection。我毫不懷疑任何這樣的專案都會很復雜。您必須使用所提供的證據結構來構建必要的相等性。然后畢竟......你真正得到了什么？這看起來像是一個死胡同。
轉載請註明出處，本文鏈接：https://www.uj5u.com/yidong/355874.html
標籤：haskell type-level-computation higher-kinded-types type-kinds undecidable-instan
下一篇：使用鏡頭映射記錄的兩個欄位