Search code examples
haskellsemanticstype-systems

How is the syntax of type systems read?

I have the following types for functions:

Quad = square · square
Square :: Integer -> Integer (So this function takes an integer as an input and outputs an integer)

The operator · is used in the definition of quad with type:

(·) :: (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer

I am unsure how the above is read as and the meaning behind it.

Solution

  • The double :: suggests this is Haskell, but the general principles are the same across all ML inspired languages (most, and type theoretic convention, is to use a single :).

    The :: symbol says that its left hand side has the type of its right hand side. So

    1 :: Integer

    The -> constructs a function type.

    timesTwo :: Integer -> Integer

    Further, -> is right associative.

    plus :: Integer -> Integer -> Integer

    says the function plus takes an integer and gives back a function which takes an integer and gives back an integer. This is equivalent to taking two integers, but is technically different (and in a sense, simpler). It is known as currying.

    square :: Integer -> Integer

    says that square takes an integer and returns an integer.

    Often, in type theory and functional programming languages we make use of type variables, so

    id :: forall a. a -> a
id x = x

    says that for any type a id is a function from a value of that type to another value of the same type. Your . operator makes more sense when it is given a more general type using variables

    (·) :: (b -> c) -> (a -> b) -> a -> c
f . g x = f (g (x))

    is the function composition function. It is a higher order function that takes two functions as arguments. More formally, for any types a, b, and c, (.) is a function from a function from b to c to a function from a to b to a function from a to c. The final function is just the composition of the two argument functions.

    You have specialized . to only work on Integers. But, the idea is the same. You take two functions from Integer -> Integer and an Integer, you apply the first function, and then apply the second function the the result.

    (.) or (+) is just Haskell for "this is an infix operator but I want to talk about it right now in prefix form."

    So, Quad is just a function from Integer -> Integer that calls square on its argument, and then calls square again on the result. It would be the same as

    quad x = square (square x)

    (haskell is case sensitive, and functions must start with lowercase letters)