Type keyword in class and instance declarations

Question

I was looking through 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, say a :: A and b :: B into a new value that has the functionality of both a and b.

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

Also I don't know what the ~ symbol means below.

Could someone explain the below code from Data.Has.TypeList works?

-- | 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 syntax inside typeclass and instance declarations is a part of TypeFamilies extension. Type families can be thought as functions from types to types. There is a great detailed explanation of type and data families in the Haskell wiki (see the link).

Applied to type classes, type families become associated types. In this regard they are very close to FunctionalDependencies, that is, they allow unambigous instance resolution. The need for this is amply explained in the GHC manual.

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

I'll try to read class and instance declaration so it will be clear what they mean.

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

Declare multiparameter typeclass Append a b with an associated type a :++: b and one method function (.++.) which takes values of types a and b and yields a value of type a :++: b. We also set (.++.) to be right-associative with priority 5.

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

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

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

Declare an instance of Append a b with first parameter in the form x ::: y for arbitrary x and y and arbitrary second parameter b given that there is already an instance of Append y b declared. Associated type a :++: b (here (x ::: y) :++: b, obviously) is declared to be equal to x ::: (y :++: b). Method definition is also clear here: it takes a pair of values and another value and constructs another pair where first element is the same as in the first argument and the second element is second element from the first argument combined with second argument with .++. method. We are allowed to use .++. because of Append y b constraint

These are type signatures of (.++.) method in class declaration and instance declarations:

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

Note that in each instance very abstract a :++: b transforms to more concrete type. It is plain b in first case and more complex x ::: (y :++: b), itself written in terms of :++:.

Such declaration of associated type is needed to tell the type system that there is some type (a :++: b in this case) which is uniquely determined by a and b alone. That is, if typechecker knows that in certain expression a and b types are equal to, say, Int and Double, and:

1. there is a constraint Append a b;
2. there is a type class instance Append Int Double with the associated type declared, say, as type Int :++: Double = String,

then the typechecker will know that if he meet type a :++: b it will know that in fact this type is String.

As for ~, it is called 'Lazy pattern match'. It is very clearly explained here.

Feel free to ask if something is still not clear.