Vous utilisez un système de type «fort» dans le monde réel, par exemple, pour des applications Web à grande échelle?

Je sais que c'est une question très large, ambiguë et peut-être philosophique. Dans une certaine mesure, le mot-clé le plus important de la question - système de type «fort» - lui-même est mal défini . Alors, laissez-moi essayer d'expliquer ce que je veux dire.

Contexte général de la question

Nous avons construit une application web à très grande échelle dans Ruby on Rails et nous sommes généralement satisfaits de notre pile. Lorsque nous le voulons, nous pouvons expédier des trucs très rapidement - quelque chose qui fonctionne pour 90% du cas «commercial», sans trop se soucier de 10% des cas de pointe. D'un autre côté, avec l'aide des révisions de code et de la couverture des tests, nous pouvons être lents et délibérés et nous assurer de couvrir toutes les bases - encore une fois, uniquement dans des situations qui méritent un examen et une sécurité plus étroits.

Cependant, au fur et à mesure que l'équipe grandit, j'ai commencé à me sentir mal à l'aise avec l'absence d'un «filet de sécurité» cuit directement dans notre tapis.

Nous avons récemment commencé à faire du développement natif Android sur Java. Et j'ai été (agréablement) rappelé la sécurité offerte par un langage compilé / statique / fortement typé.

• Les variables mal orthographiées, les types de données incorrects, les appels de fonctions incorrects et une multitude d'erreurs triviales sont détectés par votre IDE lui-même. Tout cela parce que l'EDI peut se connecter au compilateur et vérifier certains aspects de la «correction» du programme.
• Besoin de changer une signature de fonction? Facile. Le compilateur + IDE peut vous aider à repérer TOUS les sites d'appel.
• Besoin de vous assurer que certaines exceptions sont toujours gérées? Vérifié les exceptions à votre secours.

Maintenant, bien que ces caractéristiques de sécurité aient leurs avantages, je connais bien leurs inconvénients. Plus encore, dans le monde du Java "lourd". Par conséquent, au lieu de Java, j'ai commencé à regarder le flot de langages modernes "fortement typés" sur lesquels les gens ont commencé à travailler ces jours-ci. Par exemple: Scala, Rust, Haskell, etc. Ce qui m'intéresse le plus, c'est la puissance de leurs systèmes de types et les contrôles statiques / de compilation.

Maintenant, la question

Comment puis-je utiliser ces systèmes de type puissants et ces fonctionnalités statiques / de compilation dans des applications plus grandes?

Par exemple, comment pourrais-je aller au-delà du type standard "bonjour monde" des introductions à ces fonctionnalités puissantes? Celui qui utilise un système de type riche pour modéliser un problème de domaine commercial? Le système de saisie aide-t-il ou gêne-t-il lorsque vous êtes dans la zone 30 000 LOC +? Qu'advient-il du filet de sécurité fourni par ces systèmes de type (et vérifications au moment de la compilation) lorsque votre système interagit avec le monde extérieur faiblement typé, par exemple. via des API JSON ou XML, divers magasins de données, entrée utilisateur, etc.

Je vais donner une réponse courte en raison du manque de temps pour le moment, mais je travaille actuellement sur deux grands projets (> 100 000 LOC à Haskell) - flowbox.io et luna-lang.org. Nous utilisons Haskell pour toutes les parties, y compris le backend, le compilateur de notre langage de programmation et même l'interface graphique WebGL. Je dois admettre que le système de type fort et la machinerie semblable au "type dépendant" peuvent vous guider et vous épargner des charges et des tracas connus dans d'autres langues. Nous utilisons les types très largement et tout ce qui pourrait être vérifié lors de la compilation, le fait. En fait, au cours des 3 dernières années de développement, nous n'avons jamais rencontré d'erreur d'exécution ou de débordement de pile (et c'est quelque chose de vraiment incroyable). Les seules erreurs sont des erreurs logiques évidentes faites par les programmeurs. Beaucoup de gens disent que si quelque chose se compile dans Haskell, cela fonctionne et vous devez être sûr que cela ne vous soufflera pas un jour.

Répondre à la première partie de la question: vous pouvez en apprendre davantage sur ces puissantes fonctionnalités du système de type en lisant certains grands blogs, comme:

• Blog de Bartosz Milewski
• Celui d'Edward Kmett
• ou Gabriel Gonzales un

