Types de citoyen de première classe

Venant d'un arrière-plan C ++, je ne comprends pas pourquoi on a besoin de types / expressions de type en tant que citoyen de première classe? La seule langue que je connaisse qui prend en charge cette fonctionnalité est Aldor.

Quelqu'un at-il de la littérature sur les types de citoyens de première classe ou connaît-il les raisons pour lesquelles cela est utile?

Les types de première classe permettent ce que l'on appelle le typage dépendant . Ceux-ci permettent au programmeur d'utiliser des valeurs de types au niveau du type. Par exemple, le type de toutes les paires d'entiers est un type régulier, tandis que la paire de tous les entiers dont le nombre gauche est inférieur au nombre droit est un type dépendant. L'exemple d'introduction standard de ceci est les listes codées par longueur (généralement appelées Vectordans Haskell / Idris). Le pseudo-code suivant est un mélange d'Idris et de Haskell.

-- a natural number
data Nat = Zero | Successor Nat

data Vector length typ where
  Empty : Vector Zero typ
  (::)   : typ -> Vector length typ -> Vector (Successor length) typ

Ce morceau de code nous dit deux choses:

• La liste vide a une longueur nulle.
• consun élément sur une liste crée une liste de longueur n + 1

Cela ressemble beaucoup à un autre concept avec 0 et n + 1, n'est-ce pas? J'y reviendrai.

Que gagnons-nous de cela? Nous pouvons maintenant déterminer des propriétés supplémentaires des fonctions que nous utilisons. Par exemple: Une propriété importante de appendest que la longueur de la liste résultante est la somme des longueurs des deux listes d'arguments:

plus : Nat -> Nat -> Nat
plus          Zero n = n
plus (Successor m) n = Successor (plus m n)

append : Vector n a -> Vector m a -> Vector (plus n m) a
append Empty  ys = ys
append (x::xs) ys = x :: append xs ys

Mais dans l'ensemble, cette technique ne semble pas du tout utile dans la programmation quotidienne. Comment est - ce lié à des prises, POST/ GETdemandes et ainsi de suite?

Eh bien non (du moins pas sans efforts considérables). Mais cela peut nous aider d'autres façons:

Les types dépendants nous permettent de formuler des invariants dans les règles de code comme la façon dont une fonction doit se comporter. En les utilisant, nous obtenons une sécurité supplémentaire sur le comportement du code, similaire aux pré et postconditions d'Eiffel. Ceci est extrêmement utile pour la démonstration automatisée de théorèmes, qui est l'une des utilisations possibles d'Idris.

Pour revenir à l'exemple ci-dessus, la définition des listes codées en longueur ressemble au concept mathématique d' induction . Dans Idris, vous pouvez réellement formuler le concept d'induction sur une telle liste comme suit:

              -- If you can supply the following:
list_induction : (Property : Vector len typ -> Type) -> -- a property to show
                  (Property Empty) -> -- the base case
                  ((w : a) -> (v : Vector n a) ->
                      Property v -> Property (w :: v)) -> -- the inductive step
                  (u : Vector m b) -> -- an arbitrary vector
                  Property u -- the property holds for all vectors

Cette technique se limite aux preuves constructives, mais est néanmoins très puissante. Vous pouvez essayer d'écrire par appendinduction comme exercice.

Bien sûr, les types dépendants ne sont qu'une utilisation des types de première classe, mais c'est sans doute l'un des plus courants. Les utilisations supplémentaires incluent, par exemple, le renvoi d'un type spécifique à partir d'une fonction en fonction de ses arguments.

type_func : Vector n a -> Type
type_func Empty = Nat
type_func v     = Vector (Successor Zero) Nat

f : (v : Vector n a) -> type_func v
f Empty = 0
f vs    = length vs :: Empty

C'est un exemple absurde, mais il montre quelque chose que vous ne pouvez pas émuler sans des types de première classe.