2

I'm just starting to learn haskell and I'm trying to implement lists in a pure lambda calculus way (such as described in the wikipedia page for Church encoding).

The following function produces a "cannot construct the infinite type" at compile time. However, when I execute the code of the function interactively, it works. This is the code of the function:

showl l = isempty' l 0 (head' l)

And here is how I run it interactively (it works):

let l = (cons' 7 empty') in isempty' l 0 (head' l)

With the function showl, I want to get the first element of a list (not a haskell list, but a list as defined in Church encoding) if it is not empty, and 0 otherwise. In details, isempty' l returns a Church boolean, namely the function \ a b -> a if the list l is empty (True), and \ a b -> b otherwise (False). This way, if True, showl returns 0, and `(head' l)' otherwise (the first element of the list).

I suppose it's a problem with type inference, as suggested by the other questions about infinit type errors. But I don't see it, and since it works interactively, it must be fine... I'm confused.

Thanks

(the exact compiler output:

Occurs check: cannot construct the infinite type: t = t1 -> t -> t2
Probable cause: `isempty'' is applied to too many arguments
In the expression: isempty' l 0 (head' l)
In the definition of `showl': showl l = isempty' l 0 (head' l)
Failed, modules loaded: none.

and the functions I wrote to define Church style lists:

-- True and False
t a b = a
f a b = b

-- pairs
pair a b z = z a b
fst' p = p t
snd' p = p f

-- lists
empty' f x = x
isempty' l = l (\ a b -> f) t
cons' a l f x = f a (l f x)
head' l = l t 0
tail' l = fst' (l (\x p -> pair (snd' p) (cons' x (snd' p))) (pair empty' empty'))

)

3
  • 1
    Have you tried tacking explicit type declarations on all your functions? This usually leads to more useful compiler errors.
    – tdammers
    Aug 20, 2011 at 12:27
  • I doubt this will compile without explicit annotations, since your functions may need rank-2-types.
    – fuz
    Aug 20, 2011 at 13:14
  • Ok, I'm working on declaring type explicitly. I'll update my post when I have some news. Aug 20, 2011 at 13:19

1 Answer 1

4

It seems the compiler is getting confused here. Given an explicit type signature for your function (using Rank2Types), it compiles nicely and works just fine.

{-# LANGUAGE Rank2Types #-}

type List a = forall b. (a -> b -> b) -> b -> b

showl :: Num a => List a -> a 
showl l = isempty' l 0 (head' l)

When running it interactively it works because the concrete types are available.

5
  • Thanks. So I've been reading about rankNtypes and rank2types, but I really don't understand what they're about. What is the difference between a rank1 and rank2 type? Aug 23, 2011 at 12:29
  • @flagadabla: A rank 1 type can only have the forall in the outermost position, while higher ranked types can have the forall more deeply nested. This is useful when you want to require that a function argument is polymorphic. For example, a function like foo f = f "hello" + f 2 can only work if the function f is polymorphic, so we have to give it a rank 2 type like foo :: (forall a. a -> Int) -> Int.
    – hammar
    Aug 23, 2011 at 15:11
  • @flagadabla: As well as what hammar said, note that foralls behave much like additional arguments, in that they're right-associative and can be reordered freely as long as they're to the left of the type variable they quantify. So forall a. a -> (forall b. b -> a) is still a rank 1 type, because it can be reordered as forall a b. a -> b -> a. They also behave much like lambdas in a way; they bind variables in a scope extending as far to the right as possible. Aug 23, 2011 at 21:25
  • (I tried to add this as an answer to format the code, but it got deleted!?) Did you get a version of this with explicit types to work? I had some problems; for example, a = cons' "a" empty' at = tail' a :t at tail_a :: ([Char] -> a -> b) -> a -> a :t empty' empty' :: a -> b -> b Types don't match. Also, ab = cons' "a" (cons' "b" empty') head' ab ERROR - Cannot infer instance *** Instance : Num [Char] *** Expression : head' ab
    – guthrie
    Jan 14, 2012 at 14:18
  • @guthrie: Yes, answers are supposed to answer the question. If you have problems, you should ask a new question. Anyway, I wrote a gist some time ago with explicitly typed Church lists. Have a look at that.
    – hammar
    Jan 14, 2012 at 14:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.