Lambda the Ultimate

With assignment deadlines pending, I've had to find myself some little project with which to procrastinate. To this end I've dug out my recurring goal to write a simple theorem prover.

Last night I wrote a bit of code to represent the expression ASTs of my language and some transformations on the same. Essentially I am representing ASTs as a binary tree (to be extended with other arities later) with labels on leaves and internal nodes:

data Tree b l
= Leaf l
| Branch b (Tree b l) (Tree b l)

The leaves of a Tree b l represent propositions and are labelled with a name :: l and the branches represent [binary] operators and are labelled :: b. In use, b and l are often the same type merely treated differently: Branch 0 (Leaf 0) (Leaf 1) might, for example, might represent the formula p ∨ q.

I'm familiar with Haskell's treatment of type- and data-constructors as being in separate name-spaces, and seem to recall reading that name-spaces are first-class in Scheme.

My questions are these: How advisable is it to separate the "name-spaces" of values and operators as I've done? If I'm to extend my system to support languages like the λ-calculus in the future, would it be better to use a single name-space now and require that the parser ensure that the user doesn't treat a value as an operator?