Scheme - Re: type terminology

Author

Re: type terminology

Joe Marshall

2004-05-12, 9:12 pm

Matthias Blume <find@my.address.elsewhere> writes:

> "Anton van Straaten" <anton@appsolutions.com> writes:
>
>
> Yes, indeed. Types are syntactic constructs, and as with all calculi
> we often wish to /interpret/ these constructs according to some
> semantics.

It is usually nice to be talking *about* something rather than just
talking. Since static typists generally use phrases like `no runtime
errors', it seems that running a program might have some relevance.
Assertions made in the type system are statements about the potential
behavior of programs.

> One possible approach is to interpret types as sets of values.

Er, yes. That is, after all, what programs manipulate. But you are
implying that there are other interpretations (other than the obvious
`they are syntactic tokens in the type calculus'). In the realm of
real, running programs, what other useful interpretation could they
have that is not trivially isomorphic to `sets of values'?

(That's only semi-rhetorical. Although I cannot fathom what other
interpretation you could give to `integer' other than `integer', I'd
be happy to be enlightened.)

--
~jrm

Matthias Blume

2004-05-12, 9:12 pm

Joe Marshall <prunesquallor@comcast.net> writes:

> Matthias Blume <find@my.address.elsewhere> writes:
>
>
> It is usually nice to be talking *about* something rather than just
> talking.

Yes, usually. But all over mathematical logic, we clearly separate
"just talking" and "talking about". For example in the
lambda-calculus, there are terms, and there are rules for manipulating
terms that are completely mechanical, i.e., one can carry them out
without referring to any sort of "meaning" of lambda terms. And that
is a good thing as otherwise a computer could not do the manipulation.
Coming up with a consistent meaning for these terms is a completely
different game (and, at least in the case of lambda, a much much
harder one).

> Since static typists generally use phrases like `no runtime
> errors', it seems that running a program might have some relevance.

Yes.

> Assertions made in the type system are statements about the potential
> behavior of programs.

Not a-priori. The connection between properties of the type system
and properties of the running program have to be stated as theorems
and lemmas, and then they have to be proved. Certainly, the
construction of particular type systems was done with those properties
(and their provability) in mind, but that does not change the fact
that the type system in and by itself does not "say" anything -- we
have to interpret it.

>
> Er, yes. That is, after all, what programs manipulate. But you are
> implying that there are other interpretations (other than the obvious
> `they are syntactic tokens in the type calculus').

Well, at the very least, even what "value" means depends on what kind
of semantics we use for the dynamic part of the language, so "set of
values" is less immediate than you might imagine. And then, for
certain technical reasons, some interpretations of types found it
necessary to augment plain values with, e.g., indices, so types are
interpreted as sets of indexed values, etc.

> In the realm of
> real, running programs, what other useful interpretation could they
> have that is not trivially isomorphic to `sets of values'?

Just take effects systems. Effects systems are also type systems of a
certain kind, but the "types" tell you about the potential effects
that a computation might have. If you want to map these things
straight to sets of values, you need to have values that represent
computations. Obviously, this can and has been done (monads), but it
is not strictly necessary to understand the type system.

Matthias

Joe Marshall

2004-05-12, 9:12 pm

> Joe Marshall <prunesquallor@comcast.net> writes:

Matthias Blume <find@my.address.elsewhere> writes:[color=darkred]
>
> Yes, usually. But all over mathematical logic, we clearly separate
> "just talking" and "talking about". For example in the
> lambda-calculus, there are terms, and there are rules for manipulating
> terms that are completely mechanical, i.e., one can carry them out
> without referring to any sort of "meaning" of lambda terms. And that
> is a good thing as otherwise a computer could not do the manipulation.

The rules are intended to have a particular semantic meaning, though.
Certainly I could make up a rule called `Joe Conversion' that allows
you to replace a lambda expression of the form \x.\y.xy with \z.42,
and I could get the computer to perform this and even prove theorems
using this construct, but it won't *mean* anything useful.

