What type of math: a & # 8594; b & # 8594; c

Question

I often see declarations such as this when viewing Haskell:

a -> (b -> c) 

I understand that it describes a function that accepts something of type a and returns a new function that accepts something of type b and returns something of type c. I also understand that types are associative (change: I was wrong about this - see comments below), so the above could be rewritten in such a way as to get the same result:

 (a -> b) -> c 

This will describe a function that takes something of type a and something of type b and returns something of type c.

I also heard that you can make an addition (edit: indeed, the word I was looking for here is double - see comments below) to the function by switching arrows:

 a <- b <- c 

which, I think, is equivalent

 c -> b -> a 

but I'm not sure.

My question is: what is the name of this math? I would like to know more about this so that I can use it to help me write better programs. I'm interested in learning things like the function of a free function, and what other conversions can be performed in type declarations.

Thanks!

Answer 1

Broadly speaking, it falls into the Lambda Calculus area .

Since this notation is associated with function types, an output type may also be of interest to you.

(The incorrect assumptions you made regarding associativity should already be sufficiently clarified by the other answers, so I will not repeat this)

Answer 2

Type declarations are not associative, a -> (b -> c) not equivalent (a -> b) -> c . In addition, you cannot “switch” the arrows, a <- b <- c - invalid syntax.

The usual reference to associativity in this case is that -> it is associative , which means that a -> b -> c interpreted as a -> (b -> c) .

Answer 3

 a -> (b -> c) 

and

 (a -> b) -> c 

not equivalent in Haskell. This is a type theory that can be based on category theory.

The first is a function that takes an argument of type a and returns a function of type b -> c . While the latter is a function that takes a function of type a -> b as an argument and returns a value of type c .

What do you mean by feature addition? The type of the inverse function of a function of type a -> (b -> c) is of type (b -> c) -> a .

Answer 4

Functions like a->b->c , which are actually the goals of functions like you said, are examples of Currying