Yup. I deliberately ignored ⊥ to simplify the presentation (and I make no apologies for doing so!)
There are a couple of posts by Dan Piponi where he explores how to count inhabitants of types when you properly account for ⊥:
http://blog.sigfpe.com/2008/02/how-many-functions-are-there-from-to.html
He does it by counting the number of functions () -> () (where () is of course inhabited by both () and ⊥), and concludes that the number of functions () -> () depends on the semantics of the language:
1 in a total language (like Agda) or in mathematics.
3 in a lazy language (like Haskell) when working completely lazily.
4 in Haskell, when using seq to enforce strictness.
3 in a strict language (like ML).
He then goes on to analyse the relationship between point-set topology and computability, showing that the set of computable functions is in a 1-1 correspondence to the set of continuous functions, under the appropriate topology:
http://blog.sigfpe.com/2008/01/what-does-topology-have-to-do-with.html
http://blog.sigfpe.com/2008/02/what-is-topology.html
http://blog.sigfpe.com/2008/03/what-does-topology-have-to-do-with.html
Fascinating stuff - but you can see why I decided not to talk about it!
Edit: Aha, I just realized who you are, and that we've met before..!