Les fonctions n’ont pas que des types: elles SONT des types. Et les types. Et sortingomphe Aidez-nous à rétablir l’esprit

Je faisais ma routine habituelle “Lire un chapitre de LYAH avant le coucher”, ayant l’impression que mon cerveau se développait avec chaque échantillon de code. À ce stade, j’étais convaincu que je comprenais le caractère génial de Haskell et que je devais maintenant comprendre les bibliothèques standard et les classes de types afin de pouvoir commencer à écrire de vrais logiciels.

Je lisais donc le chapitre sur les foncteurs applicatifs lorsque, tout à coup, le livre affirmait que les fonctions ne se limitent pas à des types, mais à des types et peuvent être traitées comme telles (par exemple, en en faisant des instances de classes de type). (->) est un constructeur de type comme les autres.

Mon esprit a encore une fois explosé et j’ai immédiatement sauté hors du lit, j’ai démarré l’ordinateur, je suis allé à GHCi et j’ai découvert ce qui suit:

Prelude> :k (->) (->) :: ?? -> ? -> * 
  • Qu’est-ce que cela signifie?
  • Si (->) est un constructeur de type, quels sont les constructeurs de valeurs? Je peux deviner, mais je n’aurais aucune idée de la façon dont le définir dans les data (->) ... = ... | ... | ... traditionnelles data (->) ... = ... | ... | ... data (->) ... = ... | ... | ... data (->) ... = ... | ... | ... format Il est assez facile de le faire avec tout autre constructeur de type: data Either ab = Left a | Right b data Either ab = Left a | Right b . Je soupçonne que mon incapacité à l’exprimer sous cette forme est liée à la signature de type extrêmement étrange.
  • Qu’est-ce que je viens de découvrir? Les types similaires ont des signatures aimables comme * -> * -> * . En y pensant … (->) apparaît aussi en gentilles signatures! Est-ce que cela signifie que non seulement c’est un constructeur de type, mais aussi un constructeur gentil? Est-ce lié aux points d’interrogation dans la signature de type?

J’ai lu quelque part (j’aimerais pouvoir le retrouver, Google me manque) sur la possibilité d’étendre arbitrairement les systèmes de types en allant des valeurs aux types de valeurs, aux types de types, aux types de caractères, à quelque chose de différent, à quelque chose d’autre de quelque chose, et ainsi de suite pour toujours. Est-ce que cela se reflète dans la signature aimable pour (->)? Parce que j’ai également rencontré la notion de cube Lambda et le calcul de constructions sans prendre le temps de les étudier réellement, et si je me souviens bien, il est possible de définir des fonctions qui prennent les types et les types de retour, prennent des valeurs et renvoient des valeurs. , prendre des types et renvoyer des valeurs, et prendre des valeurs qui renvoient des types.

Si j’avais à deviner la signature de type pour une fonction qui prend une valeur et renvoie un type, je l’exprimerais probablement comme ceci:

 a -> ? 

ou éventuellement

 a -> * 

Bien que je ne vois aucune raison fondamentale immuable pour laquelle le deuxième exemple ne pourrait pas facilement être interprété comme une fonction allant de la valeur de type a à une valeur de type *, où * est juste un synonyme de type chaîne ou quelque chose.

Le premier exemple exprime mieux une fonction dont le type transcende une signature de type dans mon esprit: “une fonction qui prend une valeur de type a et renvoie quelque chose qui ne peut pas être exprimé en tant que type”.

Vous touchez tellement de points intéressants dans votre question, alors je crains que cela ne soit une longue réponse 🙂

Genre de (->)

Le type de (->) est * -> * -> * si nous ne tenons pas compte des insertions Boxity GHC. Mais il n’y a pas de circularité, les -> s du genre (->) sont des flèches gentilles et non des flèches de fonction. En effet, pour les distinguer, les flèches peuvent être écrites sous la forme (=>) , puis le type de (->) est * => * => * .

Nous pouvons considérer (->) comme un constructeur de type, ou plutôt comme un opérateur de type. De même, (=>) peut être considéré comme un opérateur gentil , et comme vous le suggérez dans votre question, nous devons aller plus loin. Nous y reviendrons plus tard dans la section Audelà des types , mais d’abord:

Comment la situation se présente dans un langage typé

Vous demandez comment la signature de type rechercherait une fonction qui prend une valeur et renvoie un type. C’est impossible à faire dans Haskell: les fonctions ne peuvent pas retourner les types! Vous pouvez simuler ce comportement en utilisant des classes de type et des familles de types, mais laissez-nous pour illustration changer la langue pour le langage typé de manière dépendante Agda . Ceci est un langage avec une syntaxe similaire à Haskell où les types de jonglage avec les valeurs sont une seconde nature.

Pour avoir quelque chose à travailler, nous définissons un type de données de nombres naturels, par souci de commodité dans la représentation unaire, comme dans Peano Arithmetic . Les types de données sont écrits dans le style GADT :

 data Nat : Set where Zero : Nat Succ : Nat -> Nat 

Set est équivalent à * dans Haskell, le “type” de tous les (petits) types, tels que les nombres naturels. Cela nous indique que le type de Nat est Set , alors que dans Haskell, Nat n’aurait pas de type, il aurait un genre, à savoir * . Dans Agda, il n’y a pas de genre, mais tout a un type.

Nous pouvons maintenant écrire une fonction qui prend une valeur et renvoie un type. Ci-dessous se trouve la fonction qui prend un nombre naturel n et un type, et fait itérer le constructeur de List n appliqué à ce type. (Dans Agda, [a] est généralement écrit List a )

 listOfLists : Nat -> Set -> Set listOfLists Zero a = a listOfLists (Succ n) a = List (listOfLists na) 

