Type constructors vs. data constructors (Haskell)

We have

data Vector a = MkVector a a

then, it is said that Vector builds types, because its signature (in category Hask ) is

> :k Vector
Vector :: * -> *

that is, it takes a type and returns a type (the "hole" * is a type). A type constructor can only take types ( * ) and return types ( * ), whereas a constructor of values can take anything ( Int , String , ...) and return anything ( Int , String , ...). The difference between * and String , Int , Bool , ... is the same difference between String and "cabra" , "melón" , ...

For example, we can see how

> :k Vector Int
Vector Int :: *

is now a "final" type, we've built a type.

By cons, MkVector is a normal and current function, let's see

> :t MkVector
MkVector :: a -> a -> Vector a

that takes two values and returns another value.

As you see, the currificación can be applied indifferently to types as to functions, that is to say, we can have the constructor of types

data Vector' índice valor = MkVector' [(índice, valor)]

with signature

> :k Vector'
Vector' :: * -> * -> *

and we can currify it in the first argument to get another type constructor, let's see

> :k Vector' String
Vector' String :: * -> *

which is still a type constructor (a function in Hask ).

Thus, Vector builds types and MkVector values, because the first one is a function on the types (the category Hask ) and the second one a function on values.

In Haskell, the types expand at compile time, losing any information about them in the result. However, the compilation process can be used to "execute code" , for example Turing machine in the type system .

  

But why is it called (Vector a) contructor of types ?, I can not do anything with (Vector a) , I can not build anything, it's the identifier of the type itself depending on the type that has a .

Vector a is not a type constructor, but Vector (without the a parameter) is the type constructor.

In Haskell we can say that there are two sublanguages:

• The language of expressions or terms ;
• The language of the types .

For example, in this definition:

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (a:as) = f a : map f as

... (a -> b) -> [a] -> [b] is a type and f a : map f as is an expression. Type constructors are one of the "ingredients" that we combine to write compound types. Note that in the compound type (a -> b) -> [a] -> [b] , -> and [] are type constructors! (The two with their special syntax- -> is infixed, for example.)

We also mention the type constructors when we use the class system. Using your same example:

instance Functor Vector where
  fmap f (MakeVector x y) = MakeVector (f x) (f y)

Josejuan's response mentions the signatures of the types such as Vector :: * -> * ("kinds" in English). Class Functor applies to types with signature * -> * , so in my declaration we use Vector and not, say, Vector a :

-- EJEMPLO ERRÓNEO:
instance Functor (Vector a) where ... 

... since Vector a has the signature * , which is not compatible with Functor . But this depends on the signature of the class-for example the class Monoid applies to types with signature * , so we write:

import Data.Monoid

instance Monoid a => Monoid (Vector a) where
  mempty = MakeVector mempty mempty
  MakeVector a b 'mappend' MakeVector c d = 
      MakeVector (a 'mappend' c) (b 'mappend' d)