🚀 go-pugleaf

In article  <STEPHEN.92Apr16043927@estragon.uchicago.edu> Stephen P Spackman writes:
]In article <15343@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
]|
]|That is just another way of saying that types are static properties of
]|programs, which is far from a universal view.  It also happens to be
]|the case that sets make an excelent implementation of types.
]
]Ha ha. First off, "type" is a technical term from mathematical logic,
]and it has various approximate implementations in programming
]languages, but that isn't going to change the idea; just as you're
]never going to persuade me that floating point numbers really ARE the
]Reals, just because that's the approximation some languages use (for
]whatever excellent reasons they might have).

No one claims that floating point numbers are the Reals, and no one
claims that programming language types are Russel's logical types.
You are introducing a bogosity by taking a technical term from one
field and trying to apply its definition to the same term in another
field where the definition does not apply. (Furthermore, it is not
clear that Russel's types belonged to expressions either.  He seems to
have been a bit confused about the difference between "type of a
propositional function" and "type of an expression used to describe a
propositional function").

]Secondly, sets aren't even very nice mathematical objects, let alone a
]sound basis for computation. The whole idea of approaching computation
]non-constructively is a little, er, bizarre, n'est ce pas? To
]implement a set-based language semantics you have to implement the
]universal equality relation on which set theory is founded. So tell
]me, how do you compare functions?

You are introducing a further bogosity by taking the term "set" and
deciding that it refers to the objects of a particular axiomatic
system.  The term is far more general than that, and can refer to any
unordered collection without duplicates -- even to such collections in
a system that compares functions intensionally (by their text or their
name) rathern than extionsionally as most (but not all) logical
theories do.

]... I've used a language with
]an undecidable type system, of course, and it isn't so bad (in fact it
]may be well worth it to get types like "list of primes"). But I'm
]really unhappy about having nontermination while trying to check type
]conformity *at runtime*...

Then use a type system based on sets restricted to those with
decidable membership conditions.

] Intuitively, it seems to me that in order to pass a
]function as an argument under this scheme, I'd have to have listed all
]the *particular* arguments that can be passed...

That is because you are making assumptions about how much information
is required for a type (probably because you are still thinking of a
type in the Russelian sense).  If "type" is defined to be just "set of
values" or "any object of which this predicate is true", then the set
of _all_ functions (definable in the language) is a type, and you can
ask whether something is a function without asking anything about its
arguments.  It appears that you are also making an unwaranted
assumption about what types are used for.  It is not the case that you
automatically check the types of parameters.  With dynamic typing, a
function can take any parameters and must do its own explicit
type-checking if it needs something of a special type.
-- 
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman