Abuser de l'algèbre des types de données algébriques - pourquoi cela fonctionne-t-il?

L'expression «algébrique» pour les types de données algébriques semble très suggestive pour une personne ayant une formation en mathématiques. Permettez-moi d'essayer d'expliquer ce que je veux dire.

Après avoir défini les types de base

• Produit •
• syndicat +
• Singleton X
• Unité 1

et en utilisant le raccourci X²pour X•Xet 2Xpour X+Xet cetera, nous pouvons ensuite définir des expressions algébriques pour par exemple les listes liées

data List a = Nil | Cons a (List a) ↔ L = 1 + X • L

et arbres binaires:

data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²

Maintenant, mon premier instinct en tant que mathématicien est de devenir fou avec ces expressions et d'essayer de résoudre pour Let T. Je pourrais le faire par substitution répétée, mais il semble beaucoup plus facile d'abuser horriblement de la notation et de prétendre que je peux la réorganiser à volonté. Par exemple, pour une liste chaînée:

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

où j'ai utilisé l'expansion de la série de puissance d' 1 / (1 - X)une manière totalement injustifiée pour dériver un résultat intéressant, à savoir qu'un Ltype est soit Nil, soit il contient 1 élément, ou il contient 2 éléments, ou 3, etc.

Cela devient plus intéressant si nous le faisons pour les arbres binaires:

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - √(1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X⁴ + ...

encore une fois, en utilisant l'extension de la série de puissance (fait avec Wolfram Alpha ). Cela exprime le fait non évident (pour moi) qu'il n'y a qu'un seul arbre binaire avec 1 élément, 2 arbres binaires avec deux éléments (le deuxième élément peut être à gauche ou à droite), 5 arbres binaires avec trois éléments, etc. .

Donc ma question est - qu'est-ce que je fais ici? Ces opérations semblent injustifiées (quelle est exactement la racine carrée d'un type de données algébrique de toute façon?) Mais elles conduisent à des résultats sensibles. le quotient de deux types de données algébriques a-t-il un sens en informatique, ou s'agit-il simplement d'une supercherie notationnelle?

Et, peut-être plus intéressant encore, est-il possible d'étendre ces idées? Existe-t-il une théorie de l'algèbre des types qui autorise, par exemple, des fonctions arbitraires sur les types, ou les types nécessitent-ils une représentation en série de puissance? Si vous pouvez définir une classe de fonctions, alors la composition des fonctions at-elle un sens?

Clause de non-responsabilité: Une grande partie de cela ne fonctionne pas vraiment bien lorsque vous tenez compte de ⊥, donc je vais ignorer cela de manière flagrante pour des raisons de simplicité.

Quelques premiers points:

• Notez que "union" n'est probablement pas le meilleur terme pour A + B ici - c'est spécifiquement une union disjointe des 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 courant est simplement "type de somme".

• Les types singleton sont, en fait, tous les types d'unités. Ils se comportent de manière identique sous des manipulations algébriques et, plus important encore, la quantité d'informations présentes est toujours préservée.

• Vous voulez probablement aussi un type zéro. Haskell fournit cela comme Void. Il n'y a pas de valeurs dont le type est zéro, tout comme il y a une valeur dont le type est un.

Il manque encore une opération majeure ici, mais j'y reviendrai dans un instant.

Comme vous l'avez probablement remarqué, Haskell a tendance à emprunter des concepts à la théorie des catégories, et tout ce qui précède a une interprétation très simple en tant que telle:

• Étant donné les objets A et B dans Hask , leur produit A × B est le type unique (jusqu'à l'isomorphisme) qui permet deux projections fst : A × B → A et snd : A × B → B, où étant donné tout type C et fonctions f : C → A, g : C → B vous pouvez définir l'appariement f &&& g : C → A × B tel que fst ∘ (f &&& g) = f et de même pour g . La paramétricité garantit automatiquement les propriétés universelles et mon choix de noms moins que subtil devrait vous donner l'idée. L' (&&&)opérateur est défini dans Control.Arrow, soit dit en passant.

• Le dual de ce qui précède est le coproduit A + B avec des injections inl : A → A + B et inr : B → A + B, où étant donné tout type C et fonctions f : A → C, g : B → C, vous pouvez définir le copairing f ||| g : A + B → C tels que les équivalences évidentes se vérifient. Encore une fois, la paramétrie garantit automatiquement la plupart des pièces délicates. Dans ce cas, les injections standard sont simples Leftet Rightet le copairing est la fonction either.

De nombreuses propriétés des types de produits et de sommes peuvent être dérivées de ce qui précède. Notez que tout type singleton est un objet terminal de Hask et tout type vide est un objet initial.

