Avertissement: Un grand nombre de ce qui ne fonctionne pas vraiment tout à fait raison lorsque vous ⊥, donc je vais flagrante ne pas tenir compte que, par souci de simplicité.
Quelques points de départ:
À noter que "l'union" n'est probablement pas le meilleur terme pour A+B ici--c'est précisément un disjoints de l'union de deux types, parce que les deux côtés sont distingués, même si leurs types sont les mêmes. Pour ce que ça vaut, le terme le plus commun est tout simplement "le type de somme".
Singleton types sont, en effet, tous les types d'unités. Ils se comportent à l'identique sous des manipulations algébriques et, plus important encore, la quantité d'information présente est encore préservée.
Vous voulez probablement un zéro type. Il n'y a pas un standard, mais le nom le plus courant est - Void. Il n'existe pas de valeurs dont le type est égal à zéro, tout comme il est une valeur dont le type est une.
Il reste encore une opération d'envergure qui manque ici, mais je vais y revenir dans un instant.
Comme vous l'avez probablement remarqué, Haskell a tendance à emprunter des concepts à partir de la Catégorie de la Théorie, et de tout ce qui précède a une manière très simple de l'interprétation en tant que telle:
Compte tenu des objets A et B dans Hask, leur produit A×B est l'unique (à isomorphisme) de type qui permet à deux projections fst : A×B → A et snd : A×B → B, où compte tenu de tout type C et les fonctions f : C → A, g : C → B, vous pouvez définir le couplage f &&& g : C → A×B tels que fst ∘ f &&& g) = f et de même pour g. Parametricity garantit les propriétés universelles automatiquement et mon moins que subtile choix de noms à vous donner l'idée. L' (&&&) opérateur est défini en Control.Arrow, par la manière.
Le double de ce qui précède est la coproduct A+B avec des injections inl : A → A+B et inr : B → A+B, où compte tenu de tout type C et les fonctions f : A → C, g : B → C, vous pouvez définir la copairing f ||| g : A+B → C telle que l'évidence des équivalences maintenez-la enfoncée. Encore une fois, parametricity garantit la plupart des parties difficiles automatiquement. Dans ce cas, la norme, les injections sont tout simplement Left et Right et le copairing est la fonction either.
La plupart des propriétés du produit et la somme types peuvent être dérivées à partir de ci-dessus. Notez que tout singleton est un terminal de Hask et tout type vide est un objet initial.
De retour à ladite manquant de l'opération, dans un cartésienne fermée catégorie que vous avez exponentielle des objets qui correspondent aux flèches de la catégorie. Nos flèches sont des fonctions, nos objets sont des types avec l'aimable *, et le type A -> B se comporte en effet comme BUn dans le contexte de la manipulation algébrique de types. Si ce n'est pas évident pourquoi cela devrait tenir, tenir compte du type Bool -> A. Avec seulement deux entrées, une fonction de ce type est isomorphe a ' deux valeurs de type A, c'est à dire (A, A). Pour Maybe Bool -> A nous avons trois entrées possibles, et ainsi de suite. Aussi, d'observer que, si nous reformuler la copairing définition ci-dessus pour utiliser la notation algébrique, on obtient l'identité de CA × CB = CA+B.
Comme pour pourquoi tout cela fait sens et, en particulier, pourquoi votre utilisation de la puissance d'extension de la série est justifiée: à noter qu'une grande partie de la ci-dessus se réfère à la "habitants" d'un type (c'est à dire, les valeurs distinctes du type) afin de démontrer le comportement algébrique. Pour faire de ce point de vue explicite:
Le type de produit (A, B) représente une valeur chacun de A et B, prises indépendamment. Ainsi, pour toute valeur fixe a :: A, il est une valeur de type (A, B) pour chaque habitant de B. C'est bien sûr le produit cartésien, et le nombre d'habitants du type de produit est le produit du nombre d'habitants de ces facteurs.
Le type de somme Either A B représente une valeur de A ou B, la droite et la gauche branches distingués. Comme mentionné plus tôt, c'est une union disjointe, et le nombre d'habitants de la somme est la somme du nombre d'habitants de la additionnées.
L'exponentielle de type B -> A représente une cartographie à partir des valeurs de type B pour les valeurs de type A. Pour toute fixe argument b :: B, toute valeur de A peut être assignée; une valeur de type B -> A choisit une telle cartographie pour chaque entrée, ce qui est équivalent à un produit de plusieurs copies de A comme B a habitants, d'où l'élévation à la puissance.
Alors que c'est tentant à première pour traiter les types de jeux, qui ne fonctionne pas très bien dans ce contexte, que nous avons disjoints de l'union plutôt que la norme de l'union des ensembles, il n'est pas évident interprétation de l'intersection ou de nombreuses autres opérations, et nous n'avons généralement pas de soins sur l'appartenance (en laissant que le type checker).
D'autre part, la construction ci-dessus passent beaucoup de temps à parler de comptage des habitants, et d'énumérer les valeurs possibles d'un type est un concept utile ici. Que rapidement nous conduit à la combinatoire énumérative, et si vous consultez liés article de Wikipédia, vous trouverez que l'une des premières choses qu'il n'est de définir des "paires" et "syndicats" exactement dans le même sens comme produit et somme types par voie de génération de fonctions, puis fait de même pour les "séquences" qui sont identiques à Haskell listes en utilisant exactement la même technique que vous avez fait.
Edit: Oh, et voici un petit bonus que je pense que démontre le point frappante. Vous avez mentionné dans un commentaire que pour un arbre de type T = 1 + T^2 vous pouvez dériver de l'identité T^6 = 1, ce qui est manifestement erroné. Toutefois, T^7 = T ne détiennent, et une bijection entre les arbres et les sept-n-uplets de l'arbre peut être construit directement, cf. Andreas Blass "Sept Arbres en Une seule".
Edit×2: Sur le sujet de la "dérivé d'un type de construction mentionné dans d'autres réponses, vous pouvez également profiter de ce document à partir du même auteur , qui s'appuie sur l'idée plus loin, y compris les notions de division et d'autres intéressantes, que sais-je encore.
