# A problem with the typing system.

**Marcin 'Qrczak' Kowalczyk
**
qrczak@knm.org.pl

*3 Jun 2001 11:13:26 GMT*

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