Typově řízený vývoj s Idrisem

Recenze čtenářů

Kniha o Idrisu nabízí poutavý úvod do typově řízeného vývoje a programovacího jazyka Idris. Čtenáři ji považují za užitečnou pro pochopení pokročilých typových systémů a oceňují její srozumitelné vysvětlení. Někteří uživatelé však mají potíže s dokumentací a instalací, což může ztěžovat učení.

⬤ Poutavý a podnětný obsah, který mění pohled na programování a typové systémy.
⬤ Dobře napsaný výukový program, který je přínosný pro výuku Idrisu a typově orientovaného vývoje.
⬤ Autor je tvůrcem Idrisu, takže poskytuje pohled zevnitř.
⬤ Zdůrazňuje význam silného typování a bezpečnosti v programování.
⬤ Srozumitelná prezentace složitých konceptů dostupná i čtenářům se zkušenostmi s funkcionálním programováním.

⬤ Chybí ucelený průvodce instalací a dokumentace, což vede k potížím pro nové uživatele.
⬤ Pro některé čtenáře je jazyk neobvyklý a může je odradit omezená poptávka na trhu práce.
⬤ Vzhledem k probíraným pokročilým tématům nemusí být vhodný pro úplné začátečníky.
⬤ Byly zaznamenány potenciální problémy týkající se jeho připravenosti k výrobě, přičemž uživatelé jsou varováni před jeho používáním v živých projektech.

(na základě 11 hodnocení čtenářů)

Původní název:

Type-Driven Development with Idris

Obsah knihy:

Shrnutí

Kniha Type-Driven Development with Idris, jejímž autorem je tvůrce Idrisu, vás naučí, jak zlepšit výkon a přesnost vašich programů využitím nejmodernějšího typového systému. Tato kniha vás naučí s Idrisem, jazykem navrženým pro podporu typově řízeného vývoje.

Zakoupení tištěné knihy zahrnuje bezplatnou elektronickou knihu ve formátech PDF, Kindle a ePub od Manning Publications.

O technologii

Přestaňte bojovat s typovými chybami Typově řízený vývoj je přístup ke kódování, který zahrnuje typy jako základ vašeho kódu - v podstatě jako vestavěnou dokumentaci, kterou může překladač použít ke kontrole datových vztahů a dalších předpokladů. Díky tomuto přístupu můžete definovat specifikace již na počátku vývoje a psát kód, který se snadno udržuje, testuje a rozšiřuje. Idris je jazyk podobný Haskellu s prvotřídními závislými typy, který je ideální pro učení se technikám typově řízeného programování, které můžete použít v jakékoli kódové základně.

O knize

Vývoj řízený typy s Idrisem vás naučí, jak zlepšit výkon a přesnost kódu využitím nejmodernějšího typového systému. V této knize se naučíte typově řízený vývoj reálného softwaru a také to, jak zacházet s vedlejšími efekty, interakcí, stavem a souběžností. Na konci budete schopni vyvíjet robustní a ověřený software v Idrisu a aplikovat metody typově řízeného vývoje i na jiné jazyky.

Co je uvnitř

⬤ Pochopení závislých typů.

⬤ Typy jako jazykové konstrukce první třídy.

⬤ Typy jako průvodce konstrukcí programu.

⬤ Vyjádření vztahů mezi daty.

O čtenáři

Napsáno pro programátory se znalostí konceptů funkcionálního programování.

O autorovi

Edwin Brady vede návrh a implementaci jazyka Idris.

Obsah

ČÁST 1 - ÚVOD.

⬤ Přehled.

⬤ Začínáme s IdrisemČÁST 2 - JÁDRO IDRIS.

⬤ Interaktivní vývoj s typy.

⬤ Uživatelem definované datové typy.

⬤ Interaktivní programy: zpracování vstupů a výstupů.

⬤ Programování s typy první třídy.

⬤ Interface: použití omezených generických typů.

⬤ Rovnost: vyjadřování vztahů mezi daty.

⬤ Predikáty: vyjadřování předpokladů a smluv v typech.

⬤ Výhledy: rozšíření porovnávání vzorů.

ČÁST 3 - IDRIS A REÁLNÝ SVĚT.

⬤ Proudy a procesy: práce s nekonečnými daty.

⬤ Psaní programů se stavem.

⬤ Stavové stroje: ověřování protokolů v typech.

⬤ Závislé stavové stroje: zpracování zpětné vazby a chyb.

⬤ Typově bezpečné souběžné programování.