> Just take effects systems. Effects systems are also type systems of a
> certain kind, but the "types" tell you about the potential effects
> that a computation might have. If you want to map these things
> straight to sets of values, you need to have values that represent
> computations. Obviously, this can and has been done (monads), but it
> is not strictly necessary to understand the type system.

Ok.

Bradd W. Szonye

2004-05-12, 9:12 pm

Matthias Blume wrote:

Bradd W. Szonye writes:[color=darkred]
[color=darkred]
> Ok, one last question: The dictionary definition refers to the the
> following words: "trait", "characteristic", "group", "class", "general
> character or structure", "considered as". None of these have a clear
> definition of their own, and until you provide those, your definition
> is without meaning.

True. The dictionary definitions are very general and need some
tailoring before you can use it in a specific domain.

1. A number of people or things having in common traits or
characteristics that distinguish them as a group or class.
2. The general character or structure held in common by a number of
people or things considered as a group or class.

This is merely a natural-language description of the rule-based notation
for set description,

S = { E | E meets some criteria C }

In the first definition, "type" refers to the set; in the second, "type"
refers to the criteria used for describing the set. (Contrast that to
the definition of "class," which refers exclusively to the set.) This
ambiguity doesn't concern me much, since the two meanings are
isomorphic. For simplicity's sake, I'll use the first meaning.

What's the difference between a type and a set? For one thing, all types
are describable, which is not IIRC true of all sets. I don't know
whether that's an important difference, though, because programmers
mostly only care about a small subset of all types, the "interesting"
ones. Of course, "interesting" is subjective, so you won't find a good
general definition of it.

In practice, we care most about types like these:

domain: D = { d | d is in the domain of F }
range: R = { r | r is in the range of F }
signature: S = { d -> r | d is in D and r is in R }

And of course many programming languages strive to organize these types
so that it's easy to check them or infer them via static lexical
analysis.

> You harp on the idea that there has to be a common trait or
> characteristic without saying what that is. You claim that an
> arbitrary set is not a type because arbitrary elements do not
> necessarily have common traits. How is "being member of the same set"
> for a "common trait"?

That is a common trait, but it's insufficient to distinguish them as a
group or class. It's the same as writing

S = { E | E is an element of S }

which might be interesting in some contexts, but it doesn't actually
define a type.

C'mon, this really isn't that hard to grasp. I can't tell whether you're
being perverse, have some obsessive need for careful mathematical
definitions, or whatever, but it looks like you're going out of your way
to violently agree with me. Much of what I've written here is based on
your own description of "dynamic typing."

> Please, don't answer.

Please, if you'd quit being such an intellectual snob, it'd be much
easier to discuss things with you.
--
Bradd W. Szonye
http://www.szonye.com/bradd

Matthias Blume

2004-05-12, 9:12 pm

"Bradd W. Szonye" <bradd+news@szonye.com> writes:

> Please, if you'd quit being such an intellectual snob, it'd be much
> easier to discuss things with you.

Bradd, let's agree to no longer discuss. Ok?

Mario S. Mommer

2004-05-12, 9:12 pm

"Bradd W. Szonye" <bradd+news@szonye.com> writes:
>
> That is a common trait, but it's insufficient to distinguish them as a
> group or class. It's the same as writing
>
> S = { E | E is an element of S }
>
> which might be interesting in some contexts, but it doesn't actually
> define a type.

Bradd, you are making essentially the same mistake as Matthias,
accepting only one possible definition of type. And if the world
turned evil, and I had too chose between yours an Matthias's
definition, I would not hesitate to choose the latter, since it is at
least concrete and clear.

I think the definition of type found in the CLHS is enough for our
purposes.

http://www.lisp.org/HyperSpec/Body/glo_t.html

