¿Usar un sistema de tipo "fuerte" en el mundo real, por ejemplo, para aplicaciones web a gran escala?

Sé que esta es una pregunta muy amplia, ambigua y posiblemente filosófica. Hasta cierto punto, la palabra clave más importante en la pregunta, el sistema de tipo "fuerte", está mal definida . Entonces, déjame intentar explicar lo que quiero decir.

Contexto general de la pregunta

Hemos estado construyendo una aplicación web a gran escala en Ruby on Rails y, en general, estamos contentos con nuestra pila. Cuando lo deseamos, podemos enviar cosas realmente rápido, algo que funciona para el 90% de los casos de "negocios", sin preocuparse demasiado por los casos extremos del 10%. Por otro lado, con la ayuda de revisiones de código y cobertura de pruebas, podemos ser lentos y deliberados y asegurarnos de cubrir todas las bases, nuevamente, solo en situaciones que merecen un escrutinio y seguridad más cercanos.

Sin embargo, a medida que el equipo crece, comencé a sentirme incómodo con la falta de una "red de seguridad" integrada directamente en nuestra pila.

Recientemente comenzamos a hacer un desarrollo nativo de Android en Java. Y me recordó (gratamente) la seguridad que brinda un lenguaje compilado / estático / fuertemente tipado.

• El IDE mismo detecta las variables mal escritas, los tipos de datos incorrectos, las invocaciones de funciones incorrectas y una gran cantidad de errores triviales. Todo porque el IDE puede conectarse al compilador y verificar ciertos aspectos de la "corrección" del programa.
• ¿Necesita cambiar la firma de una función? Fácil. El compilador + IDE puede ayudarlo a detectar TODOS los sitios de llamadas.
• ¿Necesita asegurarse de que siempre se manejen ciertas excepciones? Se verificaron excepciones a su rescate.

Ahora, si bien estas características de seguridad tienen sus ventajas, también conozco sus desventajas. Más aún, en el mundo de Java "pesado". Por lo tanto, en lugar de Java, comencé a mirar la gran cantidad de lenguajes modernos, "fuertemente tipados" en los que la gente ha comenzado a trabajar en estos días. Por ejemplo: Scala, Rust, Haskell, etc. Lo que más me interesa es el poder de sus sistemas de tipos y las comprobaciones estáticas / en tiempo de compilación.

Ahora la pregunta

¿Cómo uso estos potentes sistemas de tipos y características estáticas / tiempo de compilación en aplicaciones más grandes?

Por ejemplo, ¿cómo iría más allá de las introducciones estándar de "hola mundo" a estas potentes funciones? ¿Uno que utiliza un sistema de tipo rico para modelar un problema de dominio empresarial? ¿El sistema de tipos ayuda o dificulta cuando estás en la zona de 30,000 LOC +? ¿Qué sucede con la red de seguridad proporcionada por estos sistemas de tipo (y comprobaciones en tiempo de compilación) cuando su sistema interactúa con el mundo exterior débilmente tipado, por ejemplo? a través de API JSON o XML, varios almacenes de datos, entradas de usuarios, etc.

Daré una respuesta breve debido a mi falta de tiempo en este momento, pero actualmente estoy trabajando en dos grandes proyectos (> 100.000 LOC en Haskell): flowbox.io y luna-lang.org. Utilizamos Haskell para todas las partes, incluido el backend, el compilador de nuestro lenguaje de programación e incluso la GUI basada en webGL. Tengo que admitir que el sistema de tipo fuerte y la maquinaria tipo "tipo dependiente" pueden guiarlo y salvarlo de la carga y las molestias conocidas en otros idiomas. Usamos los tipos de manera muy exhaustiva y todo lo que se puede verificar en tiempo de compilación se realiza. De hecho, durante los últimos 3 años de desarrollo, nunca, nunca encontramos ningún error de tiempo de ejecución o desbordamiento de pila (y esto es algo realmente increíble). Los únicos errores son errores lógicos obvios cometidos por los programadores. Mucha gente dice que si algo se compila en Haskell, simplemente funciona y debes estar bastante seguro de que algún día no te va a explotar.

Respondiendo a la primera parte de la pregunta: puede aprender sobre estas potentes funciones del sistema de tipos leyendo algunos blogs excelentes, como:

• Blog de Bartosz Milewski
• El de Edward Kmett
• o Gabriel Gonzales uno

