Promocja danych dla uzależnionych od wyzwań

Question

Po zapoznaniu się z ghc 7.4. przedpremierowe notatki i dokument Giving Haskell a Promotion, nadal jestem zdezorientowany, co faktycznie robisz z promowanymi typami. Na przykład podręcznik GHC podaje następujące przykłady na promowanych typach danych:

data Nat = Ze | Su Nat 

data List a = Nil | Cons a (List a) 

data Pair a b = Pair a b 

data Sum a b = L a | R b 

Jakie rodzaje zastosowań mają te rodzaje? Czy możesz podać (kod) przykłady?

Answer 1

Nat może być np. służy do konstruowania wektorów liczbowych, które można dodać tylko, jeśli mają tę samą długość, sprawdzone pod czasu kompilacji.

Answer 2

Istnieją co najmniej dwa przykłady w samym papierze:

„1. Wstęp”, mówi: „Na przykład, możemy być w stanie zapewnić, [w czasie kompilacji], że przypuszczalny drzewo czerwono-czarne naprawdę ma czerwono-czarna własność ".

"2.1 Promowanie typów danych" omawia wektory o indeksie długości (tzn. Wektory z błędem "indeks poza granicami" w czasie kompilacji).

Można również przyjrzeć się wcześniejszej pracy w tym kierunku, np. Biblioteka HList dla bezpiecznych typów list heterogenicznych i zbiorów rozszerzalnych. Oleg Kiselyov ma wiele powiązanych prac. Możesz także czytać prace dotyczące programowania z rodzajami zależnymi. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf ma wstępne przykłady obliczeń na poziomie typu w Agdzie, ale można je również zastosować do Haskella.

Z grubsza chodzi o to, że w przypadku list podano bardziej precyzyjny typ. Zamiast

head :: List a -> a 

to

head :: NotEmptyList a -> a 

Ta ostatnia funkcja głowa jest bardziej typesafe niż fomer: nigdy nie mogą być stosowane do pustych list, ponieważ spowodowałoby to błędy kompilatora.

Do wyrażania typów takich jak NotEmptyList potrzebne są obliczenia na typie. Klasy typów z zależnościami funkcjonalnymi, rodziny GAGT i (indeksowane) już zapewniają słabe formy obliczeń na poziomie typu dla haskell. Praca, o której wspomniałeś, rozwija się dalej w tym kierunku.

Zobacz implementację przy użyciu tylko klas typu Haskell98, patrz http://www.haskell.org/haskellwiki/Non-empty_list.