A problem with the typing system.
Marcin 'Qrczak' Kowalczyk
3 Jun 2001 11:13:26 GMT
Sat, 02 Jun 2001 23:03:29 +1000, Sean Seefried <email@example.com> 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
> 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 * firstname.lastname@example.org http://qrczak.ids.net.pl/
^^ SYGNATURA ZASTĘPCZA