Classe transitive "Subset" pour les ensembles de niveaux de type

Question

Je travaille avec Dominic Orchard. ensembles de niveaux de type qui suit son article de très près.

Je suis en train de construire un DSL pour exprimer la communication entre les parties au cours d'un programme concurrent synchrone. Une chose dont j'aurai besoin est la capacité d'exprimer des "sous-programmes" impliquant des sous-ensembles de la communauté originale ; ceci sera utilisé en conjonction avec fromUniversal .

Voici une version allégée de mon 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

En _clique il existe des contextes fournissant Subset recipients clq y Subset csl parties J'ai besoin que GHC comprenne d'une manière ou d'une autre que ceci implique Subset recipients parties . Mais il n'y a pas de telle instance disponible.

Comment puis-je représenter la transitivité de "subset" pour les besoins des ensembles de niveau type ?

Voici le message d'erreur :

~/.../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
   |                               ^^^^^^^^^

J'ai essayé d'ajouter simplement

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

à Lib.hs (apparemment Subset n'est pas un monde fermé ; je pensez à ) ; cela donne une variété de messages d'erreur différents selon les options du compilateur que j'utilise, ou si j'échange l'option OVERLAPS para INCOHERENT . L'essentiel semble être que GHC ne peut pas choisir une instance à utiliser, même si je promets qu'elle sera correcte.

J'ai essayé de faire le recipient type explicite dans _clique (afin que je puisse simplement ajouter les Subset recipients parties au contexte), mais il semble que peu importe ce que je fais reinterpret introduit/exige toujours une "nouvelle" x et/ou recipients Je n'ai pas trouvé de moyen de fournir le contexte pour la variable de type qui est réellement utilisée.

Il semble peu probable que cela soit impossible, mais je suis bloqué sur ce sujet depuis une journée et je suis dépassé par les événements.

Answer 1

GHC Haskell ne supporte réellement la transitivité que pour deux types de contraintes :

1. Contraintes d'égalité (nominales)

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

2. Contraintes d'égalité représentationnelle

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

Ces règles sont (très soigneusement) incorporées dans le processus de résolution des contraintes pour le système entièrement magique. ~ y Coercible Il n'y a pas d'autre transitivité dans le langage des contraintes. Le problème fondamental est que si vous avez une classe

class C a b

et vous écrivez

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

puis b est ambiguë. Lorsque GHC essaie de résoudre C a c il n'en a aucune idée. ce que b que vous voulez. Pour l'instant, il n'y a aucun moyen pour l'utilisateur d'indiquer quelle b à utiliser là où la contrainte est demandée, donc l'instance ne peut vraiment pas être utilisée.

En Subset le type en Data.Type.Set ne ressemble pas à une égalité ou Coercible contrainte, donc vous ne pouvez pas le faire.

Existe-t-il d'autres façons d'exprimer l'idée qu'une liste est un sous-ensemble d'une autre liste que GHC. puede reconnaître comme transitif ? Je ne suis pas sûr. Supposons que nous ayons quelque chose comme

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

Je serais surpris s'il était possible de définir transitive sans utiliser ses arguments de preuve. De plus, en réalité en utilisant un tel Subset' serait probablement difficile, voire impossible.

Subset' Les contraintes sont susceptibles de ressembler vaguement à l'un des éléments suivants :

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

où vous pourrez ou non utiliser les définitions fournies pour les termes suivants Union , Sort y Nub et tu devras trouver ta propre façon de faire. Intersection . Je n'ai aucun doute sur le fait qu'un tel projet sera compliqué. Vous devrez utiliser la structure des preuves qui vous sont données pour construire l'égalité nécessaire. Et puis, après tout cela... où en êtes-vous vraiment arrivés ? Cela ressemble à une impasse.

Answer 2

Jusqu'à présent, la meilleure solution que j'ai trouvée est la suivante Les fantômes des épreuves disparues que je peux utiliser pour déplacer la logique des sous-ensembles hors du système de types. C'est un peu lourd, et je ne suis pas du tout sûr de l'utiliser correctement.

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

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