One should note that this definition is so general that, almost by
definition, it contains counterexamples to anything you might
reasonably believe about types. That is why Matthias calls them "not
interesting". Why he believes that this makes it somehow wrong is
beyond me.

This definition ("our definition") is certainly more general, but from
a theoretical point of view unwieldy. In any case, that is what makes
our languages more powerful ;)

Bradd W. Szonye

2004-05-12, 9:12 pm

Matthias Blume wrote:

Bradd W. Szonye wrote:[color=darkred]

Mario S Mommer wrote:[color=darkred]
> Bradd, you are making essentially the same mistake as Matthias,
> accepting only one possible definition of type .... I think the
> definition of type found in the CLHS is enough for our purposes.

That definition begins:

type n. 1. a set of objects, usually with common structure,
behavior, or purpose.

Except for the "usually," that's exactly the same definition I gave in
the message you're replying to! The AH4 dictionary also offers a second
definition, where "type" refers to the common structure, behavior, or
purpose instead of the set itself. I ignored that alternate definition
for simplicity's sake.

My natural language definition does limit types a bit more than the CLHS
definition does, because it lacks the "usually" disclaimer. I suppose
that you could define a type as an arbitrary group of objects (so that
they have no common structure or behavior) and then never use it
anywhere (so that the objects have no common purpose), but I don't find
that particularly interesting. Note that if you use a type as (e.g.) the
domain of a function, the elements do have a common purpose, and you can
write the set as S = { E | E is in the domain of F }.

> One should note that this definition is so general that, almost by
> definition, it contains counterexamples to anything you might
> reasonably believe about types.

I agree that it's a good definition, although I don't see the point in
hedging the definition with "usually."

> That is why Matthias calls them "not interesting". Why he believes
> that this makes it somehow wrong is beyond me.

I agree. Because of that, I don't see why you said you'd prefer
Matthias's definition to the one I offered; it's essentially the same as
the CLHS definition. When I wrote that it's equivalent to the rule-based
notation for set description, I was merely describing the AH4/CLHS
definition in a mathematical context.
--
Bradd W. Szonye
http://www.szonye.com/bradd

Mario S. Mommer

2004-05-12, 9:12 pm

"Bradd W. Szonye" <bradd+news@szonye.com> writes:
> Mario S Mommer wrote:
>
> That definition begins:
>
> type n. 1. a set of objects, usually with common structure,
> behavior, or purpose.
>
> Except for the "usually," that's exactly the same definition I gave in
> the message you're replying to!

Yes, but the "usually" is there for a good reason :-)

> My natural language definition does limit types a bit more than the
> CLHS definition does, because it lacks the "usually" disclaimer. I
> suppose that you could define a type as an arbitrary group of
> objects (so that they have no common structure or behavior) and then
> never use it anywhere (so that the objects have no common purpose),
> but I don't find that particularly interesting. Note that if you use
> a type as (e.g.) the domain of a function, the elements do have a
> common purpose, and you can write the set as S = { E | E is in the
> domain of F }.

The problem with this definition is that, given any set, you have
functions that have this set as a domain. You have the identity, for
example, but you have all sorts of other functions defined arbitrarily,
and, who knows, perhaps some functions which, given enough knowledge
about them, you wouldn't consider to be defined arbitrarily.

Furthermore, if you have a predicate

P(x) = "x is of type t"

and define A = {x | P(x) }, then the predicate

Q(x) = "x is in A"

is equal to P, but according to your rules does not say anything about
the type of x.

>
> I agree that it's a good definition, although I don't see the point in
> hedging the definition with "usually."

To make it the class of all sets. I think the "usually" there also
serves to illustrate the point of a type, without condemning you to
actually have a purpose when defining a type. Useful for Zen
programming.

>
> I agree. Because of that, I don't see why you said you'd prefer
> Matthias's definition to the one I offered;

That was a bit of a joke, sorry.

