Re: More on dispatching by function return type

[Ken Shan <address@hidden>]

Joe Marshall <jrm@ccs.neu.edu> wrote in article <7k0t7w54.fsf@ccs.neu.edu> in gmane.comp.lang.lightweight:
> > Do you mean that dvi2ps would be happy to produce ps if "asked to" on
> > the command line, and also happy to produce pdf if "asked to" on the
> > command line?  
> Yes.
> 
> > Then the type of dvi2ps would not be "dvi -> (union ps pdf)" in
> > usual notation; that type means that dvi2ps may produce either ps or
> > pdf, at -its- discretion.
> As far as other program are concerned, this really is the case.  The
> program may base its choice solely on that single command line
> argument, but the fact is that sometimes dvi2ps produces a ps file,
> and sometimes a pdf file.

But your type for dvi2ps does not let it receive that command line
argument.  One possible type for dvi2ps is "bool -> dvi -> (union ps
pdf)", where the "bool" is the command line argument.  A function
from bool to X (where X is a type) is a pair of X's, so this type is
equivalent to "(dvi -> (union ps pdf), dvi -> (union ps pdf))", which in
turn is equivalent to "dvi -> ((union ps pdf), (union ps pdf))".  But
you can in fact give dvi2ps a more precise type: "dvi -> (ps, pdf)" or
"(dvi -> ps, dvi -> pdf)".

> > The type that the just-described dvi2ps would take is a conjunction
> > (intersection), not a disjunction (union): "dvi -> (intersection ps
> > pdf)", or equivalently, "(dvi->ps, dvi->pdf)".
> 
> Intersection would be a file that is both a pdf and a ps file.

Intersection would be something that can be both used as a pdf file and
used as a ps file.  Indeed, dvi2ps as a pure function converts a dvi
file to something that can be both used as a pdf file and used as a ps
file: a conjunction.  One way to represent that something is the dvi
file paired with dvi2ps itself.  Another way to represent that something
is the pdf file paired with the ps file: a pair.

> But this is just leading us to a situation where we'll have to design
> a type language expressive enough that one can reason about classes of
> output based on command line switches, and that isn't particularly
> on subject.

It is as on subject as a type language expressive enough that one can
reason about classes of output based on command lines, because those
command lines are after all just command line switches to sh.

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
1653 * Commonwealth of England * 2003 * 350 years
Get out there and love people if you want change.
China has listed the organization behind http://www.uygur.org/ as terrorist.
http://www.mps.gov.cn/webpage/showNews.asp?id=1118&biaoshi=bitGreatNews