haskell types

[sj87]

Hello, Im studing functional programming using haskell and i have problems with some excercises about types. They give me an expresion and i have to wirte down the type for that expresion. I was wondering if there is any method or something that allow me to make that without loosing the track, because some expressions are really a mess and i've got lost a lot trying to solve this kind of problems. Thanks a lot!

[Rashakil Fol]

Awesome. Haskell is the best programming language.

I'm not sure how complicated the expressions you're getting are, but there is only one way in which expressions get combined in Haskell: by function application. A good way to organize your thinking is to first get rid of all infix operators -- convert a + b to the form (+) a b, for example.

Have you ever solved geometry problems? A big part of solving geometry problems is what I've heard described as "angle chasing". You just try to find out all the information you can about the angles and lengths you have. It's not an organized process.

To figure out the types of Haskell expressions, what you do is more like "type chasing": to find out everything you can about the type of a Haskell expression. There is certainly some way of putting this into a dull algorithm, but that's not something you want to do when programming. Your real goal needs to be to be able to do this fast. Really fast.

But when they get complicated, it gets kind of hard. When it gets complicated and they've got a type error, Haskellers don't do it in their head, they litter their code with type signatures until they can see exactly where the type error is.

A lot of times, though, there's extraneous parts of the expression that you can ignore, for the purposes of looking at the whole expression's type. For example, in the function definition

nqueens n = foldr qu [[]] [1..n]
    where qu i qss = [(i,j):qs | j <- [1..n], qs <- qss, all (safe (i,j)) qs]
          safe (i,j) (x,y) = i /= x && j /= y && abs (i - x) /= abs (j - y)

you can almost forget about the function 'safe' -- the only types you're worried about are the types of i and j. (It turns out, though, that nqueens :: (Num t, Enum t) => t -> [[(t, t)]]. You can figure the t -> [[(t,t)]] part ignoring 'safe' completely, but then the restriction Num t comes from using subtraction in the 'safe' function.

The best way to get the type of an expression is to open up GHCi (or maybe Hugs) and then use :t yourExpression at the prompt. Then it tells you what the type is.

Of course, that's not much help to you :-)

Give a few examples of what kinds of expressions you might have to get the type of, and I'll answer. (I don't want to cover things you haven't learned yet or give examples that are too simple, though I've already given an example of a type with typeclass restrictions without knowing if you've gotten that far yet.)

[sj87]

Hi Rashakil Fol! Thanks for your answer!

Awesome. Haskell is the best programming language.

I'm still learning it, but so far is the best I've ever seen :D. I love making an effort to make things right and with a good theoretical background.

Give a few examples of what kinds of expressions you might have to get the type of, and I'll answer. (I don't want to cover things you haven't learned yet or give examples that are too simple, though I've already given an example of a type with typeclass restrictions without knowing if you've gotten that far yet.)

I have a few examples that I've already solved using the "type chasing" method. I was wondering if there is any other method that ensures me to get the correct answer ( not necesarilly quickly ) following an algorithm. I know it's not a good way of thinking but it would help me to verify the results for example ( without using hugs or ghci considering I won't be able to do that during an exam ). Here is one of the examples:

a = fork (fork,fork) (fork,fork) 

fork = fork (f,g) x = (f x,g x)

I want to get a 's type.

Again, thanks a lot for your help!!

[Rashakil Fol]

What does fork = fork (f,g) x = (f x,g x) mean? Did you mean to type just fork (f,g) x = (f x,g x) for that line? I'll assume you did.

We have fork (f,g) x = (f x, g x) . So we see that f and g are functions, so f :: a -> b and g :: c -> d for some types a,b,c,d. We see that f and g both receive the argument x , which means they take an argument of the same type. So a = c .

So fork :: (a -> b, a -> d) -> a -> (b,d) Then fork (fork,fork) (fork,fork) = (fork (fork,fork)) (fork,fork) . So let's look at the first part, fork (fork,fork) .

Look at the first argument: fork :: (a1 -> b1, a1 -> d1) -> (a1 -> (b1,d1)) . Look at the second argument: (fork,fork) :: ((a2 -> b2, a2 -> d2) -> (a2 -> (b2,d2)), (a3 -> b3, a3 -> d3) -> (a3 -> (b3,d3))) . Okay. Now see what types are equal by overlapping the type variables. We see that

a1 = (a2 -> b2, a2 -> d2) = (a3 -> b3, a3 -> d3)
b1 = a2 -> (b2,d2)
d1 = a3 -> (b3,d3)

It follows that

a2 = a3
b2 = b3
d2 = d3
and d1 = b1

So we have

fork (fork,fork) :: a1 -> (b1,d1)
                  = (a2 -> b2, a2 -> d2) -> (a2 -> (b2,d2), a2 -> (b2,d2))

Then fork (fork,fork) (fork,fork) fills in the type (fork,fork) :: ((a4 -> b4, a4 -> d4) -> a4 -> (b4,d4), (a5 -> b5, a5 -> d5) -> a5 -> (b5, d5)) for the argument's type of fork (fork,fork) . Which means

a2 = (a4 -> b4, a4 -> d4)
b2 = a4 -> (b4, d4)
a2 = (a5 -> b5, a5 -> d5)
d2 = a5 -> (b5, d5)

Thus a4 = a5, b4 = b5, d4 = d5 . And b2 = d2. So then the type of a is

a :: (a2 -> (b2,d2), a2 -> (b2,d2))
   = ((a4 -> b4, a4 -> d4) -> (a4 -> (b4, d4), a4 -> (b4, d4)), (a4 -> b4, a4 -> d4) -> (a4 -> (b4, d4), a4 -> (b4, d4)))

No need to write the 4s then. a :: ((a -> b, a -> d) -> (a -> (b,d), a -> (b,d)), (a -> b, a -> d) -> (a -> (b,d), a -> (b,d))) Checking with ghci you see that they call (a,b,d) by the names (t,t1,t2).

Sometimes it can be convenient in the middle of this, once you notice a type constructor taking two identical types, to make a type synonym: type Foo a = (a,a) . Then this can be written a :: Foo ((a -> b, a -> d) -> Foo (a -> (b,d))) , and it makes working with intermediate steps easier.

So, generally, I think the algorithm is, ignoring typeclasses for now, for an expression of the form x y :
1. find the type of x and the type of y .
2. overlap the type of y with the type of the first argument of x and remove unnecessary type names (unnecessary because they're replaced by more specific types, the way we replaced, say, b2 with a4 -> (b4,d4) , or unnecessary because they're equal to another type).
3. The type of the expression x y is the return type of x , with all type names replaced as applicable, based on the results of step 2.

[sj87]

Wow! I'll have to read this nice and slow, but thanks a lot for your answers! I think im beginning to understand the idea. Sorry for the mistake you noticed at the very beginning! Thanks again!