Enter a keyword in the class and instance declarations

Question

I was looking at the source code of Data.Has and trying to figure out how it works. I believe the following code is intended to allow someone to “join” two values, for example a :: A and b :: B , into a new value that has the functionality of both a and b .

I especially don't understand what type means inside class and instance declarations.

Also I do not know what the symbol ~ means.

Can someone explain the code below from Data.Has.TypeList working?

 -- | 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 ab 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 yb) => Append (x ::: y) b where type (x ::: y) :++: b = x ::: (y :++: b) ~(x ::: y) .++. b = x ::: (y .++. b) 

Answer 1

type syntax inside typeclass and instance declaration is part of the TypeFamilies extension. Type types can be considered as functions from types to types. The Haskell wiki has a detailed, detailed description of type and data families (see Link).

For class types, family types become related types. In this regard, they are very close to FunctionalDependencies , that is, they allow unambiguous resolution of the instance. The need for this is explained in detail in the GHC manual .

The type definitions in your example are very simple. ::: is another name for 2-tuples (a pair of values), and TyNil is isomorphic to the unit type () .

I will try to read the declaration of the class and instance so that it is clear what they mean.

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

Declare a multi-parameter typeclass Append ab with the associated type a :++: b and one method function (.++.) That takes values ​​of types a and b and gives a value of type a :++: b . We also set (.++.) As right-associative with priority 5.

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

Declare an instance of Append ab with a fixed first parameter ( TyNil ) and an arbitrary second parameter ( b ), where the declared type is a :++: b (in this case, TyNil :++: b ) is declared equal to b . (I will not describe what method to do, this is pretty clear).

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

Declare an instance of Append ab with the first parameter of the form x ::: y for arbitrary x and y and an arbitrary second parameter b if an already declared instance of Append yb . The associated type a :++: b (here (x ::: y) :++: b , obviously) is declared equal to x ::: (y :++: b) . The method definition is also clear here: it takes a pair of values ​​and another value and creates another pair, where the first element is the same as in the first argument, and the second element is the second element from the first argument combined with the second argument, c .++. method. We are allowed to use .++. due to Append yb limitation

These are the method type signatures (.++.) In the class declaration and instance declaration:

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

Note that in each case, the very abstract a :++: b converted to a more specific type. This is a simple b in the first case and a more complex x ::: (y :++: b) , itself written in terms of :++:

Such a declaration of a related type is necessary in order to tell the type system that in this case there is some type ( a :++: b ) that is uniquely determined only by a and b . That is, if typechecker knows that in certain expressions a and b types are equal, say, Int and Double , and:

• There is a limitation to Append ab
• there is an instance of the Append Int Double class with an associated type declared, for example, as type Int :++: Double = String ,

then typechecker will know that if it encounters type a :++: b , it will know that this type is actually String .

As for ~ , it's called a "Lazy pattern match". This is very clearly explained here .

Feel free to ask, something else is unclear.