Revenant à l'opération manquante susmentionnée, dans une catégorie fermée cartésienne, vous avez des objets exponentiels qui correspondent aux flèches de la catégorie. Nos flèches sont des fonctions, nos objets sont des types avec kind *, et le type A -> Bse comporte en effet comme B ^A dans le cadre de la manipulation algébrique des types. Si ce n'est pas évident pourquoi cela devrait tenir, considérez le type Bool -> A. Avec seulement deux entrées possibles, une fonction de ce type est isomorphe à deux valeurs de type A, c'est-à-dire (A, A). Car Maybe Bool -> Anous avons trois entrées possibles, et ainsi de suite. Notez également que si nous reformulons la définition de copairing ci-dessus pour utiliser la notation algébrique, nous obtenons l'identité C ^A × C ^B = C^{A + B} .

Quant à savoir pourquoi tout cela a du sens - et en particulier pourquoi votre utilisation de l'extension de la série de puissance est justifiée - notez qu'une grande partie de ce qui précède se réfère aux "habitants" d'un type (c'est-à-dire, des valeurs distinctes ayant ce type) afin pour démontrer le comportement algébrique. Pour rendre cette perspective explicite:

• Le type de produit (A, B)représente une valeur provenant de Aet Bprise indépendamment. Donc pour toute valeur fixe a :: A, il y a 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 des facteurs.

• Le type de somme Either A Breprésente une valeur de Aou B, avec les branches gauche et droite distinguées. Comme mentionné précédemment, il s'agit d'une union disjointe, et le nombre d'habitants du type somme est la somme du nombre d'habitants des sommets.

• Le type exponentiel B -> Areprésente un mappage des valeurs de type Baux valeurs de type A. Pour tout argument fixe b :: B, n'importe quelle valeur de Apeut lui être affectée; une valeur de type B -> Asélectionne un tel mappage pour chaque entrée, ce qui équivaut à un produit d'autant d'exemplaires Aque Bd'habitants, d'où l'exponentiation.

Bien qu'il soit tentant au début de traiter les types comme des ensembles, cela ne fonctionne pas très bien dans ce contexte - nous avons une union disjointe plutôt que l'union standard des ensembles, il n'y a pas d'interprétation évidente de l'intersection ou de nombreuses autres opérations d'ensemble, et nous ne se soucient généralement pas de l'appartenance à un ensemble (laissant cela au vérificateur de type).

D'un autre côté, les constructions ci-dessus passent beaucoup de temps à parler du comptage des habitants, et l' énumération des valeurs possibles d'un type est ici un concept utile. Cela nous amène rapidement à la combinatoire énumérative , et si vous consultez l'article Wikipédia lié, vous constaterez que l'une des premières choses qu'il fait est de définir des "paires" et des "unions" dans le même sens que les types de produits et de somme par le biais de générer des fonctions , fait de même pour les "séquences" qui sont identiques aux listes de Haskell en utilisant exactement la même technique que vous.

Edit: Oh, et voici un petit bonus qui, je pense, démontre le point de façon frappante. Vous avez mentionné dans un commentaire que pour un type d'arbre, T = 1 + T^2vous pouvez dériver l'identité T^6 = 1, ce qui est clairement faux. Cependant, T^7 = T cela tient, et une bijection entre les arbres et sept tuples d'arbres peut être construite directement, cf. "Sept arbres en un" d'Andreas Blass .

Edit × 2: Au sujet de la construction «dérivée d'un type» mentionnée dans d'autres réponses, vous pourriez également apprécier cet article du même auteur qui s'appuie sur l'idée, y compris les notions de division et d'autres joyeusetés intéressantes.

Les arbres binaires sont définis par l'équation T=1+XT^2dans le semirage des types. Par construction, T=(1-sqrt(1-4X))/(2X)est défini par la même équation dans le semirage de nombres complexes. Donc, étant donné que nous résolvons la même équation dans la même classe de structure algébrique, il ne devrait pas être surprenant de constater des similitudes.

Le hic, c'est que lorsque nous raisonnons sur les polynômes dans le semirage de nombres complexes, nous utilisons généralement le fait que les nombres complexes forment un anneau ou même un champ, nous nous retrouvons donc à utiliser des opérations telles que la soustraction qui ne s'appliquent pas aux semirings. Mais nous pouvons souvent éliminer les soustractions de nos arguments si nous avons une règle qui nous permet d'annuler des deux côtés d'une équation. C'est le genre de chose prouvé par Fiore et Leinster montrant que de nombreux arguments sur les anneaux peuvent être transférés aux demi-anneaux.

