[Haskell-cafe] Type inference for infinite structures

[Matt Collins]

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 <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