Home > Archive > Scheme > May 2004 > Pierce, types, and Scheme
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]
| Author |
Pierce, types, and Scheme
|
|
| Bradd W. Szonye 2004-05-12, 9:12 pm |
| Earlier, Anton van Straaten noted that Pierce's /Types and Programming
Languages/ mentions "dynamic checking," but that it wasn't clear about
what's being checked. In particular, he got the impression that Pierce
defines types as purely static constructs, which would preclude the
possibility of dynamic *type* checking. I've been re-reading Pierce, and
I got a different impression.
First, see the section on "Ascription and Casting" in section 15.5,
specifically the discussion of downcasting to subtypes (pp. 194-196). It
shows that both (static) type rules and (dynamic) evaluation rules may
use type information.
Pierce gives a (static) type rule for simple downcasting, T-DOWNCAST:
type(context, t1, S)
-------------------------
type(context, t1 as T, T)
In English: If the term t1 is well-typed (it has some type S), then the
term "t1 as T" has type T.
He then gives a couple of (dynamic) evaluation rules. The first rule,
E-ASCRIBE, works like the C typecast operator:
v1 as T --> v1
This rule ignores the type information. In other words, the overall
system blindly ascribes the new type T to the expression. He then offers
another rule, E-DOWNCAST, that checks the cast at runtime:
type(null, v1, T)
-----------------
v1 as T --> v1
This rule only lets the system proceed if v1 actually has type T, which
implies that v1's type is dynamically checkable at runtime! However, the
system gets stuck if v1 doesn't have the right type. Pierce notes that
most languages address this by raising an exception or using a dynamic
type test. He offers a more complicated set of rules that essentially
say, "if t1 is in T, evaluate term t2 with t1 downcast to T; otherwise,
evaluate term t3; both t2 and t3 are of some type U."
C++ takes a slightly different approach. Its dynamic_cast operator uses
variants of T-DOWNCAST and E-DOWNCAST in conjunction with a second
evaluation rule for failed downcasts:
type(context, t1, S)
------------------------------------- [T-DYNAMIC-CAST]
type(context, dynamic_cast<T>(t1), T)
type(null, v1, T)
-------------------------- [E-DYNAMIC-CAST-OK]
dynamic_cast<T>(v1) --> v1
!type(null, v1, T)
---------------------------- [E-DYNAMIC-CAST-FAILED]
dynamic_cast<T>(v1) --> NULL
(Note that these rules only cover the application of dynamic_cast to
pointer and reference values.)
C++ dynamic casting actually works a lot like Scheme's type-checking
predicates. If casting succeeds, you get a true value equivalent to the
original value; if it fails, you get a false value (NULL).
Anton wrote (in e-mail):
> In other places, it almost seemed as though Pierce might deliberately
> be avoiding the issue: he suggests using "dynamically-checked" instead
> of "dynamically-typed" as a description of languages like Scheme, but
> he doesn't explicitly say what would be being checked.
As far as I can tell, he's talking about checking types. For example, on
page 2 he writes:
The word "static" is sometimes added explicitly -- we speak of a
"statically typed programming language," for example -- to
distinguish the sorts of compile-time analyses we are considering
here from the dynamic or latent typing found in languages such as
Scheme ..., where run-time type tags are used to distinguish
different kinds of structures in the heap. Terms like "dynamically
typed" are arguably misnomers and should probably be replaced by
"dynamically checked," but the usage is standard.
I believe that Pierce is just making a fine point about types, type
systems, and type checking. As the downcasting examples show, you can
check types both statically and dynamically, which implies that types
exist both at compile time and at run time. (Many typed languages, like
C, discard the type information before run time.) The types aren't
static or dynamic; the type checking is.
Pierce defines a "type system" as a particular kind of type checking:
A type system is a tractable syntactic method for proving the
absence of certain program behaviors by classifying phrases
according to the kinds of values they compute.
General type checking also uses classification to permit syntactic
analysis. According to Church's thesis, an unrestricted grammar has the
same expressive power as a Turing machine or a mu-recursive system.
Therefore, one could (hypothetically) express a Scheme program as an
unrestricted grammar, organized such that types and type checking are
syntactic rules. Unfortunately, that kind of grammar isn't amenable to
compile-time analysis.
However, you can separate general type checks into two groups: those
which are amenable to static, compile-time analysis, and those which
require dynamic checking at run time. For example, the dynamic_cast
example uses the static rule T-DYNAMIC-CAST and the dynamic rules
E-DYNAMIC-CAST-OK and E-DYNAMIC-CAST-FAILED. Pierce calls these groups
"type rules" and "evaluation rules." He defines "type system" to include
only the static "type rules."
Given Pierce's definition, it's oxymoronic to refer to a "dynamic type
system," because the dynamic rules are part of the evaluation system,
not part of the type system.
In conclusion: "Dynamically typed" suggests that the types or the type
system are somehow dynamic, but that's meaningless for types and
oxymoronic for type systems. It really means that the language uses
dynamic type /checking./ I think that's all Pierce is trying to say: The
phrase "dynamically typed" is somewhat misleading.
> Since types in Scheme don't match Pierce's definition, one could
> conclude that the dynamic checking must be of something other property
> which is not named in the book.
I think Scheme fits Pierce's model well enough: Scheme has a universal
supertype with many subtypes (pair, number, etc.). Most functions use an
operation similar to downcasting to dynamically check types. Pierce's
model may not be very /useful/ for Scheme, because the "type rules" are
trivial in a naive implementation. However, more sophisticated
implementations use type inference, implicit typing, type declarations,
etc., which make for a more useful type system.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Felleisen 2004-05-12, 9:12 pm |
| Bradd W. Szonye wrote:
> Earlier, Anton van Straaten noted that Pierce's /Types and Programming
> Languages/ mentions "dynamic checking," but that it wasn't clear about
> what's being checked. In particular, he got the impression that Pierce
> defines types as purely static constructs, which would preclude the
> possibility of dynamic *type* checking. I've been re-reading Pierce, and
> I got a different impression.
>
That's the correct section to work from.
> First, see the section on "Ascription and Casting" in section 15.5,
> specifically the discussion of downcasting to subtypes (pp. 194-196). It
> shows that both (static) type rules and (dynamic) evaluation rules may
> use type information.
Yeap, and nobody would ever object to that.
....
> Anton wrote (in e-mail):
>
>
>
> As far as I can tell, he's talking about checking types. For example, on
> page 2 he writes:
>
> The word "static" is sometimes added explicitly -- we speak of a
> "statically typed programming language," for example -- to
> distinguish the sorts of compile-time analyses we are considering
> here from the dynamic or latent typing found in languages such as
> Scheme ..., where run-time type tags are used to distinguish
> different kinds of structures in the heap. Terms like "dynamically
> typed" are arguably misnomers and should probably be replaced by
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> "dynamically checked," but the usage is standard.
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Pierce is a nice and polite guy.
>
> I believe that Pierce is just making a fine point about types, type
> systems, and type checking. As the downcasting examples show, you can
> check types both statically and dynamically, which implies that types
> exist both at compile time and at run time.
... which of course doesn't run counter the idea that type systems are a
syntactic disciplines, as you go on to quote:
> Pierce defines a "type system" as a particular kind of type checking:
>
> A type system is a tractable syntactic method for proving the
> absence of certain program behaviors by classifying phrases
> according to the kinds of values they compute.
>
>
> Given Pierce's definition, it's oxymoronic to refer to a "dynamic type
> system," because the dynamic rules are part of the evaluation system,
> not part of the type system.
>
> In conclusion: "Dynamically typed" suggests that the types or the type
> system are somehow dynamic, but that's meaningless for types and
> oxymoronic for type systems. It really means that the language uses
> dynamic type /checking./ I think that's all Pierce is trying to say: The
> phrase "dynamically typed" is somewhat misleading.
To be concrete, he says "arguably misnomers". See above.
>
>
> I think Scheme fits Pierce's model well enough: Scheme has a universal
> supertype with many subtypes (pair, number, etc.). Most functions use an
> operation similar to downcasting to dynamically check types. Pierce's
> model may not be very /useful/ for Scheme, because the "type rules" are
> trivial in a naive implementation. However, more sophisticated
> implementations use type inference, implicit typing, type declarations,
> etc., which make for a more useful type system.
Another way of doing Scheme, and that was roughly the underlying thesis of soft
typing that PLT explored while still at Rice and still explores to some extent
with MrFlow uses a universal datatype (going back to Church and Scott):
datatype TheSchemeType = tag1 of Number
| tag2 of Boolean
| tag3 of TheSchemeType list -> TheSchemeType
(* one could also have TheSchemeType list on the right, to accommodate all
functions *)
| tag4 of TheSchemeType list
and so on.
If you now carefully read the paragraph entitled "Variants" in the Ascription
section, you see that the evaluation rule checks the tag of the record. And so
apply becomes something like :
apply(f: TheSchemeType, args : TheSchemeType list)
case f of
tag3(true_function) => true_function(args)
else => raise NotAFunction(f)
In short, what you're checking are the tags of the variant but the apply
function is staticlly typed in the UNItype TheSchemeType.
Indeed, you can now write code over this unitype in a perfectly statically typed
language like ML and you can pretend that this is a Scheme program.
Thanks for reading up. -- Matthias
P.S. The R5RS denotational semantics comes from the same direction; it just
makes more things explicit (e.g., all context information such as the
environment, the store, the continuation).
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Bradd wrote:
Matthias Felleisen wrote:[color=darkred]
> Yeap, and nobody would ever object to that.
OK. I got a different impression from your "types vs tags" article.
[color=darkred]
> ... which of course doesn't run counter the idea that type systems are
> a syntactic disciplines, as you go on to quote ....
Right, although I think the word "syntactic" has caused some confusion
in this discussion. At one extreme, it could refer to an unrestricted
grammar where "syntactic analysis" and "running the program" are
essentially the same thing. At the other extreme, it might only refer to
the LL or LALR portion of the full grammar; compilers and undergraduate
compiler-construction courses tend to reinforce this view of syntax,
because they use different methods for checking "syntax" and "types." In
the middle, some folks use "syntactic methods" as a synonym for "static
methods."
I like Pierce's definition and explanation, because he draws a clear
boundary: "A type system is a tractable syntactic method ...." First,
this reminds the reader that type-checking is still syntactic, even if
you can't fully express it as an LL or LALR grammar. Second, he limits
type systems to tractable proof methods, which implies decidable static
analysis. This eliminates both extremes above.
Later, Pierce explains the difference between type systems and safety;
the former is a conservative, static approximation of the latter. Some
operations (e.g., array indexing and downcasting) require dynamic
checking for complete safety.
Could you please comment on these definitions, which I've inferred from
Pierce's text?
Safety: Absence of certain (undesirable) program behaviors.
Type: A set of computed values.
Typing: Classification of language elements according to type.
Dynamic checking: A run-time method for ensuring safety by value typing.
Type system: A compile-time method for proving safety by phrase typing.
According to these definitions, dynamic checking and type systems are
disjoint subsets of a broader "type checking" concept that uses value
classification to ensure safety. A language's full grammar includes both
evaluation rules (including dynamic checks), which specify how programs
behave at run time, and type rules, which permit static analysis of
program safety. Together, they provide static and dynamic type checking.
This terminology is a bit counterintuitive for me; I want to use "type
system" and "type rule" for the broader type-checking concept, and I
feel that the dynamic and static rules should have parallel, qualified
names. Here's a translation of "what makes intuitive sense to Bradd" to
"Pierce's terminology":
Bradd Pierce
-------------------------------------------------------------
Type system Types, type rules, and dynamic checks
Static type system Types and type rules
Dynamic type system Types and dynamic checks
Type rule Dynamic check or type rule
Static type rule Type rule
Dynamic type rule Dynamic check
I don't actually mind Pierce's terminology; it just clashes with my
intuitive ideas of which terms best fit the concepts.
> If you now carefully read the paragraph entitled "Variants" in the
> Ascription section ....
I plan to. Thanks for the example; I get the gist of it, and I suspect
that it'll make better sense once I finish my studying.
> Thanks for reading up.
Sure. I started reading /Types and Programming Languages/ a while back,
but I keep getting side-tracked by other interests and projects. I've
been slowly working my way through several texts now, including Pierce's
book, the Unicode standard, and SICP. The problem with having eclectic
interests is that it's tough to make progress on any one point. It
doesn't help that I don't have much experience with Pierce's notation
for rules, types, etc.; every time I pick up the book, I spend a lot of
time re-reading so that I can understand his formulae.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Neelakantan Krishnaswami 2004-05-12, 9:13 pm |
| In article <slrnc9vprk.mfj.bradd+news@szonye.com>, Bradd W. Szonye wrote:
>
> Could you please comment on these definitions, which I've inferred from
> Pierce's text?
>
> Safety: Absence of certain (undesirable) program behaviors.
Yep. Note that the definition of "safety" will vary from application
to application.
> Type: A set of computed values.
> Typing: Classification of language elements according to type.
> Dynamic checking: A run-time method for ensuring safety by value typing.
> Type system: A compile-time method for proving safety by phrase typing.
These three aren't right, though. A "type" is just a phrase generated
from the grammar of types. A "type system" is a way of associating a
type with a program phrase. Notice that for a given expression
language, you can have numerous possible combinations of type
languages and type systems.
Furthermore, having a type system -- a rule for associating phrases
from a type grammar with phrases from the expression grammar -- does
not by itself guarantee safety. (You can write down any old typing
rules you like, after all.) You need to give a safety proof using the
type system and the evaluation rules to find that whether a particular
type system is safe or not.
This safety proof is conventionally (a convention invented by Matthias
Felleisen and Andrew Wright, as a matter of fact), given as a pair of
preservation and progress lemmas. "Preservation" means that if you
evaluate a well-typed term, then what it evaluates to has the same
type. "Progress" means that a well-typed term is either a value, or it
can be evaluated further. Together, they mean evaluation is a "safe"
operation -- you can't get to an ill-typed term by evaluating a
well-typed one.
You can, given a particular type system, associate a set of closed
expressions with each type, but trying to associate a type only with
values isn't a general enough notion. For example, one of my hobbies
is trying to invent a type system ensuring that all well-typed
programs terminate (but is still reasonably expressive). If you
restricted "type" to only talk about values then this wouldn't make
any sense.
--
Neel Krishnaswami
neelk@cs.cmu.edu
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Bradd wrote:
Neelakantan Krishnaswami wrote:[color=darkred]
> Yep. Note that the definition of "safety" will vary from application
> to application.
Agreed, and thanks for the confirmation.
[color=darkred]
> These three aren't right, though. [I count four. -- Bradd]
I have some questions, then.
Pierce defines "type system" thus:
A type system is a tractable syntactic method for proving the
absence of certain program behaviors by classifying phrases
according to the kinds of values they compute.
Question #1: Do you accept this definition?
I tried to infer definitions for "safety" and "type" from this
definition and from some of Pierce's examples, and then I tried to
restate it as faithfully as I could in those terms.
For "safety" I took "the absence of certain program behaviors." For
"typing" I took "classifying <things> according to types." Then I
restated Pierce's definition of "type system" as:
A tractable syntactic method for proving safety by typing phrases.
This permits a parallel definition for dynamic checking:
A run-time (syntactic?) method for ensuring safety by typing values.
Question #2: Is this reasoning OK so far, or have I already gone astray?
That leaves the definition of "type." I had some trouble with that,
because I couldn't figure out how to describe it in a way that worked
both for static phrase types and for dynamic value types. Perhaps:
A kind of values computed by a program phrase.
... but that doesn't seem to work for dynamic checking.
> A "type" is just a phrase generated from the grammar of types. A "type
> system" is a way of associating a type with a program phrase ....
That seems to agree with Pierce's definition, except that he also
specifies classification based on computed values. Is that a problem
with his definition, a problem with my understanding of it, or something
else?
> Furthermore, having a type system -- a rule for associating phrases
> from a type grammar with phrases from the expression grammar -- does
> not by itself guarantee safety.
Right, although that is the major reasons for having a type system. It
doesn't guarantee safety, but it's a method for proving safety. (IIRC,
type systems are also useful for proving the safety of optimizations and
other transformations.)
> You can, given a particular type system, associate a set of closed
> expressions with each type, but trying to associate a type only with
> values isn't a general enough notion. For example, one of my hobbies
> is trying to invent a type system ensuring that all well-typed
> programs terminate (but is still reasonably expressive). If you
> restricted "type" to only talk about values then this wouldn't make
> any sense.
Hm, it doesn't seem too weird to me. In that case, the "kinds of values"
include stuff like "expressions that terminate." I dunno. I'm not sure
what exactly Pierce means by "kinds of values."
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Felleisen 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
> Bradd wrote:
>
>
>
> Neelakantan Krishnaswami wrote:
>
>
>
> Agreed, and thanks for the confirmation.
>
>
>
>
>
>
> I have some questions, then.
>
> Pierce defines "type system" thus:
>
> A type system is a tractable syntactic method for proving the
> absence of certain program behaviors by classifying phrases
> according to the kinds of values they compute.
>
> Question #1: Do you accept this definition?
That's too many things in one definition. Just use "... syntactic method for ...
classifying phrases according to the kinds of values they compute." Then you can
prove as a consequence that the following happens:
If P is a program and P is well-typed of type T, then one of three things is
possible
(1) P -->* Value of type T
(2) P loops forever
(3) P -->* Q and Q raises an exception in a well-specified, finite set
Read P as evaluates or reduces to.
> For "safety" I took "the absence of certain program behaviors."
As Milner said, "well-typed programs don't go wrong". That was a lie, a white
lie. It really means a type system lets you predict exactly what goes wrong and
when it prints 5 it means it doesn't interpret the bit patterns of a function
pointer as 5.
> For "typing" I took "classifying <things> according to types." Then I
> restated Pierce's definition of "type system" as:
>
> A tractable syntactic method for proving safety by typing phrases.
Try this. Say you have a set and some relations on it. Then you want to say what
is true and what is false about this set. You must have a language of theorems
(a syntax) to express statements. If you don't have a language, you can't even
express statements about the set and its relations. The statements are the
potential theorems. If you also have a system for classifying some statements as
provable and if you can meta-prove that all provable statements are *true* about
the set and the relations on the set, then the proof system (a system that
relates syntactic phrases) is sound and good.
In this spirit, types are theorems that predict what kind of values can show up
where. The above kind of theorem is the meta-proof that the relations between
phrases and types mean something good for the execution of the program. The
relations are the run-time actions.
>
> This permits a parallel definition for dynamic checking:
>
> A run-time (syntactic?) method for ensuring safety by typing values.
As we all know, when your set and your relations can express full-fledged
arithmetic (Peano), you cannot possibly find a proof system that can prove all
truths.
In the same spirit, you cannot find a type system that can prove (predict) all
possible behaviors. Example: the type systems that are around don't help you
with avoiding division by 0. Not even in ML. So division-by-zero is an element
of one of those well-specified exceptions.
So, to make sure that the type soundness theorem goes through, you have to add
checks that supplement type checking.
In my mind, and that's a paper I wrote with Robby Findler, a type system comes
with a contract system, which is a system of run-time checks that the language
performs to guarantee the type soundness system and a mechanism for blaming the
party that violates it.
People can refine type systems so that 0-division is recognizable in some cases.
They can do that for many other special cases. That's type systems research.
-- Matthias
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
Matthias Felleisen wrote:[color=darkred]
> That's too many things in one definition. Just use "... syntactic
> method for ... classifying phrases according to the kinds of values
> they compute." Then you can prove as a consequence that [a well-typed
> program will behave only in certain ways].
So the rationale (proving safety/soundness) isn't essential to the
definition, because you can prove it given the rest of the definition?
That makes sense. I can understand why Pierce included it, but I also
see why it isn't necessary.
You also omitted "tractable" from your paraphrase. That goes right to
the major point I'm  about.
Pierce strongly emphasizes that type systems are static analysis
methods. In the introduction to /Types and Programming Languages,/ he
contrasts type systems with the dynamic type checking in languages like
Scheme. The tractability requirement reinforces this contrast, because
it rules out undecidable "static methods" that are equivalent to running
the program.
However, on page 195, he introduces rules for a "dynamic type test"
operation with the syntax, "if v1 in T then x->t2 else t3." This
strongly resembles the Scheme type-testing idiom, (if (T? v1) t2 t3).
While the type-test syntax does have a compile-time typing rule, it's
primarily a run-time check.
I don't know how to resolve this seeming inconsistency. The dynamic
type-test rules obviously aren't amenable to static analysis. Are they
"syntactic"? Are they part of the type system? Or are they something
different? Your comments about division by zero and contract assertions
suggest that these run-time checks are a natural and necessary part of a
type system, but Pierce's introduction says just the opposite. Could you
please clarify this?
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Felleisen 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
> Bradd W. Szonye wrote:
>
>
>
> Matthias Felleisen wrote:
>
>
>
> So the rationale (proving safety/soundness) isn't essential to the
> definition, because you can prove it given the rest of the definition?
> That makes sense. I can understand why Pierce included it, but I also
> see why it isn't necessary.
>
> You also omitted "tractable" from your paraphrase. That goes right to
> the major point I'm about.
Pure oversight. If you read the rest of my message, I think that becomes clear.
>
> Pierce strongly emphasizes that type systems are static analysis
> methods. In the introduction to /Types and Programming Languages,/ he
> contrasts type systems with the dynamic type checking in languages like
> Scheme. The tractability requirement reinforces this contrast, because
> it rules out undecidable "static methods" that are equivalent to running
> the program.
>
> However, on page 195, he introduces rules for a "dynamic type test"
> operation with the syntax, "if v1 in T then x->t2 else t3." This
> strongly resembles the Scheme type-testing idiom, (if (T? v1) t2 t3).
> While the type-test syntax does have a compile-time typing rule, it's
> primarily a run-time check.
Another way of seeing this is that he invokes the type checker at run-time.
Remember that he uses a mostly syntactic evaluation framework. That makes it
difficult to see which is what. (It's like invoking eval or compile at run-time.)
But reality is -- evaluating (if (T? v) v (raise ...Exception)) is not a proof
in the proof system. It's a "truth check". [I am assuming that you have seen the
basics of logics for this to make sense: model + truth, proof +
statements(claims) + theorems.]
>
> I don't know how to resolve this seeming inconsistency. The dynamic
> type-test rules obviously aren't amenable to static analysis. Are they
> "syntactic"? Are they part of the type system? Or are they something
> different? Your comments about division by zero and contract assertions
> suggest that these run-time checks are a natural and necessary part of a
> type system, but Pierce's introduction says just the opposite. Could you
> please clarify this?
This is where pure type people and I go separate ways. I believe that such tests
are natural. They try hard to eliminate all of them. Their ultimate goal is to
make everything not just safe but type-safe (two different notions).
-- Matthias
| |
| Joe Marshall 2004-05-12, 9:13 pm |
| Matthias Felleisen <matthias@ccs.neu.edu> writes:
> As Milner said, "well-typed programs don't go wrong". That was a lie,
> a white lie.
A white lie?! It's a WHOPPER!
| |
| Anton van Straaten 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
> Earlier, Anton van Straaten noted that Pierce's /Types and Programming
> Languages/ mentions "dynamic checking," but that it wasn't clear about
> what's being checked. In particular, he got the impression that Pierce
> defines types as purely static constructs, which would preclude the
> possibility of dynamic *type* checking. I've been re-reading Pierce, and
> I got a different impression.
For the record, what I wrote was:
> 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?
In particular, I didn't say anything about "purely static constructs", and
that's not why I proposed the conclusion that I did. My logic stems from a
core issue in this discussion: in a syntactic type system, types are
associated with terms, and if you can't type terms, you don't have types.
In dynamically-typed languages, you can't or don't type terms, ergo you
don't have types -- or, "equivalently" (per Cardelli), you have a single
universal type.
Other than the introduction, I've seen nowhere in Pierce where he talks
about checking (of anything) in the context of dynamically-typed languages.
More generally, there doesn't seem to be any literature which talks about
this in ways that a syntactic type theorist would approve of, with the
possible exception of Findler & Felleisen on contracts (ICFP 2002, maybe
ECOOP 2004).
The dynamic checking that's necessary with syntactic type systems doesn't
have a lot to do with dynamic checking in dynamically-typed languages,
unless you take the view that these languages have a single universal type
which undergoes dynamic checking of its tags. These tags aren't types,
though, since they're not applied to terms in the language. Besides, this
is clearly a degenerate case, and indeed the unitype model is considered
equivalent to the language being "untyped", because a language with a single
type is "uninteresting" from a type perspective - all terms have the same
type. You can see an example of why it's uninteresting in the question that
started the original thread: a question about what form of type equivalence
used by Scheme is meaningless, since Scheme is, to use Felleisen's word,
un(i)typed.
In summary, I think it's safe to say that at best, Pierce neatly and
diplomatically dodges the issue of what property is being dynamically
checked. You could read it either way - a syntactic type theorist would
never be deluded that "types" are being checked, whereas a naive Schemer
(such as I) might conclude the opposite, not noticing that this entails
serious inconsistencies (which don't matter much until you try to apply
syntactic type terminology to dynamically-typed languages).
Underscoring my conclusion is that Cardelli in "Type Systems" is at least as
vague on this point, although a bit more explicit about deprecating the
notion of type as a runtime concept.
Anton
| |
| Matthias Blume 2004-05-12, 9:13 pm |
| Joe Marshall <jrm@ccs.neu.edu> writes:
> Matthias Felleisen <matthias@ccs.neu.edu> writes:
>
>
> A white lie?! It's a WHOPPER!
I think it was always meant to be tongue-in-ch . "Does not go
wrong", IIRC, refers to the style of operational semantics where there
is a special value called "wrong" that gets generated in certain
erroneous situations (which we usually call "type errors"). The proof
then shows that a well-typed program will never encounter "wrong",
which is where that famous sentence came from.
Matthias
| |
| Matthias Felleisen 2004-05-12, 9:13 pm |
| Matthias Blume wrote:
> Joe Marshall <jrm@ccs.neu.edu> writes:
>
>
>
>
> I think it was always meant to be tongue-in-ch. "Does not go
> wrong", IIRC, refers to the style of operational semantics where there
> is a special value called "wrong" that gets generated in certain
> erroneous situations (which we usually call "type errors"). The proof
> then shows that a well-typed program will never encounter "wrong",
> which is where that famous sentence came from.
>
> Matthias
Yes, the sentence is clearly a pun because the word "wrong" has a technical
meaning in Milner's paper (it's an element of the domain) but the other meaning
was dead serious. There is indeed a reason for that. If you type a language
without division, array access, or variant types, you simply can't express the
possibility that something can go wrong at run-time. Ever. So for reasonably
pure languages, the theorem is true.
Naturally, nobody can write practical programs in such languages, and therefore
those of us who work on and with Scheme or other (potentially safe) languages,
just blow off this quote/sentence. We shouldn't. (I have confronted Milner about
this and he's ready to admit that this is wrong.) Instead, we should always
throw C++, a typed language, back at the person who quotes this sentence and ask
him whether C++ is preferable to Scheme. If so, walk away.
-- Matthias, the
| |
| Anton van Straaten 2004-05-12, 9:13 pm |
| Matthias Felleisen wrote:
> Yes, ["well-typed programs don't go wrong"] is clearly a pun
> because the word "wrong" has a technical meaning in Milner's
> paper (it's an element of the domain) but the other meaning
> was dead serious. There is indeed a reason for that. If you
> type a language without division, array access, or variant types,
> you simply can't express the possibility that something can
> go wrong at run-time. Ever. So for reasonably pure languages,
> the theorem is true.
>
> Naturally, nobody can write practical programs in such languages,
> and therefore those of us who work on and with Scheme or other
> (potentially safe) languages, just blow off this quote/sentence.
> We shouldn't. (I have confronted Milner about this and he's ready
> to admit that this is wrong.) Instead, we should always throw C++,
> a typed language, back at the person who quotes this sentence
> and ask him whether C++ is preferable to Scheme. If so, walk away.
If the same is intended to apply to C, this seems to imply that we should
walk away from Cardelli, who wrote in "Type Systems":
"There is little doubt, though, that production code written in untyped
languages can be maintained only with great difficulty. From the point of
view of maintainability, even weakly checked unsafe languages are superior
to safe but untyped languages (e.g., C vs. LISP)."
Discuss... ;)
Anton
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
Anton van Straaten wrote:[color=darkred]
> For the record, what I wrote was:
>
> 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 ....
>
> In particular, I didn't say anything about "purely static constructs", and
> that's not why I proposed the conclusion that I did ....
Oops, sorry if I misunderstood you. I was actually paraphrasing a
different message (the mail you sent me off-group), where you wrote,
"[Pierce's] definitions all relate to types as a static syntactic
concept ...." Guess I got the wrong impression from that; my apologies.
> My logic stems from a core issue in this discussion: in a syntactic
> type system, types are associated with terms, and if you can't type
> terms, you don't have types ....
Based on Pierce's downcasting examples and Matthias Felleisen's
explanations, it looks like you can type and manipulate terms
dynamically. For example, in the evaluation rule E-DOWNCAST,
type(null, v1, T)
-----------------
v1 as T --> v1
the premise dynamically checks whether the term v1 is associated with
type T. If it has, it can apply the syntactic reduction below the line.
Conceptually, it invokes the type-checker at run time, much like using
Scheme EVAL. (Thanks to Matthias for this analogy; I hope I'm finally
understanding this correctly.) Of course, the implementation probably
pre-calculates the possible results of the syntactic manipulation; this
is just the abstract description of what happens.
As Matthias notes, most type-system advocates try to avoid these dynamic
checks, because they're not "tractable." A static analyzer can't prove
that the rule won't "go wrong" without effectively running the program,
which is generally undecidable.
> In dynamically-typed languages, you can't or don't type terms, ergo
> you don't have types -- or, "equivalently" (per Cardelli), you have a
> single universal type.
I suspect that some Scheme compilers do type terms as a part of flow
analysis and optimization. While vanilla Scheme doesn't have nominal
typing -- I think that's the right term -- it does have "subtype
polymorphism" and some idioms that could make implicit typing possible.
> Other than the introduction, I've seen nowhere in Pierce where he
> talks about checking (of anything) in the context of dynamically-typed
> languages.
As far as I can tell, a "dynamically-typed" object system is just a
special case of subtype polymorphism. It's similar to a Java program
where all interfaces accept Object parameters and all methods use
downcasting as "poor man's polymorphism."
To get the most out of a type system, I think you'd need to reduce that
ubiquitous casting, to make the subtypes visible at compile time. You
could use explicit declarations or contracts, or you could recognize
type-testing idioms as type rules. For example, given
(if (pair? p) t1 (error ...)),
a type system could ascribe the PAIR type to p in term t1.
> The dynamic checking that's necessary with syntactic type systems
> doesn't have a lot to do with dynamic checking in dynamically-typed
> languages, unless you take the view that these languages have a single
> universal type which undergoes dynamic checking of its tags.
That's how I see it: The universal type is either a variant record or
(my preferred interpretation so far) a supertype.
> These tags aren't types, though, since they're not applied to terms in
> the language.
While the tags aren't types, they are "type residue" -- stuff that the
compiler injects into objects so that the type-checker can inspect a
term's type at run time. It's the same concept as using a C++ vtable to
dynamically check a downcast; the vtable is a kind of type tag.
Going by Pierce's discussion of ascription and dynamic type tests, the
run-time system does relate types and terms. Injecting type tags into
objects is just a concrete representation of that abstraction, an
implementation technique. (Type gurus, please correct me if I'm wrong.)
> Besides, this is clearly a degenerate case, and indeed the unitype
> model is considered equivalent to the language being "untyped",
> because a language with a single type is "uninteresting" from a type
> perspective - all terms have the same type.
True -- unless you use extensions or idiomatic syntax to make the
subtypes/variants visible to the static type checker.
> In summary, I think it's safe to say that at best, Pierce neatly and
> diplomatically dodges the issue of what property is being dynamically
> checked ....
I disagree; the ascription rules clearly check types. They don't specify
how the run-time system finds the type information; they just assume
that it's available. In the running text (and in the Featherweight Java
case study), Pierce suggests type tags as one way to make the typing
relations available to the run-time system.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Matthias Felleisen wrote:
Bradd wrote:[color=darkred]
[color=darkred]
> Pure oversight. If you read the rest of my message, I think that
> becomes clear.
OK, that makes more sense! Thanks, that helps a lot. I think I'm getting
a handle on this now, but please correct me if I'm wrong.
> Another way of seeing [Pierce's dynamic type-testing rules] is that he
> invokes the type checker at run-time. Remember that he uses a mostly
> syntactic evaluation framework. That makes it difficult to see which
> is what. (It's like invoking eval or compile at run-time.)
Aha! I was actually thinking something along those lines: Since the
"dynamic type" is undecidable at compile time, the compiler postpones
some of the syntactic reduction to run time. In practice, there are only
a couple of possible reductions, so the compiler can just leave behind a
little "type residue" (e.g., a tag) and a branch. The run-time system
checks the tag and selects the appropriate "reduction."
> But reality is -- evaluating (if (T? v) v (raise ...Exception)) is not
> a proof in the proof system. It's a "truth check".
I think I understand you here, but I'm not sure because ...
> [I am assuming that you have seen the basics of logics for this to
> make sense: model + truth, proof + statements(claims) + theorems.]
.... I didn't understand what you mean by this. Are you talking about
logic in general, or a specific technique? Please clarify, because that
string of plusses doesn't look familiar at all.
[color=darkred]
> This is where pure type people and I go separate ways. I believe that
> such tests are natural. They try hard to eliminate all of them. Their
> ultimate goal is to make everything not just safe but type-safe (two
> different notions).
Right, I definitely got that impression from Pierce's book. For example,
he mentions the ongoing research to achieve statically tractable array
bounds-checking.
That didn't quite answer my question, though. I understand that the type
folks see dynamic type checking as undesirable but sometimes necessary.
What I'm not sure is whether they're part of the "type system." It looks
to me like they're just syntactic rules postponed to run time (or, as
you put it, EVAL for types). However, I'm not sure whether type theory
sees it the same way or whether my intuition is acting up again.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Anton van Straaten 2004-05-12, 9:13 pm |
| Matthias Felleisen wrote:
> -- Matthias, the
Using a term language which I call Googlogic, I have been able to prove that
the referent of the phrase "the Matthias" is context-dependent. As is often
the case with good proofs, this one has resulted in an additional unexpected
result, detailed below.
Without providing full details of the proof (the margins on this article
being rather small), I will mention that Googlogic accepts arbitrary
HTTP-encoded terms as input, and by applying a rather complex reduction
rule, produces an answer in the form of an ordered set of "links". These
links are references to entities which contain arbitrary semantic content.
This content must be interpreted appropriately for a given proof. In the
present proof, the linked content is rigorously checked for possible
referents of the input term. In addition, the present proof relies on a
variant of Googlogic known as "Lucky Googlogic", in which the first link in
the answer set is considered to be the final answer (this is known as the
"Millionaire" rule).
For the proof, a number of input terms of the form "the <context> Matthias"
were evaluated, with various values for <context> being supplied. The
answers were checked for referents of the input term. Selected results are
summarized below, with the token "--google-->" representing the sole
Googlogic reduction rule. Details of conversion from answer link to
referent are omitted below; experienced Googlogicians should have no problem
understanding how these answers were reached.
the Matthias --google--> MatthiasMedia
the semantics Matthias --google--> Matthias Felleisen
the SML Matthias --google--> Matthias Blume
It should be clear from the above that the meaning of "the Matthias" varies
depending on the specified context.
I mentioned an unexpected result. Applying Googlogic to the expression
"Felleisen Blume" resulted in a reference to a paper "An Investigation of
Contracts as Projections", by Findler, Blume, and Felleisen - a surprisingly
relevant paper which exposes a heretofore unknown (to me) connection between
the Matthiases in question.
It's interesting to note that the rather simplistic type system of Googlogic
belies the usefulness of the language. All terms have the type "link", i.e.
it is a unityped language. However, as with Scheme, the usefulness of the
results play out at a level above that of the type system of the core term
language.
Anton
| |
| Matthias Felleisen 2004-05-12, 9:13 pm |
| Anton van Straaten wrote:
> Matthias Felleisen wrote:
>
>
>
>
> If the same is intended to apply to C, this seems to imply that we should
> walk away from Cardelli, who wrote in "Type Systems":
>
> "There is little doubt, though, that production code written in untyped
> languages can be maintained only with great difficulty. From the point of
> view of maintainability, even weakly checked unsafe languages are superior
> to safe but untyped languages (e.g., C vs. LISP)."
>
> Discuss... ;)
Yes, Luca got that piece wrong. -- Matthias
| |
| Anton van Straaten 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
> Anton van Straaten wrote:
....
>
> I disagree; the ascription rules clearly check types.
Sure, but that's within the context of a language which has typed terms. As
Matthias B. has pointed out, in that context, there has to be a type
language. If you remove the type language, all bets are off and you'll have
to give new definitions for the way things work; for a start, the ascription
rules apply to terms, which doesn't fit the dynamically-typed context, in
general.
> They don't specify
> how the run-time system finds the type information; they just assume
> that it's available. In the running text (and in the Featherweight Java
> case study), Pierce suggests type tags as one way to make the typing
> relations available to the run-time system.
Right, but in Featherweight Java, terms are typed, even though some of them
have a supertype, like Object. The tags handle the exceptional cases. If
you make all cases exceptional, as a unityped language does, you lose the
point of the type system.
Pierce's definition of "type system" describes "proving the absence of
certain program behaviors"; Dynamic checking doesn't prove anything about
the absence of certain program behaviors. Rather, it alerts you to the
presence of errors in specific cases.
Cardelli's definition of "type system" is to "prevent the occurrence of
execution errors during the running of a program". An error resulting from
a dynamic check certainly doesn't qualify.
For both Pierce and Cardelli, then, a dynamically-typed system doesn't
qualify as having a "type system". As Matthias F. has pointed out, Pierce
is polite about this: he says that "Scheme is a safe language, even though
it has no static type system". Pierce seems to include the word "static"
here as a nod to common usage, as he's noted earlier when he says "The word
'static' is sometimes added explicitly". But in addition to the definition
quoted above, Pierce makes it clear that the type systems are fundamentally
static, e.g. "A type system can be regarded as providing a kind of static
approximation to the run-time behaviors of the terms in a program"; and
"Being static, type systems are also necessarily conservative".
If you accept that Pierce doesn't consider Scheme to have a type system,
static or otherwise, then a remaining question is whether it has types. But
in the context of syntactic types, as Matthias B. has pointed out, what can
that question possibly mean, if there is no type language, no way to express
within the language that a term has a particular type? Pierce doesn't
address this question, which is where my original observation came from. He
implies that Scheme has types, mainly by some use of common terminology, but
closer analysis doesn't support the implication.
> I suspect that some Scheme compilers do type terms as a part of
> flow analysis and optimization.
No doubt. But unless they report errors at compile time, thus demonstrating
that they can "(dis)prove the absence of certain program behaviors" and
"prevent the occurrence of execution errors", then they don't have a type
system in the Pierce|syntactic sense. If they do report such errors, then
they run the "risk" of not being standard Scheme, e.g. (if
<complex-but-true-expression> 666 (car 42)) is a valid Scheme program which
shouldn't be rejected at compile time.
Note that systems which use inferencing to give types to Scheme terms, e.g.
SoftScheme, MrSpidey, and MrFlow, all involve the use of a type language
which is not part of Scheme. The same goes for Robby's contract system.
Anton
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Anton van Straaten wrote:
Bradd wrote:[color=darkred]
[color=darkred]
> Sure, but that's within the context of a language which has typed
> terms. As Matthias B. has pointed out, in that context, there has to
> be a type language.
Scheme does have a type language, albeit an informal one. For example,
R5RS 6.2.2 "Exactness" informally specifies two types (exact and inexact
numbers) and their relationship to syntactic terms (numeric literals and
expressions).
The major problem with Scheme (from the type theory point of view) is
not the lack of a type language, but the fact that expressions get
promoted to and from a single universal type so freely that it's
generally impossible to use typing for soundness proofs. The types are
there, but there's no nominal typing or language discipline to check
them without running the program.
Now keep in mind that I'm the learner, not the master, so my conclusions
above may be incorrect, heretical, etc.
> [In] Featherweight Java, terms are typed, even though some of them
> have a supertype, like Object. The tags handle the exceptional cases.
> If you make all cases exceptional, as a unityped language does, you
> lose the point of the type system.
I agree! Scheme isn't exactly "unityped" -- its universal supertype does
have a few subtypes -- but it's close enough that your point still
stands. It fits the definition (see below) but misses the intent of a
type system.
However, it still does fit the defintion, which is why I say that the
"dynamic checking" really does check types, just as a downcast in FJ
checks types.
> Pierce's definition of "type system" describes "proving the absence of
> certain program behaviors"; Dynamic checking doesn't prove anything
> about the absence of certain program behaviors. Rather, it alerts you
> to the presence of errors in specific cases.
Elsewhere, Matthias Felleisen claimed that the "proof" portion of
Pierce's definition doesn't really belong, and I agree with him. It's
the usual reason for having a type system, and it's a consequence of
having a type system, but it isn't essential to the definition.
Of course, when your type language has only a few types that it
promiscuously promotes to a universal supertype, "well-typedness" is
either trivial or undecidable (depending on how you look at it), which
isn't very useful.
> Cardelli's definition of "type system" is to "prevent the occurrence
> of execution errors during the running of a program". An error
> resulting from a dynamic check certainly doesn't qualify.
Again, that sounds like the purpose of a type system, not the definition
of one. Scheme's vestigial type system definitely fails that purpose.
> If you accept that Pierce doesn't consider Scheme to have a type
> system, static or otherwise, then a remaining question is whether it
> has types.
I don't accept that, though. I don't actually know whether he considers
it to have a type system. However, I do know that Scheme's type-like
behavior is essentially the same as subtype polymorphism, which Pierce
does consider to be a type system. I also know that it fits the
definition that Matthias Felleisen gave elsewhere in this thread. Yes,
it's a degenerate case. Yes, it fails the main purpose of a type system.
However, since it fits the definition, I don't think Pierce was dodging
when he called it "dynamically checked."
> But in the context of syntactic types, as Matthias B. has pointed out,
> what can that question possibly mean, if there is no type language, no
> way to express within the language that a term has a particular type?
> Pierce doesn't address this question, which is where my original
> observation came from.
Scheme has an (informal and vestigial) type language, so as I see it
there is no way to address that question except to deny its premises. I
can't agree that Pierce dodged the question without first knowing
whether he even considered the question.
To put it another way, there's a difference between saying that Scheme
has a horrible, nigh-useless type system and saying that it has no type
system at all. If you believe the former, then "dynamically checked"
obviously refers to Scheme's (horrible, nigh-useless) type system. If
you believe the latter, then "dynamically checked" raises the question
you asked. I suspect, but have no way of knowing, that Pierce meant the
former.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Anton van Straaten 2004-05-12, 9:13 pm |
| Bradd W. Szonye wrote:
> Scheme does have a type language, albeit an informal one.
I mentioned this in an earlier post when I raised the idea of Scheme having
imaginary or virtual types. However, such "types" aren't syntactic, pretty
much by definition, which severely limits what can be done automatically
with the "type system"; i.e., it's not really a "system", so e.g. isn't
amenable to automatic processing.
> The major problem with Scheme (from the type theory point of view) is
> not the lack of a type language, but the fact that expressions get
> promoted to and from a single universal type so freely that it's
> generally impossible to use typing for soundness proofs. The types are
> there, but there's no nominal typing or language discipline to check
> them without running the program.
I think you're saying basically the same thing as I am, although drawing
different conclusions. Without the "nominal typing or language discipline
to check them without running the program", you don't have a type system.
>
> I agree! Scheme isn't exactly "unityped" -- its universal supertype does
> have a few subtypes -- but it's close enough that your point still
> stands. It fits the definition (see below) but misses the intent of a
> type system.
>
> However, it still does fit the defintion, which is why I say that the
> "dynamic checking" really does check types, just as a downcast in FJ
> checks types.
"Fit the definition" seems like a stretch to me - see below.
>
> Elsewhere, Matthias Felleisen claimed that the "proof" portion of
> Pierce's definition doesn't really belong, and I agree with him.
I agree with the spirit of Matthias' shortened definition, but I'm not sure
that he meant to eliminate the proof portion entirely - it looks as though
he saw the proof aspect as following from the definition. Here's what he
wrote:
> That's too many things in one definition. Just use "... syntactic method
> for ... classifying phrases according to the kinds of values they
> compute." Then you can prove as a consequence that the following
> happens:
>
> If P is a program and P is well-typed of type T, then one of three
> things is possible
> (1) P -->* Value of type T
> (2) P loops forever
> (3) P -->* Q and Q raises an exception in a well-specified, finite set
>
> Read P as evaluates or reduces to.
There are multiple problems with the above w.r.t. Scheme:
(a) Scheme has no "syntactic method for classifying phrases [in general]
according to the kinds of values they compute", so, Scheme doesn't fit
Felleisen's definition of a type system. You're taking the generous
position of noticing that some trivial terms, like literals, can be typed,
but this seems pretty "uninteresting", since these types don't propagate
through the language, which means you can't easily talk about types for a
non-trivial program P.
(b) As a result of (a), the ability to prove any of points (1) through (3)
above is severely compromised. Even though the proof aspect isn't part of
the revised definition, the fact that it no longer follows from the
definition indicates that the definition hasn't been met.
Point (b) hasn't stopped people from trying to prove things about Scheme
programs, but this requires at least introducing a formal type language.
Even then, for Scheme programs in general, the results tend not to be
pretty: you easily end up with terms having huge union types which are all
but useless. (This is not to disparage the work on MrSpidey and MrFlow; but
I'm a big fan of providing hints so that they don't have to infer
*everything*, and those hints are not standard Scheme.)
> Of course, when your type language has only a few types that it
> promiscuously promotes to a universal supertype, "well-typedness" is
> either trivial or undecidable (depending on how you look at it), which
> isn't very useful.
Right. At the extreme, "unityped" is considered equivalent to "untyped".
>
> I don't accept that, though. I don't actually know whether he considers
> it to have a type system.
As I pointed out, Pierce explicitly wrote that Scheme doesn't have a static
type system, and also wrote various things indicating that the type systems
he's describing are primarily static. Sticking to Pierce, as opposed to
Felleisen's trimmed-down definition, it seems clear that Pierce wouldn't
consider Scheme to have a type system.
> However, I do know that Scheme's type-like
> behavior is essentially the same as subtype polymorphism,
> which Pierce does consider to be a type system.
Again, the lack of typed terms makes the Scheme case fundamentally
different. I'm not saying that the connection you're seeing is invalid, but
it doesn't seem consistent with Pierce's perspective.
> I also know that it fits the
> definition that Matthias Felleisen gave elsewhere in this thread.
I'm thinking Matthias F. might now be starting to see the wisdom of the
additional qualification in Pierce's definition. ;) The problem with
claiming that Scheme has a "syntactic method for classifying phrases" is
that the method doesn't apply to most phrases.
> Yes, it's a degenerate case. Yes, it fails the main purpose of a type
system.
> However, since it fits the definition, I don't think Pierce was dodging
> when he called it "dynamically checked."
It doesn't fit *Pierce's* definition, though! What I'm talking about is
based on the self-consistency of what Pierce wrote. This is not intended as
a criticism of Pierce, btw -- Cardelli does more or less the same thing.
This situation seems symptomatic of how syntactic type theory in general
doesn't address questions of dynamic type, to the point that appropriate
terminology doesn't even seem to exist (Matthias B. says we should just talk
about sets).
>
> Scheme has an (informal and vestigial) type language so as I see it
> there is no way to address that question except to deny its premises. I
> can't agree that Pierce dodged the question without first knowing
> whether he even considered the question.
I think he would have had to be incredibly lucky to write it the way it's
written without making some egregious errors, if he hadn't considered that
question (or been very familiar with the approved ways of talking around
it). As it is, his introduction is inconsistent until you factor out the
acknowledged and implied concessions to common usage.
> To put it another way, there's a difference between saying that Scheme
> has a horrible, nigh-useless type system and saying that it has no type
> system at all.
Is there? What is that difference, in terms of consequences? Not that it
affects the case re Pierce, which is based on Pierce's own definitions.
Anton
| |
| Matthias Felleisen 2004-05-12, 9:13 pm |
| Sorry I lost track of the thread so I am replying to the initial response, even
though it belongs somewhere in the middle.
One of the things that seems to get lost in the discussion of Pierce's text book
is that when you check on the variant of a type or the subclassness of a class,
you already know (proved, established) the type of the phrase:
type TST = tag1 of Number | tag2 of Boolean | tag3 of (TST -> TST) ...
... (cond [(tag of x is tag1) (+ (strip-tag x) 1)] ...) ...
In this place, you know that x has type TST. What you don't know is whether it
also belongs to the set whose members carry tag1. In short, types are not just
sets of values. ]
The 1970s saw an extensive study of types as sets and this approach flunked. It
flunked denotationally (the natural ordering on function types is wrong); it
flunked logically (it's too classical and too inefficient); it flunked in some
ways operational semantics.
Someone (in the plain type community) should at some point collect those papers
and write a Pierce-style category monograph for his CMU tasks so that readers of
this newsgroup (and others) can easily and quickly find out what types are and
what sets of values are and why they are different.
-- Matthias
| |
| Anton van Straaten 2004-05-12, 9:13 pm |
| Matthias Felleisen wrote:
> One of the things that seems to get lost in the discussion of Pierce's
text book
> is that when you check on the variant of a type or the subclassness of a
class,
> you already know (proved, established) the type of the phrase:
>
> type TST = tag1 of Number | tag2 of Boolean | tag3 of (TST -> TST) ...
>
> ... (cond [(tag of x is tag1) (+ (strip-tag x) 1)] ...) ...
>
> In this place, you know that x has type TST. What you don't know is
whether it
> also belongs to the set whose members carry tag1. In short, types are not
just
> sets of values. ]
Thanks. This is what I was trying to say when I said the ascription rules
apply to typed terms, and if the terms aren't typed, "all bets are off".
> The 1970s saw an extensive study of types as sets and this approach
flunked. It
> flunked denotationally (the natural ordering on function types is wrong);
it
> flunked logically (it's too classical and too inefficient); it flunked in
some
> ways operational semantics.
>
> Someone (in the plain type community) should at some point collect those
papers
> and write a Pierce-style category monograph for his CMU tasks so that
readers of
> this newsgroup (and others) can easily and quickly find out what types are
and
> what sets of values are and why they are different.
That would be helpful.
The aspect of this discussion which I find interesting and which still seems
(to me) unresolved is that there seems intuitively to be a stronger
connection between the informal, programming language notion of "type" and
the syntactic notion than is captured by the model in which untyped
languages have a single universal type.
There's a reason for the lack of a better formal model here: for the most
part, I'd bet humans working with Scheme programs have a much better sense
of the types of the terms in their programs than an automatic inferencing
program is able to infer, without hints. IOW, Scheme programmers regularly
work with "real" types and typed terms, even though they do so in a language
that's formally considered untyped.
This is precisely why I really love the idea of a language like Scheme which
supports optional type annotations and type inferencing, but doesn't require
that all terms be typed or typeable, beyond a universal type. This language
would allow programmers to encode their already-existing knowledge of a
program's types into the program in a way that has useful consequences. As
a minor side effect, it would allow programmers in that language to
"legitimately" talk about types, in a way that has meaning to type
theorists, because the types of many terms will have been moved out of the
programmer's head and into the program's source.
Without such a language (does MrFlow do this yet?), all we can do is imagine
that we're programming in it, and map our imaginings onto the incomplete but
malleable vessel that is Scheme. When we talk about types, we're talking
about types in the language we would be programming in, if only those
language implementors would get off their... ;)
Anton
| |
| Display Name 2004-05-12, 9:13 pm |
|
"Anton van Straaten" <anton@appsolutions.com> wrote > This is precisely why
I really love the idea of a language like Scheme which
> supports optional type annotations and type inferencing, but doesn't
require
> that all terms be typed or typeable, beyond a universal type. This
language
> would allow programmers to encode their already-existing knowledge of a
> program's types into the program in a way that has useful consequences.
As
> a minor side effect, it would allow programmers in that language to
> "legitimately" talk about types, in a way that has meaning to type
> theorists, because the types of many terms will have been moved out of the
> programmer's head and into the program's source.
Some very interesting work that does exactly this is published in:
Soft Typing - Robert Cartwright, Mike Fagan
A Practical Soft Type System for Scheme - Andrew K. Wright, Robert
Cartwright
Soft Typing with Conditional Types - Aiken, Edward L. Wimmers, T. K.
Lakshman
Regards
Andre
| |
| Bradd W. Szonye 2004-05-12, 9:13 pm |
| Matthias Felleisen wrote:
Anton van Straaten wrote:[color=darkred]
> There are multiple problems with the above w.r.t. Scheme:
>
> (a) Scheme has no "syntactic method for classifying phrases [in
> general] according to the kinds of values they compute", so, Scheme
> doesn't fit Felleisen's definition of a type system.
There are significant subsets of the language that do, however. First,
consider a subset that omits LAMBDA, IF, and the equivalent derived
forms. R5RS informally specifies many type rules, including:
(cons t1 t2) : Pair (vector t ...) : Vector
t[n] : Exact for all n
----------------------
(+ t1 t2 ...) : Exact
t[n] : Number for all n t[n] : Inexact for some n
---------------------------------------------------
(+ t1 t2 ...) : Inexact
Next, consider a slightly larger subset that permits simple variable
binding (via LAMBDA in operator position, aka LET) but still omits
general abstraction and application. Variables assume the types of the
objects bound to them. (Sorry, I don't know the notation well enough to
write a rule for that.) Unless I've missed something, this subset still
has a significant and useful type system.
Unfortunately, once you introduce IF and general LAMBDA, the type system
becomes intractable, because most terms get promoted to the universal
Object type pretty quickly. As I said earlier, it's like a Java program
where all method arguments have the Object type, and that's poorly
suited for static analysis.
> You're taking the generous position of noticing that some trivial
> terms, like literals, can be typed, but this seems pretty
> "uninteresting", since these types don't propagate through the
> language, which means you can't easily talk about types for a
> non-trivial program P.
They do propagate, though, just not across arbitrary abstraction
barriers (function calls). Note that R5RS 1.3.3, Entry format, even
describes a notation for some of Scheme's type rules.
> (b) As a result of (a), the ability to prove any of points (1) through
> (3) above is severely compromised. Even though the proof aspect isn't
> part of the revised definition, the fact that it no longer follows
> from the definition indicates that the definition hasn't been met.
It still follows from the definition. It's just that rule #1 becomes
"P -->* value of type Object" unless you restrict the program to the
statically-typed subsets of Scheme. Or to put it another way, you can
prove interesting things about portions of Scheme programs, but static
analysis doesn't work too well on whole programs.
> As I pointed out, Pierce explicitly wrote that Scheme doesn't have a
> static type system, and also wrote various things indicating that the
> type systems he's describing are primarily static.
That's an apt description. However, there are a few other things that
mitigate it. First, when Pierce explains the tractability/efficiency
requirement, he concedes that some type systems are generally
undecidable. For example, he cites one of his own type systems (I forget
which) that behaves well in practice even though it's undecidable in the
general case. Second, his concrete examples of dynamic type checking are
substantially similar to Scheme type checking. Finally, I suspect that
Pierce's claims about Scheme are oversimplified. For example, he also
explicitly claims that correct Scheme interpreters are deterministic,
which veterans of the "LETREC wars" know to be untrue. That suggests to
me that he's unaware of or at least oversimplifying some finer points.
In any case, I don't have any problem with interpreting Pierce's remark
about "dynamically-checked" languages to mean "dynamically type-checked."
There's some weirdness about that, but it's close enough that I don't
really feel the need to tear it apart.
Bradd wrote:
[color=darkred]
> Is there? What is that difference, in terms of consequences?
If you accept the former, you don't have to quibble over what
"dynamically-checked language" means!
> Not that it affects the case re Pierce, which is based on Pierce's own
> definitions.
If Pierce's definition is loose enough to undecidable (but mostly
well-behaved) type systems, I figure it's loose enough to include
Scheme, at least for the purpose of figuring out what "dynamically
checked" means.
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Matthias Felleisen 2004-05-12, 9:13 pm |
| Anton van Straaten wrote:
> The aspect of this discussion which I find interesting and which still seems
> (to me) unresolved is that there seems intuitively to be a stronger
> connection between the informal, programming language notion of "type" and
> the syntactic notion than is captured by the model in which untyped
> languages have a single universal type.
>
> There's a reason for the lack of a better formal model here: for the most
> part, I'd bet humans working with Scheme programs have a much better sense
> of the types of the terms in their programs than an automatic inferencing
> program is able to infer, without hints. IOW, Scheme programmers regularly
> work with "real" types and typed terms, even though they do so in a language
> that's formally considered untyped.
Scheme programmers (can) superimpose their own type system on their programs.
These type systems can be ML-ish (see the early soft typing efforts in PLT while
still at Rice), it can be Flow-Analysis-ish (see the MrSpidey and MrFlow soft
typing efforts) and it can be OO in the sense of Java plus polymorphism.
How to Design Programs teach program design that way.
That's the technical reason why I am a Schemer.
> This is precisely why I really love the idea of a language like Scheme which
> supports optional type annotations and type inferencing, but doesn't require
> that all terms be typed or typeable, beyond a universal type. This language
> would allow programmers to encode their already-existing knowledge of a
> program's types into the program in a way that has useful consequences. As
> a minor side effect, it would allow programmers in that language to
> "legitimately" talk about types, in a way that has meaning to type
> theorists, because the types of many terms will have been moved out of the
> programmer's head and into the program's source.
See we think alike.
If you want to do this, you need to add Andrew Wright's SoftScheme typer and
Cormac's MrSpidey and Philippe's MrFlow as separate type systems as "buttons" to
DrScheme. Of course, in our world, we can then take the union of type safety not
just one notion. That's pretty powerful and costs a huge amount of energy and
money.
-- Matthias
| |
| Anton van Straaten 2004-05-12, 11:31 pm |
| Bradd W. Szonye wrote:
> R5RS informally specifies many type rules, including:
>
> (cons t1 t2) : Pair (vector t ...) : Vector
But in Scheme, the variables 'cons' and 'vector' might refer to anything.
Except in special cases, you can't know more without whole program analysis,
a module system, or similar. Since (most of) Scheme's terms are untyped, in
particular a term like (cons t1 t2) could have almost any type, as far as we
know statically.
This means that the type rules you were writing out need to take into
account what is known about the expected values of names at runtime,
including names like +, -, *, /... That doesn't leave much of a type
system.
Of course, you could argue that with whole program analysis, some static
analysis becomes possible, and that can still be considered standard Scheme,
aside from the need to formalize the type language. The various soft typing
systems demonstrate this point -- although from what I've seen, they also
demonstrate the drawbacks when the language doesn't include any type
annotations.
> Unfortunately, once you introduce IF and general LAMBDA, the type system
> becomes intractable, because most terms get promoted to the universal
> Object type pretty quickly. As I said earlier, it's like a Java program
> where all method arguments have the Object type, and that's poorly
> suited for static analysis.
In that example, Object plays the role of a unitype, which is considered
equivalent to untyped, which essentially means "no type system", since all
terms have the same type. In the syntactic view, the Object type is only a
valid way to support "types" when terms have non-trivial types.
> In any case, I don't have any problem with interpreting Pierce's remark
> about "dynamically-checked" languages to mean "dynamically type-checked."
> There's some weirdness about that, but it's close enough that I don't
> really feel the need to tear it apart.
That only works because you're not buying totally into the syntactic
definition of "type" - which is fine, but Pierce uses that definition.
This is exactly the hedging I'm talking about : if you're willing to overload
the term "type" or don't accept the limitations that the syntactic
definition imposes, then you can read Pierce and think that "dynamically
checked" means "dynamically type-checked". But if you accept the syntactic
notion of type as being the only one that matters (not that I'm saying it
is), then "dynamically checked" can't refer to *type* checking. It can
refer to checking of tags within the unitype, i.e. which set of values
within the type are being referred to, but then the syntactic typing refrain
is that sets of values aren't types.
> Bradd wrote:
>
>
> If you accept the former, you don't have to quibble over what
> "dynamically-checked language" means!
I'm not really quibbling over that, I'm pointing out the terminological game
that syntactic type theory texts, including Pierce and Cardelli, are
playing.
In another post, I've also pointed out a defense for dynamically typed
languages, which is that programmers do their own reasoning about the types
of terms, basically creating theories about types which are tested (although
not proved) by the dynamic checking. Of course, informal theories about
types don't really count any more than informal type languages do, from the
formal type theoretical perspective.
An interesting point raised by this perspective, though, is that if type
theorists really want to be precise about their terminology claims, they
should also attempt to disallow or redefine the word "checking" in the
dynamic context. In fact, they may have focused on the wrong word entirely:
"static type checking" is supposed to imply automatic proofs, whereas
"dynamic checking" involves no such thing. Why is the word "checking" used
in both cases? We should be talking about "type proofs" and "(set)
membership tests", or some such.
Now someone please stop the Matthiases before they go and report this
discovery on the TYPES list! Ah well, at the very least I'll expect Cardelli
to cite me in his next survey paper. ;o)
> If Pierce's definition is loose enough to undecidable (but mostly
> well-behaved) type systems, I figure it's loose enough to include
> Scheme, at least for the purpose of figuring out what "dynamically
> checked" means.
My point actually goes beyond Scheme - it applies to dynamically-typed
languages in general. Some of those may have slightly less vestigial type
systems than others, but I hardly think it affects the point: from the
formal type theory perspective, "dynamic checking" isn't checking "types"
when there's no formal type language, and no way to associate types from a
type language with terms in the object language. Minor exceptions to that
are only significant if they result in a language that supports a "static
approximation to the run-time behavior of the terms in a program" [Pierce].
Anton
| |
| William D Clinger 2004-05-13, 5:32 pm |
| Matthias Felleisen <matthias@ccs.neu.edu> wrote:
> Someone (in the plain type community) should at some point collect those papers
> and write a Pierce-style category monograph for his CMU tasks so that readers of
> this newsgroup (and others) can easily and quickly find out what types are and
> what sets of values are and why they are different.
That would certainly be worthwhile, but it is easy to demonstrate
that types cannot be synonymous with sets of values in Java and
in similar languages. Here is a (untested) demonstration.
public abstract class AList {
public static void main (String[] args) {
AList x = new NonemptyList ("one", new EmptyList());
NonemptyList y = (NonemptyList) x;
System.out.println ((x == y) ? "true" : "false");
System.out.println (y.car);
}
}
class EmptyList extends AList { }
class NonemptyList extends AList {
Object car;
AList cdr;
NonemptyList (Object car, AList cdr) {
this.car = car;
this.cdr = cdr;
}
}
This program prints "true", so x and y have the same value.
But if you write x.car instead of y.car, you'll get a type
error. Therefore types are not just sets of values in Java.
Will
| |
| Matthias Blume 2004-05-13, 6:32 pm |
| cesuraSPAM@verizon.net (William D Clinger) writes:
> Matthias Felleisen <matthias@ccs.neu.edu> wrote:
>
> That would certainly be worthwhile, but it is easy to demonstrate
> that types cannot be synonymous with sets of values in Java and
> in similar languages. Here is a (untested) demonstration.
>
> public abstract class AList {
> public static void main (String[] args) {
> AList x = new NonemptyList ("one", new EmptyList());
> NonemptyList y = (NonemptyList) x;
> System.out.println ((x == y) ? "true" : "false");
> System.out.println (y.car);
> }
> }
>
> class EmptyList extends AList { }
> class NonemptyList extends AList {
> Object car;
> AList cdr;
> NonemptyList (Object car, AList cdr) {
> this.car = car;
> this.cdr = cdr;
> }
> }
>
> This program prints "true", so x and y have the same value.
> But if you write x.car instead of y.car, you'll get a type
> error. Therefore types are not just sets of values in Java.
Do you mean "are not" or "cannot be interpreted as"? With the former
I wholeheartedly agree (of course), but for the latter I fail to see
how it follows from your (or Matthias F.'s, for that matter) example.
I also agree with a statement that says "types cannot always be
interpreted just as sets of values", but for many languages the
approach actually does work reasonably well.
Matthias B.
| |
| Bradd W. Szonye 2004-05-14, 1:32 pm |
| Bradd W. Szonye wrote:
Anton van Straaten wrote:[color=darkred]
> But in Scheme, the variables 'cons' and 'vector' might refer to anything.
Remember, this was in reference to a subset that forbids arbitrary
procedures, so any shadowing or reassignment of those names (e.g., with
SET!) is statically visible.
[color=darkred]
> That only works because you're not buying totally into the syntactic
> definition of "type" - which is fine, but Pierce uses that definition.
I do accept the syntactic definition; I just don't agree that
"syntactic" implies "static," as I explained in my followups to Ray
Dillinger and Will Clinger. I have no idea whether my position on this
is reasonable; I've been trying to get clarification from the local
"type gurus" with little luck (partly, it seems, because this issue is a
bit controversial).
> In another post, I've also pointed out a defense for dynamically typed
> languages, which is that programmers do their own reasoning about the
> types of terms, basically creating theories about types which are
> tested (although not proved) by the dynamic checking.
Yes, that was interesting. I don't have a coherent response yet, though,
so I've been putting off my followup.
> An interesting point raised by this perspective, though, is that if
> type theorists really want to be precise about their terminology
> claims, they should also attempt to disallow or redefine the word
> "checking" in the dynamic context. In fact, they may have focused on
> the wrong word entirely: "static type checking" is supposed to imply
> automatic proofs, whereas "dynamic checking" involves no such thing.
> Why is the word "checking" used in both cases?
As the great type gurus Page and Plant wrote,
There's a sign on the wall but she wants to be sure
'Cause you know sometimes words have two meanings
Hope this helps!
--
Bradd W. Szonye
http://www.szonye.com/bradd
| |
| Anton van Straaten 2004-05-14, 2:32 pm |
| Bradd W. Szonye wrote:
> Bradd W. Szonye wrote:
>
> Anton van Straaten wrote:
anything.[color=darkred]
>
> Remember, this was in reference to a subset that forbids arbitrary
> procedures, so any shadowing or reassignment of those names
> (e.g., with SET!) is statically visible.
Fine, but that means you're saying that there's a subset of Scheme which can
be said to have a syntactic type system, which is part of what I'm saying:
that to be able to say you have a type system in the syntactic sense, you
can't use unrestricted Scheme, you have to use types in type-like ways.
>
>
> I do accept the syntactic definition; I just don't agree that
> "syntactic" implies "static," as I explained in my followups to Ray
> Dillinger and Will Clinger. I have no idea whether my position on this
> is reasonable;
I'm having difficulty understanding the basis for your position, based on
the syntactic type literature. Here are some quotes, the first two from
Pierce and the rest from Cardelli's "Type Systems":
"A type system can be regarded as calculating a kind of static
approximation to the run-time behaviors of the terms in a program."
"Being static, type systems are necessarily also conservative..."
"The fundamental purpose of a type system is to prevent the occurence of
execution errors during the running of a program."
"Only program sources that comply with a type system should be considered
real programs of a typed language; the other sources should be discarded
before they are run."
"The checking process in [untyped] languages is called dynamic checking;
LISP is an example of such a language. These languages are strongly checked
even though they have neither static checking, nor a type system."
"The primary goal of a type system is to ensure language safety by ruling
out all untrapped errors in all program runs."
"Thus, the declared goal of a type system is usually to ensure good
behavior of all programs, by distinguishing between well typed and ill typed
programs."
So, you seem to be coming up with an interpretation of syntactic type theory
that's at odds with the literature. I do understand the technical argument
you're making, but I don't understand how you can claim that it's not in
conflict with the standard definitions.
> I've been trying to get clarification from the local "type gurus"
> with little luck (partly, it seems, because this issue is a bit
> controversial).
See my most recent response to Ray Dillinger in the "Bottom" thread. The
reason this issue is controversial is precisely because syntactic implies
static, at least in this context. When you're dealing with something you
can statically prove, like the fact that a term always has a particular type
(even if it's a union or superclass type), that's clearly syntactic. When
you're dealing with something that has to be checked at runtime, whether it
can be considered syntactic is woolier. Cardelli touches on this, talking
about dynamic tests in Simula67 and Modula-3:
"These languages are still (slightly improperly) considered statically
checked, partially because the dynamic type tests are defined on the basis
of the static type system. That is, the dynamic tests for type equality are
compatible with the algorithm that the typechecker uses to determine type
equality at compile time."
So the dynamic tests are considered kosher because of their connection to
the type system. Maybe this could be phrased more formally (just guessing
here) by saying that if the dynamic tests provide a faithful semantic model
for the syntactic type system, then they can be considered part of the
syntactic type system. Otherwise, they're just ad-hoc runtime behavior.
>
> As the great type gurus Page and Plant wrote,
>
> There's a sign on the wall but she wants to be sure
> 'Cause you know sometimes words have two meanings
>
> Hope this helps!
Thanks, that's about as authoritative as it gets!
Anton
| |
| Bradd W. Szonye 2004-05-14, 6:32 pm |
| Bradd wrote:
Anton van Straaten wrote:[color=darkred]
> I'm having difficulty understanding the basis for your position, based
> on the syntactic type literature. Here are some quotes, the first two
> from Pierce and the rest from Cardelli's "Type Systems":
>
> "A type system can be regarded as calculating a kind of static
> approximation to the run-time behaviors of the terms in a program."
>
> "Being static, type systems are necessarily also conservative..."
I believe that "static" and "approximation" and "conservative" are
consequences of the desire for tractable analysis, not a consequence of
the syntactic model.
Let's first consider what "static" and "dynamic" mean. "Static" refers
to the program itself, which does not change, and "dynamic" refers to
some aspect of its run-time behavior, which progresses from initial to
final conditions. Exactly what that means depends on the program's model
of computation. For example:
Model Static Dynamic
automata automaton state transition
grammar program text reduction
functional system of functions application
Static analysis, static methods, etc. refer to techniques that operate
on the static program text (or machine, or system of functions), rather
than observing the program's dynamic behavior. In principle, static
methods can do just about anything with the program, even simulate its
dynamic behavior or explore all possible control paths. However, that
generally exposes the static method to the program's halting and safety
issues, and we normally want to avoid that.
Therefore, when we say "static method," we often mean "tractable static
method." Also, note that "tractable method" implies "static method,"
because observation of dynamic behavior isn't generally tractable. It's
the tractability requirement that mandates conservative approxmation.
What of "syntactic," then? That merely states that type systems are
grammars, that they use the syntactic model of computation. Indeed, it
seems to me that types and type rules are syntactic abstractions
analogous to values and functions in the lambda caluclus. However,
there's nothing inherently static about syntactic methods; indeed, some
interpreters operate directly on ASTs.
I conclude that "static" follows from "tractable," not from "syntactic."
Since Pierce concedes later that tractability is closer to a very, very
strong guideline than an actual requirement, I also conclude that the
syntactic requirement is fundamental to the concept of types, but static
tractability is not. Therefore, it seems reasonable to me to apply type
concepts to "unityped" languages, even if those languages lack /useful/
type systems.
On to Cardelli's statements:
> "The fundamental purpose of a type system is to prevent the occurence
> of execution errors during the running of a program."
> "The primary goal of a type system is to ensure language safety by
> ruling out all untrapped errors in all program runs."
I see a difference between a language with a type system that fails this
fundamental purpose and a language with no type system at all.
> "Only program sources that comply with a type system should be
> considered real programs of a typed language; the other sources should
> be discarded before they are run."
This doesn't seem relevant, because we should also discard Scheme
programs that don't comply with Scheme's vestigial type system (and some
Scheme compilers even enforce that).
> "The checking process in [untyped] languages is called dynamic
> checking; LISP is an example of such a language. These languages are
> strongly checked even though they have neither static checking, nor a
> type system."
Pierce makes a comment like this too, and it strikes me as Orwellian
oversimplification. Note that Pierce oversimplifies in the other
direction when describing Scheme's safety; he incorrectly claims that
Scheme completely specifies the behavior of a correct interpreter. I'm
even more suspicious of the way Pierce and Cardelli both tolerate
dynamic checking and undecidable type rules in so-called "typed"
languages but (as I see it) arbitrarily use the same criteria to declare
some languages "untyped."
I'd rather say that Scheme is a "poorly-typed" language, because that
encourages examination of the type-system elements it does have. For
example, you can use types to reason about subprograms, even if whole
programs defy analysis. In contrast, by calling it "untyped" it seems to
me that they're sweeping this stuff under the rug.
> So, you seem to be coming up with an interpretation of syntactic type
> theory that's at odds with the literature.
No, it's at odds with one specific conclusion, that "unityped" languages
like Scheme are effectively "untyped," largely because Scheme /isn't/
unityped. It's true that Scheme programs generally defy static typing,
but there's more to it than that. However, Pierce's and Cardelli's
oversimplified descriptions ignore the "more to it," just as Pierce's
description of Scheme interpreters glossed over the whole order of
evaluation thing.
--
Bradd W. Szonye
http://www.szonye.com/bradd
|
|
|
|
|