En fait, il existe de nombreux autres blogs sympas (comme la planète Haskell ). Quoi qu'il en soit, la meilleure méthode pour vraiment comprendre les systèmes de types avancés est de développer une bibliothèque open source utile. Nous (chez Flowbox & New Byte Order) publions un grand nombre de bibliothèques (vous pouvez les trouver sur Hackage), donc si vous ne savez pas quoi développer, vous pouvez toujours vous impliquer dans nos projets - envoyez-moi simplement un e-mail chaque fois que vous vouloir (courrier disponible sur luna-lang.org ).

Eh bien, le typage faible vs fort est défini de façon assez vague. En outre, étant donné que le plus proche d'une utilisation générale du «typage fort» est de renvoyer des choses qui rendent difficile la conversion de types, ce qui ne laisse rien de plus pour décrire des systèmes de types encore plus forts. C'est comme dire que si vous pouvez transporter moins de 30 livres, vous êtes faible, et tous ceux qui peuvent soulever plus sont dans la même catégorie de «fort» - une distinction trompeuse.

Je préfère donc la définition:

• Les systèmes mal typés utilisent des types pour vous empêcher de faire certaines choses (comme des erreurs)
• Les systèmes fortement typés utilisent des types pour faire des choses pour vous

Qu'est-ce que je veux dire par faire des choses pour vous? Eh bien, examinons l'écriture d'une API de conversion d'image dans le framework Servant (dans Haskell, mais vous n'avez pas vraiment besoin de le savoir pour suivre, vous verrez ...)

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

Cela signifie que nous voulons certains modules, y compris le package Servant et le plug-in JuicyPixels pour Servant, et que le point d'entrée principal du programme est d'exécuter la fonction de `` conversion '' sur le port 8001 en tant que serveur utilisant le backend Warp. Ignorez le bit de langue.

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

Cela signifie que la fonction de conversion est un serveur où l'API doit correspondre au type 'ConversionApi' et les demandes sont traitées par la fonction handler

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

Ceci spécifie le ConvesionApitype. Il dit que nous devons accepter les types de contenu entrants spécifiés par la liste '[BMP, GIF, JPEG 50, PNG, TIFF, RADIANCE], et les traiter comme une DynamicImage, et que nous devons renvoyer une DynamicImage convertie dans la même plage de contenu les types. Ne vous inquiétez pas exactement de ce que:> signifie, considérez-le comme une magie heureuse pour l'instant.

Donc, étant donné ma définition préférée, un système faiblement typé peut désormais garantir des choses comme:

• Vous ne renvoyez pas le mauvais type de contenu sortant
• Vous n'analysez pas la demande entrante comme un type de contenu incorrect
• Si notre serveur était plus compliqué, cela nous empêcherait de créer des URI malformés, mais nous ne renvoyons en fait aucune page HTML contenant des liens (et le type garantit que nous ne pouvons pas!)
• Un système de typage faible vraiment ambitieux pourrait même vérifier pour s'assurer que nous traitons de manière exhaustive tous les types de contenu entrant et sortant, permettant au type d'agir également comme un document de spécification au lieu d'une simple contrainte.

Tous les objectifs élevés, mais pas suffisamment pour être considérés comme un système fortement typé, compte tenu de la définition ci-dessus. Et maintenant, nous devons passer à la partie difficile de l'écriture du code qui suit cette spécification. Dans un système de type très fort , nous écrivons:

handler = return

Et puis nous avons terminé. Ça y est , il n'y a plus de code à écrire . Il s'agit d'un serveur Web entièrement opérationnel (modulo toutes les fautes de frappe que j'ai manquées). Le type a dit au compilateur tout ce dont il a besoin pour créer notre serveur Web à partir des types et des packages (modules techniquement) que nous avons définis et importés.

Alors, comment apprenez-vous à le faire à l'échelle de l'application principale? Eh bien, ce n'est vraiment pas très différent de les utiliser dans des applications à plus petite échelle. Les types absolus ne se soucient pas de la quantité de code écrit les concernant.

L'inspection des types d'exécution est quelque chose que vous voudrez probablement éviter, car cela élimine une énorme quantité d'avantages et permet aux types de rendre votre projet plus compliqué à travailler, plutôt que d'avoir des types simplifiant les choses.

