Why does using a comma in Haskell function application cause different types?

  • A+
Category:Languages

I have run these haskell function in ghci then got those output, but i dont know how to explain it. What is the difference between g(x,y) and g(x y) and how the yield that output.

*Main> let  j g (x, y) = g(x,y) *Main> :t j j :: ((a, b) -> t) -> (a, b) -> t  *Main> let  j g (x, y) = g(x y) *Main> :t j j :: (t1 -> t2) -> (t3 -> t1, t3) -> t2 

 


What is the difference between g(x,y) and g(x y) and how the yield that output.

Well Haskell has - compared to the gross of programming languages - an "unusual" syntax (compared to very common languages like C, Java, etc.) how to describe function applications.

f x is a function application with f the function, and x the parameter. The brackets are not necessary (in contract to for example programming languages like C, Java, C#, etc.). But can be written, so f(x) is interpreted as f (x) and since (x) is simply x, the two are equivalent.

With that in mind if we look at g (x y) we see two function applications: x y, and g (x y). In a programming language like Java, this would look like g(x(y)). g, and x are thus both functions (where the "output type" of x should be the same as the "input type" of g). We perform function application with x the function and y the parameter, and the result is a parameter in a function application with g the function.

Haskell also has tuples. For example (4, 2) a 2-tuple. (x, y) is a 2-tuple as well: x is the first element, and y the second. If we thus write g (x, y), the we perform a function application with g the function, and (x, y) (a 2-tuple) the parameter. So that means that x has type a, and y has type b, then g has type (a, b) -> c.

With that in mind, we can derive the signature of functions, for example:

j g (x, y) = g (x,y) 

We see here that j has "two" parameters (in Haskell all functions have one parameter, the result of that function takes then another parameter), so we start by describing the signature of the function as:

j :: a -> b -> c g :: a (x, y) :: b g (x, y) :: c 

Since (x, y) is a tuple, we specialize the type of (x, y) as (d, e), so that means that the signature changes to:

j :: a -> (d, e) -> c g :: a (x, y) :: b ~ (d, e) g (x, y) :: c x :: d y :: e 

(the tilde ~ stands for the fact that the two types are the same)

Since we call g with (x, y) as parameter, we know that g is a function. The input type is the type of the parameter (x, y), so (d, e), whereas its result type is here the type of the result of j g (x, y), hence c, so we derive that g has type (d, e) -> c, so that means that:

j :: ((d, e) -> c) -> (d, e) -> c g :: a ~ ((d, e) -> c) (x, y) :: b ~ (d, e) g (x, y) :: c x :: d y :: e 

Then all constraints are satisfied, hence the type of j is:

j :: ((d, e) -> c) -> (d, e) -> c 

I leave deriving the type of j g (x, y) = g(x y) as an exercise.

Comment

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: