Newsgroups: comp.lang.misc
Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!sdd.hp.com!elroy.jpl.nasa.gov!decwrl!stanford.edu!neon.Stanford.EDU!brm
From: brm@neon.Stanford.EDU (Brian R. Murphy)
Subject: Re: Dynamic typing (part 3)
Message-ID: <1991Apr1.010526.26781@neon.Stanford.EDU>
Keywords: type inference static dynamic lisp ml
Sender: brm@cs.stanford.edu
Organization: Computer Science Department, Stanford University, Ca , USA
References: <1211@optima.cs.arizona.edu> <3073:Mar2820:38:5191@kramden.acf.nyu.edu>
Date: Mon, 1 Apr 1991 01:05:26 GMT
Lines: 50

In article <3073:Mar2820:38:5191@kramden.acf.nyu.edu> brnstnd@kramden.acf.nyu.edu (Dan Bernstein) writes:
>The problem with this argument is that neither model is more general
>than the other, or simpler, or much more expressive. Given a statically
>typed language with structs, an ``all'' type, and the set of types, you
>can set up pairs (value,type) and poof! there's dynamic typing. Given a
>dynamically typed language with assertions, you can assert that a value
>has some type and poof! there's static typing. A good preprocessor will
>smooth out the differences either way; so, all else being equal, you
>might as well choose the model that produces better code, i.e., static
>typing (at least with current technology).

Unfortunately, given a statically-typed language with higher-order
functions and an "all" type, type inference appears to be
undecideable.  Thus your statically-typed language _requires_ type
declarations, whereas in a dynamically-typed language we can get by
without them.

Note, however, that I'm not certain of its undecideability.  Thatte, in
    @INPROCEEDINGS{Thatte88,
        AUTHOR = "S. Thatte",
        TITLE = "Type Inference with Partial Types",
        BOOKTITLE = "Automata, Languages and Programming: 15th
			International Colloquium",
        MONTH = jul,
        YEAR = 1988,
        PAGES = "615-629",
        Publisher = "Springer-Verlag Lecture Notes in Computer Science, 
				vol. 317"}
attempted such a system and failed to find one.  The problem is that,
whereas in standard ML-like type inference you wind up with a set of
equations to solve, here you have a set of inclusion constraints.
When all type constructors are monotonic (as all ML type constructors
are except for "->"), and your only inclusion rules are:
	x <= All       for all x
	x <= y         if  x == y
	e1(x) <= e2(y) if  x <= y  and  e1(y) <= e2(y)
then solving a set of such constraints is pretty simple.  If you allow
nonmonotonic type constructors:
	x->y  <=  a->b if  y <= b  and  a <= x
					------  (antimonotonic part)
then things get trickier, and it seems quite likely that sets of
inclusion constraints cannot in general be solved.

If anyone knows a reference for whether or not this problem is
decideable, please send me email (as I don't read these type flame
wars too carefully).  If it is decideable, then I retract my complaint
above...

						-Brian Murphy
						 brm@cs.stanford.edu