En tant que tel, il s'agit principalement de s'entraîner à modéliser des choses avec des types. Les deux principales façons de modéliser des choses (ou de construire des choses en général) sont de bas en haut et de haut en bas. De haut en bas commence avec le plus haut niveau d'opérations, et lorsque vous construisez le modèle, vous avez des pièces où vous reportez la modélisation à plus tard. La modélisation ascendante signifie que vous commencez par les opérations de base, tout comme vous commencez par les fonctions de base, puis créez des modèles de plus en plus grands jusqu'à ce que vous ayez entièrement capturé le fonctionnement du projet. De bas en haut est plus concret et probablement plus rapide à construire, mais de haut en bas peut mieux informer vos modèles de niveau inférieur sur la façon dont ils doivent réellement se comporter.

Les types sont la façon dont les programmes se rapportent aux mathématiques, littéralement, donc il n'y a pas vraiment de limite supérieure sur la complexité de leur complication, ou un point où vous pouvez en finir avec eux. Pratiquement toutes les ressources en dehors des cours universitaires de niveau supérieur sont toutes consacrées au fonctionnement des types dans une langue particulière, vous devez donc en décider également.

Du mieux que je puisse offrir, les types peuvent être stratifiés comme suit:

• Très faiblement typé, des choses comme JavaScript où [] + {} est défini
• Faible type comme Python, où vous ne pouvez pas faire [] + {}, mais cela n'est vérifié que lorsque vous essayez
• Faible type comme C ou Java, où vous ne pouvez pas faire [] + {}, mais qui est vérifié au moment de la compilation, mais vous n'avez pas les fonctionnalités de type plus avancées
• À cheval sur la frontière entre les types faiblement et fortement typés, comme la métaprogrammation de modèles C ++ et le code Haskell plus simple où les types ne font qu'appliquer des propriétés.
• Complètement dans Fortement typé, comme les programmes Haskell plus compliqués où les types font des choses, comme indiqué ci-dessus
• Le très fortement typé, comme Agda ou Idris, où les types et les valeurs interagissent et peuvent se contraindre. C'est aussi fort que les systèmes de types, et leur programmation équivaut à écrire des preuves mathématiques sur ce que fait votre programme. Remarque: coder dans Agda ce n'est pas littéralement écrire des preuves mathématiques, les types sont des théories mathématiques et les fonctions avec ces types sont des exemples constructifs prouvant ces théories.

Généralement, plus vous descendez dans cette liste, plus les types peuvent faire pour vous, mais tout en bas, vous grimpez dans la stratosphère et l'air devient un peu mince - l'écosystème du package est beaucoup plus petit et vous '' Je vais devoir écrire plus de choses vous-même que d'avoir trouvé une bibliothèque appropriée. La barrière à l'entrée augmente également au fur et à mesure que vous descendez, car vous devez comprendre suffisamment le système de type pour écrire des programmes à grande échelle.

Je viens de commencer à travailler sur l'équipe centrale d'une grande plateforme écrite en Scala. Vous pouvez consulter les applications open source réussies, comme Scalatra, Play ou Slick pour voir comment elles gèrent certaines de vos questions plus détaillées sur les interactions avec les formats de données dynamiques.

L'un des grands avantages que nous avons trouvés du typage fort de Scala est dans la formation des utilisateurs. L'équipe principale peut prendre des décisions et appliquer ces décisions dans le système de types. Ainsi, lorsque d'autres équipes qui sont beaucoup moins familiarisées avec les principes de conception doivent interagir avec le système, le compilateur les corrige et l'équipe principale ne corrige pas constamment les choses dans tirer des demandes. C'est un énorme avantage dans un grand système.

Bien sûr, tous les principes de conception ne peuvent pas être appliqués dans un système de types, mais plus votre système de types est solide, plus vous pouvez appliquer de principes de conception dans le compilateur.

Nous pouvons également faciliter les choses pour les utilisateurs. Souvent, pour eux, ils ne font que travailler avec des collections ou des classes de cas normales, et nous le convertissons automatiquement en JSON ou quoi que ce soit selon les besoins pour le transport réseau.

Un typage fort permet également de faire des différenciations entre des éléments comme les entrées non désinfectées et désinfectées, ce qui peut contribuer à la sécurité.

Un typage fort aide également vos tests à se concentrer davantage sur votre comportement réel , au lieu d'avoir besoin d'un tas de tests qui testent simplement vos types. Cela rend les tests beaucoup plus agréables, plus ciblés et donc plus efficaces.

Le principal inconvénient est la méconnaissance de la langue et du paradigme de la langue, et cela peut être corrigé avec le temps. A part cela, nous avons trouvé que cela valait bien l'effort.

