Tipos como ciudadano de primera clase

Viniendo de un entorno de C ++, no entiendo por qué uno necesita tipos / expresiones de tipo como ciudadano de primera clase. El único idioma que sé que admite esta función es Aldor.

¿Alguien tiene alguna literatura sobre tipos como ciudadano de primera clase o sabe algunas razones por las que es útil?

Los tipos de primera clase habilitan algo llamado tipeo dependiente . Estos permiten al programador usar valores de tipos a nivel de tipo. Por ejemplo, el tipo de todos los pares de enteros es un tipo regular, mientras que el par de todos los enteros con el número izquierdo más pequeño que el número derecho es un tipo dependiente. El ejemplo introductorio estándar de esto son las listas codificadas por longitud (típicamente llamadas Vectoren Haskell / Idris). El siguiente pseudocódigo es una mezcla de Idris y 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

Este código nos dice dos cosas:

• La lista vacía tiene longitud cero.
• consAl incorporar un elemento a una lista, se crea una lista de longitud. n + 1

Esto se ve muy similar a otro concepto con 0 y n + 1, ¿no? Volveré a eso.

¿Qué ganamos con esto? Ahora podemos determinar propiedades adicionales de las funciones que utilizamos. Por ejemplo: una propiedad importante de appendes que la longitud de la lista resultante es la suma de las longitudes de las dos listas de argumentos:

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

Pero en general, esta técnica no parece ser muy útil en la programación diaria. ¿Cómo se relaciona esto con los sockets, POST/ GETpeticiones, etc.?

Bueno, no lo hace (al menos no sin un esfuerzo considerable). Pero puede ayudarnos de otras maneras:

Los tipos dependientes nos permiten formular invariantes en el código: reglas sobre cómo debe comportarse una función. Con estos, obtenemos seguridad adicional sobre el comportamiento del código, similar a las condiciones previas y posteriores de Eiffel. Esto es extremadamente útil para la demostración automatizada de teoremas, que es uno de los posibles usos de Idris.

Volviendo al ejemplo anterior, la definición de listas codificadas por longitud se asemeja al concepto matemático de inducción . En Idris, puedes formular el concepto de inducción en una lista como la siguiente:

              -- 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

Esta técnica se limita a pruebas constructivas, pero es muy poderosa. Puedes intentar escribir appendinductivamente como ejercicio.

Por supuesto, los tipos dependientes son solo un uso de los tipos de primera clase, pero podría decirse que es uno de los más comunes. Los usos adicionales incluyen, por ejemplo, devolver un tipo específico de una función en función de sus argumentos.

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

Este es un ejemplo sin sentido, pero demuestra algo que no se puede emular sin tipos de primera clase.