[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Sat, May 4, 2013 at 5:49 PM, Kalani Thielen <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list] > > I'm familiar with thinking of types as sets and logical connectives (type > constructors) as operations on sets. So the type A*B has size |A|*|B|, the > product of the sizes of two sets. A->B has size |B|^|A| and this works out > well (e.g.: Bool->Bool has size 2^2 = 4: not, id, const True, const False). > > So like you say, type negation corresponds to a continuation on that type > (where a continuation doesn't return any value at all, satisfying the empty > type). So ~A=A->_|_. That interpretation works out really well too, > because identities like A+B=~A->B can be read as compilation techniques for > variants (with the obvious construction and destruction approaches). > > But I'm not sure that I've got a straight story on this interpretation of > negation, quite. I think that it's suggesting that the size of the set of > continuations A->_|_ is |_|_|^|A|, or 0^|A|, which should be 0, right? So > there are 0 continuations -- they're impossible to construct? > My wild guess is that a continuation type ~A is a co-inductive type, and the correspondence with cardinality of sets works only for inductive types. Inductive types are the smallest sets built according to the specification, while co-inductive types are the largest sets meeting some constraints. Therefore the latter have infinite cardinality.