Bien que ce ne soit pas une réponse directe (puisque je n'ai pas encore travaillé sur +30.000 bases de code LOC dans haskell :( ..), je vous implore de consulter https://www.fpcomplete.com/business/resources/case-studies / qui présente de nombreuses études de cas de haskell dans des contextes industriels réels.

Un autre bon article est IMVU, qui décrit leur expérience en passant à haskell - http://engineering.imvu.com/2014/03/24/what-its-like-to-use-haskell/ .

De son expérience personnelle dans des applications plus importantes, le type système très bien vous aide, surtout si vous essayez de coder autant que vous le pouvez dans les types. Le vrai pouvoir est vraiment évident quand il s'agit de refactoriser les choses - ce qui signifie que la maintenance et autres deviennent une tâche beaucoup moins inquiétante.

Je vais vider quelques liens vers des ressources que je recommande, car vous posez beaucoup de questions à la fois:

• Petite série sur les optimisations communes, dans haskell
• Penser en types
• Puisque vous êtes dans le monde du développement Web, je vous suggère de vérifier Yesod , qui est l'un des cadres Web très étonnants de haskell (propose des itinéraires de type sécurisé et bien plus encore).

Pour terminer, le traitement du monde extérieur se fait de plusieurs manières. Il existe des bibliothèques pour vous assurer que les choses de votre côté sont de type sécurisé, comme Aeson pour JSON, Esqueleto pour SQL et bien d'autres.

Ce que j'ai vu:

J'ai travaillé sur quelques grandes applications Web Ruby (Rails), une grande application Web Haskell et plusieurs plus petites. Avec cette expérience, je dois dire que la vie de travail sur les applications Haskell est beaucoup plus facile que dans Rails à des égards tels que la maintenance et la courbe d'apprentissage inférieure. Je suis d'avis que ces avantages sont à la fois dus au système de type de Haskell et au style de programmation fonctionnel. Cependant, contrairement à beaucoup, je pense que la partie "statique" du système de saisie n'est qu'une grande commodité dans la mesure où il y a encore des avantages à tirer lors de l'utilisation de contrats dynamiques.

Ce que je crois

Il existe un joli package appelé Contracts Ruby qui fournit des fonctionnalités principales qui, selon moi, aident les projets Haskell à obtenir de meilleures caractéristiques de maintenance. Contrats Ruby effectue ses vérifications au moment de l'exécution, il est donc préférable lorsqu'il est associé à une convergence de test élevée, mais il fournit toujours la même documentation en ligne et l'expression d'intention et de sens que l'utilisation d'annotations de type dans des langages tels que Haskell.

Réponse à la question

Pour répondre aux questions posées ci-dessus, il existe de nombreux endroits où l'on peut se familiariser avec Haskell et d'autres langues avec des systèmes de type avancés. Cependant, et pour être parfaitement honnête, bien que ces sources de documentation soient excellentes en elles-mêmes, elles semblent toutes un peu décevantes par rapport à la pléthore de documentation et de conseils pratiques trouvés dans Ruby, Python, Java et d'autres langages de ce type. En tout cas, Real World Haskell vieillit mais reste une bonne ressource.

Catégorie Théorie

Si vous choisissez Haskell, vous rencontrerez une grande quantité de littérature traitant de la théorie des catégories. La théorie des catégories à mon humble avis est utile mais pas nécessaire. Étant donné sa prévalence dans la communauté Haskell, il est facile de confondre les avantages et les inconvénients des types avec des sentiments sur le caractère pratique de la théorie des catégories. Il est utile de se rappeler que ce sont deux choses différentes, c'est-à-dire que les implémentations guidées par la théorie des catégories peuvent être faites dans des langages typés dynamiquement aussi bien que statiques (modulo les avantages du système de types). Les systèmes de types avancés en général ne sont pas liés à la théorie des catégories et la théorie des catégories n'est pas liée aux systèmes de types.

Plus sur les types

Au fur et à mesure que vous en apprendrez plus sur la programmation avec les types et les techniques qui s'y trouvent (ce qui se produit assez rapidement parce que c'est amusant), vous voudrez exprimer plus avec le système de types. Dans ce cas, j'examinerais certaines des ressources suivantes et me joindrais à moi pour informer les fournisseurs d'outils que nous voulons que les outils de qualité industrielle avec ces fonctionnalités ne soient emballés que dans quelque chose qui expose une interface facile à utiliser (comme Contracts Ruby):

• Introduction à la programmation dans ATS

• Types de raffinement LiquidHaskell via SMT et abstraction de prédicat

• Développement piloté par type avec Idris

