[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: address@hidden*Subject*: Re: More on dispatching by function return type*From*: Ken Shan <address@hidden>*Date*: Thu, 18 Dec 2003 21:34:09 -0500*References*: <20031216220502.GA14825@eecs.harvard.edu> <brq7lcch.fsf@ccs.neu.edu> <20031217170748.GA29716@eecs.harvard.edu> <ptenjq36.fsf@ccs.neu.edu> <20031217213740.GB30731@eecs.harvard.edu> <7k0t7w54.fsf@ccs.neu.edu>*Sender*: address@hidden*User-agent*: tin/1.7.2-20031104 ("Eriskay") (UNIX) (Linux/2.6.0-test11 (i686))

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

**References**:**More on dispatching by function return type***From:*Ken Shan <ken@digitas.harvard.edu>

**Re: More on dispatching by function return type***From:*Joe Marshall <jrm@ccs.neu.edu>

**Re: More on dispatching by function return type***From:*Ken Shan <ken@digitas.harvard.edu>

**Re: More on dispatching by function return type***From:*Joe Marshall <jrm@ccs.neu.edu>

**Re: More on dispatching by function return type***From:*Ken Shan <ken@digitas.harvard.edu>

**Re: More on dispatching by function return type***From:*Joe Marshall <jrm@ccs.neu.edu>

- Prev by Date:
**Re: More on dispatching by function return type** - Next by Date:
**Re: More on dispatching by function return type** - Previous by thread:
**Re: More on dispatching by function return type** - Next by thread:
**Re: More on dispatching by function return type** - Index(es):