[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: More on dispatching by function return type
Joe Marshall <email@example.com> wrote in article <firstname.lastname@example.org> 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?
> > 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.