A problem with the typing system.

[Marcin 'Qrczak' Kowalczyk]

Sat, 02 Jun 2001 23:03:29 +1000, Sean Seefried <s350366@student.uq.edu.au> pisze:

> zero = \s z ->z
> succ x = \s z -> s x (x s z).
> 
> I don't think it's important that I explain why I want the extra
> occurrence of x there.

I don't understand what the extra x means, so I can only explain what
errors mean. I don't know what do you want to archieve.

>  Occurs check: cannot construct the infinite type:
>  t = (t -> t3 -> t2) -> t2 -> t1

The type of 's' is requested to take as its first argument 'x',
which is a function which takes as its first argument 's' again.
So the type of 's' would have to appear as a proper part of itself.

> data Church = Ch (forall a.(a -> a -> a) -> a -> a)

I would expect
    data Church = Ch (forall a. (a -> a) -> a)
but perhaps it has something to do with your extra 'x'...

> succ x = Ch(\s z -> s x (unCh x s z)
> 
> which gives the strange typing error:
> 
> Inferred type is less polymorphic than expected
>  Quantified type variable `a' is unified with `Church'

The constructor Ch has type
    (forall a. (a -> a -> a) -> a -> a) -> Church
and must be applied to a value which is polymorphic itself, i.e. which
could be assigned the type '(a -> a -> a) -> a -> a' for any 'a',
without knowing anything about the particular choice of 'a'. The type
allows a user of the resulting Church value to choose any type for
'a' and use this argument on this type - that's why it must work for
all of them. But
    \s z -> s x (unCh x s z)
doesn't have sufficiently general type: 'x' has type Church (because
'unCh' is applied to 'x'), so 's' takes only Church as argument, so
what should happen if the user instantiates it with something other
than Church?

> Is this sort of typing possible within Haskell.

I don't know how it's supposed to behave with the extra 'x', so I
can't tell what type it could have.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK