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