I'm attempting to implement church numerals in Haskell, but I've hit a minor problem. Haskell complains of an infinite type with
Occurs check: cannot construct the infinite type: t = (t -> t1) -> (t1 -> t2) -> t2
when I try and do subtraction. I'm 99% positive that my lambda calculus is valid (although if it isn't, please tell me). What I want to know, is whether there is anything I can do to make haskell work with my functions.
module Church where
type (Church a) = ((a -> a) -> (a -> a))
makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)
numChurch x = (x succ) 0
showChurch x = show $ numChurch x
succChurch = \n -> \f -> \x -> f (n f x)
multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1
powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1)
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)
subChurch = \m -> \n -> (n predChurch) m
The problem is that
predChurch
is too polymorphic to be correctly inferred by Hindley-Milner type inference. For example, it is tempting to write:but this type is not correct. A
Church a
takes as its first argument ana -> a
, but you are passingn
a two argument function, clearly a type error.The problem is that
Church a
does not correctly characterize a Church numeral. A Church numeral simply represents a number -- what on earth could that type parameter mean? For example:That typechecks, but
foo
is most certainly not a Church numeral. We need to restrict the type. Church numerals need to work for anya
, not just a specifica
. The correct definition is:You need to have
{-# LANGUAGE RankNTypes #-}
at the top of the file to enable types like this.Now we can give the type signature we expect:
You must give a type signature here because higher-rank types are not inferrable by Hindley-Milner.
However, when we go to implement
subChurch
another problem arises:I am not 100% sure why this happens, I think the
forall
is being too liberally unfolded by the typechecker. It doesn't surprise me though; higher rank types can be a bit brittle because of the difficulties they present to a compiler. Besides, we shouldn't be using atype
for an abstraction, we should be using anewtype
(which gives us more flexibility in definition, helps the compiler with typechecking, and marks the places where we use the implementation of the abstraction):And we have to modify
predChurch
to roll and unroll as necessary:Same with
subChurch
:But we don't need type signatures anymore -- there is enough information in the roll/unroll to infer types again.
I always recommend
newtype
s when creating a new abstraction. Regulartype
synonyms are pretty rare in my code.This definition of
predChurch
doesn't work in simply typed lambda calculus, only in the untyped version. You can find a version ofpredChurch
that works in Haskell here.I have encountered the same problem. And I solved it without adding type signature.
Here's the solution, with
cons
car
copied from SICP.You can find full source here.
I'm really amazed after writing
sub m n = n pred m
, and load it in ghci without type error!Haskell code is so concise! :-)