Andreas Rossberg schrieb:
AFAICT, ADT describes a type whose values can only be accessed by a
certain fixed set of operations. Classes qualify for that, as long as
they provide proper encapsulation.
The first sentence is true if you associate a semantics (i.e. axioms)
with the operations.
Matthias Blume schrieb:
Erlang relies on a combination of purity, concurrency, and message
passing, where messages can carry higher-order values.
Data structures are immutable, and each computational agent is a
thread. Most threads consist a loop that explicitly passes state
around. It
Darren New [EMAIL PROTECTED] writes:
Andreas Rossberg wrote:
AFAICT, ADT describes a type whose values can only be accessed by a
certain fixed set of operations.
No. AFAIU, an ADT defines the type based on the operations. The stack
holding the integers 1 and 2 is the value (push(2, push(1,
Joe Marshall wrote:
Andreas Rossberg wrote:
Which is why this actually is a very bad example to chose for dynamic
typing advocacy... ;-)
Actually, this seems a *good* example. The problem seems to be that
you end up throwing the baby out with the bathwater: your static type
system
Paul Rubin schrieb:
It starts to look like sufficiently powerful static type systems are
confusing enough, that programming with them is at least as bug-prone
as imperative programming in dynamically typed languages. The static
type checker can spot type mismatches at compile time, but the
David Hopwood wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
I believe this example requires recursive types. It can also be expressed
in a gradual typing system, but possibly only using an unknown ('?') type.
ISTR that O'Caml at one point (before version
Paul Rubin wrote:
David Hopwood [EMAIL PROTECTED] writes:
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where
David Hopwood wrote:
Pascal Costanza wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
Pascal Costanza wrote:
David Hopwood wrote:
Pascal Costanza wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a
David Hopwood wrote:
Pascal Costanza wrote:
David Hopwood wrote:
Pascal Costanza wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically
Pascal Costanza [EMAIL PROTECTED] writes:
Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.
The whole point of static type systems is to make sure that
David Hopwood wrote:
(In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)
Not necessarily. You can replace the primitive eval by compile, which
delivers a function encapsulating the program, so you can check the type
of the
Matthias Blume wrote:
Pascal Costanza [EMAIL PROTECTED] writes:
Whether you consider something you cannot do with statically typed
languages a bad idea or not is irrelevant. You were asking for things
that you cannot do with statically typed languages.
The whole point of static type
Andreas Rossberg wrote:
David Hopwood wrote:
(In the case of eval, OTOH,
the erroneous code may cause visible side effects before any run-time
error occurs.)
Not necessarily. You can replace the primitive eval by compile, which
delivers a function encapsulating the program, so you can
Matthias Blume wrote:
How does this create such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the replace the code model
along with a translate the data where necessary at the time of
Pascal Costanza [EMAIL PROTECTED] writes:
And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed.
Maybe. The interesting question then is whether you can express the
kinds of dynamic updates that are relevant in practice. Because a
static
David Hopwood wrote:
Joe Marshall wrote:
The point is that there exists (by construction) programs that can
never be statically checked.
I don't think you've shown that. I would like to see a more explicit
construction of a dynamically typed [*] program with a given specification,
Marshall [EMAIL PROTECTED] writes:
Matthias Blume wrote:
How does this create such a problem? The problem is there in either
approach. In fact, I believe that the best chance we have of
addressing the problem is by adopting the replace the code model
along with a translate the data where
Matthias Blume wrote:
Pascal Costanza [EMAIL PROTECTED] writes:
And I am convinced that updating a running system in the style of,
e.g., Erlang, can be statically typed.
Maybe. The interesting question then is whether you can express the
kinds of dynamic updates that are relevant in
Andreas Rossberg wrote:
~/ ocaml -rectypes
Objective Caml version 3.08.3
# let rec blackhole x = blackhole;;
val blackhole : 'b - 'a as 'a = fun
The problem is, though, that almost everything can be typed once you
have unrestricted recursive types (e.g. missing
Marshall [EMAIL PROTECTED] writes:
Yes, an important question (IMHO the *more* important question
than the terminology) is what *programs* do we give up if we
wish to use static typing? I have never been able to pin this
one down at all.
Well, given Turing Machine equivalence...
I'd mention
Marshall [EMAIL PROTECTED] wrote:
Yes, an important question (IMHO the *more* important question
than the terminology) is what *programs* do we give up if we
wish to use static typing? I have never been able to pin this
one down at all.
You'd need to clarify what you mean by use static
Marshall [EMAIL PROTECTED] writes:
There are also what I call packaging issues, such as
being able to run partly-wrong programs on purpose so
that one would have the opportunity to do runtime analysis
without having to, say, implement parts of some interface
that one isn't interested in
Chris Smith schreef:
So it seems to me that we have this ideal point at which it is
possible to write all correct or interesting programs, and impossible
to write buggy programs.
I think that is a misconception. Even at the idealest point it will be
possible (and easy) to write buggy
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs are straightforwardly expressible.
In a
Ketil Malde wrote:
Marshall [EMAIL PROTECTED] writes:
There are also what I call packaging issues, such as
being able to run partly-wrong programs on purpose so
that one would have the opportunity to do runtime analysis
without having to, say, implement parts of some interface
that one
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs are straightforwardly
On Mon, 26 Jun 2006 13:02:33 -0600, Chris Smith [EMAIL PROTECTED]
wrote:
George Neuner gneuner2/@comcast.net wrote:
I worked in signal and image processing for many years and those are
places where narrowing conversions are used all the time - in the form
of floating point calculations
Ketil Malde [EMAIL PROTECTED] writes:
Marshall [EMAIL PROTECTED] writes:
There are also what I call packaging issues, such as
being able to run partly-wrong programs on purpose so
that one would have the opportunity to do runtime analysis
without having to, say, implement parts of some
Chris F Clark wrote:
Very impressive. It looks right to me and simple enough to
understand. I must find the time to learn a modern FP language. Can
you write a fold for this that prints the data as a binary tree of
triples? I have to believe it isn't that hard
{- Refactoring this as a
Marshall wrote:
Yes, an important question (IMHO the *more* important question
than the terminology) is what *programs* do we give up if we
wish to use static typing? I have never been able to pin this
one down at all.
It would depend on the type system, naturally.
It isn't clear to me
The C++ type system is Turing complete, although in practical terms
it limits how much processing power it will spend on types at
compile time.
I think templates only have to expand to seven levels, so you are
severely limited here.
You can adjust the iteration-depth. However, as
Joe Marshall wrote:
Marshall wrote:
Yes, an important question (IMHO the *more* important question
than the terminology) is what *programs* do we give up if we
wish to use static typing? I have never been able to pin this
one down at all.
It would depend on the type system, naturally.
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs are
George Neuner gneuner2/@comcast.net wrote:
We're talking at cross purposes. I'm questioning whether a strong
type system can be completely static as some people here seem to
think. I maintain that it is simply not possible to make compile time
guarantees about *all* runtime behavior and that,
Dr.Ruud [EMAIL PROTECTED] wrote:
So it seems to me that we have this ideal point at which it is
possible to write all correct or interesting programs, and impossible
to write buggy programs.
I think that is a misconception. Even at the idealest point it will be
possible (and easy) to
David Hopwood wrote:
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
Joe Marshall wrote:
Marshall wrote:
Yes, an important question (IMHO the *more* important question
than the terminology) is what *programs* do we give up if we
wish to use static typing? I have never been able to pin this
one down at all.
It would depend on the type system, naturally.
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
David Hopwood wrote:
Marshall wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed
David Hopwood ...nospamuk wrote:
A good debugger is invaluable regardless of your attitude
to type systems.
I found that certain language features help greatly in pinning
the errors, when programming in my own impure fp language
(PILS).
Originally, I implemented a single-stepping debugger
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs are straightforwardly
Marshall wrote:
Joe Marshall wrote:
Marshall wrote:
It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages. It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).
Joe Marshall wrote:
It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages. It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).
Looking back in comp.lang.lisp, I
Marshall wrote:
Joe Marshall wrote:
Looking back in comp.lang.lisp, I see these examples:
(defun noisy-apply (f arglist)
(format t I am now about to apply ~s to ~s f arglist)
(apply f arglist))
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
But
Pascal Costanza wrote:
David Hopwood wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
In a statically typed language that has a dynamic type, all
dynamically typed programs
QCD Apprentice wrote:
Joe Marshall wrote:
Marshall wrote:
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
Certainly! As soon as you can reflect on the type system you can
construct
George Neuner wrote:
That was interesting, but the authors' method still involves runtime
checking of the array bounds. IMO, all they really succeeded in doing
was turning the original recursion into CPS and making the code a
little bit clearer.
Hmm. There is a comparison in both the
Pascal Costanza [EMAIL PROTECTED] wrote:
You can ignore the #'. In Scheme this as follows:
(define blackhole (argument)
blackhole)
It just means that the function blackhole returns the function blackhole.
So, in other words, it's equivalent to (Y (\fa.f)) in lambda calculus,
where \
Joe Marshall wrote:
It isn't clear to me which programs we would have to give up, either.
I don't have much experience in sophisticated typed languages. It is
rather easy to find programs that baffle an unsophisticated typed
language (C, C++, Java, etc.).
Looking back in comp.lang.lisp, I
David Hopwood wrote:
Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
forall a . a - #'blackhole.
David Hopwood wrote:
Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
forall a . a - #'blackhole.
Joe Marshall wrote:
David Hopwood wrote:
Joe Marshall wrote:
(defun blackhole (argument)
(declare (ignore argument))
#'blackhole)
This is typeable in any system with universally quantified types (including
most practical systems with parametric polymorphism); it has type
forall a . a -
David Hopwood [EMAIL PROTECTED] writes:
Note that I'm not claiming that you can check any desirable property of
a program (that would contradict Rice's Theorem), only that you can
express any dynamically typed program in a statically typed language --
with static checks where possible and
On Sun, 25 Jun 2006 20:11:22 +0200, Anton van Straaten
[EMAIL PROTECTED] wrote:
[EMAIL PROTECTED] wrote:
In this context, the term latently-typed language refers to the
language that a programmer experiences, not to the subset of that
language which is all that we're typically able to
Chris Smith wrote:
What makes static type systems interesting is not the fact that these
logical processes of reasoning exist; it is the fact that they are
formalized with definite axioms and rules of inference, performed
entirely on the program before execution, and designed to be entirely
John Thingstad wrote:
On Sun, 25 Jun 2006 20:11:22 +0200, Anton van Straaten
[EMAIL PROTECTED] wrote:
[EMAIL PROTECTED] wrote:
...
\sarcasm One step further, and somebody starts calling C a latently
memory-safe language, because a real programmer knows that his code
is in a safe
Joachim Durchholz wrote:
Anton van Straaten schrieb:
Marshall wrote:
Can you be more explicit about what latent types means?
Sorry, that was a huge omission. (What I get for posting at 3:30am.)
The short answer is that I'm most directly referring to the types in
the programmer's
Rob Thorpe [EMAIL PROTECTED] writes:
I think statements like this are confusing, because there are
different interpretations of what a value is.
But I mean the value as the semantics of the program itself sees it.
Which mostly means the datum in memory.
I don't agree with that. Generally,
Anton van Straaten [EMAIL PROTECTED] wrote:
I'm not trying to call programmer reasoning in general a type system.
I'd certainly agree that a programmer muddling his way through the
development of a program, perhaps using a debugger to find all his
problems empirically, may not be reasoning
Chris Smith [EMAIL PROTECTED] writes:
I've since abandoned any attempt to be picky about use of the word
type. That was a mistake on my part. I still think it's legitimate
to object to statements of the form statically typed languages X, but
dynamically typed languages Y, in which it is
Chris Smith [EMAIL PROTECTED] writes:
Joachim Durchholz [EMAIL PROTECTED] wrote:
Assume a language that
a) defines that a program is type-correct iff HM inference establishes
that there are no type errors
b) compiles a type-incorrect program anyway, with an establishes
rigorous semantics
Anton van Straaten [EMAIL PROTECTED] writes:
But a program as seen by the programmer has types: the programmer
performs (static) type inference when reasoning about the program, and
debugs those inferences when debugging the program, finally ending up
with a program which has a perfectly good
Gabriel Dos Reis wrote:
[EMAIL PROTECTED] writes:
| think that it is too relevant for the discussion at hand. Moreover,
| Harper talks about a relative concept of C-safety.
Then, I believe you missed the entire point.
I think the part of my reply you snipped addressed it well enough.
Matthias Blume wrote:
I agree with Bob Harper about safety being language-specific and all
that. But, with all due respect, I think his characterization of C is
not accurate.
[...]
AFAIC, C is C-unsafe by Bob's reasoning.
Agreed.
Of course, C can be made safe quite easily:
Define a
David Hopwood [EMAIL PROTECTED] writes:
Matthias Blume wrote:
I agree with Bob Harper about safety being language-specific and all
that. But, with all due respect, I think his characterization of C is
not accurate.
[...]
AFAIC, C is C-unsafe by Bob's reasoning.
Agreed.
Of course, C can
Marshall wrote:
I stand corrected: if one is using C and writing self-modifying
code, then one *can* zip one's pants.
Static proofs notwithstanding, I'd prefer a dynamic check just prior to
this operation.
I want my code to be the only self-modifying thing around here.
--
David Hopwood wrote:
Joe Marshall wrote:
I do this quite often. Sometimes I'll develop `in the debugger'. I'll
change some piece of code and run the program until it traps. Then,
without exiting the debugger, I'll fix the immediate problem and
restart the program at the point it
On Sun, 25 Jun 2006 14:28:22 -0600, Chris Smith [EMAIL PROTECTED]
wrote:
George Neuner gneuner2/@comcast.net wrote:
Undecidability can always be avoided by adding annotations, but of
course that would be gross overkill in the case of index type widening.
Just what sort of type annotation
George Neuner gneuner2/@comcast.net wrote:
On Sun, 25 Jun 2006 14:28:22 -0600, Chris Smith [EMAIL PROTECTED]
wrote:
George Neuner gneuner2/@comcast.net wrote:
Undecidability can always be avoided by adding annotations, but of
course that would be gross overkill in the case of index type
Andrew McDonagh schrieb:
Joachim Durchholz wrote:
Chris Smith schrieb:
Joachim Durchholz [EMAIL PROTECTED] wrote:
Sorry, I have to insist that it's not me who's stretching terms here.
All textbook definitions that I have seen define a type as the
set/operations/axioms triple I mentioned
Darren New schrieb:
Marshall wrote:
Also: has subtyping polymorphism or not, has parametric polymorphism or
not.
And covariant or contravariant.
That's actually not a design choice - if you wish to have a sound type
system, all input parameters *must* be contravariant, all output
Anton van Straaten schrieb:
Joachim Durchholz wrote:
Anton van Straaten schrieb:
There's a close connection between latent types in the sense I've
described, and the tagged values present at runtime. However, as
type theorists will tell you, the tags used to tag values at runtime,
as
I wrote:
These informal systems, which may not prove what they claim to prove
are my concept of a type system.
Chris Smith [EMAIL PROTECTED] replied:
Okay, that works. I'm not sure where it gets us, though
Ok, we'll get there. First, we need to step back in time, to when there
was
Joachim Durchholz wrote:
That's actually not a design choice
It's certainly a choice you can get wrong, as you say. ;-)
I mean, if without runtime safety is a choice, I expect picking the
wrong choice here can be. :-)
--
Darren New / San Diego, CA, USA (PST)
Native Americans used
Chris F Clark [EMAIL PROTECTED] wrote:
Ok, we'll get there. First, we need to step back in time, to when there
was roughly algol, cobol, fortran, and lisp. Back then, at least as I
understood things, there were only a few types that generally people
understood integer, real, and (perhaps)
Chris F Clark wrote:
Thus, as we traverse a list, the first element might be an integer,
the second a floating point value, the third a sub-list, the fourth
and fifth, two more integers, and so on. If you look statically at
the head of the list, we have a very wide union of types going by.
George Neuner wrote:
I can know that my conversion of floating point to integer is going to
produce a value within a certain range ... but, in general, the
compiler can't determine what that range will be. All it knows is
that a floating point value is being truncated and the stupid
I wrote:
The important thing is the dynamicism of lisp allowed one to write
polymorphic programs, before most of us knew the term.
Chris Smith [EMAIL PROTECTED] writes:
Sure. In exchange for giving up the proofs of the type checker, you
could write all kinds of programs. To this day, we
Greg Buchholz [EMAIL PROTECTED] writes:
Chris F Clark wrote:
Thus, as we traverse a list, the first element might be an integer,
the second a floating point value, the third a sub-list, the fourth
and fifth, two more integers, and so on. If you look statically at
the head of the list,
Chris F Clark wrote:
And to me the question is what kinds of types apply to these dynamic
programs, where in fact you may have to solve the halting problem to
know exactly when some statement is executed. I expect that some
programs have type signatures that exceed the expressibility of any
Chris F Clark [EMAIL PROTECTED] wrote:
And to me the question is what kinds of types apply to these dynamic
programs, where in fact you may have to solve the halting problem to
know exactly when some statement is executed.
Yes, I believe (static) type systems will always end up approximating
On 22 Jun 2006 08:42:09 -0700, [EMAIL PROTECTED] wrote:
Darren New schrieb:
I'm pretty sure in Pascal you could say
Type Apple = Integer; Orange = Integer;
and then vars of type apple and orange were not interchangable.
No, the following compiles perfectly fine (using GNU Pascal):
program
David Hopwood wrote:
But since the relevant feature that the languages in question possess is
dynamic tagging, it is more precise and accurate to use that term to
describe them.
So you're proposing to call them dynamically-tagged languages?
Also, dynamic tagging is only a minor help in this
Marshall wrote:
Chris F Clark wrote:
I'm particularly interested if something unsound (and perhaps
ambiguous) could be called a type system. I definitely consider such
things type systems.
I don't understand. You are saying you prefer to investigate the
unsound over the sound?
The
Marshall wrote:
This means that there's a sense in which the language that the
programmer programs in is not the same language that has a formal
semantic definition. As I mentioned in another post, programmers are
essentially mentally programming in a richer language - a language which
George Neuner schrieb:
The point is really that the checks that prevent these things must be
performed at runtime and can't be prevented by any practical type
analysis performed at compile time. I'm not a type theorist but my
opinion is that a static type system that could, a priori, prevent
Dimitri Maziuk schrieb:
That is the basic argument in favour of compile time error checking,
extended to runtime errors. I don't really care if it's the compiler
or runtime that tells the luser your code is broken, as long as it
makes it clear it's *his* code that's broken, not mine.
You can
[EMAIL PROTECTED] schrieb:
Joachim Durchholz wrote:
A type is the encoding of these properties. A type
varying over time is an inherent contradiction (or another abuse of the
term type).
No. It's just a matter of definition, essentially.
E.g. in Smalltalk and Lisp, it does make sense to
Chris F Clark schrieb:
Chris F Clark schrieb:
In that sense, a static type system is eliminating tags, because the
information is pre-computed and not explicitly stored as a part of the
computation. Now, you may not view the tag as being there, but in my
mind if there exists a way of
Darren New schrieb:
John W. Kennedy wrote:
360-family assembler, yes. 8086-family assembler, not so much.
And Burroughs B-series, not at all. There was one ADD instruction, and
it looked at the data in the addresses to determine whether to add ints
or floats. :-)
I heard that the
Anton van Straaten schrieb:
Marshall wrote:
Can you be more explicit about what latent types means?
Sorry, that was a huge omission. (What I get for posting at 3:30am.)
The short answer is that I'm most directly referring to the types in
the programmer's head.
Ah, finally that
Marshall schrieb:
It seems we have languages:
with or without static analysis
with or without runtime type information (RTTI or tags)
with or without (runtime) safety
with or without explicit type annotations
with or without type inference
Wow. And I don't think that's a complete list,
Anton van Straaten schrieb:
It seems we have languages:
with or without static analysis
with or without runtime type information (RTTI or tags)
with or without (runtime) safety
with or without explicit type annotations
with or without type inference
Wow. And I don't think that's a complete
Andreas Rossberg schrieb:
Luca Cardelli has given the most convincing one in his seminal tutorial
Type Systems, where he identifies typed and safe as two orthogonal
dimensions and gives the following matrix:
| typed | untyped
---+---+--
safe | ML|
In comp.lang.functional Joachim Durchholz [EMAIL PROTECTED] wrote:
[...] Even ML and Pascal have ways to circumvent the type system, [...]
Show me a Standard ML program that circumvents the type system.
-Vesa Karvonen
--
http://mail.python.org/mailman/listinfo/python-list
Joachim Durchholz write:
Another observation: type safeness is more of a spectrum than a clearcut
distinction. Even ML and Pascal have ways to circumvent the type system,
No. I'm not sure about Pascal, but (Standard) ML surely has none. Same
with Haskell as defined by its spec. OCaml has a
Joachim Durchholz wrote:
Andreas Rossberg schrieb:
Luca Cardelli has given the most convincing one in his seminal
tutorial Type Systems, where he identifies typed and safe as two
orthogonal dimensions and gives the following matrix:
| typed | untyped
Joachim Durchholz wrote:
Andreas Rossberg schrieb:
Luca Cardelli has given the most convincing one in his seminal
tutorial Type Systems, where he identifies typed and safe as two
orthogonal dimensions and gives the following matrix:
| typed | untyped
Chris F Clark wrote:
Chris Smith [EMAIL PROTECTED] writes:
Unfortunately, I have to again reject this idea. There is no such
restriction on type theory. Rather, the word type is defined by type
theorists to mean the things that they talk about.
Do you reject that there could be
1 - 100 of 466 matches
Mail list logo
