À mon avis, la valeur de conteneurs (comme dans le conteneur de la théorie) est leur homogénéité. Que l'uniformité donne des possibilités considérables d'utilisation contenant des représentations que la base de spécifications exécutables, et peut-être même assisté par ordinateur programme de dérivation.
Conteneurs: un outil théorique, pas un bon moment de l'exécution de la représentation des données stratégie
Je ne recommande fixpoints de (normalisée) des conteneurs à un but d'intérêt général de façon à mettre en œuvre des structures de données récursives. C'est, il est utile de savoir qu'un foncteur a (jusqu'à iso) une présentation sous la forme d'un conteneur, car il indique que le conteneur générique fonctionnalité (qui est facilement mis en œuvre, une fois pour toutes, grâce à l'uniformité) peut être instancié à votre foncteur, et ce comportement vous devriez vous attendre. Mais cela ne veut pas dire qu'un conteneur de mise en œuvre sera efficace dans une manière pratique. En effet, je préfère généralement de premier ordre encodages (tags et les tuples, plutôt que des fonctions) de premier ordre des données.
Pour fixer la terminologie, nous disons que le type Cont de conteneurs (sur Set, mais d'autres catégories sont disponibles) est donnée par un constructeur <| d'emballage de deux champs, de formes et de positions
S : Set
P : S -> Set
(C'est la même signature de données qui est utilisée pour déterminer un Sigma type ou d'un type de Pi, ou un W type, mais cela ne signifie pas que les conteneurs sont les mêmes que pour l'une de ces choses, ou que ces choses sont les mêmes que les uns les autres.)
L'interprétation d'une telle chose comme un foncteur est donnée par
[_]C : Cont -> Set -> Set
[ S <| P ]C X = Sg S \ s -> P s -> X -- I'd prefer (s : S) * (P s -> X)
mapC : (C : Cont){X Y : Set} -> (X -> Y) -> [ C ]C X -> [ C ]C Y
mapC (S <| P) f (s , k) = (s , f o k) -- o is composition
Et nous sommes déjà à gagner. C'est map mis en œuvre une fois pour toutes. De plus, le foncteur lois tenir par le calcul seul. Il n'est pas nécessaire pour la récursivité sur la structure des types de construction de l'opération, ou pour prouver que les lois.
Les Descriptions sont dénormalisée conteneurs
Personne n'est d'essayer de prétendre que, du point de vue opérationnel, Nat <| Fin donne une efficace mise en œuvre de la liste, c'est qu'en faisant cette identification nous apprendre quelque chose d'utile sur la structure de listes.
Permettez-moi de dire quelque chose à propos de descriptions. Pour le bénéfice des lecteurs paresseux, permettez-moi de les reconstruire.
data Desc : Set1 where
var : Desc
sg pi : (A : Set)(D : A -> Desc) -> Desc
one : Desc -- could be Pi with A = Zero
_*_ : Desc -> Desc -> Desc -- could be Pi with A = Bool
con : Set -> Desc -- constant descriptions as singleton tuples
con A = sg A \ _ -> one
_+_ : Desc -> Desc -> Desc -- disjoint sums by pairing with a tag
S + T = sg Two \ { true -> S ; false -> T }
Les valeurs en Desc de décrire les foncteurs dont fixpoints donner les types de données. Qui foncteurs décrivent-elles?
[_]D : Desc -> Set -> Set
[ var ]D X = X
[ sg A D ]D X = Sg A \ a -> [ D a ]D X
[ pi A D ]D X = (a : A) -> [ D a ]D X
[ one ]D X = One
[ D * D' ]D X = Sg ([ D ]D X) \ _ -> [ D' ]D X
mapD : (D : Desc){X Y : Set} -> (X -> Y) -> [ D ]D X -> [ D ]D Y
mapD var f x = f x
mapD (sg A D) f (a , d) = (a , mapD (D a) f d)
mapD (pi A D) f g = \ a -> mapD (D a) f (g a)
mapD one f <> = <>
mapD (D * D') f (d , d') = (mapD D f d , mapD D' f d')
Il est inévitable d'avoir à travailler par récurrence plus de descriptions, de sorte qu'il est plus difficile de travailler. Le foncteur de lois, trop, ne sont pas gratuits. Nous obtenons une meilleure représentation des données, sur le plan opérationnel, parce que nous n'avons pas besoin de recourir à fonctionnels codages lorsque le béton tuples fera. Mais nous devons travailler plus fort pour écrire des programmes.
Notez que chaque récipient a une description:
sg S \ s -> pi (P s) \ _ -> var
Mais il est également vrai que chaque description a une présentation comme une isomorphe conteneur.
ShD : Desc -> Set
ShD D = [ D ]D One
PosD : (D : Desc) -> ShD D -> Set
PosD var <> = One
PosD (sg A D) (a , d) = PosD (D a) d
PosD (pi A D) f = Sg A \ a -> PosD (D a) (f a)
PosD one <> = Zero
PosD (D * D') (d , d') = PosD D d + PosD D' d'
ContD : Desc -> Cont
ContD D = ShD D <| PosD D
C'est-à-dire, les conteneurs sont une forme normale pour les descriptions. C'est un exercice pour montrer qu' [ D ]D X est naturellement isomorphe a' [ ContD D ]C X. Qui rend la vie plus facile, parce que dire que faire pour les descriptions, il suffit, en principe, de dire ce qu'il faut faire pour leurs formes normales, les conteneurs. Le ci-dessus mapD opération pourrait, en principe, être obtenue par fusion de la isomorphisms à la définition uniforme de l' mapC.
Différentiel de structure: les conteneurs montrer le chemin
De même, si nous avons une notion de l'égalité, on peut dire ce qu'est un trou de contextes pour les conteneurs de manière uniforme
_-[_] : (X : Set) -> X -> Set
X -[ x ] = Sg X \ x' -> (x == x') -> Zero
dC : Cont -> Cont
dC (S <| P) = (Sg S P) <| (\ { (s , p) -> P s -[ p ] })
C'est le cas, la forme d'un trou de contexte dans un conteneur est la paire de la forme du contenant d'origine et de la position du trou; les positions sont des positions d'origine en dehors de celui du trou. C'est la preuve pertinents version de "multiplier par l'indice, décrémenter l'index" lors de la différenciation de puissance de la série.
Ce traitement uniforme nous donne la spécification à partir de laquelle on peut tirer des siècles de l'ancien programme pour calculer la dérivée d'un polynôme.
dD : Desc -> Desc
dD var = one
dD (sg A D) = sg A \ a -> dD (D a)
dD (pi A D) = sg A \ a -> (pi (A -[ a ]) \ { (a' , _) -> D a' }) * dD (D a)
dD one = con Zero
dD (D * D') = (dD D * D') + (D * dD D')
Comment puis-je vérifier que mon dérivés de l'opérateur pour les descriptions sont correctes? Par le contrôle contre la dérivée de conteneurs!
Ne tombez pas dans le piège de penser que juste parce que une présentation d'une idée n'est pas utile sur le plan opérationnel qu'il ne peut pas être conceptuellement utile.
Sur la Libéralisation des monades
Une dernière chose. L' Freer astuce montants de réorganiser l'arbitraire d'un foncteur d'une manière particulière (commutation à Haskell)
data Obfuncscate f x where
(:<) :: forall p. f p -> (p -> x) -> Obfuncscate f x
mais ce n'est pas une alternative à conteneurs. C'est une légère nourrissage d'un conteneur de présentation. Si nous avions une forte existentiels et des types dépendants, on pourrait écrire
data Obfuncscate f x where
(:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x
de sorte qu' (exists p. f p) représente des formes (où vous pouvez choisir votre représentation de positions, puis les marque place avec sa position), et fst choisit les existentielle témoin d'une forme (la position de la représentation que vous avez choisi). Il a le mérite d'être bien évidemment strictement positif exactement parce que c'est une boite de présentation.
En Haskell, bien sûr, vous avez à curry les existentielle, qui, heureusement, laisse une dépendance seulement sur le type de projection. C'est la faiblesse de l'existentiel qui justifie l'équivalence des Obfuncscate f et f. Si vous essayez cette astuce dans un type dépendant de la théorie avec de fortes existentiels, l'encodage perd son caractère unique parce que vous pouvez le projet et de distinguer les différents choix de représentation pour les postes. C'est, je peut représenter Just 3 par
Just () :< const 3
ou par
Just True :< \ b -> if b then 3 else 5
et dans Coq, disons, ceux-ci sont sensiblement distinctes.
Défi: caractérisation des fonctions polymorphes
Chaque fonction polymorphe entre les types de conteneurs est donné d'une manière particulière. Il n'y a que l'uniformité de travail afin de clarifier notre compréhension de nouveau.
Si vous avez quelques
f : {X : Set} -> [ S <| T ]C X -> [ S' <| T' ]C X
il est (extensionally) données par les données suivantes, qui ne font aucune mention d'éléments que ce soit:
toS : S -> S'
fromP : (s : S) -> P' (toS s) -> P s
f (s , k) = (toS s , k o fromP s)
C'est la seule manière de définir une fonction polymorphe entre les conteneurs est-à-dire comment traduire entrée formes de sortie de formes, puis dire comment remplir les positions de sortie à partir des positions d'entrée.
Pour votre préférée à la représentation de foncteurs strictement positif, donner un de même serré la caractérisation des fonctions polymorphes, ce qui élimine l'abstraction sur le type de l'élément. (Pour les descriptions, je voudrais utiliser exactement leur reducability à conteneurs.)
Défi: la capture "transposabilité"
Étant donné deux foncteurs, f et g, il est facile de dire ce que leur composition f o g est: (f o g) x encapsule les choses en f (g x), nous donnant "f-structures d' g-structures". Mais pouvez-vous facilement imposer la condition supplémentaire que l'ensemble de l' g des structures stockées dans l' f de la structure ont la même forme?
Disons qu' f >< g des captures de la transposables fragment d' f o g, où tous les g des formes sont les mêmes, de sorte qu'on peut tout aussi bien tourner la chose dans un g-structure de l' f-structures. E. g., alors qu' [] o [] donne lambeaux de listes de listes, [] >< [] donne rectangulaire de matrices, [] >< Maybe propose des listes qui sont soit toutes Nothing ou tous Just.
Donnez >< pour votre préférée à la représentation de foncteurs strictement positif. Pour les conteneurs, c'est facile.
(S <| P) >< (S' <| P') = (S * S') <| \ { (s , s') -> P s * P' s' }
Conclusion
Les conteneurs, en leur normalisé Sigma-puis-Pi formulaire ne sont pas destinés à être une machine efficace de représentation de données. Mais la connaissance qu'un foncteur, mis en œuvre, cependant, a une présentation sous la forme d'un conteneur, nous aide à comprendre sa structure et lui donner l'équipement utile. De nombreuses constructions peuvent être donnés de façon abstraite pour les conteneurs, une fois pour toutes, quand elles doivent être données au cas par cas pour d'autres présentations. Donc, oui, c'est une bonne idée d'en apprendre sur les conteneurs, si ce n'est à saisir les raisons de la plus de des constructions spécifiques vous réellement mettre en œuvre.
