[Haskell-cafe] Type inference for infinite structures
sebastian.sylvan at gmail.com
Thu Dec 22 20:14:26 EST 2005
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
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.
More information about the Haskell-Cafe