[Haskell-cafe] Type inference for infinite structures

[Sebastian Sylvan]

On 12/23/05, Matt Collins <mattcol at gmail.com> 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