Escriba palabra clave en clase y declaraciones de instancia

Question

Estaba buscando el código fuente Data.Has y tratando de ver cómo funciona. Creo que el siguiente código está destinado a permitir que alguien "Unir" dos valores, digamos a :: A y b :: B en un nuevo valor que tiene la funcionalidad de a y b.

Particularmente no entiendo qué significa type dentro de la clase y las declaraciones de instancia.

Además, no sé qué significa el símbolo ~ a continuación.

¿Podría alguien explicar el siguiente código de Data.Has.TypeList obras?

-- | 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 sintaxis dentro clase de tipos y declaraciones de instancias es una parte de TypeFamilies extensión. Las familias tipo pueden considerarse funciones de tipos a tipos. Hay una gran explicación detallada de las familias de tipos y datos en la wiki de Haskell (ver el enlace).

Aplicado a las clases de tipo, las familias de tipo se convierten en tipos asociados. En este sentido, están muy cerca de FunctionalDependencies, es decir, permiten una resolución de instancia no ambigua. La necesidad de esto está ampliamente explicada in the GHC manual.

Las definiciones de tipo en su ejemplo son muy simples. ::: es otro nombre para 2-tuple (un par de valores), y TyNil es isomorfo a la unidad tipo ().

Intentaré leer la declaración de la clase y la instancia para que quede claro lo que significan.

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

Declare multiparamétrico clase de tipos Append a b con una función de un método (.++.) tipo asociado a :++: b y que toma valores de tipos a y b y produce un valor de tipo a :++: b. También establecemos (.++.) ser asociativo por la derecha con prioridad 5.

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

Declarar una instancia de Append a b con primer parámetro fijo (TyNil) y segundo parámetro arbitrario (b), donde asocia tipo a :++: b (en este caso es TyNil :++: b) se declara igual a b. (No describiré qué método hago, es bastante claro).

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

Declarar una instancia de Append a b con primer parámetro en la forma x ::: y para arbitraria x y y y arbitraria segundo parámetro b dado que ya hay una instancia de Append y b declarado. El tipo asociado a :++: b (aquí (x ::: y) :++: b, obviamente) se declara igual a x ::: (y :++: b).La definición del método también es clara aquí: toma un par de valores y otro valor y construye otro par donde el primer elemento es el mismo que en el primer argumento y el segundo elemento es el segundo elemento del primer argumento combinado con el segundo argumento con el método .++.. Se nos permite utilizar .++. debido Append y b restricción

Estas son las firmas de tipos de (.++.) método de declaración y declaraciones de instancias de clases:

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

Tenga en cuenta que en cada caso muy abstracto a :++: b transforma el tipo más concreto . Es simple b en el primer caso y más complejo x ::: (y :++: b), escrito en términos de :++:. Se necesita

Tal declaración de tipo asociado para indicar al sistema tipo que hay algún tipo (a :++: b en este caso) que es determinado unívocamente por a y b solo. Es decir, si typechecker sabe que en cierta expresión a y b tipos son iguales a, por ejemplo, Int y Double, y:

1. hay una restricción Append a b;
2. hay una instancia de clase de tipo Append Int Double con el tipo asociado declarada, por ejemplo, como type Int :++: Double = String,

entonces el typechecker sabrán que si él cumple con el tipo a :++: b se sabe que en realidad este tipo es String.

En cuanto a ~, se llama 'Lazy pattern match'. Está muy claramente explicado here.

No dude en preguntar si algo no está claro todavía.