Premièrement, j'ai l'impression qu'il y a une confusion dans les réponses entre typé faiblement contre fortement typé et statique versus dynamiquement typé. Lier l'OP fourni fait clairement la distinction:

Un système de type fort est un système de type qui a une restriction au moment de la compilation ou une fonctionnalité au moment de l'exécution que vous trouvez attrayante.

Un système de type faible est un système de type qui n'a pas cette restriction ou fonctionnalité.

Par exemple, C, C ++ et Java sont typés statiquement puisque les variables sont typées au moment de la compilation. Pourtant, C et C ++ peuvent être considérés comme faiblement typés car le langage permet de contourner les restrictions à l'aide de void *pointeurs et de transtypages. Plus sur ce sujet.

Sur cette distinction, un typage fort ne peut être que meilleur. Plus l'échec est précoce, mieux c'est.

Cependant, lors de l'écriture de grands programmes, je ne pense pas que le système de type joue un rôle important. Le noyau Linux est composé de dix millions de LOC écrit en C et assembleur et est considéré comme un programme très stable, il est à des kilomètres de mes 200 lignes Java qui sont probablement pleines de failles de sécurité. De même, bien que les "langages de script" typés dynamiquement souffrent d'une mauvaise réputation lorsqu'il s'agit d'écrire de gros programmes, il y a parfois des preuves qu'il n'est pas mérité (comme Python Django, plus de 70k LOC)

À mon avis, c'est une question de qualité. La responsabilité de l'évolutivité des grandes applications ne devrait être assumée que par les programmeurs et les architectes et leur volonté de rendre l'application propre, testée, bien documentée, etc.

Où peut-on lire comment utiliser ces puissants systèmes de type et ces fonctions statiques / de compilation dans des applications plus grandes?

de la réponse précédente https://www.fpcomplete.com/business/resources/case-studies/

Comment peut-on aller au-delà du type standard "bonjour monde" d'introduction à ces fonctionnalités puissantes?

c'est vraiment comme n'importe quelle autre langue pour se renforcer

Comment peut-on utiliser un système de type riche pour modéliser un problème de domaine métier?

En utilisant des types de données abstraits, ou plus généralement le polymorphisme

Le système de saisie aide-t-il ou gêne-t-il lorsque vous êtes dans la zone 30 000 LOC +?

Ça aide tout du long. le système de type vous aide à écrire le code car il vous indique la forme du résultat que vous souhaitez obtenir. En fait, Agda écrit du code pour vous.

PS: ne faites pas l'erreur d'avoir un système de type et d'avoir à écrire les types vous-même, ce qui est idiot: l'ordinateur peut le faire pour vous.

Qu'advient-il du filet de sécurité fourni par ces systèmes de type (et des contrôles au moment de la compilation) lorsque votre système interagit avec le monde extérieur faiblement typé, par exemple. via des API JSON ou XML, divers magasins de données, entrée utilisateur, etc.

C'est génial, car connaître la structure des valeurs via les types signifie que l'ordinateur peut déduire un moyen d'écrire (dé) sérialiseur pour vous.

Si vous voulez vraiment en savoir plus sur les types et l'abstraction, la meilleure introduction est Sur la compréhension des types, de l'abstraction des données et du polymorphisme

C'est un papier, pas une étude de cas avec de jolies images, mais c'est instructif

En tant que programmeur .net qui travaille beaucoup sur les applications Web, je vois à la fois le côté typé C # et Javascript non typé.

Je ne suis pas sûr d'avoir vu de la littérature sur les questions que vous posez. Avec une langue dactylographiée, vous tenez toutes ces choses pour acquises. Avec un modèle non typé, vous voyez que la définition des types est une surcharge inutile.

Personnellement, je ne pense pas que vous puissiez nier qu'un langage fortement typé offre les avantages que vous décrivez à un coût très faible (par rapport à l'écriture de tests unitaires équivalents). L'interaction avec des systèmes faiblement typés implique généralement des types génériques, tels que des tableaux ou des dictionnaires d'objets, tels que DataReader, ou une utilisation créative de la chaîne ou de la nouvelle classe dynamique. Essentiellement, tout fonctionne, vous obtenez simplement une erreur d'exécution au lieu du temps de compilation.

Si vous voulez écrire un programme très court, peut-être en définissant une fonction en quelques lignes pour travailler avec une application plus grande, alors vous n'avez tout simplement pas de place pour déclarer des classes. C'est sûrement le créneau des langages non typés tels que JS occupent?