Typy jako obywatel pierwszej klasy

Pochodząc z języka C ++ nie rozumiem, dlaczego jako obywatel pierwszej klasy potrzebne są typy / wyrażenia typu? Jedynym znanym mi językiem obsługującym tę funkcję jest Aldor.

Czy ktoś ma literaturę na temat typów jako obywatel pierwszej klasy lub wie, dlaczego jest to przydatne?

Typy pierwszej klasy umożliwiają coś, co nazywa się pisaniem zależnym . Umożliwiają one programiście stosowanie wartości typów na poziomie typu. Na przykład typ wszystkich par liczb całkowitych jest typem regularnym, a para wszystkich liczb całkowitych z lewą liczbą mniejszą niż prawa liczba jest typem zależnym. Standardowym przykładem tego są listy zakodowane długością (zwykle nazywane Vectorw Haskell / Idris). Poniższy pseudo-kod jest mieszanką Idris i Haskell.

-- a natural number
data Nat = Zero | Successor Nat

data Vector length typ where
  Empty : Vector Zero typ
  (::)   : typ -> Vector length typ -> Vector (Successor length) typ

Ten fragment kodu mówi nam dwie rzeczy:

• Pusta lista ma długość zero.
• consumieszczenie elementu na liście tworzy listę długości n + 1

Wygląda to bardzo podobnie do innej koncepcji z 0 i n + 1prawda? Wrócę do tego.

Co z tego zyskujemy? Możemy teraz określić dodatkowe właściwości używanych funkcji. Na przykład: Ważną właściwością appendjest to, że długość wynikowej listy jest sumą długości dwóch list argumentów:

plus : Nat -> Nat -> Nat
plus          Zero n = n
plus (Successor m) n = Successor (plus m n)

append : Vector n a -> Vector m a -> Vector (plus n m) a
append Empty  ys = ys
append (x::xs) ys = x :: append xs ys

Ale w sumie ta technika nie wydaje się przydatna w codziennym programowaniu. Jak to się ma do gniazd, POST/GET żądań i tak dalej?

Cóż, nie robi tego (przynajmniej nie bez znacznego wysiłku). Ale może nam pomóc na inne sposoby:

Zależne typy pozwalają nam formułować niezmienniki w regułach kodu, tak jak funkcja musi się zachowywać. Korzystając z nich, zyskujemy dodatkowe bezpieczeństwo dotyczące zachowania kodu, podobne do warunków wstępnych i końcowych Eiffela. Jest to niezwykle przydatne do automatycznego potwierdzania twierdzeń, co jest jednym z możliwych zastosowań Idris.

Wracając do powyższego przykładu, definicja list zakodowanych długością przypomina matematyczną koncepcję indukcji . W Idris możesz sformułować pojęcie indukcji na takiej liście w następujący sposób:

              -- If you can supply the following:
list_induction : (Property : Vector len typ -> Type) -> -- a property to show
                  (Property Empty) -> -- the base case
                  ((w : a) -> (v : Vector n a) ->
                      Property v -> Property (w :: v)) -> -- the inductive step
                  (u : Vector m b) -> -- an arbitrary vector
                  Property u -- the property holds for all vectors

Ta technika ogranicza się do konstruktywnych dowodów, ale mimo to jest bardzo potężna. Możesz spróbować pisaćappend indukcyjnie jako ćwiczenie.

Oczywiście typy zależne są tylko jednym zastosowaniem typów pierwszej klasy, ale prawdopodobnie jest to jeden z najczęstszych. Dodatkowe zastosowania obejmują na przykład zwracanie określonego typu z funkcji na podstawie jej argumentów.

type_func : Vector n a -> Type
type_func Empty = Nat
type_func v     = Vector (Successor Zero) Nat

f : (v : Vector n a) -> type_func v
f Empty = 0
f vs    = length vs :: Empty

Jest to nonsensowny przykład, ale pokazuje coś, czego nie można naśladować bez typów pierwszej klasy.