Home > Archive > Scheme > May 2004 > type equivalence
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
|
|
| sharky 2004-04-29, 1:13 am |
| what form of type equivalence does Scheme use? Is it name or structure
equivalence? I checked out R5RS, and there was no reference to it.
Maybe because there is no user-defined types in the standard there is no
need to specify a form of type equivalence? if anyone can shed some
light on this i would appreciate it. thanks.
-- sharky
| |
| Marlene Miller 2004-04-29, 1:13 am |
| Hi sharky.
I don't know enough about Scheme to answer you question. But I'll just add a
note. Take a look at R5RS 1.1 3rd paragragh and R5RS 3.2.
"sharky" <bluemimic@hotmail.com> wrote in message
news:c5Zjc.1301$%o1.30@lakeread03...
> what form of type equivalence does Scheme use? Is it name or structure
> equivalence? I checked out R5RS, and there was no reference to it.
> Maybe because there is no user-defined types in the standard there is no
> need to specify a form of type equivalence? if anyone can shed some
> light on this i would appreciate it. thanks.
>
> -- sharky
| |
| Barry Margolin 2004-04-29, 3:31 am |
| In article <c5Zjc.1301$%o1.30@lakeread03>,
sharky <bluemimic@hotmail.com> wrote:
> what form of type equivalence does Scheme use? Is it name or structure
> equivalence? I checked out R5RS, and there was no reference to it.
> Maybe because there is no user-defined types in the standard there is no
> need to specify a form of type equivalence? if anyone can shed some
> light on this i would appreciate it. thanks.
Scheme doesn't have user-defined types. It also doesn't have parameter
type declarations for functions, so there's no point where one would
need to determine whether two functions accept the "same" type.
--
Barry Margolin, barmar@alum.mit.edu
Arlington, MA
*** PLEASE post questions in newsgroups, not directly to me ***
| |
| Matthias Felleisen 2004-04-29, 2:21 pm |
| sharky wrote:
> what form of type equivalence does Scheme use? Is it name or structure
> equivalence? I checked out R5RS, and there was no reference to it.
> Maybe because there is no user-defined types in the standard there is no
> need to specify a form of type equivalence? if anyone can shed some
> light on this i would appreciate it. thanks.
Scheme is an un(i)typed language so the question can't come up. [That's
what Barry said in different words.]
Types: a *syntactic* discipline for enforcing abstraction. That is, a
way to use FOO and BAR as values of TypeFOO and TypeBAR so that someone
something guarantees that FOO and BAR cannot flow into the same operation.
Ergo, one of the things you can do is to use the *same* bit pattern for
both and nothing bad will ever happen. [Just because people abuse the word
"type" in many contexts doesn't mean that they have the right to use it.]
Tags: some languages equip every value with the (conceptual) equivalent of a tag
to enforce some distinctions between classes of values. With tags, you can still
enforce some sanity for the operations of your program. Like types, (conceptual)
tags can help you ensure that your (primitive) operations never process the
wrong kind of value.
Note: some languages (Java) and some language implementations (SoftScheme) use
both types and tags. Because of that you can't really say that values are truly
tagged. A type checker may have found that your values flow in the right manner
anyway and may therefore not need a tag.
Nominal vs structural typing refers to Types. Hence, the question doesn't make
sense.
-- Matthias
| |
| Joe Marshall 2004-04-29, 9:12 pm |
| Matthias Felleisen <matthias@ccs.neu.edu> writes:
> Types: a *syntactic* discipline for enforcing abstraction. That is, a
> way to use FOO and BAR as values of TypeFOO and TypeBAR so that someone
> something guarantees that FOO and BAR cannot flow into the same operation.
> Ergo, one of the things you can do is to use the *same* bit pattern for
> both and nothing bad will ever happen. [Just because people abuse the word
> "type" in many contexts doesn't mean that they have the right to use it.]
>
> Tags: some languages equip every value with the (conceptual)
> equivalent of a tag to enforce some distinctions between classes of
> values. With tags, you can still enforce some sanity for the
> operations of your program. Like types, (conceptual) tags can help you
> ensure that your (primitive) operations never process the wrong kind
> of value.
What am I to make of this, then?
=> (car 42)
car: expects argument of type <pair>; given 42
[unknown source]: (car 42)
| |
| Matthias Felleisen 2004-04-29, 9:12 pm |
| Joe Marshall wrote:
> Matthias Felleisen <matthias@ccs.neu.edu> writes:
>
>
>
>
> What am I to make of this, then?
>
> => (car 42)
> car: expects argument of type <pair>; given 42
> [unknown source]: (car 42)
Abuse of language. -- Matthias
| |
| Anton van Straaten 2004-04-29, 9:12 pm |
| Matthias Felleisen wrote:
> Types: a *syntactic* discipline for enforcing abstraction. That is, a
> way to use FOO and BAR as values of TypeFOO and TypeBAR so that someone
> something guarantees that FOO and BAR cannot flow into the same operation.
> Ergo, one of the things you can do is to use the *same* bit pattern for
> both and nothing bad will ever happen. [Just because people abuse the word
> "type" in many contexts doesn't mean that they have the right to use it.]
>
> Tags: some languages equip every value with the (conceptual) equivalent of
a tag
> to enforce some distinctions between classes of values. With tags, you can
still
> enforce some sanity for the operations of your program. Like types,
(conceptual)
> tags can help you ensure that your (primitive) operations never process
the
> wrong kind of value.
Pierce used the term "type tags" to refer to these tags, in the introduction
to his book, "Types and Programming Languages". By the above definitions,
should Pierce's usage be considered incorrect? Might the "classes of
values" referred to above be called "types"?
If the answer to the latter question is no, presumably because in this view
a "type" should be considered strictly a notational concept, then what terms
should be used to cover the issues surrounding the tagging of values by
class? For example, what should we call a language which equips every value
with a tag, and checks that the tags match expectations at runtime?
If there is a description of PLT Scheme anywhere, for example, which
describes the language's tagging of values, and checking of tags, in terms
consistent with the above definitions, that would be helpful.
Anton
| |
| Bradd W. Szonye 2004-04-29, 9:12 pm |
| > Matthias Felleisen wrote:
Anton van Straaten <anton@appsolutions.com> wrote:[color=darkred]
> Pierce used the term "type tags" to refer to these tags, in the introduction
> to his book, "Types and Programming Languages". By the above definitions,
> should Pierce's usage be considered incorrect? Might the "classes of
> values" referred to above be called "types"? ...
Indeed, that's a primary definiton of the word "type": "A number of
people or things having in common traits or characteristics that
distinguish them as a group or class." Matthias's claim doesn't match
any descriptive or prescriptive definition of "type" that I've ever
seen, and it doesn't seem to have any practical value. It precludes
concepts like polymorphic types for no good reason that I can define. I
can only hope that he's joking.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Blume 2004-04-29, 9:12 pm |
| "Bradd W. Szonye" <bradd+news@szonye.com> writes:
>
> Anton van Straaten <anton@appsolutions.com> wrote:
>
> Indeed, that's a primary definiton of the word "type": "A number of
> people or things having in common traits or characteristics that
> distinguish them as a group or class." Matthias's claim doesn't match
> any descriptive or prescriptive definition of "type" that I've ever
> seen, and it doesn't seem to have any practical value. It precludes
> concepts like polymorphic types for no good reason that I can define. I
> can only hope that he's joking.
Since I have been in this type (pun intended) of discussion too many
times already to not be tired of fighting over words, I would have
tried to put it slightly differently than the other Matthias did.
This being said, however, I do not see why his claim precludes
polymorphic types.
(the other) Matthias
| |
| Anton van Straaten 2004-04-30, 9:43 pm |
| Matthias Blume wrote:
> Since I have been in this type (pun intended) of discussion too many
> times already to not be tired of fighting over words, I would have
> tried to put it slightly differently than the other Matthias did.
I don't want to fight over words, but I am curious as to what terms are
considered appropriate for the runtime value classification systems which
most people (other than type theorists, apparently) know as "types". The
term "tag" seems insufficiently specific - and rather
implementation-centric, in any case, focusing on an aspect of the mechanism,
rather than the overall concept being expressed.
Without alternative terms, there's little choice but to continue using
well-established terms, and this can hardly be considered abuse of language.
Anton
| |
| Matthias Felleisen 2004-05-04, 3:57 pm |
| Bradd W. Szonye wrote:
>
>
> Anton van Straaten <anton@appsolutions.com> wrote:
>
Benli uses the exact same distinction, just different words. The emphasis is on
type-and-tags not type. His addition of the word "type" is a nod to the rest of
the world for making up a bad word and sticking to it.
[color=darkred]
> Matthias's claim doesn't match any descriptive or prescriptive definition of "type" that I've ever
> seen,
It's not mine. It's due to John Reynolds, and it took me many years to accept
it. But I now buy it lock-stock-and-barrel.
> and it doesn't seem to have any practical value.
Tell John :-)
> It precludes
> concepts like polymorphic types for no good reason that I can define.
John invented the terminlogy in the context of explaining polymorphic types. I
have worked for years on a "dynamic" explanation of forall x :: Type. x -> x and
I know that I won't come close. Robby Findler has an idea, though it isn't
written up and I am hesitant to talk about things we haven't explored
theoretically.
If it weren't for the connection to polymorphism I probably would still spout
silly ideas about types and run-time in all seriousness. (Of course that doesn't
prevent me from abusing language myself.)
> I can only hope that he's joking.
Nope. -- Matthias
| |
| Bradd W. Szonye 2004-05-04, 3:57 pm |
| Bradd W. Szonye wrote:
Matthias Felleisen wrote:[color=darkred]
> It's not mine. It's due to John Reynolds, and it took me many years to
> accept it. But I now buy it lock-stock-and-barrel.
I was referring to your claim that it's "abusive" to call a tagged type
a "type." While I don't deny that there's value in distinguishing
syntactic types and tagged types, to hijack a well-established term like
"type" and call its traditional use "abusive" is, well, abusive!
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
> Matthias Blume wrote:
>
> I don't want to fight over words, but I am curious as to what terms are
> considered appropriate for the runtime value classification systems which
> most people (other than type theorists, apparently) know as "types". The
> term "tag" seems insufficiently specific - and rather
> implementation-centric, in any case, focusing on an aspect of the mechanism,
> rather than the overall concept being expressed.
What's wrong with the word "(total) predicate"? A Scheme "type" is
given by a function that returns #t or #f for any given argument
value, and we consider the things it returns true for as the values of
the "type". The only special things about Scheme type predicates is
that they are supposed to be very efficient (and runtime tags tend to
be used for that). I personally also prefer another restriction which
happens to be true in Scheme, namely that the predicate is a pure
function of the argument value, i.e., it must not depend on state.
(This restriction rules out "list?" as a type predicate in Scheme.)
To me, types are terms in a /language of types/. While types can
often be interpreted as sets of values, such sets can also be
characterized in many other ways. One such way is to use a total pure
predicate as the indicator function of the set -- which is what Scheme
does. So Scheme has sets of values which could very well be thought
of as the interpretation of types is some language of types, but such
a language of types is currently not part of Scheme.
We could make up a trivial language of types for Scheme as follows:
Type ::= number | integer | rational | real | complex | pair | symbol |
string | vector | procedure | port | nil
But this does not do us much good unless we do something with this
language. The first thing to do is to come up with some relational
theory of types: which types are equal (answer: none -- they are all
pairwise distinct except, maybe, for "complex" and "number"), and
which types are "subtypes" of other types ("integer" <= "rational",
"rational" <= "real", "real" <= "complex", "complex" <= "number", plus
all the things you get from transitivity), etc.
But even that is not helping with anything until we start assigning
types to terms. Now we have a _type system_, and we can begin to ask
interesting questions about its rules such as: Does it tell the truth
(i.e., if a term e has type t, is it true that e always evaluates to a
value that is within t's interpretation)? or: Does it tell us
anything interesting about the terms in the term language (e.g., can a
well-typed program always make progress until it reaches a value)?
[Notice that the phrasing of the first question makes use of an
interpretation of types as sets of values. This can be avoided by
asking for type preservation: Do the typing rules assing the same type
to a term with a redex and its corresponding reduced term? This
property is commonly known as "subject reduction".]
The bottom line is that the word "type" is reserved for those
syntactic phrases in a language of types, and Scheme does not really
have such a language.
Matthias
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| "Bradd W. Szonye" <bradd+news@szonye.com> writes:
> Bradd W. Szonye wrote:
>
> Matthias Felleisen wrote:
>
> I was referring to your claim that it's "abusive" to call a tagged type
> a "type." While I don't deny that there's value in distinguishing
> syntactic types and tagged types, to hijack a well-established term like
> "type" and call its traditional use "abusive" is, well, abusive!
The term "type" was well-established in mathematics long before it was
hijacked and abused to mean "tagged value".
| |
| Matthias Felleisen 2004-05-04, 3:57 pm |
| Bradd W. Szonye wrote:
> Bradd W. Szonye wrote:
>
>
>
> Matthias Felleisen wrote:
>
>
>
> I was referring to your claim that it's "abusive" to call a tagged type
> a "type." While I don't deny that there's value in distinguishing
> syntactic types and tagged types, to hijack a well-established term like
> "type" and call its traditional use "abusive" is, well, abusive!
The word "abusive" has a different connotation than "abuse of language". I
sincerely hope that you just misspoke. -- Matthias
| |
| ifconfig 2004-05-04, 3:57 pm |
| "Matthias Blume" <find@my.address.elsewhere> wrote in message
news:m17jvttq7b.fsf@tti5.uchicago.edu...
> "Anton van Straaten" <anton@appsolutions.com> writes:
> [snip]
> ... I personally also prefer another restriction which
> happens to be true in Scheme, namely that the predicate is a pure
> function of the argument value, i.e., it must not depend on state.
> (This restriction rules out "list?" as a type predicate in Scheme.)
I don't see why this rules out list? - (define (list? l) (cond ((equal? l
empty) #t) ((pair? l) (list? (cdr l))) (else #f))) does not depend on
state...
> [Once again, snip]
--
ifconfig
BAGOS
http://bagos.sourceforge.net
| |
| Lauri Alanko 2004-05-04, 3:57 pm |
| In article <c75vtv$r6u$1@news2.netvision.net.il>,
ifconfig <dor@ntr.co.il> wrote:
>
> I don't see why this rules out list? - (define (list? l) (cond ((equal? l
> empty) #t) ((pair? l) (list? (cdr l))) (else #f))) does not depend on
> state...
Yes, it does. If l is a pair, then (set-cdr! l '()) makes l a list,
and (set-cdr! l #f) makes it a non-list.
Lauri Alanko
la@iki.fi
| |
| ifconfig 2004-05-04, 3:57 pm |
| If i is an integer that (set! i 'x) makes i a symbol... I don't see the
difference.
--
ifconfig
BAGOS
http://bagos.sourceforge.net
"Lauri Alanko" <la@iki.fi> wrote in message
news:c761d1$3ir$2@oravannahka.helsinki.fi...
> In article <c75vtv$r6u$1@news2.netvision.net.il>,
> ifconfig <dor@ntr.co.il> wrote:
l[color=darkred]
>
> Yes, it does. If l is a pair, then (set-cdr! l '()) makes l a list,
> and (set-cdr! l #f) makes it a non-list.
>
>
> Lauri Alanko
> la@iki.fi
| |
| Marcin 'Qrczak' Kowalczyk 2004-05-04, 3:57 pm |
| On Mon, 03 May 2004 21:10:19 +0200, ifconfig wrote:
> If i is an integer that (set! i 'x) makes i a symbol... I don't see the
> difference.
It doesn't turn the object previously bound to i into a symbol.
It makes the i variable point to a different object.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| "ifconfig" <dor@ntr.co.il> writes:
> If i is an integer that (set! i 'x) makes i a symbol... I don't see the
> difference.
Then i is not an integer, it is a variable holding an integer.
| |
| Anton van Straaten 2004-05-04, 3:57 pm |
| Matthias Blume wrote:
> "Anton van Straaten" <anton@appsolutions.com> writes:
>
which[color=darkred]
The[color=darkred]
mechanism,[color=darkred]
>
> What's wrong with the word "(total) predicate"? A Scheme "type" is
> given by a function that returns #t or #f for any given argument
> value, and we consider the things it returns true for as the values of
> the "type". The only special things about Scheme type predicates is
> that they are supposed to be very efficient (and runtime tags tend to
> be used for that).
I think there's something else special. Taken together, Scheme provides a
comprehensive system in which every value is tagged, with a tag that's not
modifiable by users of the language. These tags are used in characteristic
ways throughout the language and its operators. Neither the term "tag" nor
"total predicate" fully captures the nature of this system as a whole, in
the way that the terminology surrounding "types" do. "Tag" and "predicate"
describe aspects of the system, but may require qualification even then.
As you point out, "Scheme has sets of values which could very well be
thought of as the interpretation of types in some language of types". That
seems like a reasonable argument for applying the terminology of types to
this area, as has been done in practice.
But I'm more interested in the expected consequences of the assertion that
there's an abuse of language occurring. If there isn't any good, accepted,
alternative terminology that doesn't qualify as an abuse, the assertion
seems to have no possible effect, destined to be filed under "things to
consider acting on when an appropriate response comes into existence".
If alternative terminology does already exist, I'd be interested in any
references that talk about dynamically-typed languages in terms which
acknowledge the view of types as purely syntactic. It's not just a question
of a single word, but a whole range of term usages in different contexts.
I notice that the Pierce book mentions the idea that the term
"dynamically-checked" should be used instead of "dynamically-typed", but
what it is that's being checked isn't mentioned explicitly. Since Pierce
also defines types in syntactic terms, one could conclude that the dynamic
checking must be of some other property which is not named in the book. Is
this symptomatic of a terminological void?
> The bottom line is that the word "type" is reserved for those
> syntactic phrases in a language of types, and Scheme does
> not really have such a language.
Saying that "the word 'type' is reserved" assumes the conclusion. I haven't
seen any real explanation of why the word *should* be reserved for that
purpose. Terms are overloaded all the time (cf. functor). Presumably, the
premise in this case is along the lines that it's dangerous or undesirable
to confuse syntactic types with dynamic types, and so a different name
should be used to underscore the difference in semantics. But the argument
could also be made that qualified versions of the same word should be used,
to capture the overlap in semantics.
I'm guessing that the argument against using variations of the same term in
both cases is that the relationship between the two meanings of the term is
not fully explored, and one runs the risk of diluting the rigor of the term
as used in the syntactic sense, or conversely, implying unwarranted rigor
for dynamic notions of type. Something along these lines would make sense
to me, but it still creates a need for alternative terminology.
> The term "type" was well-established in mathematics long before it
> was hijacked and abused to mean "tagged value".
Hmm, time for me to hit the old philosophy books again, and see just how
badly mathematicians mangled the term when they hijacked it from logic, the
way they did with "functor". ;)
I liked the description at
http://www.cs.cornell.edu/Info/Peop...es/Xtype_doc.ht
ml :
"Ontic Types and Ontic Mood - The ontic 'mood' is that of a priori
discourse about values; it is the one most like informal, pre-theoretical
discourse. Thus, one talks about numbers, functions, pairs, etc. In this
mood, a type is a class of values." (Philosophy again: the concept of ontic
mood is due to Heidegger.)
Is Scheme an ontically-typed language? ;)
Anton
| |
| Bradd W. Szonye 2004-05-04, 3:57 pm |
| Bradd W. Szonye wrote:
Matthias Felleisen wrote:[color=darkred]
> The word "abusive" has a different connotation than "abuse of
> language".
Not in my dialect.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| William D Clinger 2004-05-04, 3:57 pm |
| Matthias Blume wrote:
> The term "type" was well-established in mathematics long before it was
> hijacked and abused to mean "tagged value".
Reynolds's definition basically coincides with the usage of "type"
in logic and mathematics. So the hijackers and abusers of that
word would be those whose usages are at odds with Reynolds's.
Will
| |
| Anton van Straaten 2004-05-04, 3:57 pm |
| William D Clinger wrote:
> Matthias Blume wrote:
>
> Reynolds's definition basically coincides with the usage of "type"
> in logic and mathematics. So the hijackers and abusers of that
> word would be those whose usages are at odds with Reynolds's.
On his home page, Reynolds writes:
"A second area of interest is the semantics of types. The last fifteen
years have seen the discovery of a variety of type systems that have vastly
enlarged our notions of what types are and how they might be used. My goal
is to understand the meaning of these systems and to find a general concept
of type of which they are all instances."
That gives me hope that he may be considering a less narrow view of type
than has been proposed in this thread.
Anton
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
> William D Clinger wrote:
>
>
> On his home page, Reynolds writes:
>
> "A second area of interest is the semantics of types. The last fifteen
> years have seen the discovery of a variety of type systems that have vastly
> enlarged our notions of what types are and how they might be used. My goal
> is to understand the meaning of these systems and to find a general concept
> of type of which they are all instances."
>
> That gives me hope that he may be considering a less narrow view of type
> than has been proposed in this thread.
I don't know why you have to call this view "narrow". IMO, the many
different things that "type" can mean (while being consistent with
mathematical and logical usage -- as well as Reynolds' or, as we have
seen, Felleisen's) already cover such a broad field so that adding the
tiny sliver which says "type = set of tagged values" amounts to
nothing particularly interesting.
Matthias
| |
| Anton van Straaten 2004-05-04, 3:57 pm |
| Matthias Blume wrote:
> "Anton van Straaten" <anton@appsolutions.com> writes:
>
was[color=darkred]
fifteen[color=darkred]
vastly[color=darkred]
goal[color=darkred]
concept[color=darkred]
>
> I don't know why you have to call this view "narrow". IMO, the many
> different things that "type" can mean (while being consistent with
> mathematical and logical usage -- as well as Reynolds' or, as we have
> seen, Felleisen's) already cover such a broad field so that adding the
> tiny sliver which says "type = set of tagged values" amounts to
> nothing particularly interesting.
Without that tiny sliver, it's narrower, even though that still leaves a
broad field. Perhaps I should have emphasized the positive and said
"...considering a broader view of type..."
Whether the tiny sliver of types as tagged values is interesting, is a
matter of opinion, I agree.
One part I'm having a bit of difficulty with is that a language with
syntactic types can be mapped quite directly to one which uses tagged values
instead (regardless of how perverse that might seem). Given a good account
of the mapping between syntactic types and tagged values, one could imagine
wanting a single general term which can be specialized to cover both cases.
"Type" seems like it could be a good fit!
Anton
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
> Whether the tiny sliver of types as tagged values is interesting, is a
> matter of opinion, I agree.
Sure. The more important question is whether it is appropriate.
> One part I'm having a bit of difficulty with is that a language with
> syntactic types can be mapped quite directly to one which uses tagged values
> instead (regardless of how perverse that might seem).
Actually, I highly doubt that. It might work for simply typed
calculi, it will show serious strain when you try it with HM-style
parametric polymorphism, or structural subtyping, or existentials, or
abstraction, or row-polymorphism, or.... Finally, I have no idea how
it would play with effects systems (which are type systems, too).
Matthias
| |
| Matthias Felleisen 2004-05-04, 3:57 pm |
| Matthias Blume wrote:
> "Anton van Straaten" <anton@appsolutions.com> writes:
>
>
> Actually, I highly doubt that. It might work for simply typed
> calculi, it will show serious strain when you try it with HM-style
> parametric polymorphism, or structural subtyping, or existentials, or
> abstraction, or row-polymorphism, or.... Finally, I have no idea how
> it would play with effects systems (which are type systems, too).
While I agree with the second Matthias concerning the thesis, I disagree with
him on the reasons:
1. I spent a sabbatical with the POP group at CMU to study types from Harper,
Reynolds, and the rest of them. Believe me, John wouldn't consider type tags as
a type discipline. If you don't believe me, send him email and report on the
newsgroup. He'll probably respond. Or send email to Bob Harper.
2. So, as Bob Harper and others have pointed out many times on related
newsgroups, let me restate again that you cannot express everything with
run-time predicates and tags that you can express with types as a syntactic
discipline of abstraction. [This is the agreeement.]
3. The ability to restrict is as important as the ability to express.
Restrictive power and expressive power come in pairs. Some of the things that
you can express with syntactic types, you can simulate with type tags, and some
you can't. [This is the slight disagreement.]
- When you write the function \ x : int.x + 1 in ML, and the program with this
function type checks, you have a guarantee that (1) the function is never
applied to anything but integers and (2) that it always produces an integer. The
+ will never raise an exception. You have a FORALL inputs. ... Program ...
guarantee rather than a guarantee of the form FORALL inputs of program that I
testes: ... Program ...
- When you write the contracted MzScheme function \x : integer? . (x + 1) :
integer?, you only have the guarantee that (1) if the function is applied to a
boolean, the source module of the function call is blamed and (2) if the
function produces (for some obscure reason) a boolean the source module of the
function is blamed.
- Parametric polymorphism (be that inferred or explicitly stated) is something
that I don't know how to simulate in type tags. As I have stated before, and I
repeat, we have ideas, we're pursuing it, but I believe that this is pretty much
a lost cause in general.
- Structural subtyping: see mzscheme's class system.
- Existentials: see mzscheme's struct system. It is generative and therefore
gives you exact same power as the generative datatypes of ML.
- etc.
4. Everyone who makes statements about types should make sure he has read the
relevant fundamental papers and a few more. I find that the more people speak
out on types and related issues, the less they have read. Dear newsgroup
readers, computer science is a scientific discipline in the spirit of
mathematics, logic, electrical engineering (yes, I abused "scientific" here) and
similar disciplines on campus. It is not a "teach your self some random stuff in
21 days" thing. Read up on what you want to discuss and then condemn types or do
research on them.
-- Matthias, the
| |
| Anton van Straaten 2004-05-04, 3:57 pm |
| Matthias Felleisen wrote:
....<nice summary snipped>...
> Some of the things that you can express with syntactic types,
> you can simulate with type tags, and some you can't.
This is really what I was getting at, but I overstated it. I should have
said something more like this:
"One part I'm having a bit of difficulty with is that [some of the things
that you can express with syntactic types, you can simulate with type tags].
Given a good account of the mapping between syntactic types and tagged
values, one could imagine wanting a single general term which can be
specialized to cover both cases."
The point is that there is some technical correspondence there, and a
history of acknowledging that correspondence in terminology. That
terminological history is reflected in documents like RnRS and others, and
in language implementations such as PLT Scheme, as well as in wide, common
usage outside the Scheme world. That existing usage can't easily be
dismissed as "abuse", much as it might seem convenient to do so.
> 4. Everyone who makes statements about types should make sure he
> has read the relevant fundamental papers and a few more. I find that
> the more people speak out on types and related issues, the less they
> have read. Dear newsgroup readers, computer science is a scientific
> discipline in the spirit of mathematics, logic, electrical engineering
(yes,
> I abused "scientific" here) and similar disciplines on campus. It is not a
> "teach your self some random stuff in 21 days" thing. Read up on what
> you want to discuss and then condemn types or do research on them.
For my part, I'm not really attempting to make statements about types. I
responded to the assertion about abuse of the term "type". I'm perfectly
willing to take that on faith, given the source, especially since I don't
plan to spend even 21 days studying in order to reach a conclusion on the
matter. But I still have a problem: there don't seem to be good
alternatives to some of the common usages of type terminology related to
tagged values. As I've pointed out previously, this leaves little
alternative but to continue using the "abusive"[*] terminology. As such,
this is not actually abuse of language, but rather appropriate use in a
different context, particularly if it is understood that these two meanings
of "type" are not the same.
I'll repeat my request for references to sources which use acceptable
terminology to discuss languages which rely on runtime "types". I'd be
happy to shift my use of terminology, and communicate that usage to others,
if I had some good examples of what's considered appropriate.
Anton
[*] adjective form of "abuse", used in the sense "characterized by wrong or
improper use or action".
| |
| Mario S. Mommer 2004-05-04, 3:57 pm |
|
Matthias Felleisen <matthias@ccs.neu.edu> writes:
> 4. Everyone who makes statements about types should make sure he has
> read the relevant fundamental papers and a few more.
I would like to know more about this particular subject. Can you
recomend a few good starting points? That said, do the authors of
these papers have an exclusive divine licence on the use and meaining
of the word "type"?
> I find that the more people speak out on types and related issues,
> the less they have read. Dear newsgroup readers, computer science is
> a scientific discipline in the spirit of mathematics, logic,
> electrical engineering (yes, I abused "scientific" here) and similar
> disciplines on campus. It is not a "teach your self some random
> stuff in 21 days" thing. Read up on what you want to discuss and
> then condemn types or do research on them.
Might well be, although afaict, the condemnation of anything at all is
on your side. You and others seem to think that they are The Chosen
Keepers Of The One True Meaning Of The Word "Type", and call every
other use an abuse. Excuse me, but it is very hard for me to find that
position reasonable.
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| Matthias Felleisen <matthias@ccs.neu.edu> writes:
> Matthias Blume wrote:
>
>
>
> While I agree with the second Matthias concerning the thesis, I
> disagree with him on the reasons:
I disagree with those reasons myself, as I have discovered on second
thought. But my disagreement seems to be somewhat different than
yours, in fact, I don't really see much of a disagreement in what you
write.
> 1. I spent a sabbatical with the POP group at CMU to study types from
> Harper, Reynolds, and the rest of them. Believe me, John wouldn't
> consider type tags as a type discipline. If you don't believe me,
> send him email and report on the newsgroup. He'll probably
> respond. Or send email to Bob Harper.
That was the impression that I had, too.
> 2. So, as Bob Harper and others have pointed out many times on related
> newsgroups, let me restate again that you cannot express everything
> with run-time predicates and tags that you can express with types
> as a syntactic discipline of abstraction. [This is the agreeement.]
Indeed.
> 3. The ability to restrict is as important as the ability to
> express. Restrictive power and expressive power come in pairs. Some
> of the things that you can express with syntactic types, you can
> simulate with type tags, and some you can't. [This is the slight
> disagreement.]
I agree with the topical statement and disagree with the claim that
we have a disagreement here. :-)
> - When you write the function \ x : int.x + 1 in ML, and the program
> with this function type checks, you have a guarantee that (1) the
> function is never applied to anything but integers and (2) that it
> always produces an integer. The + will never raise an exception. You
> have a FORALL inputs. ... Program ... guarantee rather than a
> guarantee of the form FORALL inputs of program that I testes: ...
> Program ...
>
> - When you write the contracted MzScheme function \x : integer? . (x +
> 1) : integer?, you only have the guarantee that (1) if the function
> is applied to a boolean, the source module of the function call is
> blamed and (2) if the function produces (for some obscure reason) a
> boolean the source module of the function is blamed.
>
> - Parametric polymorphism (be that inferred or explicitly stated) is
> something that I don't know how to simulate in type tags. As I have
> stated before, and I repeat, we have ideas, we're pursuing it, but I
> believe that this is pretty much a lost cause in general.
Right (about the tags). But I believe that one could extend
ho-contracts with "poly" -- something akin to the capital-\Lambda from
system F. Parametric polymorphism would then be simulated by
functions from contracts to contracts. However, doing so requires
"polymorphic" contracts to be instantiated explicitly (which is
analogous to doing a type application in system F). The "ho" and
"poly" can be seen as special cases of a "pi" which is analogous to
the product type constructor in the lambda cube. (But I have not
worked out the semantics in detail, so there might be problems with
this that I am currently not aware of.)
> - Structural subtyping: see mzscheme's class system.
I have to take your word for it, but a quick glance at the
documentation on the MzScheme site did not make this obvious. So you
say, for example, that a class with fields a and b is a subclass of
any other class that has a field a and also of any other class that
has a field b, regardless of the "extends" relation given by class
definitions?
> - Existentials: see mzscheme's struct system. It is generative and
> therefore gives you exact same power as the generative datatypes of
> ML.
But ML datatypes aren't existentials at their full power. They should
be considered a form of abstraction, and ML-style abstraction, when
modeled using existentials, corresponds to a "pack" followed
immediately by an "unpack". Full-blown existentials (like the
terribly misnamed "forall" construct in Haskell) let you do more than
that.
Matthias B.
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| Mario S. Mommer <m_mommer@yahoo.com> writes:
> That said, do the authors of these papers have an exclusive divine
> licence on the use and meaining of the word "type"?
No, of course not. They have /earned/ that right by having laid the
foundations to and performed important parts of the relevant research.
>
> Might well be, although afaict, the condemnation of anything at all is
> on your side. You and others seem to think that they are The Chosen
> Keepers Of The One True Meaning Of The Word "Type", and call every
> other use an abuse. Excuse me, but it is very hard for me to find that
> position reasonable.
Accusations of "hijacking" the word "type" have been going back and
forth for ages now. It is a historical fact that, in mathematics and
logic, the word was coined to mean what "our" side thinks it means.
Sure, language changes over time, and if the "other" side keeps at it,
we will soon have to find a new word in order to be able to avoid
confusion. Nobody is the "Chosen Keeper" of a word's meaning, but we
should all strife to avoid ambiguities which really serve nobody.
Language is not constant, but we should not change the meaning of
words gratuituously since, for communication, we have to rely on a
common interpretation. This thread and many of its less civilised
predecessors amply demonstrate how communication and mutual
understanding is inhibited by incompatible vocabulary.
Matthias
| |
| Marcin 'Qrczak' Kowalczyk 2004-05-04, 3:57 pm |
| On Tue, 04 May 2004 09:28:46 -0400, Matthias Felleisen wrote:
> - When you write the function \ x : int.x + 1 in ML, and the program with this
> function type checks, you have a guarantee that (1) the function is never
> applied to anything but integers and (2) that it always produces an integer. The
> + will never raise an exception.
This is not true. It will throw exception on overflow (in SML). In OCaml
it will just silently produce a wrong result. So the guarantees either
don't exist or are wrong.
> - When you write the contracted MzScheme function \x : integer? . (x + 1) :
> integer?, you only have the guarantee that (1) if the function is applied to a
> boolean, the source module of the function call is blamed and (2) if the
> function produces (for some obscure reason) a boolean the source module of the
> function is blamed.
Well, but it works, as opposed to the ML version which is limited to
something smaller than machine word range.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> writes:
> On Tue, 04 May 2004 09:28:46 -0400, Matthias Felleisen wrote:
>
>
> This is not true. It will throw exception on overflow (in SML).
He meant that it will not throw an exception indicating a problem with
either argument or result not belonging to the set of ints. (By the
way, given that "int" is free here we can't be sure whether this will
ever throw an exception. If the function is preceded by a definition
that says
type int = IntInf.int
then it will never throw an exception.
> In OCaml it will just silently produce a wrong result.
What is the "wrong" result? Ocaml's integer + operator works modulo
2^32. Besides, the type of the function did not say anything about
the particular result value, only about the set of values that it has
to belong to.
> So the guarantees either don't exist or are wrong.
They exist and are right (but have to be correctly stated for that purpose).
>
> Well, but it works, as opposed to the ML version which is limited to
> something smaller than machine word range.
??
Matthias
| |
| Lauri Alanko 2004-05-04, 3:57 pm |
| In article <3dFlc.4143$8S1.2344@newsread2.news.atl.earthlink.net>,
Anton van Straaten <anton@appsolutions.com> wrote:
> One part I'm having a bit of difficulty with is that a language with
> syntactic types can be mapped quite directly to one which uses tagged values
> instead (regardless of how perverse that might seem). Given a good account
> of the mapping between syntactic types and tagged values, one could imagine
> wanting a single general term which can be specialized to cover both cases.
> "Type" seems like it could be a good fit!
I'd say the mapping between types and tags goes much more naturally
the other way: a tagged value can be seen as a Dynamic, ie. a run-time
type representation paired with a value of that type.
Since dynamics and intensional polymorphism already do run-time
analysis on types (and these are presumably "real" types), why are
languages with ubiquitous tags then so qualitatively different that
they cannot be said to have types?
It can be said that expressions and variables have types, while values
have tags. However, in operational semantics values _are_ expressions
(closed normal forms), so how come I can say "|- v : int", and it is
about real types, but if I say "(int? v) --> #t", it cannot possibly
have anything to do with types?
(Saying that it's the difference between static and dynamic semantics
is not really an answer, since there are type systems with reduction
rules, and languages with run-time typing judgements.)
Lauri Alanko
la@iki.fi
| |
| Lauri Alanko 2004-05-04, 3:57 pm |
| In article <m1y8o8qlq0.fsf@tti5.uchicago.edu>,
Matthias Blume <find@my.address.elsewhere> wrote:
> Sure, language changes over time, and if the "other" side keeps at it,
> we will soon have to find a new word in order to be able to avoid
> confusion. Nobody is the "Chosen Keeper" of a word's meaning, but we
> should all strife to avoid ambiguities which really serve nobody.
I think this battle has already been lost, and persisting at it will
do more harm than good. What is important is that everyone be aware of
the distinction, and uses appropriate clarifications when necessary.
Would it be so unbearably humiliating for an MLer to add that
horrendous attribute "static" when talking about types to a lisper?
Would it be so hard for a lisper to add "dynamic" when talking about
what _he_ considers to be types to an MLer?
Everyone can still grumble "but those are not _real_ types, dammit!"
Just be sure to mutter it under your breath and not aloud. :)
Lauri Alanko
la@iki.fi
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| Lauri Alanko <la@iki.fi> writes:
> In article <3dFlc.4143$8S1.2344@newsread2.news.atl.earthlink.net>,
> Anton van Straaten <anton@appsolutions.com> wrote:
>
> I'd say the mapping between types and tags goes much more naturally
> the other way: a tagged value can be seen as a Dynamic, ie. a run-time
> type representation paired with a value of that type.
Right. But notice that in static type systems with Dynamic, there is
only one type "Dynamic" which is effectively a huge discriminated sum
type. So you don't have to dig so deep: a simple "datatype" in ML has
the same properties. It pairs a value of some (other) type with
runtime information sufficient to be able to find out later which
particular type the so-packaged value originally belonged to. The
whole trick is really in having the corresponding "case" construct
with its associated typing rule in the term language -- which makes it
possible to reason statically about what's going on.
> Since dynamics and intensional polymorphism already do run-time
> analysis on types (and these are presumably "real" types), why are
> languages with ubiquitous tags then so qualitatively different that
> they cannot be said to have types?
Notice that you were careful with the wording in the previous
paragraph by saying "runtime type /representation/". Again, types are
terms in a language of types. Without such a language of types, tags
are just (parts of) values, nothing more and nothing less. In the
presence of a type language, tags can be used to encode certain
aspects of those static types at runtime.
By the way, I think it is misleading to say that dynamics do runtime
analysis on types. They really do runtime analysis of /values/ in a
way that plays nicely with an interesting and useful static typing
discipline.
> It can be said that expressions and variables have types, while values
> have tags. However, in operational semantics values _are_ expressions
> (closed normal forms), so how come I can say "|- v : int", and it is
> about real types, but if I say "(int? v) --> #t", it cannot possibly
> have anything to do with types?
Nobody says it cannot. In fact, it can. It /is/ possible to use the
term language itself as the language of types (or as part thereof).
This happens, to some extend, in all type systems with dependent
types. A related example is that of "singleton types" which are types
that are inhabited by precisely one proper value and which (when used
in a type system) can express the fact that some expression will
evaluate to one particular value. (Type systems are closely related
to dataflow analysis, and singleton types thus correspond to the kind
of information that one would use to do, e.g., value propagation in
a compiler.)
You can single out a sublanguage of Scheme which contains only total
predicates that don't depend on state. This sublanguage /can/ be seen
as a language of types. For example, you can use the set of expressions
{ PAIR?, SYMBOL?, NUMBER?, ... }
of Scheme expressions (pretending they don't depend on state, which in
reality they do, unfortunately), and think of this as the language of
types. But notice that this by itself isn't all that interesting
until one also provides some sort of relational theory of types and
rules how these types relate to expressions of the term language. In
other words, just making up a language of types that exists in a
vacuum is not enough to be the least bit interesting.
Matthias
| |
| Marcin 'Qrczak' Kowalczyk 2004-05-04, 3:57 pm |
| On Tue, 04 May 2004 10:27:34 -0500, Matthias Blume wrote:
>
> He meant that it will not throw an exception indicating a problem with
> either argument or result not belonging to the set of ints.
Substutute an arithmetic expression which can overflow the machine
word in an intermediate value even if arguments and the eventual result
fit. Then you have no idea when it can stop working if you look only at
the type.
>
> What is the "wrong" result? Ocaml's integer + operator works modulo
> 2^32.
Ok, not "wrong" but "almost always undesirable, rarely expected".
It's not modulo 2^32 but modulo 2^31 or 2^63, depending on the
architecture, and with the upper half of the range shifted to negative
numbers. Why would someone want these conditions of wrapping? The only
thing I can imagine is computing a hash of an object.
This behavior is purely accidental - it's just what is most easily
implemented. Trading correctness for speed.
It happens that in OCaml (I don't know about SML implementations) a
solution which uses bignums is less efficient than it could be if it was
the primary int representation, because *all* numbers are heap-allocated,
including those which fit in a machine word. This applies both to
Big_int.t (always a bignum) and Num.t (hybrid representation). This
discourages bignums except when absolutely necessary, and thus in practice
most code works on ints, and thus their correctness guarantees are always
modulo 2^31 or 2^63.
The guarantees are tricky to get right in the case of intermediate values
which might overflow. It can be quite unobvious what is the precise range
of inputs yields correct output. Most people don't bother to precisely
specify the range, they only ensure that it doesn't overflow when the
inputs are far from int limits.
Moral: there can be an unexpected gap between static types and guarantees
about sensible result.
# perl -e 'use POSIX; setuid(0x40000000); exec "ruby", "-e", "puts Process.uid"'
-1073741824
>
> ??
The MzScheme version doesn't have the problem with reaching machine word
size. For me it's more important than a static guarantee (which must
either admit that the input range is restricted to -2^30..2^30-2 or will
be wrong).
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Thant Tessman 2004-05-04, 3:57 pm |
| Matthias Blume wrote:
> [...] Nobody is the "Chosen Keeper" of a word's meaning, but we
> should all strife to avoid ambiguities which really serve nobody.
Don't follow politics much, do you... :-)
-thant
| |
| Matthias Blume 2004-05-04, 3:57 pm |
| Marcin 'Qrczak' Kowalczyk <qrczak@knm.org.pl> writes:
> On Tue, 04 May 2004 10:27:34 -0500, Matthias Blume wrote:
>
>
> Substutute an arithmetic expression which can overflow the machine
> word in an intermediate value even if arguments and the eventual result
> fit. Then you have no idea when it can stop working if you look only at
> the type.
In no way does this contradict what either of the two Matthiases said.
>
> Ok, not "wrong" but "almost always undesirable, rarely expected".
So what? The type does not say "returns the expected and desired
result" but merely "returns an int". Where is the disagreement?
> Moral: there can be an unexpected gap between static types and guarantees
> about sensible result.
Why is that "unexpected"?
> The MzScheme version doesn't have the problem with reaching machine word
> size.
If you use the appropriate static type in Haskell, Ocaml, or SML, the
same is true. (The stuff about efficiency has absolutely nothing to
do with type systems but only with the quality of this aspect of the
implementation in question.)
> For me it's more important than a static guarantee (which must
> either admit that the input range is restricted to -2^30..2^30-2 or will
> be wrong).
For me the opposite is true. (In real programs I almost never run
into problems with the range of integers.)
Matthias B.
| |
| Mario S. Mommer 2004-05-04, 3:57 pm |
|
Matthias Blume <find@my.address.elsewhere> writes:
> It is a historical fact that, in mathematics and logic, the word was
> coined to mean what "our" side thinks it means. Sure, language
> changes over time, and if the "other" side keeps at it, we will soon
> have to find a new word in order to be able to avoid
> confusion. Nobody is the "Chosen Keeper" of a word's meaning, but we
> should all strife to avoid ambiguities which really serve nobody.
> Language is not constant, but we should not change the meaning of
> words gratuituously since, for communication, we have to rely on a
> common interpretation.
While there is some truth to what you say, I do not believe that
mathematicians, nor anyone else, would be particularly threatened by a
multiple use of the word "type". If some confusion seems inevitable,
it costs no time and energy to make a clarification and be done with
it. It would save the world from quite some flammage, and pave the way
to some reasonable exchange.
BTW, the question for leads to information about this subject (types,
not the word "type") was meant seriously. I'd really like to know more
about it. What are, in your view, the papers one should read to get
started?
| |
| Marcin 'Qrczak' Kowalczyk 2004-05-04, 3:57 pm |
| On Tue, 04 May 2004 11:15:33 -0500, Matthias Blume wrote:
> For me the opposite is true. (In real programs I almost never run
> into problems with the range of integers.)
It's quite common that a program working on files is restricted to files
of 2GB in size on 32-bit architectures. For example Linux "du" started to
support larger sizes as recently as in March 2003 (of course previously it
would just give an incorrect result without a warning).
* * *
Actually what provoked my reaction was that a few w s ago I listened to
a talk about a tool for proving properties of Java programs, and there
was an argument for formal verification methods and for checked exceptions:
the Ariane 5 crash.
The funny thing is that it crashed because of an overflow of a 16-bit
type (and failure to handle it correctly). The tool in question, which
translated constraints from Java into Coq in order to help in proving
them, didn't deal with integer overflow at all. It assumed that the native
Java int corresponds to Coq unbounded int, and that addition corresponds
to addition, so the "proof" obtained should not in fact be carried over to
the source program.
And Java arithmetic overflow is an unchecked exception that doesn't need
to be declared. So it's silly to show this example as what lack of formal
verification can lead to, and at the same time present checked exceptions
as an example of static verification tool.
While I agree that static types are very helpful in finding errors,
too often I see claims that they prove more than they in fact do.
--
__("< Marcin Kowalczyk
\__/ qrczak@knm.org.pl
^^ http://qrnik.knm.org.pl/~qrczak/
| |
| Pascal Costanza 2004-05-04, 3:57 pm |
|
Matthias Blume wrote:
> Language is not constant, but we should not change the meaning of
> words gratuituously since, for communication, we have to rely on a
> common interpretation. This thread and many of its less civilised
> predecessors amply demonstrate how communication and mutual
> understanding is inhibited by incompatible vocabulary.
"Type" is de facto ambiguous, whether you want it or not. "Static
typing" vs. "dynamic typing" is not.
Pascal
--
1st European Lisp and Scheme Workshop
June 13 - Oslo, Norway - co-located with ECOOP 2004
http://www.cs.uni-bonn.de/~costanza/lisp-ecoop/
| |
| William D Clinger 2004-05-04, 3:57 pm |
| Matthias Felleisen <matthias@ccs.neu.edu> wrote:
> - When you write the function \ x : int.x + 1 in ML, and the program with this
> function type checks, you have a guarantee that (1) the function is never
> applied to anything but integers and (2) that it always produces an integer.
> The + will never raise an exception....
Not even an Overflow exception? That contradicts the SML97 basis at
http://www.smlnj.org//doc/basis/pag...G:INTEGER.+:VAL
Sorry to be so picky, but the "never raises an exception" canard is
one of my pet peeves.
Some static type systems guarantee that no *type* exception will ever
be raised at run time, where *type* exception is carefully defined to
exclude all exceptions that might be raised at run time.
Will
| |
| Matthias Felleisen 2004-05-04, 5:47 pm |
| Mario S. Mommer wrote:
> Matthias Felleisen <matthias@ccs.neu.edu> writes:
>
>
>
> I would like to know more about this particular subject. Can you
> recomend a few good starting points? That said, do the authors of
> these papers have an exclusive divine licence on the use and meaining
> of the word "type"?
>
>
>
>
> Might well be, although afaict, the condemnation of anything at all is
> on your side. You and others seem to think that they are The Chosen
> Keepers Of The One True Meaning Of The Word "Type", and call every
> other use an abuse. Excuse me, but it is very hard for me to find that
> position reasonable.
A scientific discipline needs a fixed terminlogy. People who wish to contribute
must study what people have to say in selective conferences and refereed
journals. If you're not willing to do that, but if you're instead interested in
re-raising terminology questions time and again, you may find science
unreasonable and irrational.
I definitely recommend that you start with Reynolds's papers from the 70s and
80s and then work your way through the development of Cardelli's paper on types
in the Handbook, Mitchell/Plotkin/Harper on abstract types and modules, and
probably some early Haskell programming papers thrown in.
-- Matthias
| |
| Mario S. Mommer 2004-05-04, 7:41 pm |
|
Matthias Felleisen <matthias@ccs.neu.edu> writes:
> Mario S. Mommer wrote:
>
> A scientific discipline needs a fixed terminlogy. People who wish to
> contribute must study what people have to say in selective conferences
> and refereed journals. If you're not willing to do that, but if you're
> instead interested in re-raising terminology questions time and again,
> you may find science unreasonable and irrational.
Well, this is a public forum, not a refereed scientific journal
specialized on some obscure corner of CS. If you wish to communicate
with people of different backgrounds, you must accept the fact that
there are different established terminologies[1]. It is you, BTW, and
M. B., which raise that questions over terminology over and over
again, simply by claiming that your use is the only correct one.
> I definitely recommend that you start with Reynolds's papers from the
> 70s and 80s and then work your way through the development of
> Cardelli's paper on types in the Handbook, Mitchell/Plotkin/Harper on
> abstract types and modules, and probably some early Haskell
> programming papers thrown in.
Aha.
Can you recommend some modern survey paper as a complement to that
program? I would really like to grasp the issues you are trying to
address, and what the central results are about.
---
[1] ...or should we harass physicians and biologists for their use of
the word "function"?
| |
| Daniel C. Wang 2004-05-04, 7:41 pm |
| {stuff deleted}
>
> Can you recommend some modern survey paper as a complement to that
> program? I would really like to grasp the issues you are trying to
> address, and what the central results are about.
http://citeseer.ist.psu.edu/cardelli97type.html
| |
| Matthias Blume 2004-05-04, 7:41 pm |
| Mario S. Mommer <m_mommer@yahoo.com> writes:
> Matthias Felleisen <matthias@ccs.neu.edu> writes:
>
> Well, this is a public forum, not a refereed scientific journal
> specialized on some obscure corner of CS.
And that makes it better how? In fact, it makes it worse. Using
confusing terminology in one of those refereed fora would be
recognized as such immediately and cause no further harm. The same is
not true for a newsgroup, so all the more it would make sense to
listen to those who try to explain what the established terminology in
the relevant scientific community is and /accept/ their explanation.
> If you wish to communicate with people of different backgrounds, you
> must accept the fact that there are different established
> terminologies[1].
No. That is not the only possible thing to do, and probably not the
best either. The other possibility is to explain to those with
different background what the established scientific vocabulary is and
means so that everybody is on the same page.
> It is you, BTW, and
> M. B., which raise that questions over terminology over and over
> again, simply by claiming that your use is the only correct one.
But if it /is/? What else can we do? :-)
[...]
> [1] ...or should we harass physicians and biologists for their use of
> the word "function"?
Not until they start to talk, in a belligerent tone, to
mathematicians, trying to "explain" to them that their use of the word
"function" is confusion and non-standard, and that they should prefix
it with the word "mathematical", even in conversations that started
with a question about "surjective functions" and "idempotency" (i.e.,
topics that clearly make sense only for the mathematical meaning).
This very thread is a great example of this phenomenon: The OP asked
about structural or name equivalence of types -- something that
clearly makes sense only if by "type" we mean "phrases of a language
of types" and not for "type = set of tagged values".
M. B.
| |
| Lauri Alanko 2004-05-04, 9:37 pm |
| In article <m1fzafre0v.fsf@tti5.uchicago.edu>,
Matthias Blume <find@my.address.elsewhere> wrote:
> This very thread is a great example of this phenomenon: The OP asked
> about structural or name equivalence of types -- something that
> clearly makes sense only if by "type" we mean "phrases of a language
> of types" and not for "type = set of tagged values".
"Clearly"? I can see a quite straightforward interpretation for tagged
values: Given
(define-struct foo (bar baz))
(define-struct quux (bar baz))
, what will
(quux? (make-foo 'fro 'bozz))
return?
Lauri Alanko
la@iki.fi
| |
| Matthias Blume 2004-05-04, 9:37 pm |
| Lauri Alanko <la@iki.fi> writes:
> In article <m1fzafre0v.fsf@tti5.uchicago.edu>,
> Matthias Blume <find@my.address.elsewhere> wrote:
>
> "Clearly"? I can see a quite straightforward interpretation for tagged
> values: Given
>
> (define-struct foo (bar baz))
> (define-struct quux (bar baz))
>
> , what will
>
> (quux? (make-foo 'fro 'bozz))
>
> return?
But this question _is_ talking about the type _language_ (i.e., here
the language of structure declarations)!
(The OP also explicitly mentioned R5RS which does not even have
DEFINE-STRUCT.)
Cheers,
Matthias
| |
| Bradd W. Szonye 2004-05-05, 12:45 am |
| > Matthias Blume wrote:
Anton van Straaten wrote:[color=darkred]
> I don't want to fight over words, but I am curious as to what terms
> are considered appropriate for the runtime value classification
> systems which most people (other than type theorists, apparently) know
> as "types". The term "tag" seems insufficiently specific - and rather
> implementation-centric, in any case, focusing on an aspect of the
> mechanism, rather than the overall concept being expressed.
That was my impression too, especially if you consider "in-between"
types like C++ objects, where part of the type is syntactic and part of
it is a run-time tag.
> Without alternative terms, there's little choice but to continue using
> well-established terms, and this can hardly be considered abuse of
> language.
Agreed. Especially in a Scheme newsgroup; R5RS refers to Scheme's
"tagged values" as "types."
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Bradd W. Szonye 2004-05-12, 9:12 pm |
| > Mario S. Mommer <m_mommer@yahoo.com> writes:
Matthias Blume wrote:[color=darkred]
> Not until they start to talk, in a belligerent tone, to
> mathematicians, trying to "explain" to them that their use of the word
> "function" is confusion and non-standard ....
That sounds a lot like what the other Matthias did, though. He started
to talk, in what sounded to me like a belligerent tone, to Schemers,
trying to "explain" to us that our use of the word "type" is confusing
and an "abuse of language."
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Blume 2004-05-12, 9:12 pm |
| "Bradd W. Szonye" <bradd+news@szonye.com> writes:
>
> Matthias Blume wrote:
>
> That sounds a lot like what the other Matthias did, though. He started
> to talk, in what sounded to me like a belligerent tone, to Schemers,
> trying to "explain" to us that our use of the word "type" is confusing
> and an "abuse of language."
The main difference is that he was right about it.
I could understand the uproad (a little bit) if there would at least
be something mildly interesting in the meaning of the word "type" as
Schemers understand it. But there isn't. There is nothing that
fundamentally sets it apart from (as I have explained) "computable
predicate". So its only purpose seems to be in providing fuel for
flames.
Question such as the one raised by the OP do not even make sense under
this interpretation. I have no idea why people insist on clinging to
the word "type" where it is not appropriate(*).
M.B.
(*) Actually, I do have a conjecture: Considering that the same people
always wind up in knots when someone calls Scheme "untyped", it must
by something like "type envy". Have to check with a psychologist
whether such a thing exists... :-)
| |
| Anton van Straaten 2004-05-12, 9:12 pm |
| Matthias Blume wrote:
> I could understand the uproad (a little bit) if there would at least
> be something mildly interesting in the meaning of the word "type" as
> Schemers understand it. But there isn't. There is nothing that
> fundamentally sets it apart from (as I have explained) "computable
> predicate". So its only purpose seems to be in providing fuel for
> flames.
Regardless of whether it's "interesting", there's a concept relating to
value classification in dynamically-checked languages which needs
terminology. For better or worse, the terms used in this context derive
from the term "type", precisely because of interpretations like that of
types as sets of values which you've just referred to in another post.
By contrast, there doesn't appear to be an existing body of terminology
surrounding "computable predicate", "total predicate" etc. in this context,
either in academia or anywhere else. Evidence to the contrary is welcome.
As a matter of interest, if you remove the word "syntactic" from the
original definition Felleisen gave for types, you get a perfect description
of the runtime interpretation of types as tagged values:
"Types: a discipline for enforcing abstraction. That is, a way to use FOO
and BAR as values of TypeFOO and TypeBAR so that someone [or] something
guarantees that FOO and BAR cannot flow into the same operation."
As a discipline for enforcing abstraction, syntactic types and tagged values
have much in common, even if the latter requires more manual work and is a
lot less statically tractable. Tags allow authentication of the "types" of
values, and allow abstraction boundaries to be enforced. It's this
commonality that has led to overloading of the term, and you can see
evidence of these origins in papers going back at least to the 1970's.
> Question such as the one raised by the OP do not even make sense
> under this interpretation. I have no idea why people insist on clinging
to
> the word "type" where it is not appropriate(*).
The OP  two of the meanings of the word "type". This has little
bearing on the appropriateness of the term in the context of
dynamically-checked languages. Felleisen's response was much broader than
that, describing all non-syntactic use of the word "type" as abuse.
I understand the desirability of avoiding confusion by defining separate
terms for distinct concepts. The problem I see here is that an attempt is
being made to proscribe a term without appropriate alternatives being
offered (see below). This seems almost Orwellian, and understandably
provokes a reaction on several levels, some of them merely pragmatic, as in
"OK, what should I say instead?", which is what I've been trying to ask.
You've kindly offered alternatives around the word "predicate" (computable,
total). But this doesn't appear to be a developed body of terminology with
precedents in this context. Exploring that terminology: we have
dynamically-checked languages. They use predicates to do dynamic checks of
values. What is the property they are checking for? Membership in a class.
Can we give this membership in a class a name? How about "type", for the
kinds of reasons covered above? No? OK, what then?
If you have an answer to the latter question, I'm sure the authors of HtDP
would like to hear it, because as I've pointed out, some of the language in
that book appears to be working around the lack of an appropriate term for
this concept.
Anton
| |
| Matthias Blume 2004-05-12, 9:12 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
> They use predicates to do dynamic checks of values. What is the
> property they are checking for? Membership in a class.
I'd call it membership in a /set/. And membership in a set is
membership in a set. Why invent another word for that? (And, of
course, if all sets are subsets of some universal set U, then
membership in a set is simply a total function from U to {0,1} --- a
predicate.)
> Can we give this membership in a class a name? How about "type", for the
> kinds of reasons covered above? No? OK, what then?
Set. (In mathematics, a function has a domain and a range, both of
which are sets.) A "dynamic type test" in Scheme is merely a set
membership test. This is why vanilla Scheme has such a restricted
collection of "types": set membership must be effectively computable
for all values.
[NB: Higher-order contracts weaken this constraint by (effectively)
only requiring recursive enumerability of the /complements/ of the
sets that contracts denote.]
Matthias
| |
| Anton van Straaten 2004-05-12, 9:12 pm |
| Matthias Blume wrote:
> "Anton van Straaten" <anton@appsolutions.com> writes:
>
>
> I'd call it membership in a /set/. And membership in a set is
> membership in a set. Why invent another word for that?
First, not all sets qualify for the role which "type" plays, so part of
what's wanted is a more specific term. But more importantly, there are many
contexts in which a more concise term is useful. Examples:
* "What type is that value?" vs. "What set is that value a member of?"
* "Dynamically-typed language" vs. "Dynamically set-membership-checked
language". At least the latter gives a better answer than Cardelli to
*what* is being dynamically checked ("good behavior"?!)
* "type-checking" vs. "set-membership checking". Related to this are
phrases like runtime type check, or runtime type information, which arise
even in languages which have crude syntactic type systems, like C or C++.
* a name for things like "integers", "strings", etc. We can talk about the
set of integers, but the term "type" is still useful here: we can say that a
value is of integer type, as opposed to that the value is a member of the
set of integers, for example. Saying that a value "is an integer" might be
fine in many situations, but there are other cases where we want to focus
more explicitly on the question of which set it is a member of, and what
kind of set that is (the kind we call a "type").
There are many more ways in which the term is used. Without roughly equally
convenient alternatives for all these usages, disputing the validity or
appropriateness of the terms used in these contexts is moot. It's
effectively saying "wouldn't it be nice if we had less overloaded
alternatives". That's a wish that applies to terminology throughout the
sciences.
> Set. (In mathematics, a function has a domain and a range, both of
> which are sets.) A "dynamic type test" in Scheme is merely a set
> membership test. This is why vanilla Scheme has such a restricted
> collection of "types": set membership must be effectively computable
> for all values.
Thanks. I used "class" mainly because I'd been gathering phrases from HtDP
for one of my other posts, and "class" was one of its more commonly used
terms, so was in my short-term cache.
Anton
| |
| Ray Blaak 2004-05-12, 9:12 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
[promoting the use of the term "type"]
Don't sweat it. The comp sci theory freaks can use the term "type" in
mathematically precise way.
The comp sci everyone-else freaks are quite used to the term "type" in the way
you are advocating.
As usual, language is highly context dependent, and humans are good at dealing
with that.
So, know the context, and if further precision is needed to make it clear how
you use a term, well, that's what adjectives were invented for: run-time type,
static type, syntactic type.
The various uses of "type" presented here are indeed well established. People
know what you mean, and communication of concepts is what is important.
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
rAYblaaK@STRIPCAPStelus.net The Rhythm has my soul.
| |
| Matthias Blume 2004-05-12, 9:12 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
> Matthias Blume wrote:
>
> First, not all sets qualify for the role which "type" plays, so part of
> what's wanted is a more specific term. But more importantly, there are many
> contexts in which a more concise term is useful. Examples:
>
> * "What type is that value?" vs. "What set is that value a member of?"
Well, the funny thing is, to be able to /ask/ that question, you have
to have a /naming scheme/ for these sets. Those names are, in fact, a
form of types.
> * a name for things like "integers", "strings", etc. We can talk about the
> set of integers, but the term "type" is still useful here:
There is the phrase "int" -- which is a type, and the set of integers
-- which is an interpretation of that phrase. The point is to not
confuse the two.
I know the difference between the two questions in my world, but I am
not sure what difference you are getting at when "checking types" and
"testing set membership" are precisely the same.
> we can say that a value is of integer type, as opposed to that the
> value is a member of the set of integers, for example.
> Saying that a value "is an integer" might be
> fine in many situations, but there are other cases where we want to focus
> more explicitly on the question of which set it is a member of, and what
> kind of set that is (the kind we call a "type").
I am not sure what kind of difference in meaning you are getting at
here. Both questions ask whether the value in question has some
property, and in your case the two properties seem to be exactly
identical.
> There are many more ways in which the term is used.
I can't think of a single one which has a well-defined meaning for
which there isn't already a good name. Yes, I can see that people use
"type" when they should have used "set". I sometimes catch myself
doing the same, and in certain situations there really is not that
much harm (e.g., in the "int" vs. "set of integers" case). But the
whole point of using types is to get away from those sets: sets are
big, often infinite, perhaps undecidable or otherwise hard to handle.
By using types, one can work things out mechanically (i.e.,
syntactically) without consulting the meaning of types.
> Without roughly equally convenient alternatives for all these
> usages, disputing the validity or appropriateness of the terms used
> in these contexts is moot.
Again, I still don't really know what "all these usages" are.
Keeping the distinction between types and their interpretations
straight is a matter of precision of speech. In mathematics, the
people who pay attention to precision of speech most closely are the
logicians. And programming languages are a form of logic. We should
at least try to not confuse levels, i.e., don't confuse a syntactic
phrase with its meaning in some model.
Matthias
| |
| Matthias Blume 2004-05-12, 9:12 pm |
| Ray Blaak <rAYblaaK@STRIPCAPStelus.net> writes:
> The various uses of "type" presented here are indeed well established. People
> know what you mean,
Not true, as the beginning of this very thread nicely demonstrates.
| |
| Ray Blaak 2004-05-12, 9:12 pm |
| Matthias Blume <find@my.address.elsewhere> writes:
> Ray Blaak <rAYblaaK@STRIPCAPStelus.net> writes:
>
>
> Not true, as the beginning of this very thread nicely demonstrates.
Are you seriously saying that in literature about lisp-like languages, the
terms "run-time type checking", "dynamic types", "the type of a value", are
not well established?
I have been encountering them since my very first programming 101 course, way
back when.
If you are only saying that it is easy to run into situations where there is
confusion among the readers, I will grant you that, especially on Usenet.
What I don't buy, however, is that the term "type" is somehow a kind of abuse.
Sure, the math freaks have dibs on its "real" meaning, especially in a formal
context, but in other comp sci contexts that "run-time" meaning is quite
common.
When someone demonstrates such confusion in a thread like this, instead of
hearing "ah, you are abusing the term", I would prefer to hear "ah, in this
situation the term is refering to blah blah blah, and as such your objections
do not apply...".
--
Cheers, The Rhythm is around me,
The Rhythm has control.
Ray Blaak The Rhythm is inside me,
rAYblaaK@STRIPCAPStelus.net The Rhythm has my soul.
| |
| Anton van Straaten 2004-05-12, 9:12 pm |
| Matthias Blume wrote:
> "Anton van Straaten" <anton@appsolutions.com> writes:
....
>
> Well, the funny thing is, to be able to /ask/ that question, you have
> to have a /naming scheme/ for these sets. Those names are, in fact,
> a form of types.
That's fine with me, and doesn't conflict with anything I'm saying. But
syntactic type theories don't seem to be happy unless variables are
annotated with their types, or the type of a variable can be deduced. By
the syntactic definition of type, if that's not possible, then you're not
dealing with type distinctions. But it's exactly at the point that types
become focused on variables instead of values, that the terminological
disconnect begins.
This goes back to the question of generality: there seems to be a broader
general concept here, of which syntactic types and "runtime types" can be
seen as two instances, although perhaps not in any metatheory that a
syntactic type theorist would be happy with. "Runtime types" may be a
theoretically uninteresting instance of this general concept, but they exist
in real languages (or interpretations of real languages), and they bear a
relationship to the syntactic kind of type.
>
> There is the phrase "int" -- which is a type, and the set of integers
> -- which is an interpretation of that phrase. The point is to not
> confuse the two.
I'm all for not confusing things. Using general terms like "set" doesn't
help avoid confusion, though, when by "set" you mean something more
specific, as in:
"a set which belongs to the collection of sets which a language uses to
enforce abstractions in a way similar to the way in which types are used in
languages with syntactic types."
That sentence could be reduced to the word "type", qualified by some
appropriate term like "dynamic" or "runtime".
> I know the difference between the two questions in my world, but I am
> not sure what difference you are getting at when "checking types" and
> "testing set membership" are precisely the same.
I can't, off the top of my head, provide a rigorous definition of a runtime
type, other than the implied definition above. Mapping from a syntactic
perspective, I would say that there's clearly an aspect which the programmer
manages implicitly - i.e. instead of explicitly annotating variables as
being of a particular type, one's mental model of a program incorporates
those annotations (ideally). From this perspective, dynamically-checked
languages seem woefully incomplete, and you might call the types in question
"imaginary types", "virtual types", or "incomplete types". Working with
such languages involves "manual type inference". I'm sure you're loving
this. ;)
However, there was a time in mathematics where "imaginary numbers" were
considered rather esoteric and of limited interest, although they later
turned out to be much more important. Type theory may be in a somewhat
similar place now. Current syntactic type theories are excellent as far as
they go, but the idea that the wilderness that lies beyond them is
uninteresting seems in conflict with the current practice of programming
languages - where if anything, use of dynamically-checked languages has been
increasing. That may be just because mainstream languages with friendly and
good syntactic type systems don't exist, but I'm not sure that's all there
is to it, even if you are. ;)
Here's a nice fuzzy question just to muddy things: will "strong AI" be
syntactically typed?
> I can't think of a single one which has a well-defined meaning for
> which there isn't already a good name.
You may be right, but I'd like to see papers or other work which uses this
non-"type" terminology, with respect to dynamically-checked languages, and
other than material which mentions dynamic issues in passing as part of a
treatment of syntactic typing. That would answer my question about how the
various different needs for terminology are addressed. If such material
doesn't exist, then we're really discussing reinventing the terminology,
which sounds like fun, but is a different discussion.
> Keeping the distinction between types and their interpretations
> straight is a matter of precision of speech. In mathematics, the
> people who pay attention to precision of speech most closely are the
> logicians. And programming languages are a form of logic. We should
> at least try to not confuse levels, i.e., don't confuse a syntactic
> phrase with its meaning in some model.
One way to do that is to recognize that we're talking about two different,
overloaded meanings of the same word.
The two meanings may be related in the sense of theories and models for
those theories, but that's not completely clear to me, since even if you
develop a language for Scheme's "types", you still aren't going to be
classifying the types of all Scheme variables - or if you do, you're
creating a different language. If you don't identify the types of the
variables, syntactic theories say you don't have types, afaict.
Anton
| |
| Anton van Straaten 2004-05-12, 9:12 pm |
| Ray Blaak wrote:
> When someone demonstrates such confusion in a thread like this,
> instead of hearing "ah, you are abusing the term", I would prefer
> to hear "ah, in this situation the term is refering to blah blah blah,
> and as such your objections do not apply...".
That's what I've been getting at, just in more excruciating detail.
Anton
| |
| Matthias Blume 2004-05-12, 9:12 pm |
| "Anton van Straaten" <anton@appsolutions.com> writes:
> Matthias Blume wrote:
> ...
>
> That's fine with me, and doesn't conflict with anything I'm saying. But
> syntactic type theories don't seem to be happy unless variables are
> annotated with their types, or the type of a variable can be deduced. By
> the syntactic definition of type, if that's not possible, then you're not
> dealing with type distinctions.
This is not true. You are now talking about /type systems/ or a
/typing discipline/, i.e., rules that assign types to terms of the
term language. Yes, to some of us types become a lot more interesting
in the context of such systems, but it is possible to consider types
without having a language that has (syntactic) typing rules. In fact,
if we only bothered to write down a set of names that get interpreted
as those sets of values that you think are Scheme's types, then we had
a type /language/ for Scheme (albeit an extremely primitive one). A
more interesting example is the Findler/Felleisen language of
higher-order contracts. Again, there are no typing rules, and types
(i.e., terms in the language of types) are used as a form of assertion
that gets checked at runtime instead.
> This goes back to the question of generality: there seems to be a broader
> general concept here, of which syntactic types and "runtime types" can be
> seen as two instances, although perhaps not in any metatheory that a
> syntactic type theorist would be happy with. "Runtime types" may be a
> theoretically uninteresting instance of this general concept, but they exist
> in real languages (or interpretations of real languages), and they bear a
> relationship to the syntactic kind of type.
Yes. But Scheme (vanilla Scheme, unlike, e.g., DrScheme) does not
have even this variety of types (although one can imagine adding it
trivially). In any case, type /tags/ are not types but merely an
implementation technique to efficiently perform membership tests in
the sets of values that types (given a suitable type language and its
interpretation) denote.
>
> I'm all for not confusing things. Using general terms like "set" doesn't
> help avoid confusion, though, when by "set" you mean something more
> specific, as in:
>
> "a set which belongs to the collection of sets which a language uses to
> enforce abstractions in a way similar to the way in which types are used in
> languages with syntactic types."
I don't know what you mean by "enforce abstraction" here. I see no
conceptual difference at all between SYMBOL? or INTEGER? on the one
side and (LAMBDA (x) (AND (SYMBOL? x) (INTEGER? x))) or (LAMBDA (x) (<
x 10)) on the other, and yet, the former are considered type tests
while the latter are not. My point is, the division of predicates
into type predicates and "other" predicates in Scheme is completely
arbitrary, and it has absolutely nothing to do with enforcement of
abstractions.
>
> I can't, off the top of my head, provide a rigorous definition of a runtime
> type, other than the implied definition above.
Sorry, I still don't know what that implied definition is.
> However, there was a time in mathematics where "imaginary numbers" were
> considered rather esoteric and of limited interest, although they later
> turned out to be much more important. Type theory may be in a somewhat
> similar place now.
I find this idea preposterous, to be extremely frank.
> Here's a nice fuzzy question just to muddy things: will "strong AI" be
> syntactically typed?
I don't even know what the question means, but I'll try to run it by
Dave McAllester one of these days and see what he thinks...
>
> One way to do that is to recognize that we're talking about two different,
> overloaded meanings of the same word.
No, we are not. Not until someone gives a definition of the "other"
meaning...
> The two meanings may be related in the sense of theories and models for
> those theories, but that's not completely clear to me, since even if you
> develop a language for Scheme's "types", you still aren't going to be
> classifying the types of all Scheme variables
As I said, that's not necessary for types to be types. Now you are
also asking for static typing rules, which are the next step, so to
speak.
> If you don't identify the types of the variables, syntactic theories
> say you don't have types, afaict.
Wrong.
Let me try to summarize it this way:
1. Types: terms of a certain language (the "type language")
2. Static typing: a set of rules (typing rules) which assign types (see 1.)
to expressions of the term language
2.1. Soundness: very roughly speaking: given an interpretation of types
as sets of values, the property that an expression of
type t (according to the typing rules) evaluates only
to values that are in the interpretation of t
This property can (and usually will) be characterized purely
syntactically by a combination of a subject reduction lemma and
a progress lemma. Using this approach one can prove soundness
without considering any particular semantic model.
3. Dynamic typing: an interpretation of types as sets of values
together with a runtime mechanism to test for (non-)membership in
those sets
So in all cases types are syntactic things. Important differences
between static and dynamic checking are characterized by the different
answers to these questions:
a) When does the checking take place?
b) Is a semantic model of types (i.e., an interpretation as sets of
values aka. predicates) required? | | |