Thanks Sebastian, I guess I was ignoring the type of Succ like you said. Glad to have passed that mental barrier! On 23/12/2005, at 12:14 PM, Sebastian Sylvan wrote:

On 12/23/05, Matt Collins wrote:

...

Hi everyone,

I'm relatively new to Haskell and was a bit troubled by the problem of assigning a type to infinite structures. To give a clear example, suppose we have

data Nat = Zero | Succ Nat omega = Succ omega

What type then does omega have? According to GHCi, omega :: Nat. But surely this can only be the case if we already have that omega :: Nat (on the right hand side of the equation)?

I can see that the type assignment is valid, but is it necessarily the case? Does it not, somehow, sidestep the inductive base case of the definition of a Nat?

omega :: Nat so, Succ omega :: Nat, as well (see the second constructor in the data type Nat).

So there is no ambituity. Succ requires that its argument is of type Nat, and the result of applying Succ to a Nat is also of type Nat.

It's hard to explain this better than that, I think you've just got stuck in some mental barrier. I think the a good "track" to start thinking in would be to consider that the type inference starts with the type of Succ (which is Nat->Nat), given that we know that its argument is Nat, and that the result is Nat, so the left hand side must also be Nat.

/S

-- Sebastian Sylvan +46(0)736-818655 UIN: 44640862