Cela signifie que beaucoup de vos connaissances mathématiques sur les anneaux peuvent être transférées de manière fiable aux types. En conséquence, certains arguments impliquant des nombres complexes ou des séries de puissances (dans l'anneau des séries de puissances formelles) peuvent être transférés aux types de manière complètement rigoureuse.

Cependant, il y a plus dans l'histoire que ça. C'est une chose de prouver que deux types sont égaux (disons) en montrant que deux séries de puissance sont égales. Mais vous pouvez également déduire des informations sur les types en inspectant les termes de la série de puissances. Je ne suis pas sûr de ce que devrait être la déclaration officielle ici. (Je recommande de Brent Yorgey document sur les espèces combinatoires pour un travail qui est étroitement lié , mais les espèces sont pas les mêmes que les types.)

Ce que je trouve complètement époustouflant, c'est que ce que vous avez découvert peut être étendu au calcul. Les théorèmes sur le calcul peuvent être transférés au semirage des types. En fait, même les arguments sur les différences finies peuvent être transférés et vous constatez que les théorèmes classiques de l'analyse numérique ont des interprétations dans la théorie des types.

S'amuser!

Il semble que tout ce que vous faites est d'élargir la relation de récurrence.

L = 1 + X • L
L = 1 + X • (1 + X • (1 + X • (1 + X • ...)))
  = 1 + X + X^2 + X^3 + X^4 ...

T = 1 + X • T^2
L = 1 + X • (1 + X • (1 + X • (1 + X • ...^2)^2)^2)^2
  = 1 + X + 2 • X^2 + 5 • X^3 + 14 • X^4 + ...

Et puisque les règles pour les opérations sur les types fonctionnent comme les règles pour les opérations arithmétiques, vous pouvez utiliser des moyens algébriques pour vous aider à comprendre comment développer la relation de récurrence (car ce n'est pas évident).

Je n'ai pas de réponse complète, mais ces manipulations ont tendance à «simplement fonctionner». Un article pertinent pourrait être Objects of Categories as Complex Numbers de Fiore et Leinster - je suis tombé sur celui-ci en lisant le blog de sigfpe sur un sujet connexe ; le reste de ce blog est une mine d'or pour des idées similaires et vaut le détour!

Soit dit en passant, vous pouvez également différencier les types de données - cela vous donnera la fermeture éclair appropriée pour le type de données!

L'algèbre des processus de communication (ACP) traite de types d'expressions similaires pour les processus. Il offre l'addition et la multiplication en tant qu'opérateurs de choix et de séquence, avec des éléments neutres associés. Sur cette base, il existe des opérateurs pour d'autres constructions, telles que le parallélisme et la perturbation. Voir http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes . Il existe également un article en ligne intitulé "Une brève histoire de l'algèbre des processus".

Je travaille sur l'extension des langages de programmation avec ACP. En avril dernier, j'ai présenté un document de recherche aux Scala Days 2012, disponible sur http://code.google.com/p/subscript/

Lors de la conférence, j'ai démontré un débogueur exécutant une spécification récursive parallèle d'un sac:

Sac = A; (Sac et a)

où A et un pour les actions d'entrée et de sortie; le point-virgule et l'esperluette représentent la séquence et le parallélisme. Voir la vidéo sur SkillsMatter, accessible à partir du lien précédent.

Une spécification de sac plus comparable à

L = 1 + X • L

serait

B = 1 + X & B

ACP définit le parallélisme en termes de choix et de séquence en utilisant des axiomes; voir l'article Wikipedia. Je me demande à quoi servirait l'analogie du sac

L = 1 / (1-X)

La programmation de style ACP est pratique pour les analyseurs de texte et les contrôleurs GUI. Spécifications telles que

searchCommand = cliqué (searchButton) + clé (Entrée)

cancelCommand = cliqué (cancelButton) + touche (Échap)

peut être écrit de manière plus concise en rendant implicites les deux raffinements "cliqué" et "clé" (comme ce que Scala permet avec les fonctions). On peut donc écrire:

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

Le côté droit contient désormais des opérandes qui sont des données plutôt que des processus. À ce niveau, il n'est pas nécessaire de savoir quels raffinements implicites transformeront ces opérandes en processus; ils ne se raffineraient pas nécessairement en actions de saisie; les actions de sortie s'appliqueraient également, par exemple dans la spécification d'un robot de test.

Les processus obtiennent ainsi les données comme compagnons; ainsi j'invente le terme "algèbre d'élément".

Séries de calcul et de maclaurine avec types

Voici un autre ajout mineur - un aperçu combinatoire des raisons pour lesquelles les coefficients dans une expansion de série devraient «fonctionner», en se concentrant en particulier sur les séries qui peuvent être dérivées en utilisant l' approche Taylor-Maclaurin du calcul. NB: l'exemple de développement de séries que vous donnez du type liste manipulée est une série Maclaurin.

Étant donné que d'autres réponses et commentaires traitent du comportement des expressions de type algébrique (sommes, produits et exposants), cette réponse élidera ce détail et se concentrera sur le type «calcul».

Vous remarquerez peut-être des virgules inversées qui soulèvent des charges lourdes dans cette réponse. Il y a deux raisons:

• nous sommes en train de donner des interprétations d'un domaine à des entités d'un autre et il semble approprié de délimiter de telles notions étrangères de cette manière.
• certaines notions pourront être formalisées plus rigoureusement, mais la forme et les idées semblent plus importantes (et prennent moins de place pour écrire) que les détails.

Définition de la série Maclaurin

La série Maclaurin d'une fonction f : ℝ → ℝest définie comme

f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f⁽ⁿ⁾(0)Xⁿ + ...

où f⁽ⁿ⁾signifie la ndérivée e de f.

Pour être en mesure de donner un sens à la série Maclaurin telle qu'interprétée avec les types, nous devons comprendre comment nous pouvons interpréter trois choses dans un contexte de type:

• un dérivé (éventuellement multiple)
• appliquer une fonction à 0
• des termes comme (1/n!)

et il s'avère que ces concepts issus de l'analyse ont des équivalents appropriés dans le monde des types.

Qu'est-ce que j'entends par «contrepartie appropriée»? Elle devrait avoir la saveur d'un isomorphisme - si nous pouvons préserver la vérité dans les deux sens, les faits pouvant être dérivés dans un contexte peuvent être transférés dans l'autre.

Calcul avec types

Que signifie donc la dérivée d'une expression de type? Il s'avère que pour une grande classe d'expressions de types et de foncteurs bien comportés («différenciables»), il existe une opération naturelle qui se comporte suffisamment pour être une interprétation appropriée!

Pour gâcher la punchline, l'opération analogue à la différenciation est celle de faire des «contextes à un trou». C'est un excellent endroit pour approfondir ce point particulier, mais le concept de base d'un contexte à un trou ( da/dx) est qu'il représente le résultat de l'extraction d'un seul sous-élément d'un type particulier ( x) d'un terme (de type a), en préservant toutes les autres informations, y compris celles nécessaires pour déterminer l'emplacement d'origine du sous-élément. Par exemple, une façon de représenter un contexte à un trou pour une liste consiste à utiliser deux listes: une pour les éléments qui ont précédé celle extraite et une pour les éléments qui ont suivi.

La motivation pour identifier cette opération avec différenciation vient des observations suivantes. Nous écrivons da/dxpour signifier le type de contextes à un trou pour type aavec trou de type x.

d1/dx = 0
dx/dx = 1
d(a + b)/dx = da/dx + db/dx
d(a × b)/dx = a × db/dx + b × da/dx
d(g(f(x))/dx = d(g(y))/dy[f(x)/a] × df(x)/dx

Ici, 1et 0représentent des types avec exactement un et exactement zéro habitants, respectivement, +et ×représentent des types de somme et de produit comme d'habitude. fet gsont utilisés pour représenter des fonctions de type, ou des formateurs d'expression de type, et [f(x)/a]signifie l'opération de substitution f(x)de chacun adans l'expression précédente.

Cela peut être écrit dans un style sans point, écrit f'pour signifier la fonction dérivée de type fonction f, ainsi:

(x ↦ 1)' = x ↦ 0
(x ↦ x)' = x ↦ 1
(f + g)' = f' + g'
(f × g)' = f × g' + g × f'
(g ∘ f)' = (g' ∘ f) × f'

ce qui peut être préférable.

NB les égalités peuvent être rendues rigoureuses et exactes si nous définissons des dérivées en utilisant des classes d'isomorphisme de types et de foncteurs.

Maintenant, nous remarquons en particulier que les règles de calcul relatives aux opérations algébriques d'addition, de multiplication et de composition (souvent appelées règles de somme, de produit et de chaîne) se reflètent exactement par l'opération de `` faire un trou ''. De plus, les cas de base de `` faire un trou '' dans une expression constante ou le terme xlui-même se comportent également comme une différenciation, donc par induction, nous obtenons un comportement de différenciation pour toutes les expressions de type algébrique.

Maintenant, nous pouvons interpréter la différenciation, que signifie la n«dérivée» d'une expression de type dⁿe/dxⁿ? Il s'agit d'un type représentant des ncontextes locaux: des termes qui, lorsqu'ils sont «remplis» de ntermes de type, xproduisent un e. Il y a une autre observation clé liée à ' (1/n!)' venir plus tard.

La partie invariante d'un foncteur de type: application d'une fonction à 0

Nous avons déjà une interprétation pour 0dans le monde des types: un type vide sans membres. Que signifie, d'un point de vue combinatoire, lui appliquer une fonction de type? Plus concrètement, en supposant qu'il fs'agit d'une fonction de type, à quoi f(0)ressemble-t-elle? Eh bien, nous n'avons certainement pas accès à quoi que ce soit de type 0, donc toutes les constructions f(x)qui nécessitent un ne xsont pas disponibles. Il ne reste que les termes accessibles en leur absence, que nous pouvons appeler la partie «invariante» ou «constante» du type.

Pour un exemple explicite, prenez le Maybefoncteur, qui peut être représenté algébriquement par x ↦ 1 + x. Lorsque nous appliquons cela à 0, nous obtenons 1 + 0- c'est comme 1: la seule valeur possible est la Nonevaleur. De même, pour une liste, nous obtenons uniquement le terme correspondant à la liste vide.

Lorsque nous le rapportons et interprétons le type f(0)comme un nombre, il peut être considéré comme le décompte du nombre de termes de type f(x)(pour n'importe quel x) pouvant être obtenus sans accès à un x: c'est-à-dire le nombre de termes "de type vide" .

Assembler: interprétation complète d'une série Maclaurin

Je crains de ne pas pouvoir penser à une interprétation directe appropriée du (1/n!)type.

Si nous considérons, cependant, le type f⁽ⁿ⁾(0)à la lumière de ce qui précède, nous voyons qu'il peut être interprété comme le type de ncontextes -place pour un terme de type f(x)qui ne contient pas déjà un x - c'est-à-dire lorsque nous les `` intégrons '' nfois , le terme résultant a exactement n x s, ni plus, ni moins. L'interprétation du type f⁽ⁿ⁾(0)sous forme de nombre (comme dans les coefficients de la série Maclaurin de f) est simplement un décompte du nombre de ces ncontextes vides . Nous y sommes presque!

Mais où (1/n!)finit-il? L'examen du processus de «différenciation» de type nous montre que, lorsqu'il est appliqué plusieurs fois, il préserve «l'ordre» dans lequel les sous-termes sont extraits. Par exemple, considérez le terme (x₀, x₁)de type x × xet l'opération de «faire un trou» deux fois. Nous obtenons les deux séquences

(x₀, x₁)  ↝  (_₀, x₁)  ↝  (_₀, _₁)
(x₀, x₁)  ↝  (x₀, _₀)  ↝  (_₁, _₀)
(where _ represents a 'hole')

même si les deux viennent du même terme, car il y a 2! = 2moyen de prendre deux éléments en deux, en préservant l'ordre. En général, il existe desn! moyens d'extraire des néléments n. Donc, pour obtenir le nombre de configurations d'un type de foncteur qui ont des néléments, nous devons compter le type f⁽ⁿ⁾(0)et diviser par n!, exactement comme dans les coefficients de la série Maclaurin.

La division par n!se révèle donc être interprétable simplement comme elle-même.

Réflexions finales: définitions «récursives» et analyticité

Tout d'abord, quelques observations:

• si une fonction f: ℝ → ℝ a une dérivée, cette dérivée est unique
• de même, si une fonction f: ℝ → ℝ est analytique, elle a exactement une série polynomiale correspondante

Puisque nous avons la règle de chaîne, nous pouvons utiliser la différenciation implicite , si nous formalisons les dérivés de type en classes d'isomorphisme. Mais la différenciation implicite ne nécessite aucune manœuvre extraterrestre comme la soustraction ou la division! Nous pouvons donc l'utiliser pour analyser les définitions de types récursifs. Pour prendre votre exemple de liste, nous avons

L(X) ≅ 1 + X × L(X)
L'(X) = X × L'(X) + L(X)

puis nous pouvons évaluer

L'(0) = L(0) = 1

pour obtenir le coefficient de X¹dans la série Maclaurin.

Mais puisque nous sommes convaincus que ces expressions sont en effet strictement `` différenciables '', ne serait-ce qu'implicitement, et puisque nous avons la correspondance avec les fonctions ℝ → ℝ, où les dérivées sont certainement uniques, nous pouvons être assurés que même si nous obtenons les valeurs en utilisant '' opérations illégales, le résultat est valide.

Maintenant, de manière similaire, pour utiliser la deuxième observation, en raison de la correspondance (est-ce un homomorphisme?) Avec les fonctions ℝ → ℝ, nous savons que, à condition que nous soyons convaincus qu'une fonction a une série de Maclaurin, si nous pouvons trouver une série à tous , les principes énoncés ci-dessus peuvent être appliqués pour le rendre rigoureux.

Quant à votre question sur la composition des fonctions, je suppose que la règle de chaîne fournit une réponse partielle.

Je ne sais pas à combien d'ADT de style Haskell cela s'applique, mais je pense que c'est beaucoup sinon la totalité. J'ai découvert une preuve vraiment merveilleuse de ce fait, mais cette marge est trop petite pour la contenir ...

Maintenant, ce n'est certainement qu'une façon de comprendre ce qui se passe ici et il y a probablement beaucoup d'autres façons.

Résumé: TL; DR

• le type 'différenciation' correspond à ' faire un trou '.
• appliquer un foncteur 0nous donne les termes «vides» pour ce foncteur.
• Les séries de puissance de Maclaurin correspondent donc (quelque peu) rigoureusement à l'énumération du nombre de membres d'un type foncteur avec un certain nombre d'éléments.
• la différenciation implicite rend cela plus étanche.
• l'unicité des dérivés et l'unicité des séries de puissance signifient que nous pouvons truquer les détails et cela fonctionne.

Théorie des types dépendants et fonctions de type «arbitraires»

Ma première réponse à cette question était élevée sur les concepts et faible sur les détails et réfléchie à la sous-question, «que se passe-t-il?»; cette réponse sera la même mais concentrée sur la sous-question, «pouvons-nous obtenir des fonctions de type arbitraire?».

Une extension des opérations algébriques de somme et de produit sont les soi-disant `` grands opérateurs '', qui représentent la somme et le produit d'une séquence (ou plus généralement, la somme et le produit d'une fonction sur un domaine) généralement écrits Σet Πrespectivement. Voir la notation Sigma .

Donc la somme

a₀ + a₁X + a₂X² + ...

pourrait être écrit

Σ[i ∈ ℕ]aᵢXⁱ

où aest une séquence de nombres réels, par exemple. Le produit serait représenté de manière similaire avec Πau lieu de Σ.

Lorsque vous regardez de loin, ce type d'expression ressemble beaucoup à une fonction «arbitraire» dans X; nous sommes bien entendu limités aux séries exprimables et à leurs fonctions analytiques associées. Est-ce un candidat pour une représentation dans une théorie des types? Absolument!

La classe des théories de type qui ont des représentations immédiates de ces expressions est la classe des théories de type «dépendantes»: les théories avec des types dépendants. Naturellement, nous avons des termes qui dépendent des termes, et dans des langages comme Haskell avec des fonctions de type et une quantification de type, des termes et des types selon les types. Dans un cadre dépendant, nous avons en outre des types selon les termes. Haskell n'est pas un langage typé de manière dépendante, bien que de nombreuses fonctionnalités des types dépendants puissent être simulées en torturant un peu le langage .

Curry-Howard et types dépendants

L'isomorphisme de Curry-Howard a commencé sa vie comme une observation que les termes et les règles de jugement de type du calcul lambda simplement typé correspondent exactement à la déduction naturelle (telle que formulée par Gentzen) appliquée à la logique propositionnelle intuitionniste, les types tenant lieu de propositions et des termes remplaçant les preuves, bien que les deux soient inventés / découverts indépendamment. Depuis lors, il a été une énorme source d'inspiration pour les théoriciens des types. L'une des choses les plus évidentes à considérer est de savoir si, et comment, cette correspondance pour la logique propositionnelle peut être étendue aux logiques de prédicat ou d'ordre supérieur. Les théories de type dépendantes sont d'abord nées de cette voie d'exploration.

Pour une introduction à l'isomorphisme de Curry-Howard pour le calcul lambda de type simple, voir ici . Par exemple, si nous voulons prouver, A ∧ Bnous devons prouver Aet prouver B; une preuve combinée est simplement une paire de preuves: une pour chaque conjoint.

En déduction naturelle:

Γ ⊢ A    Γ ⊢ B
Γ ⊢ A ∧ B

et dans le calcul lambda simplement tapé:

Γ ⊢ a : A    Γ ⊢ b : B
Γ ⊢ (a, b) : A × B

Des correspondances similaires existent pour les ∨types de somme et de somme, →et les types de fonction, et les différentes règles d'élimination.

Une proposition non démontrable (intuitivement fausse) correspond à un type inhabité.

En gardant à l'esprit l'analogie des types comme propositions logiques, nous pouvons commencer à réfléchir à la façon de modéliser les prédicats dans le monde des types. Il existe de nombreuses façons de formaliser cela (voir cette introduction à la théorie des types intuitionnistes de Martin-Löf pour une norme largement utilisée), mais l'approche abstraite observe généralement qu'un prédicat est comme une proposition avec des variables de terme libres, ou, alternativement, une fonction prenant des termes pour des propositions. Si nous permettons aux expressions de type de contenir des termes, alors un traitement dans le style du calcul lambda se présente immédiatement comme une possibilité!

En ne considérant que les preuves constructives, de quoi constitue une preuve ∀x ∈ X.P(x)? Nous pouvons la considérer comme une fonction de preuve, en prenant des termes ( x) aux preuves de leurs propositions correspondantes ( P(x)). Ainsi , les membres (preuves) du type (proposition) ∀x : X.P(x)sont des « fonctions dépendantes », qui , pour chaque xà Xdonner un terme de type P(x).

Et alors ∃x ∈ X.P(x)? Nous avons besoin de tout membre X, xainsi qu'une preuve de P(x). Les membres (preuves) du type (proposition) ∃x : X.P(x)sont donc des «paires dépendantes»: un terme distingué xdans X, avec un terme de type P(x).

Notation: je vais utiliser

∀x ∈ X...

pour les déclarations réelles sur les membres de la classe X, et

∀x : X...

pour les expressions de type correspondant à la quantification universelle sur le type X. De même pour ∃.

Considérations combinatoires: produits et sommes

En plus de la correspondance de Curry-Howard des types avec propositions, nous avons la correspondance combinatoire des types algébriques avec des nombres et des fonctions, qui est le point principal de cette question. Heureusement, cela peut être étendu aux types dépendants décrits ci-dessus!

Je vais utiliser la notation module

|A|

représenter la «taille» d'un type A, rendre explicite la correspondance décrite dans la question, entre les types et les nombres. Notez que c'est un concept en dehors de la théorie; Je ne prétends pas qu'il doit y avoir un tel opérateur dans la langue.

Comptons les membres possibles (entièrement réduits, canoniques) de type

∀x : X.P(x)

qui est le type de fonctions dépendantes prenant des termes xde type Xen termes de type P(x). Chacune de ces fonctions doit avoir une sortie pour chaque terme de X, et cette sortie doit être d'un type particulier. Pour chaque xdans X, puis, cela donne |P(x)|« choix » de sortie.

La punchline est

|∀x : X.P(x)| = Π[x : X]|P(x)|

ce qui bien sûr n'a pas beaucoup de sens si Xc'est le cas IO (), mais est applicable aux types algébriques.

De même, un terme de type

∃x : X.P(x)

est le type de paires (x, p)avec p : P(x), donc donné tout xen Xnous pouvons construire une paire appropriée avec un membre P(x), ce qui donne |P(x)|« choix ».

Par conséquent,

|∃x : X.P(x)| = Σ[x : X]|P(x)|

avec les mêmes mises en garde.

Cela justifie la notation commune pour les types dépendants dans les théories utilisant les symboles Πet Σ, en fait, de nombreuses théories brouillent la distinction entre `` pour tous '' et `` produit '' et entre `` il y a '' et `` somme '', en raison des correspondances susmentionnées.

Nous approchons!

Vecteurs: représentant des tuples dépendants

Pouvons-nous maintenant encoder des expressions numériques comme

Σ[n ∈ ℕ]Xⁿ

comme expressions de type?

Pas assez. Bien que nous puissions considérer de manière informelle la signification d'expressions comme Xⁿdans Haskell, où Xest un type et nun nombre naturel, c'est un abus de notation; il s'agit d'une expression de type contenant un nombre: clairement pas une expression valide.

D'un autre côté, avec des types dépendants dans l'image, les types contenant des nombres sont précisément le point; en fait, les tuples ou «vecteurs» dépendants sont un exemple très souvent cité de la façon dont les types dépendants peuvent fournir une sécurité pragmatique au niveau du type pour des opérations telles que l'accès aux listes . Un vecteur n'est qu'une liste avec des informations au niveau du type concernant sa longueur: précisément ce que nous recherchons pour des expressions de type comme Xⁿ.

Pendant la durée de cette réponse, laissez

Vec X n

être le type de longueur- nvecteurs de Xvaleurs de type.

Techniquement, nil s'agit, plutôt que d'un nombre naturel réel , d'une représentation dans le système d'un nombre naturel. Nous pouvons représenter les nombres naturels ( Nat) dans le style Peano comme zéro ( 0) ou le successeur ( S) d'un autre nombre naturel, et pour n ∈ ℕmoi j'écris ˻n˼pour signifier le terme dans Natlequel représente n. Par exemple, ˻3˼est S (S (S 0)).

Ensuite nous avons

|Vec X ˻n˼| = |X|ⁿ

pour tout n ∈ ℕ.

Types Nat: promotion de ℕ termes en types

Maintenant, nous pouvons encoder des expressions comme

Σ[n ∈ ℕ]Xⁿ

comme types. Cette expression particulière donnerait naissance à un type qui est bien sûr isomorphe au type de listes de X, comme identifié dans la question. (Non seulement cela, mais d'un point de vue théorique de catégorie, la fonction de type - qui est un foncteur - prenant Xle type ci-dessus est naturellement isomorphe au foncteur List.)

Une dernière pièce du puzzle des fonctions «arbitraires» est de savoir comment coder, par

f : ℕ → ℕ

des expressions comme

Σ[n ∈ ℕ]f(n)Xⁿ

de sorte que nous pouvons appliquer des coefficients arbitraires à une série de puissance.

Nous comprenons déjà la correspondance des types algébriques avec les nombres, ce qui nous permet de mapper des types aux nombres et des fonctions de type aux fonctions numériques. On peut aussi aller dans l'autre sens! - en prenant un nombre naturel, il existe évidemment un type algébrique définissable avec autant de membres de terme, que nous ayons ou non des types dépendants. Nous pouvons facilement le prouver en dehors de la théorie des types par induction. Ce dont nous avons besoin, c'est d'un moyen de mapper des nombres naturels aux types, à l' intérieur du système.

Une réalisation agréable est que, une fois que nous avons des types dépendants, la preuve par induction et la construction par récursivité deviennent intimement similaires - en fait, c'est la même chose dans de nombreuses théories. Puisque nous pouvons prouver par induction qu'il existe des types qui répondent à nos besoins, ne devrions-nous pas pouvoir les construire?

Il existe plusieurs façons de représenter les types au niveau du terme. J'utiliserai ici une notation Haskellish imaginaire avec *pour l'univers des types, lui-même généralement considéré comme un type dans un cadre dépendant. ¹

De même, il existe au moins autant de façons de noter «l' ℕélimination» qu'il y a de théories de type dépendantes. J'utiliserai une notation de correspondance de motifs Haskellish.

Nous avons besoin d'une cartographie, αde Natà *, avec la propriété

∀n ∈ ℕ.|α ˻n˼| = n.

La pseudodéfinition suivante suffit.

data Zero -- empty type
data Successor a = Z | Suc a -- Successor ≅ Maybe

α : Nat -> *
α 0 = Zero
α (S n) = Successor (α n)

On voit donc que l'action de αreflète le comportement du successeur S, ce qui en fait une sorte d'homomorphisme. Successorest une fonction de type qui «ajoute un» au nombre de membres d'un type; c'est-à-dire |Successor a| = 1 + |a|pour tous ceux adont la taille est définie.

Par exemple α ˻4˼(qui est α (S (S (S (S 0))))), est

Successor (Successor (Successor (Successor Zero)))

et les termes de ce type sont

Z
Suc Z
Suc (Suc Z)
Suc (Suc (Suc Z))

nous donnant exactement quatre éléments: |α ˻4˼| = 4.

De même, pour tout n ∈ ℕ, nous avons

|α ˻n˼| = n

comme demandé.

1. De nombreuses théories exigent que les membres de *soient de simples représentants de types, et une opération est fournie en tant que mappage explicite des termes de type *à leurs types associés. D'autres théories permettent aux types littéraux eux-mêmes d'être des entités au niveau du terme.

Fonctions «arbitraires»?

Nous avons maintenant l'appareil pour exprimer une série de puissance entièrement générale sous forme de type!

Les séries

Σ[n ∈ ℕ]f(n)Xⁿ

devient le type

∃n : Nat.α (˻f˼ n) × (Vec X n)

où se ˻f˼ : Nat → Nattrouve une représentation appropriée dans le langage de la fonction f. Nous pouvons voir ceci comme suit.

|∃n : Nat.α (˻f˼ n) × (Vec X n)|
    = Σ[n : Nat]|α (˻f˼ n) × (Vec X n)|          (property of ∃ types)
    = Σ[n ∈ ℕ]|α (˻f˼ ˻n˼) × (Vec X ˻n˼)|        (switching Nat for ℕ)
    = Σ[n ∈ ℕ]|α ˻f(n)˼ × (Vec X ˻n˼)|           (applying ˻f˼ to ˻n˼)
    = Σ[n ∈ ℕ]|α ˻f(n)˼||Vec X ˻n˼|              (splitting product)
    = Σ[n ∈ ℕ]f(n)|X|ⁿ                           (properties of α and Vec)

À quel point est-ce «arbitraire»? Nous sommes limités non seulement aux coefficients entiers par cette méthode, mais aux nombres naturels. En dehors de cela, fpeut être n'importe quoi, étant donné un langage Turing complet avec des types dépendants, nous pouvons représenter n'importe quelle fonction analytique avec des coefficients de nombres naturels.

Je n'ai pas étudié l'interaction de ceci avec, par exemple, le cas fourni dans la question de List X ≅ 1/(1 - X)ou quel sens possible de tels 'types' négatifs et non entiers pourraient avoir dans ce contexte.

Espérons que cette réponse va dans une certaine mesure pour explorer jusqu'où nous pouvons aller avec des fonctions de type arbitraire.