Dezvoltare orientată pe tip cu Idris

Recenzii ale cititorilor

Cartea despre Idris oferă o introducere captivantă în dezvoltarea bazată pe tipuri și în limbajul de programare Idris. Cititorii o consideră utilă pentru înțelegerea sistemelor de tip avansate și apreciază explicațiile sale clare. Cu toate acestea, unii utilizatori se luptă cu documentația și instalarea, ceea ce poate îngreuna experiența de învățare.

⬤ Conținut captivant și provocator care schimbă perspectivele asupra programării și sistemelor de tipuri.
⬤ Tutorial bine scris care este benefic pentru învățarea Idris și a dezvoltării bazate pe tipuri.
⬤ Autorul este creatorul Idris, oferind o perspectivă din interior.
⬤ Subliniază importanța tipării puternice și a securității în programare.
⬤ Prezentarea clară a conceptelor complexe disponibile cititorilor cu experiență în programarea funcțională.

⬤ Lipsa unui ghid de instalare și a unei documentații cuprinzătoare, ceea ce conduce la dificultăți pentru noii utilizatori.
⬤ Unii cititori consideră limbajul puțin obișnuit și pot fi descurajați de cererea limitată pe piața muncii.
⬤ Poate să nu fie potrivit pentru începătorii compleți din cauza subiectelor avansate abordate.
⬤ Probleme potențiale observate în ceea ce privește disponibilitatea sa pentru producție, utilizatorii fiind avertizați cu privire la utilizarea sa în proiecte reale.

(pe baza a 11 recenzii ale cititorilor)

Titlul original:

Type-Driven Development with Idris

Conținutul cărții:

Rezumat

Type-Driven Development with Idris, scrisă de creatorul Idris, vă învață cum să îmbunătățiți performanța și acuratețea programelor dvs. profitând de un sistem de tipuri de ultimă generație. Această carte vă învață cu Idris, un limbaj conceput pentru a susține dezvoltarea orientată pe tipuri.

Achiziționarea cărții tipărite include o carte electronică gratuită în format PDF, Kindle și ePub de la Manning Publications.

Despre tehnologie

Nu vă mai luptați cu erorile de tip Dezvoltarea bazată pe tipuri este o abordare a codării care îmbrățișează tipurile ca fundament al codului dumneavoastră - în esență, ca documentație încorporată pe care compilatorul o poate utiliza pentru a verifica relațiile dintre date și alte ipoteze. Cu această abordare, puteți defini specificațiile la începutul dezvoltării și puteți scrie cod care este ușor de întreținut, testat și extins. Idris este un limbaj de tip Haskell cu tipuri dependente de primă clasă, care este perfect pentru a învăța tehnici de programare bazate pe tipuri pe care le puteți aplica în orice bază de cod.

Despre carte

Type-Driven Development with Idris vă învață cum să îmbunătățiți performanța și acuratețea codului dvs. profitând de un sistem de tipuri de ultimă generație. În această carte, veți învăța dezvoltarea bazată pe tipuri a software-ului din lumea reală, precum și cum să gestionați efectele secundare, interacțiunea, starea și concurența. Până la sfârșit, veți putea dezvolta software robust și verificat în Idris și veți putea aplica metodele de dezvoltare bazate pe tipuri în alte limbaje.

Ce este în interior

⬤ Înțelegerea tipurilor dependente.

⬤ Tipurile ca construcții lingvistice de primă clasă.

⬤ Tipurile ca ghid pentru construcția programelor.

⬤ Exprimarea relațiilor dintre date.

Despre cititor

Scris pentru programatorii care cunosc conceptele de programare funcțională.

Despre autor

Edwin Brady conduce proiectarea și implementarea limbajului Idris.

Tabla de conținut

PARTEA 1 - INTRODUCERE.

⬤ Overview.

⬤ Începerea cu IdrisPART 2 - CORE IDRIS.

⬤ Dezvoltare interactivă cu tipuri.

⬤ Tipuri de date definite de utilizator.

⬤ Programe interactive: procesarea intrărilor și ieșirilor.

⬤ Programarea cu tipuri de primă clasă.

⬤ Interfețe: utilizarea tipurilor generice constrânse.

⬤ Egalitate: exprimarea relațiilor dintre date.

⬤ Predicate: exprimarea ipotezelor ș i a contractelor în tipuri.

⬤ Views: extinderea potrivirii modelelor.

PARTEA 3 - IDRIS ȘI LUMEA REALĂ.

⬤ Streams și procese: lucrul cu date infinite.

⬤ Scrierea de programe cu stare.

⬤ Mașini cu stare: verificarea protocoalelor în tipuri.

⬤ Mașini de stare dependente: gestionarea feedback-ului și a erorilor.

⬤ Programarea concurentă în condiții de siguranță a tipului.