De hecho, hay muchos otros buenos blogs por ahí (como el planeta Haskell ). De todos modos, el mejor método para comprender realmente los sistemas de tipos avanzados es desarrollar una biblioteca útil de código abierto. Nosotros (en Flowbox y New Byte Order) estamos lanzando muchas bibliotecas (las puedes encontrar en Hackage), por lo que si no tienes idea de qué desarrollar, siempre puedes participar en nuestros proyectos, solo envíame un correo electrónico cuando lo desees. querer (correo disponible en luna-lang.org ).

Bueno, la escritura débil frente a la fuerte está bastante vagamente definida. Además, dado que lo más cercano a un uso general de 'tipeo fuerte' es referir cosas que dificultan la conversión de tipos, eso no deja nada más para describir sistemas de tipos aún más fuertes. Es como decir que si puedes cargar menos de 30 libras eres débil, y todos los que pueden levantar más están en la misma categoría de 'fuerte', una distinción engañosa.

Entonces prefiero la definición:

• Los sistemas con tipos débiles usan tipos para evitar que usted haga ciertas cosas (como errores)
• Los sistemas fuertemente tipados usan tipos para hacer cosas por usted

¿Qué quiero decir con hacer cosas por ti? Bueno, examinemos cómo escribir una API de conversión de imágenes en el marco Servant (en Haskell, pero realmente no necesita saberlo para seguir, verá ...)

