3 ms·

Pedants would add that the analogy with number of inhabitants is all a little screwed up in Haskell since bottom is an implicit inhabitant of all data types, wh

Pedants would add that the analogy with number of inhabitants is all a little screwed up in Haskell since bottom is an implicit inhabitant of all data types, which means that e.g. Either Void () has a different number of inhabitants than () and so they cannot strictly speaking be made isomorphic. Strict languages can sidestep this problem to an extent but still end up with "wrong" numbers of inhabitants for e.g. T -> (), since (\_ -> ()) is different from (\_ -> undefined). So the only guys living in pure algebraic bliss are the total functional programmers like the Agda aficionados.

crntaylor 14y ago
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..!
jonsterling 14y ago
True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom. And I would go as far as to claim that for our purposes, `Either Void ()` can indeed be made isomorphic with `()`, since the functions the converts between them will be total: they will provide a unique canonical term of the one for every canonical term of the other. It makes no sense to say that it's not total on the grounds that “it is not accounting for the extra inhabitant, the bottom”, because bottom is not a canonical term of any type. So the isomorphism is very real, and can be trusted as such. It's better to maintain an attainable definition of totality in a language, and a distinction between canonical and non-canonical terms, than to just say “There is no total function, because Bottom!”, whence we lose important distinctions for reasoning and gain nothing. For these reasons, I tend to use the term “inhabited by” to refer to canonical terms.
dons 14y ago
http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publicat... Fast and loose reasoning is morally correct.

crntaylor 14y ago

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..!

jonsterling 14y ago

True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom. And I would go as far as to claim that for our purposes, `Either Void ()` can indeed be made isomorphic with `()`, since the functions the converts between them will be total: they will provide a unique canonical term of the one for every canonical term of the other. It makes no sense to say that it's not total on the grounds that “it is not accounting for the extra inhabitant, the bottom”, because bottom is not a canonical term of any type. So the isomorphism is very real, and can be trusted as such. It's better to maintain an attainable definition of totality in a language, and a distinction between canonical and non-canonical terms, than to just say “There is no total function, because Bottom!”, whence we lose important distinctions for reasoning and gain nothing. For these reasons, I tend to use the term “inhabited by” to refer to canonical terms.

dons 14y ago

http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publicat... Fast and loose reasoning is morally correct.