Quelques exemples:

 listOfLists Zero Bool = Bool listOfLists (Succ Zero) Bool = List Bool listOfLists (Succ (Succ Zero)) Bool = List (List Bool) 

Nous pouvons maintenant créer une fonction de map qui fonctionne sur listsOfLists . Nous devons prendre un nombre naturel qui correspond au nombre d’itérations du constructeur de liste. Les cas de base sont lorsque le nombre est Zero , alors listOfList est juste l’identité et nous appliquons la fonction. L’autre est la liste vide et la liste vide est renvoyée. Le cas de l’étape est un petit mouvement impliquant: nous appliquons mapN à la tête de la liste, mais cela a une couche de moins d’imbrication et mapN au rest de la liste.

 mapN : {ab : Set} -> (a -> b) -> (n : Nat) -> listOfLists na -> listOfLists nb mapN f Zero x = fx mapN f (Succ n) [] = [] mapN f (Succ n) (x :: xs) = mapN fnx :: mapN f (Succ n) xs 

Dans le type de mapN , l’argument Nat est nommé n , donc le rest du type peut en dépendre. Il s’agit donc d’un exemple de type dépendant d’une valeur.

En parallèle, il existe également deux autres variables nommées, à savoir les premiers arguments, a et b , de type Set . Les variables de type sont implicitement universellement quantifiées dans Haskell, mais ici nous devons les épeler et spécifier leur type, à savoir Set . Les crochets sont là pour les rendre invisibles dans la définition, car ils sont toujours déductibles des autres arguments.

Set est abstrait

Vous demandez ce que sont les constructeurs de (->) . Une chose à souligner est que Set (ainsi que * dans Haskell) est abstrait: vous ne pouvez pas y créer de motif. Donc c’est illégal Agda:

 cheating : Set -> Bool cheating Nat = True cheating _ = False 

Encore une fois, vous pouvez simuler une correspondance de modèle sur des constructeurs de types dans Haskell en utilisant des familles de types, un exemple classique est donné sur le blog de Brent Yorgey . Peut-on définir -> dans l’Agda? Comme nous pouvons renvoyer des types de fonctions, nous pouvons définir une propre version de -> comme suit:

 _=>_ : Set -> Set -> Set a => b = a -> b 

(Les opérateurs infixes sont écrits _=>_ plutôt que (=>) ) Cette définition a très peu de contenu et ressemble beaucoup à un synonyme de type dans Haskell:

 type Fun ab = a -> b 

Au-delà des genres: les tortues tout en bas

Comme promis ci-dessus, tout dans Agda a un type, mais alors le type de _=>_ doit avoir un type! Cela touche votre sharepoint vue sur les sortes, qui sont, pour ainsi dire, une couche au-dessus de Set (les types). Dans Agda, cela s’appelle Set1 :

 FunType : Set1 FunType = Set -> Set -> Set 

Et en fait, il y en a toute une hiérarchie! Set est le type de “petits” types: les types de données dans le haskell. Mais nous avons ensuite Set2 , Set3 , Set3 , etc. Set1 est le type de types qui mentionne Set . Cette hiérarchie vise à éviter les incohérences telles que le paradoxe de Girard.

Comme indiqué dans votre question, -> est utilisé pour les types et les types dans Haskell, et la même notation est utilisée pour les espaces de fonctions à tous les niveaux dans Agda. Cela doit être considéré comme un opérateur de type intégré, et les constructeurs sont l’abstraction lambda (ou les définitions de fonctions). Cette hiérarchie de types est similaire à celle de System Fomega , et vous trouverez plus d’informations dans les chapitres suivants de Types et langages de programmation de Pierce .

Systèmes de type pur

Dans Agda, les types peuvent dépendre de valeurs et les fonctions peuvent renvoyer des types, comme illustré ci-dessus, et nous avons également une hiérarchie de types. Une étude systématique des différents systèmes des calculs lambda est étudiée plus en détail dans les systèmes de type pur. Une bonne référence est Lambda Calculi with Types de Barendregt, où PTS est présenté à la page 96, et de nombreux exemples à la page 99 et suivantes. Vous pouvez également en lire plus sur le cube lambda.

Tout d’abord, le ?? -> ? -> * ?? -> ? -> * ?? -> ? -> * type est une extension spécifique au GHC. Le ? et ?? sont juste là pour traiter avec les types sans boîte, qui se comportent différemment que * (qui doit être mis en boîte, pour autant que je sache). Donc ?? peut être n’importe quel type normal ou un type sans boîte (par exemple Int# ); ? peut être l’un de ceux-ci ou un tuple sans boîte. Il y a plus d’informations ici: Haskell Weird Kinds: Genre de (->) est ?? ->? -> *

Je pense qu’une fonction ne peut pas renvoyer un type sans boîte parce que les fonctions sont paresseuses. Comme une valeur paresseuse est une valeur ou un thunk, elle doit être encadrée. Boxed signifie simplement que c’est un pointeur plutôt qu’une simple valeur: c’est comme Integer() vs int en Java.

Comme vous n’allez probablement pas utiliser les types non-boxés dans le code de niveau LYAH, vous pouvez imaginer que le type de -> est juste * -> * -> * .

Depuis le ? et ?? sont fondamentalement juste version plus générale de * , ils n’ont rien à voir avec des sortes ou quelque chose comme ça.

Cependant, puisque -> est juste un constructeur de type, vous pouvez l’appliquer en partie; Par exemple, (->) e est une instance de Functor et Monad . Comprendre comment écrire ces exemples est un bon exercice d’étirement.

En ce qui concerne les constructeurs de valeurs, ils doivent simplement être lambdas ( \ x -> ) ou des déclarations de fonction. Les fonctions étant si fondamentales pour le langage, elles ont leur propre syntaxe.