> When I wrote that it's equivalent to the rule-based notation for set
> description, I was merely describing the AH4/CLHS definition in a
> mathematical context.

Yes, up to the issue that whether things share a common trait or not
lies in the eyes of the beholder, so that IMO it is not a definition
which is watertight.

I don't think the vastness of what falls under this definition is a
reason to worry. There are quite a few interesting subcategories of
the category of all sets :-)

Bradd W. Szonye

2004-05-12, 9:12 pm

> "Bradd W. Szonye" writes:

Mario S Mommer wrote:[color=darkred]
> ... The problem with this definition is that, given any set, you have
> functions that have this set as a domain ....

Sure, you can come up with some use for just about any set. If you're
actually using Q = { 1 q { foo } 42 } as the domain of some function in
your system, it's reasonable to call that set a "type," because its
elements have a common purpose in that system, but normally I'd just
call it an arbitrary set, not a "type."

> You have the identity, for example ....

I'm a bit

. The identity function does not have Q as its domain.
Q is in its domain, and so are the elements of Q, but so are lots of
other things. In other words, everything in Q has the identity trait in
common, but that doesn't distinguish them as a group. I see that as a
weakness of the CLHS definition: It captures the "common trait" idea but
not the "distinguishes them as a group" idea.

> ... but you have all sorts of other functions defined arbitrarily,
> and, who knows, perhaps some functions which, given enough knowledge
> about them, you wouldn't consider to be defined arbitrarily.

Again, I see that as a weakness of the CLHS definition. I think a useful
definition of "type" must consider the set's role within a system. While
Q may be a type in some systems, usually it's just an arbitrary set.
There are a lot of types in the "Universe" system, but I don't normally
care about that system -- I care about the system I'm creating in my
program.

These are the defining qualities of a "type" in my opinion:

1. A type is a set of objects with a common trait.
2. The common trait defines the set.
3. All objects in the system but not in the type lack that trait.
4. Some object in the system depends on the type or its defining trait.

The first quality is the same as the CLHS definition. The other three
qualities establish concreteness, differentiation, and relevance. The
CLHS definition lacks those qualities, but I feel that they're important
to the concept of "type."

> Furthermore, if you have a predicate
>
> P(x) = "x is of type t"
>
> and define A = {x | P(x) }, then the predicate
>
> Q(x) = "x is in A"
>
> is equal to P, but according to your rules does not say anything about
> the type of x.

I don't see what you're getting at here. I suspect that one of us is
misunderstanding the other. First, which x are you talking about? There
are three in your example.

There are at least four types in your example: the type t, the set of
all x for which P(x) is true, the set A, and the set of all x for which
Q(x) is true. All of these sets are equivalent. I'm not sure whether we
should also consider the types equivalent, though, because their
defining traits are different.

[color=darkred]
> To make it the class of all sets.

See, I don't think all sets are types, because I think a type must be
relevant to the system at hand. Otherwise, there's no point in calling
them "types" instead of "sets," except maybe as a point of tradition.

> I think the "usually" there also serves to illustrate the point of a
> type, without condemning you to actually have a purpose when defining
> a type. Useful for Zen programming.

Are you joking again?

Programs have lots of implicit types. For example, every time you define
a function, you also implicitly define a few types, including: the
function's domain, the function's range, and the set of all functions
with the same domain->range "signature." When you explicitly define a
type, you're usually just giving a name to a type that already exists
(or that you expect to exist in the future).

Anyway, the "relevance" quality (#4 above) covers this. It's not a type
trait unless it's relevant to the current system somehow. I suppose that
includes an explicit type definition that you never use again, although
of course there's little point in doing that except maybe as Zen
documentation.

[color=darkred]
> Yes, up to the issue that whether things share a common trait or not
> lies in the eyes of the beholder, so that IMO it is not a definition
> which is watertight.

The "relevance" quality takes away the subjectivity: The programmed
system is the "beholder," not the programmer.

> I don't think the vastness of what falls under this definition is a
> reason to worry. There are quite a few interesting subcategories of
> the category of all sets :-)

