Classe tipo - Type class

Questo articolo riguarda i sistemi di tipo polimorfico in informatica. Per la classe matematica dei tipi di ordine di una data cardinalità, vedere il Glossario della teoria degli insiemi § T .
Da non confondere con la classe (programmazione di computer) .

In informatica , una classe di tipi è un costrutto di sistema di tipi che supporta il polimorfismo ad hoc . Ciò si ottiene aggiungendo vincoli alle variabili di tipo nei tipi parametricamente polimorfici . Tale vincolo in genere coinvolge una classe di tipo Te una variabile di tipo a e significa che apuò essere istanziata solo su un tipo i cui membri supportano le operazioni di overload associate a T.

Le classi di tipo sono state implementate per la prima volta nel linguaggio di programmazione Haskell dopo essere state proposte per la prima volta da Philip Wadler e Stephen Blott come un'estensione di "eqtypes" in Standard ML e sono state originariamente concepite come un modo per implementare aritmetica e operatori di uguaglianza sovraccaricati in un modo di principio. In contrasto con gli "eqtypes" di Standard ML, l'overload dell'operatore di uguaglianza attraverso l'uso di classi di tipo in Haskell non richiede modifiche estese del frontend del compilatore o del sistema di tipi sottostante.

Dalla loro creazione, sono state scoperte molte altre applicazioni delle classi di tipo.

Panoramica

Le classi di tipo vengono definite specificando un insieme di nomi di funzioni o costanti, insieme ai rispettivi tipi, che devono esistere per ogni tipo che appartiene alla classe. In Haskell, i tipi possono essere parametrizzati; una classe Eqdi tipi destinata a contenere tipi che ammettono l'uguaglianza sarebbe dichiarata nel modo seguente: 

class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool

dove aè un'istanza della classe di tipo Eqe adefinisce le firme della funzione per 2 funzioni (le funzioni di uguaglianza e disuguaglianza), ciascuna delle quali accetta 2 argomenti di tipo ae restituisce un valore booleano.

