Programowanie oparte na typach z Idris

Opinie czytelników

Książka o Idris oferuje wciągające wprowadzenie do programowania opartego na typach i języka programowania Idris. Czytelnicy uważają ją za pomocną w zrozumieniu zaawansowanych systemów typów i doceniają jej jasne wyjaśnienia. Jednak niektórzy użytkownicy zmagają się z dokumentacją i instalacją, co może utrudniać naukę.

⬤ Angażująca i prowokująca do myślenia treść, która zmienia perspektywę programowania i systemów typów.
⬤ Dobrze napisany samouczek, który jest korzystny dla nauki Idris i programowania opartego na typach.
⬤ Autor jest twórcą Idrisa, co zapewnia wewnętrzną perspektywę.
⬤ Podkreśla znaczenie silnego typowania i bezpieczeństwa w programowaniu.
⬤ Przejrzysta prezentacja złożonych koncepcji dostępna dla czytelników z doświadczeniem w programowaniu funkcjonalnym.

⬤ Brak kompleksowego przewodnika instalacji i dokumentacji, co prowadzi do trudności dla nowych użytkowników.
⬤ Niektórzy czytelnicy uznają ten język za nietypowy i mogą być zniechęceni ograniczonym popytem na rynku pracy.
⬤ Może nie być odpowiednia dla zupełnie początkujących ze względu na poruszane zaawansowane tematy.
⬤ Potencjalne problemy związane z gotowością produkcyjną, a użytkownicy ostrzegają przed używaniem go w projektach na żywo.

(na podstawie 11 opinii czytelników)

Oryginalny tytuł:

Type-Driven Development with Idris

Zawartość książki:

Streszczenie

Type-Driven Development with Idris, napisana przez twórcę Idris, uczy, jak poprawić wydajność i dokładność programów, korzystając z najnowocześniejszego systemu typów. Ta książka uczy za pomocą Idris, języka zaprojektowanego do wspierania programowania opartego na typach.

Zakup książki drukowanej obejmuje bezpłatny eBook w formatach PDF, Kindle i ePub od Manning Publications.

O technologii

Przestań walczyć z błędami typu Programowanie oparte na typach to podejście do kodowania, które obejmuje typy jako podstawę kodu - zasadniczo jako wbudowaną dokumentację, której kompilator może użyć do sprawdzenia relacji danych i innych założeń. Dzięki takiemu podejściu można definiować specyfikacje na wczesnym etapie rozwoju i pisać kod, który jest łatwy w utrzymaniu, testowaniu i rozszerzaniu. Idris jest językiem podobnym do Haskella z pierwszorzędnymi, zależnymi typami, który jest idealny do nauki technik programowania opartych na typach, które można zastosować w dowolnej bazie kodu.

O książce

Type-Driven Development with Idris uczy, jak poprawić wydajność i dokładność kodu, korzystając z najnowocześniejszego systemu typów. W tej książce dowiesz się, jak tworzyć oprogramowanie oparte na typach, a także jak radzić sobie z efektami ubocznymi, interakcjami, stanem i współbieżnością. Pod koniec będziesz w stanie tworzyć solidne i zweryfikowane oprogramowanie w Idris i stosować metody programowania oparte na typach w innych językach.

What's Inside

⬤ Zrozumienie typów zależnych.

⬤ Typy jako pierwszorzędne konstrukcje językowe.

⬤ Typy jako przewodnik po budowie programu.

⬤ Wyrażanie relacji między danymi.

O czytelniku

Napisana dla programistów znających koncepcje programowania funkcyjnego.

O autorze

Edwin Brady kieruje projektowaniem i implementacją języka Idris.

Spis treści

CZĘŚĆ 1 - WPROWADZENIE.

⬤ Przegląd.

⬤ Rozpoczęcie pracy z IdrisCzęść 2 - CORE IDRIS.

⬤ Interaktywny rozwój z typami.

⬤ Typy danych zdefiniowane przez użytkownika.

⬤ Programy interaktywne: przetwarzanie danych wejściowych i wyjściowych.

⬤ Programowanie z użyciem typów pierwszej klasy.

⬤ Interfejsy: korzystanie z ograniczonych typów ogólnych.

⬤ Równość: wyrażanie relacji między danymi.

⬤ Predykaty: wyrażanie założeń i kontraktów w typach.

⬤ Views: rozszerzanie dopasowywania wzorców.

CZĘŚĆ 3 - IDRIS I ŚWIAT RZECZYWISTY.

⬤ Strumienie i procesy: praca z nieskończonymi danymi.

⬤ Pisanie programów ze stanem.

⬤ Maszyny stanów: weryfikacja protokołów w typach.

⬤ Zależne maszyny stanów: obsługa informacji zwrotnych i błędów.

⬤ Programowanie współbieżne bezpieczne dla typów.