Digitare la parola chiave nelle dichiarazioni di classe e istanza

Question

Guardavo attraverso il codice sorgente di Data.Has e cercando di capire come funziona. Credo che il seguente codice sia destinato a consentire a qualcuno di "Unire" due valori, ad esempio a :: A e b :: B in un nuovo valore che abbia la funzionalità di entrambi a e b.

In particolare non capisco cosa significhi type all'interno della classe e delle dichiarazioni di istanza.

Inoltre, non conosco il significato del simbolo ~ di seguito.

Qualcuno potrebbe spiegare il codice seguente da Data.Has.TypeList funziona?

-- | Provides type-list functionality 

module Data.Has.TypeList where 

import Control.Applicative 
import Data.Monoid (Monoid (..)) 
import Test.QuickCheck (Arbitrary (..), CoArbitrary (..)) 
import Data.Typeable 
import Data.Data 
-- | Cons a type onto type-list. 
data a ::: b = a ::: b deriving (Show,Eq,Ord,Read,Bounded,Typeable,Data) 

-- | The empty type-list. 
data TyNil = TyNil deriving (Read,Typeable,Data) 

-- | Appends a type-list and another. 
class Append a b where 
    type a :++: b 
    (.++.) :: a -> b -> a :++: b 
infixr 5 :++: 

-- Implementation of Append 

instance Append TyNil b where 
    type TyNil :++: b = b 
    _ .++. b = b 

instance (Append y b) => Append (x ::: y) b where 
    type (x ::: y) :++: b = x ::: (y :++: b) 
    ~(x ::: y) .++. b = x ::: (y .++. b) 

Answer 1

type sintassi all'interno dichiarazioni typeclass ed istanza è parte di TypeFamilies estensione. Le famiglie di tipi possono essere pensate come funzioni da tipi a tipi. C'è una grande spiegazione dettagliata delle famiglie di tipi e di dati nel wiki Haskell (vedi il link).

Applicate alle classi di tipi, le famiglie di tipi diventano tipi associati. A questo proposito sono molto vicini a FunctionalDependencies, cioè consentono una risoluzione dell'istanza non ambigua. La necessità di questo è ampiamente spiegata in the GHC manual.

Le definizioni di tipo nell'esempio sono molto semplici. ::: è un altro nome per 2-tupla (una coppia di valori) e TyNil è isomorfo al tipo di unità ().

Proverò a leggere la dichiarazione di classe e istanza in modo che sia chiaro cosa significano.

class Append a b where 
    type a :++: b 
    (.++.) :: a -> b -> a :++: b 
infixr 5 :++: 

dichiarare multiparametrica typeclass Append a b un tipo associato a :++: b e funzione un metodo (.++.) che assume valori di tipo a e b e produce un valore di tipo a :++: b. Abbiamo inoltre stabilito (.++.) essere destra-associativo con priorità 5.

instance Append TyNil b where 
    type TyNil :++: b = b 
    _ .++. b = b 

dichiarare un'istanza di Append a b con il primo parametro fisso (TyNil) e secondo parametro arbitrario (b), dove tipo a :++: b associata (in questo caso è TyNil :++: b) è dichiarato uguale a b. (Non descriverò quale metodo, è abbastanza chiaro).

instance (Append y b) => Append (x ::: y) b where 
    type (x ::: y) :++: b = x ::: (y :++: b) 
    ~(x ::: y) .++. b = x ::: (y .++. b) 

dichiarare un'istanza di Append a b con primo parametro nella forma x ::: y per arbitraria x e y e arbitraria secondo parametro b dato che v'è già un esempio di Append y b dichiarato. Il tipo associato a :++: b (qui (x ::: y) :++: b, ovviamente) è dichiarato uguale a x ::: (y :++: b).La definizione del metodo è chiara qui: prende una coppia di valori e un altro valore e costruisce un'altra coppia dove il primo elemento è lo stesso del primo argomento e il secondo elemento è il secondo elemento dal primo argomento combinato con il secondo argomento con il metodo .++.. Siamo autorizzati ad utilizzare .++. a causa di Append y b vincolo

Questi sono di tipo firme di (.++.) metodo nelle dichiarazioni di dichiarazione e un'istanza di classe:

(.++.) ::    a  -> b -> a :++: b 
(.++.) ::    TyNil -> b -> b 
(.++.) :: Append y b => x ::: y -> b -> x ::: (y :++: b) 

Si noti che in ogni caso molto astratto a :++: b trasforma al tipo più concreto . È semplice b nel primo caso e più complesso x ::: (y :++: b), a sua volta scritto in termini di :++:. è necessario

Detta decisione di tipo associato per indicare al sistema tipo che v'è un certo tipo (a :++: b in questo caso) che è determinato unicamente da a e b solo. Cioè, se coontrollore dei tipo sa che in certa espressione a e b tipi sono uguali, per esempio, Int e Double, e:

1. esiste un vincolo Append a b;
2. c'è un'istanza di tipo di classe Append Int Double con il tipo associato dichiarato, per esempio, come type Int :++: Double = String,

poi coontrollore dei tipo sapranno che se incontrano tipo a :++: b si sa che in realtà questo tipo è String.

Come per ~, si chiama "Lazy pattern match". È spiegato molto chiaramente here.

Non esitate a chiedere se qualcosa non è ancora chiaro.