Sviluppo guidato dai tipi con Idris

Recensioni dei lettori

Il libro su Idris offre un'introduzione accattivante allo sviluppo guidato dai tipi e al linguaggio di programmazione Idris. I lettori lo trovano utile per comprendere i sistemi di tipi avanzati e ne apprezzano le spiegazioni chiare. Tuttavia, alcuni utenti hanno difficoltà con la documentazione e l'installazione, il che può ostacolare l'esperienza di apprendimento.

⬤ Contenuti coinvolgenti e stimolanti che cambiano le prospettive sulla programmazione e sui sistemi di tipi.
⬤ Tutorial ben scritto, utile per imparare Idris e lo sviluppo guidato dai tipi.
⬤ L'autore è il creatore di Idris e offre una prospettiva da insider.
⬤ Sottolinea l'importanza della tipizzazione forte e della sicurezza nella programmazione.
⬤ Presentazione chiara di concetti complessi, disponibile per i lettori con esperienza di programmazione funzionale.

⬤ Mancanza di una guida all'installazione e di una documentazione completa, con conseguenti difficoltà per i nuovi utenti.
⬤ Alcuni lettori trovano il linguaggio poco comune e potrebbero essere scoraggiati dalla scarsa richiesta nel mercato del lavoro.
⬤ Potrebbe non essere adatto ai principianti assoluti a causa degli argomenti avanzati trattati.
⬤ Sono stati riscontrati potenziali problemi per quanto riguarda la disponibilità alla produzione e gli utenti sono stati avvertiti di non utilizzarlo in progetti reali.

(basato su 11 recensioni dei lettori)

Titolo originale:

Type-Driven Development with Idris

Contenuto del libro:

Sintesi

Type-Driven Development with Idris, scritto dal creatore di Idris, insegna come migliorare le prestazioni e l'accuratezza dei programmi sfruttando un sistema di tipi all'avanguardia. Questo libro vi insegna a utilizzare Idris, un linguaggio progettato per supportare lo sviluppo guidato dai tipi.

L'acquisto del libro stampato include un eBook gratuito nei formati PDF, Kindle e ePub di Manning Publications.

Informazioni sulla tecnologia

Smettere di lottare contro gli errori di tipo Lo sviluppo orientato ai tipi è un approccio alla codifica che considera i tipi come le fondamenta del codice, essenzialmente come documentazione incorporata che il compilatore può utilizzare per verificare le relazioni tra i dati e altre ipotesi. Con questo approccio è possibile definire le specifiche fin dalle prime fasi dello sviluppo e scrivere codice facile da mantenere, testare ed estendere. Idris è un linguaggio simile a Haskell con tipi dipendenti di prima classe, perfetto per imparare le tecniche di programmazione orientata ai tipi che si possono applicare a qualsiasi base di codice.

Informazioni sul libro

Type-Driven Development with Idris insegna come migliorare le prestazioni e l'accuratezza del codice sfruttando un sistema di tipi all'avanguardia. In questo libro imparerete lo sviluppo guidato dai tipi di un software reale e come gestire gli effetti collaterali, l'interazione, lo stato e la concorrenza. Alla fine, sarete in grado di sviluppare software robusto e verificato in Idris e di applicare i metodi di sviluppo guidato dai tipi ad altri linguaggi.

Cosa contiene

⬤ Comprendere i tipi dipendenti.

⬤ I tipi come costrutti linguistici di prima classe.

⬤ I tipi come guida alla costruzione dei programmi.

⬤ Esprimere le relazioni tra i dati.

Informazioni sul lettore

Scritto per programmatori con conoscenza dei concetti di programmazione funzionale.

Informazioni sull'autore

Edwin Brady guida la progettazione e l'implementazione del linguaggio Idris.

Indice dei contenuti

PARTE 1 - INTRODUZIONE.

⬤ Panoramica.

⬤ Iniziare con IdrisParte 2 - CORE IDRIS.

⬤ Sviluppo interattivo con i tipi.

⬤ I tipi di dati definiti dall'utente.

⬤ Programmi interattivi: elaborazione di input e output.

⬤ Programmazione con tipi di prima classe.

⬤ Interfacce: utilizzo di tipi generici vincolati.

⬤ Uguaglianza: esprimere relazioni tra i dati.

⬤ Predicati: esprimere ipotesi e contratti nei tipi.

⬤ Visioni: estendere la corrispondenza dei modelli.

PARTE 3 - IDRIS E IL MONDO REALE.

⬤ Streams e processi: lavorare con dati infiniti.

⬤ Scrivere programmi con lo stato.

⬤ Macchine a stati: verifica dei protocolli nei tipi.

⬤ Macchine a stati dipendenti: gestione di feedback ed errori.

⬤ Programmazione concorrente sicura per i tipi.