{-# LANGUAGE
    TypeOperators,
    DataKinds
    #-}

import Codec.Picture
import Data.Proxy
import Network.Wai.Handler.Warp (run)
import Servant
import Servant.JuicyPixels

main :: IO ()
main = run 8001 conversion

Esto significa que queremos algunos módulos, incluido el paquete Servant y el complemento JuicyPixels para Servant, y que el punto de entrada principal del programa es ejecutar la función de 'conversión' en el puerto 8001 como el servidor que utiliza el backend Warp. Ignora el bit del idioma.

conversion :: Application
conversion = serve (Proxy :: Proxy ConversionApi) handler

Esto significa que la función de conversión es un servidor donde la API debe coincidir con el tipo 'ConversionApi' y las funciones son manejadas por la función handler

type ConversionApi
     = ReqBody '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage
    :> Post '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE] DynamicImage

Esto especifica el ConvesionApitipo. Dice que deberíamos aceptar los tipos de contenido entrante especificados por la lista '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE], y manejarlos como una imagen dinámica, y que deberíamos devolver una imagen dinámica convertida en el mismo rango de contenido tipos. No se preocupe exactamente por lo que:> significa, solo piense en ello como magia feliz por ahora.

Entonces, dada mi definición preferida, un sistema de tipo débil ahora puede garantizar cosas como:

• No devuelve el tipo de contenido saliente incorrecto
• No analiza la solicitud entrante como el tipo de contenido incorrecto
• Si nuestro servidor fuera más complicado, nos impediría crear URI con formato incorrecto, pero en realidad no devolveremos ninguna página HTML que contenga enlaces (¡y el tipo asegura que no podamos!)
• Un sistema de escritura débil realmente ambicioso podría incluso verificar para asegurarse de que estamos manejando exhaustivamente todos los tipos de contenido entrante y saliente, permitiendo que el tipo también actúe como un documento de especificación en lugar de solo una restricción.

Todos los objetivos elevados, pero en realidad no son suficientes para calificar como un sistema fuertemente tipado, dada la definición anterior. Y ahora tenemos que llegar a la parte difícil de escribir código que siga esta especificación. En un sistema de tipos realmente fuerte , escribimos:

handler = return

Y luego terminamos. Eso es todo, no hay más código para escribir . Este es un servidor web totalmente operativo (módulo de cualquier error tipográfico que me perdí). El tipo le ha dicho al compilador todo lo que necesita para crear nuestro servidor web a partir de los tipos y los paquetes (módulos técnicamente) que definimos e importamos.

Entonces, ¿cómo aprende a hacer esto en la escala de aplicación principal? Bueno, en realidad no es muy diferente de usarlos en aplicaciones de menor escala. A los tipos que son absolutos no les importa cuánto código se escriba en relación con ellos.

La inspección de tipo de tiempo de ejecución es algo que probablemente querrá evitar, ya que reduce una gran cantidad del beneficio y permite que los tipos hagan que su proyecto sea más complicado de trabajar, en lugar de hacer que los tipos simplifiquen las cosas.

Como tal, es principalmente una cuestión de práctica modelar cosas con tipos. Las dos formas principales de modelar cosas (o construir cosas en general) son de abajo hacia arriba y de arriba hacia abajo. De arriba hacia abajo comienza con el nivel más alto de operaciones, y a medida que construye el modelo, tiene partes en las que difiere el modelado hasta más tarde. El modelado de abajo hacia arriba significa que comienza con operaciones básicas, al igual que comienza con funciones básicas, luego construye modelos cada vez más grandes hasta que haya capturado completamente la operación del proyecto. De abajo hacia arriba es más concreto y probablemente más rápido de construir, pero de arriba hacia abajo puede informar mejor a sus modelos de nivel inferior sobre cómo deben comportarse realmente.

Los tipos son cómo los programas se relacionan con las matemáticas, literalmente, por lo que no hay realmente un límite superior sobre lo complicados que pueden llegar a ser, o un punto en el que se puede "terminar" de aprender sobre ellos. Prácticamente todos los recursos fuera de los cursos universitarios de nivel superior están dedicados a cómo funcionan los tipos en un idioma en particular, por lo que también debe decidir eso.

Lo mejor que puedo ofrecer, los tipos se pueden estratificar así:

• Muy débilmente tipado, cosas como JavaScript donde se define [] + {}
• Tecleado débilmente como Python, donde no puedes hacer [] + {}, pero eso no se verifica hasta que lo intentas
• Tecleado débilmente como C o Java, donde no puede hacer [] + {}, pero se verifica en el momento de la compilación, sin embargo, no tiene las características de tipo más avanzadas
• A caballo entre el tipo débil y fuertemente tipado, como la metaprogramación de plantillas de C ++ y el código de Haskell más simple donde los tipos solo imponen propiedades.
• Completamente en Tipografía fuerte, como programas Haskell más complicados donde los tipos hacen cosas, como se muestra arriba
• Muy fuertemente tipado, como Agda o Idris, donde los tipos y valores interactúan y pueden restringirse entre sí. Esto es tan fuerte como los sistemas de tipos, y programar en ellos es lo mismo que escribir pruebas matemáticas sobre lo que hace su programa. Nota: codificar en Agda no es literalmente escribir pruebas matemáticas, los tipos son teorías matemáticas y las funciones con esos tipos son ejemplos constructivos que prueban esas teorías.

En general, cuanto más baja en esta lista, más pueden hacer los tipos por usted, pero al final, está subiendo a la estratosfera y el aire se está volviendo un poco más delgado: el ecosistema del paquete es mucho más pequeño y usted ' Tendrás que escribir más cosas tú mismo en lugar de haber encontrado una biblioteca relevante. La barrera de entrada también aumenta a medida que desciende, ya que debe comprender el sistema de tipos lo suficiente como para escribir programas a gran escala.

Acabo de comenzar a trabajar en el equipo central de una gran plataforma escrita en Scala. Puede ver aplicaciones exitosas de código abierto, como Scalatra, Play o Slick para ver cómo manejan algunas de sus preguntas más detalladas sobre las interacciones con formatos de datos dinámicos.

Una de las grandes ventajas que hemos encontrado del tipeo fuerte de Scala es la educación del usuario. El equipo central puede tomar decisiones y aplicar esas decisiones en el sistema de tipos, por lo que cuando otros equipos que están mucho menos familiarizados con los principios de diseño tienen que interactuar con el sistema, el compilador los corrige y el equipo central no está corrigiendo constantemente las cosas. Solicitudes de extracción. Esta es una gran ventaja en un sistema grande.

Por supuesto, no todos los principios de diseño pueden aplicarse en un sistema de tipos, pero cuanto más fuerte sea su sistema de tipos, más principios de diseño puede aplicar en el compilador.

También podemos hacer las cosas más fáciles para los usuarios. A menudo, para ellos solo están trabajando con colecciones regulares o clases de casos, y lo estamos convirtiendo a JSON o lo que sea automáticamente según sea necesario para el transporte de red.

La escritura fuerte también ayuda a hacer diferenciaciones entre cosas como entradas no desinfectadas y desinfectadas, que pueden ayudar con la seguridad.

La escritura fuerte también ayuda a que sus pruebas se centren más en su comportamiento real , en lugar de necesitar un montón de pruebas que solo prueben sus tipos. Hace que las pruebas sean mucho más agradables, más enfocadas y, por lo tanto, más efectivas.

La principal desventaja es la falta de familiaridad con el lenguaje y el paradigma del lenguaje, y eso se puede corregir con el tiempo. Aparte de eso, hemos encontrado que vale la pena el esfuerzo.

Si bien no es una respuesta directa (dado que aún no he trabajado en más de 30.000 bases de código LOC en haskell :( ..), le imploro que consulte https://www.fpcomplete.com/business/resources/case-studies / que presenta muchos estudios de caso de haskell en entornos reales de la industria.

Otro buen artículo es IMVU, que describe su experiencia cambiando a haskell: http://engineering.imvu.com/2014/03/24/what-its-like-to-use-haskell/ .

Por experiencia personal en aplicaciones de mayor tamaño, el tipo de sistema muy mucho que ayuda, sobre todo si se intenta codificar tanto como sea posible en los tipos. El verdadero poder es realmente obvio cuando se trata de refactorizar cosas, lo que significa que el mantenimiento y tal se convierten en una tarea mucho menos preocupante.

Voy a volcar un par de enlaces a recursos que recomiendo, ya que está haciendo muchas preguntas a la vez:

• Pequeñas series sobre optimizaciones comunes, en haskell
• Pensando en tipos
• Dado que se encuentra en el mundo de desarrollo web, le sugiero que consulte Yesod , que es uno de los marcos web muy sorprendentes en Haskell (cuenta con rutas de tipo seguro y mucho más).

Como comentario final, el trato con el mundo exterior se realiza de varias maneras. Hay bibliotecas para asegurarse de que las cosas en su extremo sean seguras, como Aeson para JSON, Esqueleto para SQL y muchas más.

Lo que he visto:

He trabajado algunas aplicaciones web grandes de Ruby (Rails), una aplicación web grande de Haskell y varias más pequeñas. Con esa experiencia, debo decir que la vida laboral en las aplicaciones de Haskell es mucho más fácil que en Rails en aspectos como el mantenimiento y la curva de aprendizaje inferior. Soy de la opinión de que estos beneficios se deben tanto al sistema de tipos de Haskell como al estilo de programación funcional. Sin embargo, a diferencia de muchos, creo que la parte "estática" del sistema de tipos es solo una gran conveniencia, ya que todavía hay beneficios al usar contratos dinámicos.

Lo que creo

Hay un buen paquete llamado Contracts Ruby que proporciona algunas de las características principales que creo ayudan a los proyectos de Haskell a lograr mejores características de mantenimiento. Contratos Ruby realiza sus comprobaciones en tiempo de ejecución, por lo que es mejor cuando se combina con convergencia de prueba alta, pero aún proporciona la misma documentación en línea y expresión de intención y significado que el uso de anotaciones de tipo en idiomas como Haskell.

Responder a la pregunta

Para responder las preguntas planteadas anteriormente, hay muchos lugares donde uno puede familiarizarse con Haskell y otros idiomas con sistemas de tipos avanzados. Sin embargo, y para ser sincero, si bien estas fuentes de documentación son excelentes por sí mismas, todas parecen un poco decepcionantes en comparación con la gran cantidad de documentación y consejos prácticos que se encuentran en Ruby, Python, Java y otros lenguajes similares. En cualquier caso, el mundo real Haskell está envejeciendo pero sigue siendo un buen recurso.

Teoría de la categoría

Si elige Haskell, se encontrará con una gran cantidad de literatura sobre la teoría de la categoría. La teoría de la categoría de mi humilde opinión es útil pero no necesaria. Dada su prevalencia en la comunidad de Haskell, es fácil combinar los pros y los contras de los tipos con sentimientos sobre la practicidad de la teoría de categorías. Es útil recordar que son dos cosas diferentes, es decir que las implementaciones guiadas por la teoría de la categoría se pueden hacer en lenguajes dinámicamente tipados, así como estáticos (módulo de los beneficios que proporciona el sistema de tipos). Los sistemas de tipos avanzados en general no están sujetos a la teoría de categorías y la teoría de categorías no está vinculada a los sistemas de tipos.

Más sobre tipos

A medida que aprenda más sobre la programación con tipos y las técnicas que contiene (lo que sucede bastante rápido porque es divertido), querrá expresar más con el sistema de tipos. En ese caso, examinaría algunos de los siguientes recursos y me uniría para informar a los proveedores de herramientas que queremos que las herramientas de calidad industrial con estas características solo se empaqueten en algo que exponga una interfaz fácil de usar (como Contracts Ruby):

• Introducción a la programación en ATS

• Tipos de refinamiento de LiquidHaskell mediante SMT y abstracción de predicados

• Desarrollo guiado por tipo con Idris

Primero, siento que hay una confusión en las respuestas entre tipado débilmente y tipado fuertemente, y estático versus tipado dinámicamente. Enlace el OP proporcionado claramente hace la distinción:

Un sistema de tipo fuerte es un sistema de tipo que tiene una restricción de tiempo de compilación o una característica de tiempo de ejecución que le resulta atractiva.

Un sistema de tipo débil es un sistema de tipo que carece de esa restricción o característica.

Por ejemplo, C, C ++ y Java se escriben estáticamente, ya que las variables se escriben en tiempo de compilación. Sin embargo, C y C ++ pueden considerarse débilmente tipados porque el lenguaje permite eludir las restricciones mediante void *punteros y conversiones. Más sobre este tema.

En esta distinción, la escritura fuerte solo puede ser mejor. Cuanto antes falle, mejor.

Sin embargo, al escribir programas grandes, no creo que el sistema de tipos juegue un papel importante. El kernel de Linux tiene diez millones de LOC escritos en C y ensamblados y se considera un programa muy estable, está a millas de distancia de mis 200 líneas Java que probablemente estén llenas de agujeros de seguridad. Del mismo modo, aunque los "lenguajes de script" escritos dinámicamente sufren una mala reputación cuando se trata de escribir programas grandes, ocasionalmente hay pruebas de que no se lo merece (como Python Django, más de 70k LOC)

En mi opinión, se trata de estándares de calidad. La responsabilidad de la escalabilidad de las aplicaciones grandes solo debe ser responsabilidad de los programadores y los arquitectos y su voluntad de hacer que la aplicación sea limpia, probada, bien documentada, etc.

¿Dónde se puede leer acerca de cómo usar estos potentes sistemas de tipos y características estáticas / tiempo de compilación en aplicaciones más grandes?

de la respuesta anterior https://www.fpcomplete.com/business/resources/case-studies/

¿Cómo se puede ir más allá de las introducciones estándar de "hola mundo" a estas potentes funciones?

es realmente como cualquier otro idioma para fortalecer

¿Cómo se puede usar un sistema de tipo rico para modelar un problema de dominio empresarial?

Mediante el uso de tipos de datos abstractos, o más generalmente polimorfismo

¿El sistema de tipos ayuda o dificulta cuando estás en la zona de 30,000 LOC +?

Ayuda todo el camino. el sistema de tipos lo ayuda a escribir el código, ya que le indica la forma del resultado que desea tener. En realidad, Agda escribe el código para usted.

PD: no cometa el error de tener un sistema de tipos y tener que escribir los tipos usted mismo, lo cual es idiota: la computadora puede hacerlo por usted.

¿Qué sucede con la red de seguridad proporcionada por estos sistemas de tipo (y comprobaciones en tiempo de compilación) cuando su sistema interactúa con el mundo exterior débilmente tipado, por ejemplo? a través de API JSON o XML, varios almacenes de datos, entradas de usuarios, etc.

Es genial, ya que conocer la estructura de valores a través de tipos significa que la computadora puede inferir una forma de escribir (des) serializador para usted.

Si realmente desea saber acerca de los tipos y la abstracción, la mejor introducción es Sobre la comprensión de los tipos, la abstracción de datos y el polimorfismo

Es un trabajo, no un estudio de caso con imágenes bonitas, pero es esclarecedor.

Como programador .net que trabaja mucho en aplicaciones web, veo tanto el lado C # escrito como el Javascript sin tipo.

No estoy seguro de haber visto literatura sobre las preguntas que haces. Con un lenguaje mecanografiado, da todas estas cosas por sentado. Con uno sin tipo, verá la definición de los tipos como gastos generales innecesarios.

Personalmente, no creo que pueda negar que un lenguaje fuertemente tipado ofrece los beneficios que describe a un costo muy bajo (en comparación con escribir pruebas unitarias equivalentes). La interacción con sistemas de tipo débil generalmente implica tipos genéricos, como matrices o diccionarios de objetos, como DataReader, o el uso creativo de cadenas o la nueva clase dinámica. Esencialmente, todo funciona, solo obtienes un error de tiempo de ejecución en lugar de tiempo de compilación.

Si desea escribir un programa muy corto, tal vez definiendo una función en un par de líneas para trabajar con una aplicación más grande, entonces simplemente no tiene espacio para declarar clases. ¿Seguramente este es el nicho que ocupan los idiomas sin tipo como JS?