How is the syntax of type systems read?

Question

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.

Answer 1

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)