I'm working with Dominic Orchard's type-level-sets library, which follows his paper pretty closely.
I'm building a DSL for expressing communication between parties during a synchronous concurrent program. One thing I'm going to need is the ability to express "sub-programs" involving sub-sets of the original community; this will be used in conjunction with fromUniversal.
Here's a parred down version of my code:
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
Within _clique, there are contexts providing Subset recipients clq and Subset csl parties; I need GHC to somehow understand that this implies Subset recipients parties. But there's no such instance available.
How can I represent the transitivity of "subset" for the purposes of type-level sets?
Here's the error message:
~/.../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
| ^^^^^^^^^
I tried simply adding
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...
CodePudding user response：
So far the best solution I've been able to come up with is Ghosts of Departed Proofs, which I can use to move the logic of subsets out of the type-system. It's a bit clunky, and I'm not at all sure I'm using it correctly.
Subset.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
In this version unionOfSubsets isn't being used; in practice it would be nice to have real/better proofs for this and other similar properties.
Lib.hs
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
CodePudding user response：
GHC Haskell only really supports transitivity for two types of constraints:
(Nominal) equality constraints
(a ~ b, b ~ c) => a ~ cRepresentational equality constraints
(Coercible a b, Coercible b c) => Coercible a c
These rules are (very carefully) baked into the constraint solving process for the entirely magical ~ and Coercible constraints; there is no other transitivity in the constraint language. The basic problem is that if you have a class
class C a b
and you write
instance (C a b, C b c) => C a c
then b is ambiguous. When GHC is trying to solve C a c, it has no idea what b you want. There is not, at present, any way for the user to indicate which b to use where the constraint is demanded, so the instance really can't be used.
The Subset type in Data.Type.Set does not look like an equality or Coercible constraint, so you just can't do it.
Are there other ways to express the idea of a list being a subset of another list that GHC can recognize as transitive? I'm not sure. Suppose we had something like
class Subset' a b
transitive :: (Subset' a b, Subset' b c) => SomeProof a b -> SomeProof b c -> Dict (Subset' a c)
I would be surprised if it were possible to define transitive without using its proof arguments. Furthermore, actually using such a Subset' would likely be difficult, or even impossible.
Subset' constraints are likely to look vaguely like one of the following:
type Subset' a b = Union a b ~ Nub (Sort b)
type Subset' a b = Intersection a b ~ Nub (Sort a)
where you may or may not be able to use the provided definitions of Union, Sort, and Nub, and you'd have to come up with your own Intersection. I have no doubt whatsoever that any such project will be complicated. You'll have to use the structure of the evidence you're given to construct the necessary equality. And then after all that ... where have you really gotten? This looks like a dead end.