Sure, but I see types as being fundamentally *pragmatic* subsets, so I
prefer a definition that limits the definition to sets that the system
actually uses (quality #4). I don't see any point in making "type"
synonymous with "set" or with dwelling on the fact that some
hypothetical system might depend on an arbitrary set.
--
Bradd W. Szonye
http://www.szonye.com/bradd

Neelakantan Krishnaswami

2004-05-12, 9:12 pm

In article <4qqsut53.fsf@ccs.neu.edu>, Joe Marshall wrote:
> Matthias Blume <find@my.address.elsewhere> writes:
>
> The rules are intended to have a particular semantic meaning, though.
> Certainly I could make up a rule called `Joe Conversion' that allows
> you to replace a lambda expression of the form \x.\y.xy with \z.42,
> and I could get the computer to perform this and even prove theorems
> using this construct, but it won't *mean* anything useful.

It's useful to distinguish between the syntactic proof rules of a
logic, and the semantic equations that hold in the particular
interpretation you are using to modelling the logic with. This is
because the same logic can have many different interpretations, and
proofs that use only the logical rules will hold in all models of the
logic.

This bears a resemblance the idea of programming against an abstract
interface rather than a concrete implementation. I don't know enough
math to make this statement precise, though I find that proofs that
are careful about this are clearer in just the same way that programs
that are careful about data abstraction read better.

(This, incidentally, touches on one of the great mysteries to me: why
aren't all good programmers also capable mathematicians? To the extent
that I have any feeling for good mathematical style at all, it derives
from the habits I learned as a programmer.)

--
Neel Krishnaswami
neelk@cs.cmu.edu

Mario S. Mommer

2004-05-12, 9:12 pm

Well, I want a definition of type which allows me to reason
mathematically about them. The class of "sets with a purpose" do not
really fit this requirement, that's all.

I'll stick with the one from the CL spec.

"Bradd W. Szonye" <bradd+news@szonye.com> writes:
>
> I'm a bit

. The identity function does not have Q as its domain.

In modern mathematics, at least, functions are distinguished not only
by their values, but also by their domain and codomain. Thus, if A and
B are sets, and A is a subset of B, the identity I:A -> A is
considered to be different from the identity I:B -> B.

David Van Horn

2004-05-12, 9:12 pm

Mario S. Mommer wrote:
> Well, I want a definition of type which allows me to reason
> mathematically about them. The class of "sets with a purpose" do not
> really fit this requirement, that's all.
>
> I'll stick with the one from the CL spec.

Er... sets with a purpose is essentially what the CL spec gives:

type n. 1. a set of objects, usually with common structure, behavior, or
purpose. (Note that the expression ``X is of type Sa'' naturally implies that
``X is of type Sb'' if Sa is a subtype of Sb.) 2. (immediately following the
name of a type) a subtype of that type. ``The type vector is an array type.''

There is a *huge* body of literature on types in programming languages. If
you're looking for a definition that allows mathematical reasoning, why not
refer to that for a definition of types rather the Common Lisp language
specification?

David

Mario S. Mommer

2004-05-12, 9:12 pm

David Van Horn <dvanhorn@cs.uvm.edu> writes:
> Mario S. Mommer wrote:
>
> Er... sets with a purpose is essentially what the CL spec gives:
>
> type n. 1. a set of objects, usually with common structure, behavior,
^^^^^^^
> or purpose. [...]

That is the difference.

> There is a *huge* body of literature on types in programming
> languages. If you're looking for a definition that allows
> mathematical reasoning, why not refer to that for a definition of
> types rather the Common Lisp language specification?

The discussion was wether there are definitions that accomodate the
needs of dynamically typed languages, and the claim was that there is
none. I found a good one in the CL spec.

Sponsored Links