Rodzaj (teoria typów)

Rodzaj – w teorii typów, schemat konstruktora typu. System rodzajów jest najczęściej rachunkiem lambda z typami prostymi, wyposażonym w typ pierwotny, oznaczony jako $*$ i nazywany „typem”, który jest rodzajem dowolnego typu danych, który nie wymaga parametryzacji.

Ponieważ operatory typów wyższego rzędu są rzadko spotykane w językach programowania, w większości praktyk programistycznych rodzaje są używane do rozróżnienia typów danych od konstruktorów typów używanych do implementacji polimorfizmu parametrycznego. Rodzaje pojawiają się, jawnie lub niejawnie, w językach, których systemy typów oferują programiście swobodny dostęp do polimorfizmu parametrycznego, przykładowo jak C++, Haskellu i Scali.

Przykłady

• $*$, wymawiane jako „typ”, jest rodzajem wszystkich typów danych. Przykładami typów rodzaju $*$ są całkowitoliczbowe typy danych, logiczne typy danych, a w funkcyjnych językach programowania typy monomorficznych funkcji.
• $*\to *$ jest rodzajem jednoargumentowego konstruktora typu, przykładem czego może być lista.
• $*\to *\to *$ jest rodzajem konstruktora typu o dwóch parametrach (przekazywanych poprzez currying), przykładowo pary lub typu funkcji (nie mylić z wynikiem jego aplikacji, który jest „gotowym” typem funkcji, a więc rodzaju $*$ ).
• $(*\to *)\to *$ jest rodzajem unarnego operatora wyższego rzędu parametryzowanego jednoargumentowymi konstruktorami typów. Przykładem takiego operatora może być tablica mieszająca mapująca liczby na liczby parametryzowana typem kontenera („bucket”) użytego do rozwiązywania kolizji.

Rodzaje w Haskellu

(Uwaga : dokumentacja Haskella używa tej samej strzałki zarówno dla typów, jak i rodzajów funkcji.)

System rodzajów Haskella 98 obejmuje dokładnie dwa rodzaje:

• $*$, wymawiane "typ" to rodzaj wszystkich typów danych.
• $k_1\to k_2$ jest rodzajem konstruktora typu, który przyjmuje typ rodzaju $k_1$ i produkuje rodzaj rodzaju $k_2$.

Konstruktor typu przyjmuje jeden lub więcej argumentów by stworzyć końcowy typ danych. W ten sposób Haskell realizuje typy parametryczne. Przykładowo [] (lista) jest takim konstruktorem typu — by stać się pełnoprawnym typem potrzebuje jednego argumentu określającego typ elementów listy. Z tego powodu [Int] (lista liczb całkowitych), [Float] (lista liczb zmiennoprzecinkowych), a nawet [ [ Int ] ] (lista list liczb całkowitych) są prawidłowymi aplikacjami konstruktora typu []. Stąd można wywnioskować, że [] jest typem rodzaju $*\to *$. Ponieważ Int ma rodzaj $*$, aplikacja [] do niego daje [Int], rodzaju $*$.

Rekonstrukcja rodzajów

Standardowy Haskell nie dopuszcza rodzajów polimorficznych, mimo pełnego wsparcia typów polimorficznych. Stąd w poniższym przykładzie:

data Tree z = Leaf | Fork (Tree z) (Tree z)

teoretycznie rodzaj parametru z może być dowolny, jednakże Haskell domyślnie zakłada, że parametry konstruktorów danych są opisywane przez typ rodzaju

$*$

, chyba że deklaracja wprost wskazuje inaczej (patrz poniżej). Z tego powodu kompilator odrzuci następujące użycie Tree :

type FunnyTree = Tree []     -- błąd

Konkretnie rzecz ujmując, rodzaj [], czyli

$*\to *$

, nie pasuje do domyślnego rodzaju z, czyli

$*$

. Operatory wyższych rzędów są w pełni akceptowane, jeśli tylko spełniają założenia kontroli rodzajów. Przykładowo:

data App unt z = Z (unt z)

ma rodzaj

$(*\to *)\to *\to *$

. To znaczy, że unt jest jednoargumentowym konstruktorem typu, którego parametr jest zwykłym typem (

$*$

). Warto nadmienić, że GHC oferuje rozszerzenie PolyKinds, które wraz z KindSignatures wprowadza rodzaje polimorficzne. Na przykład, następujący kod przechodzi kontrolę typów i rodzajów:

data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree []     --  OK

Od wersji GHC 8.0.1 typy i rodzaje traktowane jak równoprawne koncepty.

Zobacz też

• System F