Note :
Le livre sur Idris offre une introduction attrayante au développement basé sur les types et au langage de programmation Idris. Les lecteurs le trouvent utile pour comprendre les systèmes de types avancés et apprécient ses explications claires. Cependant, certains utilisateurs éprouvent des difficultés avec la documentation et l'installation, ce qui peut entraver l'expérience d'apprentissage.
Avantages:⬤ Un contenu engageant et stimulant qui change les perspectives sur la programmation et les systèmes de types.
⬤ Tutoriel bien écrit qui est bénéfique pour l'apprentissage d'Idris et du développement basé sur les types.
⬤ L'auteur est le créateur d'Idris, ce qui lui confère un point de vue d'initié.
⬤ Souligne l'importance d'un typage fort et de la sécurité dans la programmation.
⬤ Présentation claire de concepts complexes accessibles aux lecteurs ayant une expérience de la programmation fonctionnelle.
⬤ Absence de guide d'installation et de documentation complets, entraînant des difficultés pour les nouveaux utilisateurs.
⬤ Certains lecteurs trouvent le langage peu courant et peuvent être découragés par la demande limitée sur le marché du travail.
⬤ Peut ne pas convenir aux débutants complets en raison des sujets avancés qui y sont abordés.
⬤ Des problèmes potentiels ont été relevés en ce qui concerne l'aptitude à la production, les utilisateurs étant mis en garde contre l'utilisation de ce logiciel dans des projets en cours.
(basé sur 11 avis de lecteurs)
Type-Driven Development with Idris
Résumé
Type-Driven Development with Idris, écrit par le créateur d'Idris, vous apprend à améliorer les performances et la précision de vos programmes en tirant parti d'un système de types de pointe. Ce livre vous apprend à utiliser Idris, un langage conçu pour supporter le développement guidé par les types.
L'achat du livre imprimé inclut un livre électronique gratuit aux formats PDF, Kindle et ePub de Manning Publications.
À propos de la technologie
Cessez de lutter contre les erreurs de type Le développement guidé par les types est une approche du codage qui considère les types comme la base de votre code - essentiellement comme une documentation intégrée que votre compilateur peut utiliser pour vérifier les relations entre les données et d'autres hypothèses. Cette approche permet de définir des spécifications dès le début du développement et d'écrire un code facile à maintenir, à tester et à étendre. Idris est un langage de type Haskell avec des types dépendants de première classe, parfait pour apprendre les techniques de programmation par type que vous pouvez appliquer dans n'importe quelle base de code.
A propos du livre
Type-Driven Development with Idris vous apprend à améliorer les performances et la précision de votre code en tirant parti d'un système de types à la pointe de la technologie. Dans ce livre, vous apprendrez à développer des logiciels réels en fonction des types, ainsi qu'à gérer les effets secondaires, l'interaction, l'état et la concurrence. À la fin, vous serez en mesure de développer des logiciels robustes et vérifiés dans Idris et d'appliquer les méthodes de développement axées sur les types à d'autres langages.
Ce qu'il y a à l'intérieur
⬤ Compréhension des types dépendants.
⬤ Les types en tant que constructions de première classe du langage.
⬤ Les types comme guide pour la construction de programmes.
⬤ L'expression des relations entre les données.
A propos du lecteur
Ecrit pour les programmeurs ayant une connaissance des concepts de la programmation fonctionnelle.
À propos de l'auteur
Edwin Brady dirige la conception et l'implémentation du langage Idris.
Table des matières
PARTIE 1 - INTRODUCTION.
⬤ Vue d'ensemble.
⬤ Démarrer avec IdrisPartie 2 - CORE IDRIS.
⬤ Développement interactif avec les types.
⬤ Types de données définis par l'utilisateur.
⬤ Programmes interactifs : traitement des entrées et des sorties.
⬤ Programmation avec des types de première classe.
⬤ Interfaces : utilisation de types génériques contraints.
⬤ L'égalité : expression des relations entre les données.
⬤ Prédicats : expression des hypothèses et des contrats dans les types.
⬤ Vues : étendre le filtrage des motifs.
PARTIE 3 - L'IDRIS ET LE MONDE RÉEL.
⬤ Les flux et les processus : travailler avec des données infinies.
⬤ L'écriture de programmes avec état.
⬤ Les machines à états : vérifier les protocoles dans les types.
⬤ Les machines à états dépendants : gérer le retour d'information et les erreurs.
⬤ Programmation concurrente à sécurité de type.
© Book1 Group - tous droits réservés.
Le contenu de ce site ne peut être copié ou utilisé, en tout ou en partie, sans l'autorisation écrite du propriétaire.
Dernière modification: 2024.11.14 07:32 (GMT)