🚀 go-pugleaf

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