  The space complexity of functional programs is not well understood. In
particular, traditional implementation techniques are tailored to time
efficiency, and space efficiency induces time inefficiencies, as it prefers
re-computing to saving. Girard's geometry of interaction underlies an
alternative approach based on the interaction abstract machine (IAM), claimed
as space efficient in the literature. It has also been conjectured to provide a
reasonable notion of space for the lambda-calculus, but such an important
result seems to be elusive.
  In this paper we introduce a new intersection type system precisely measuring
the space consumption of the IAM on the typed term. Intersection types have
been repeatedly used to measure time, which they achieve by dropping
idempotency, turning intersections into multisets. Here we show that the space
consumption of the IAM is connected to a further structural modification,
turning multisets into trees. Tree intersection types lead to a finer
understanding of some space complexity results from the literature. They also
shed new light on the conjecture about reasonable space: we show that the usual
way of encoding Turing machines into the lambda calculus cannot be used to
prove that the space of the IAM is a reasonable cost model.
