Exploring Haskell's Type System: From data constructors to :t and :k

A beginner's guide to understanding Haskell's type system

·

5 min read

In Haskell, every value has a specific type and the type of a value determines the set of operations that can be performed on it. Haskell is a statically typed language, which means that the type of a value must be known at compile-time. Types are a way to classify values and provide a way for the compiler to check that we are using values in a way that makes sense.

Type synonym

The type keyword in Haskell is used to create a type synonym, which defines a new name for an existing type. It allows you to give an existing type a new name for the purpose of making your code more readable and maintainable. A type synonym does not create a new type, it just provides an alternative name for an existing type, it's just an alias.

type IntList = [Int]
type Name = String

We can use the IntList just as [Int] here:

sumList :: IntList -> Int
sumList [] = 0
sumList (x:xs) = x + sumList xs 
sumList [1,2,3] -- 6

Data constructor

The data keyword in Haskell is used to define new algebraic data types, which consist of one or more data constructors. Each data constructor defines a new value that can be created from the type. Data constructors can take one or more arguments, and return a value of the new type.

For example, the following code defines a new type Shape with two data constructors Circle and Rectangle:

data Shape = Circle Float | Rectangle Float Float

Each data constructor takes different arguments, Circle takes one float argument and Rectangle takes two float arguments. These data constructors can be used to create values of the new type Shape:

let circle = Circle 3.5
let rectangle = Rectangle 2.0 4.0

Here, the Shape is a type. Circle and Rectangle are a data constructors.

Next, let's use :t and :k to check the type information

:t

We can use :t to check the type of an expression in Ghci. It's a shorthand for the :type command.

When you type an expression followed by :t in the REPL or ghci, it will show you the type of that expression. For example:

ghci> :t 1
1 :: Num a => a
ghci> :t (+)
add :: Num a => a -> a -> a

The Circle is a data constructor, which has a type of Float -> Shape Means when it get a Float, it will become a Shape. Similarly, for Rectangle, it needs 2 Floats to become a Shape .

ghci> :t Circle
Circle :: Float -> Shape
ghci> :t Circle 1
Circle 1 :: Shape
ghci> :t Rectangle
Rectangle :: Float -> Float -> Shape
ghci> :t Rectangle 1
Rectangle 1 :: Float -> Shape
ghci> :t Rectangle 1 2
Rectangle 1 2 :: Shape

Nothing has a type of Maybe a. and Just has a type of a -> Maybe a, because Just requires an argument to make it a Maybe a Type.

ghci> :t Just
Just :: a -> Maybe a
ghci>  :t Just 1
Just 1 :: Num a => Maybe a
ghci>  :t Just 'a'
Just 'a' :: Maybe Char
ghci>  :t Nothing
Nothing :: Maybe a

However, if you try to check the type of Shape, you will get an error:

ghci> :t Shape

<interactive>:1:1: error: Data constructor not in scope: Shape

Because it's not a data constructor.

We can use :k to check Shape the Kind.

:k

:k is a command used in the REPL (Read-Evaluate-Print Loop) or in the ghci (Glorious Glasgow Haskell Compilation System) to check the kind of a type. It's a shorthand for the :kind command.

A kind is a type of types, they tell us about the number of arguments that a type constructor takes, it's like a type of a type. Every type has a kind, and every term has a type. It's the number of arguments for the type constructor, not for the data constructor.

Here's an example of how you can use :k:

ghci> :k Int
Int :: *

This tells us that the type Int has a kind of *, which is the kind of a normal type.

You can use :k to check the kind of a type constructor like this:

ghci> :k Maybe
Maybe :: * -> *

Maybe has a kind of * - > * because the Maybe is defined like this:

data Maybe a = Just a | Nothing

It requires a type a.

Meanwhile, the Shape we defined above does not need a type argument. So its kind is *

ghci> :k Shape
Shape :: *

Conclusion

In conclusion, understanding the basics of Haskell's type system can be a bit tricky at first, but it's totally worth it! When you get a grip of it, you'll be able to write safer and more efficient code. With data constructors, type constructors and type synonyms, you'll be able to create your own types and define custom behavior for them. And don't forget the importance of tools like :t and :k, they are your best friends when it comes to debugging and understanding your code. All in all, this blog aimed to give you an overview of these concepts and I hope it helped you to understand them a little better, and have fun exploring the world of Haskell's type system!