[TYPES] [tag] Re: Declarative vs imperative

[Lukasz Stafiniak]

On Sat, May 4, 2013 at 5:49 PM, Kalani Thielen <kthielen at gmail.com> 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.