La variabile type ahas kind (nota anche come nell'ultima versione di GHC ), il che significa che il tipo di is TypeEq

Eq :: Type -> Constraint

La dichiarazione può essere letta come se affermasse che "il tipo aappartiene alla classe del tipo Eqse ci sono funzioni denominate (==), e (/=), dei tipi appropriati, definite su di essa". Un programmatore potrebbe quindi definire una funzione elem(che determina se un elemento è in una lista) nel seguente modo: 

elem :: Eq a => a -> [a] -> Bool
elem y []     = False
elem y (x:xs) = (x == y) || elem y xs

La funzione elemha il tipo a -> [a] -> Boolcon il contesto Eq a, che vincola i tipi che apossono variare a quelli ache appartengono alla Eqclasse del tipo. ( Nota : Haskell => può essere chiamato un "vincolo di classe".)

Un programmatore può rendere qualsiasi tipo tmembro di una data classe di tipo Cutilizzando una dichiarazione di istanza che definisce le implementazioni di tutti Ci metodi per il tipo particolare t. Ad esempio, se un programmatore definisce un nuovo tipo di dati t, può quindi rendere questo nuovo tipo un'istanza di Eqfornendo una funzione di uguaglianza sui valori di tipo tin qualsiasi modo ritengano opportuno. Una volta fatto ciò, possono utilizzare la funzione elemon [t], cioè elenchi di elementi di tipo t.

Si noti che le classi di tipo sono diverse dalle classi nei linguaggi di programmazione orientati agli oggetti. In particolare, Eqnon è un tipo: non esiste un valore di tipo Eq.

Le classi di tipo sono strettamente correlate al polimorfismo parametrico. Ad esempio, si noti che il tipo di elemcome specificato sopra sarebbe il tipo parametricamente polimorfico a -> [a] -> Boolse non fosse per il vincolo di classe del tipo " Eq a =>".

Polimorfismo di tipo superiore

Non è necessario che una classe di tipo accetti una variabile di tipo di tipo,Type ma può accettarne una di qualsiasi tipo. Queste classi di tipi con tipi più alti sono talvolta chiamate classi di costruttori (i costruttori a cui si fa riferimento sono costruttori di tipi come Maybe, piuttosto che costruttori di dati come Just). Un esempio è la Monadclasse: 

class Monad m where
  return :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

Il fatto che m sia applicato a una variabile di tipo indica che ha kind Type -> Type, cioè prende un tipo e restituisce un tipo, il tipo di Monadè quindi: 

Monad :: (Type -> Type) -> Constraint

Classi di tipo multiparametrico

Le classi di tipo consentono più parametri di tipo e quindi le classi di tipo possono essere viste come relazioni sui tipi. Ad esempio, nella libreria standard GHC , la classe IArrayesprime un'interfaccia array generale immutabile. In questa classe, il vincolo della classe di tipo IArray a eindica che aè un tipo di matrice che contiene elementi di tipo e. (Questa restrizione sul polimorfismo viene utilizzata per implementare tipi di array unboxed , ad esempio.)

Come multimethods , le classi di tipo multiparametro supportano la chiamata di diverse implementazioni di un metodo a seconda dei tipi di più argomenti e in effetti restituiscono i tipi. Le classi di tipo multiparametro non richiedono la ricerca del metodo da chiamare su ogni chiamata in fase di esecuzione; piuttosto, il metodo da chiamare viene prima compilato e archiviato nel dizionario dell'istanza della classe di tipo, proprio come con le classi di tipo a parametro singolo.

Il codice Haskell che utilizza classi di tipo multiparametro non è portabile, poiché questa funzionalità non fa parte dello standard Haskell 98. Le popolari implementazioni Haskell, GHC e Hugs , supportano classi di tipo multiparametrico.

Dipendenze funzionali

In Haskell, le classi di tipo sono state perfezionate per consentire al programmatore di dichiarare dipendenze funzionali tra i parametri di tipo, un concetto ispirato alla teoria dei database relazionali . Cioè, il programmatore può affermare che una data assegnazione di qualche sottoinsieme dei parametri di tipo determina in modo univoco i restanti parametri di tipo. Ad esempio, una monade generale mche porta un parametro di stato di tipo ssoddisfa il vincolo di classe di tipo Monad.State s m. In questo vincolo, c'è una dipendenza funzionale m -> s. Ciò significa che per una data monade mdi tipo class Monad.State, il tipo di stato accessibile da mè determinato in modo univoco. Questo aiuta il compilatore nell'inferenza del tipo , oltre ad aiutare il programmatore nella programmazione orientata al tipo .

Simon Peyton-Jones si è opposto all'introduzione delle dipendenze funzionali in Haskell per motivi di complessità.

Classi di tipi e parametri impliciti

Le classi di tipo e i parametri impliciti sono di natura molto simile, sebbene non proprio la stessa cosa. Una funzione polimorfica con un vincolo di classe di tipo come: 

sum :: Num a => [a] -> a

può essere trattato intuitivamente come una funzione che accetta implicitamente un'istanza di Num: 

sum_ :: Num_ a -> [a] -> a

L'istanza Num_ aè essenzialmente un record che contiene la definizione dell'istanza di Num a. (Questo è infatti il ​​modo in cui le classi di tipo vengono implementate sotto il cofano dal Glasgow Haskell Compiler.)

Tuttavia, c'è una differenza cruciale: i parametri impliciti sono più flessibili : puoi passare diverse istanze di Num Int. Al contrario, le classi di tipo applicano la cosiddetta proprietà di coerenza , che richiede che ci sia solo una scelta univoca di istanza per un dato tipo. La proprietà di coerenza rende le classi di tipo alquanto antimodulari, motivo per cui le istanze orfane (istanze che sono definite in un modulo che non contiene né la classe né il tipo di interesse) sono fortemente sconsigliate. D'altra parte, la coerenza aggiunge un ulteriore livello di sicurezza al linguaggio, fornendo al programmatore la garanzia che due parti disgiunte dello stesso codice condivideranno la stessa istanza.

Ad esempio, un insieme ordinato (di tipo Set a) richiede un ordinamento totale degli elementi (di tipo a) per funzionare. Ciò può essere evidenziato da un vincolo Ord a, che definisce un operatore di confronto sugli elementi. Tuttavia, ci possono essere numerosi modi per imporre un ordine totale. Poiché gli algoritmi degli insiemi sono generalmente intolleranti ai cambiamenti nell'ordinamento una volta che un insieme è stato costruito, passare un'istanza incompatibile di Ord aa funzioni che operano sull'insieme può portare a risultati errati (o arresti anomali). Pertanto, l'applicazione della coerenza Ord ain questo particolare scenario è cruciale.

Le istanze (o "dizionari") nelle classi di tipo Scala sono solo valori ordinari nel linguaggio, piuttosto che un tipo di entità completamente separato. Sebbene queste istanze siano fornite per impostazione predefinita trovando istanze appropriate nell'ambito da utilizzare come parametri effettivi impliciti per parametri formali impliciti dichiarati in modo esplicito, il fatto che siano valori ordinari significa che possono essere forniti in modo esplicito, per risolvere l'ambiguità. Di conseguenza, le classi di tipo Scala non soddisfano la proprietà di coerenza e sono effettivamente uno zucchero sintattico per i parametri impliciti.

Questo è un esempio tratto dalla documentazione di Cats: 

// A type class to provide textual representation
trait Show[A] {
  def show(f: A): String
}

// A polymorphic function that works only when there is an implicit 
// instance of Show[A] available
def log[A](a: A)(implicit s: Show[A]) = println(s.show(a))

// An instance for String
implicit val stringShow = new Show[String] {
  def show(s: String) = s
}

// The parameter stringShow was inserted by the compiler.
scala> log("a string")
a string

Coq (versione 8.2 in poi) supporta anche le classi di tipo deducendo le istanze appropriate. Le versioni recenti di Agda 2 forniscono anche una funzionalità simile, chiamata "argomenti di istanza".

Altri approcci al sovraccarico dell'operatore

In Standard ML , il meccanismo dei "tipi di uguaglianza" corrisponde approssimativamente alla classe di tipo incorporata di Haskell Eq, ma tutti gli operatori di uguaglianza sono derivati ​​automaticamente dal compilatore. Il controllo del processo da parte del programmatore è limitato alla designazione di quali componenti di tipo in una struttura sono tipi di uguaglianza e quali variabili di tipo in un intervallo di tipi polimorfici rispetto ai tipi di uguaglianza.

I moduli ei funtori di SML e OCaml possono svolgere un ruolo simile a quello delle classi di tipo di Haskell, la differenza principale è il ruolo dell'inferenza di tipo, che rende le classi di tipo adatte per polimorfismi ad hoc . Il sottoinsieme orientato agli oggetti di OCaml è ancora un altro approccio che è in qualche modo paragonabile a quello delle classi di tipo.

Nozioni correlate

Una nozione analoga per i dati sovraccaricati (implementata in GHC ) è quella di famiglia di tipi .

In C++ in particolare C++20 ha il supporto per le classi di tipo che utilizzano Concepts (C++) . A titolo illustrativo, l'esempio Haskell sopra menzionato di typeclass Eq verrebbe scritto come 

template <typename T>
concept Equal =
      requires (T a, T b) {
            { a == b } -> std::convertible_to<bool>;
            { a != b } -> std::convertible_to<bool>;
};

In Clean le classi di tipo sono simili a Haskell, ma hanno una sintassi leggermente diversa.

Rust supporta i tratti , che sono una forma limitata di classi di tipo con coerenza.

Mercurio ha classi tipo, anche se non sono esattamente le stesse di Haskell.

In Scala , le classi di tipo sono un idioma di programmazione che può essere implementato con le funzionalità del linguaggio esistenti come i parametri impliciti, non una funzionalità del linguaggio separata di per sé. A causa del modo in cui sono implementati in Scala, è possibile specificare esplicitamente quale istanza di classe di tipo utilizzare per un tipo in un punto particolare nel codice, in caso di ambiguità. Tuttavia, questo non è necessariamente un vantaggio in quanto le istanze di classi di tipo ambiguo possono essere soggette a errori.

L'assistente di prova Coq ha anche supportato le classi di tipo nelle versioni recenti. A differenza dei normali linguaggi di programmazione, in Coq, qualsiasi legge di una classe di tipo (come le leggi della monade) che sono dichiarate all'interno della definizione della classe di tipo, deve essere dimostrata matematicamente di ogni istanza di classe di tipo prima di usarle.

Guarda anche

Riferimenti

link esterno