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.
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,
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.
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
>
Anton van Straaten wrote:
> 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 exe
Andreas Rossberg wrote:
>
>~/> ocaml -rectypes
> Objective Caml version 3.08.3
>
># let rec blackhole x = blackhole;;
>val blackhole : 'b -> 'a as 'a =
>
> The problem is, though, that almost everything can be typed once you
> have unrestricted recursive types (e.g. missing a
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 releva
"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 "transl
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 specificati
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
>
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
> r
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
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
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 fun
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 tha
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 *nev
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
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 "
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 ch
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 (befor
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 <[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
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
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 -> #'blac
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 -> #
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
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,
wh
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
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 c
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
>> dynam
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))
> >
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.lis
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,
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 straight
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 debug
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"
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 lang
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
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
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 ea
George Neuner 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, in particular,
>
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
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, natur
>> 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 t
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
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 a
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 p
On Mon, 26 Jun 2006 13:02:33 -0600, Chris Smith <[EMAIL PROTECTED]>
wrote:
>George Neuner 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 reduced to integer
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 straig
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 inter
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 sta
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 progra
"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 interest
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:
> 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 m
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 approximati
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
"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
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,
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
> pr
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.
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 (perhap
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 e
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
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 run
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
pa
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/axiom
George Neuner wrote:
> On Sun, 25 Jun 2006 14:28:22 -0600, Chris Smith <[EMAIL PROTECTED]>
> wrote:
>
> >George Neuner 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 wh
On Sun, 25 Jun 2006 14:28:22 -0600, Chris Smith <[EMAIL PROTECTED]>
wrote:
>George Neuner 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 will convin
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
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.
--
http://mail.pyt
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.
>
>>
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
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 enoug
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
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
>> rig
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 whi
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 reaso
"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.
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
>
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
>>> i
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 entir
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 typical
Gabriel Dos Reis <[EMAIL PROTECTED]> writes:
> [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.
>
>First point: "safety" is a *per-langua
Chris F Clark <[EMAIL PROTECTED]> wrote:
> These informal systems, which may not prove what they claim to prove
> are my concept of a "type system".
Okay, that works. I'm not sure where it gets us, though, except for
gaining you the right to use "type system" in a completely uninteresting
sense
Gabriel Dos Reis wrote:
> I would suggest you give more thoughts to the claims made in
> http://www.seas.upenn.edu/~sweirich/types/archive/1999-2003/msg00298.html
I'm not sure I understand this. Looking at "Example 2", where C is
claimed to be "C-safe", he makes two points that I disagree with.
Scott David Daniels wrote:
> [EMAIL PROTECTED] wrote:
>
>> Huh? There is a huge, fundamental difference: namely whether a type
>> system is sound or not. A soundness proof is obligatory for any serious
>> type theory, and failure to establish it simply is a bug in the theory.
>
> So you claim Jav
[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.
First point: "safety" is a *per-language* property. Each language
comes with its own notion o
Joachim Durchholz <[EMAIL PROTECTED]> writes:
[...]
| (Yes, I'm being silly. But the point is very serious. Even with less
| silly examples, whether a language or subset is "safe" entirely
| depends on what you define to be "safe", and these definitions tend to
| vary vastly across language commu
Chris F Clark <[EMAIL PROTECTED]> (I) wrote:
> Do you reject that there could be something more general than what a
> type theorist discusses? Or do you reject calling such things a type?
Chris Smith <[EMAIL PROTECTED]> wrote:
> I think that the correspondence partly in the wrong direction to
George Neuner 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 will convince a compiler that a
> narrowing conversion which could produce an illegal value
Marshall wrote:
> Also: has subtyping polymorphism or not, has parametric polymorphism or
> not.
And covariant or contravariant.
--
Darren New / San Diego, CA, USA (PST)
Native Americans used every part
of the buffalo, including the wings.
--
http://mail.python.org/mailman/listinfo
Joachim Durchholz wrote:
>
> > but (Standard) ML surely has none.
>
> NLFFI?
>
> > Same with Haskell as defined by its spec.
>
> Um... I'm not 100% sure, but I dimly (mis?)remember having read that
> UnsafePerformIO also offered some ways to circumvent the type system.
Neither NLFFI nor unsafePe
On Sun, 25 Jun 2006 13:42:45 +0200, Joachim Durchholz
<[EMAIL PROTECTED]> wrote:
>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 t
Chris Smith wrote:
> Andrew McDonagh <[EMAIL PROTECTED]> wrote:
>> I haven't read all of this thread, I wonder, is the problem to do with
>> Class being mistaken for Type? (which is usually the issue)
>
> Hi Andrew!
Hi Chris
>
> Not much of this thread has to do with object oriented languages.
Andrew McDonagh <[EMAIL PROTECTED]> wrote:
> I haven't read all of this thread, I wonder, is the problem to do with
> Class being mistaken for Type? (which is usually the issue)
Hi Andrew!
Not much of this thread has to do with object oriented languages... so
the word "class" would be a little
Chris F Clark wrote:
> Chris F Clark (I) wrote:
>
> > I'm particularly interested if something unsound (and perhaps
> > ambiguous) could be called a type system. I definitely consider such
> > things type systems.
>
> "Marshall" <[EMAIL PROTECTED]> wrote:
>
> > I don't understand. You are saying y
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 above.
>>> N
Joachim Durchholz <[EMAIL PROTECTED]> wrote:
> > The immutability comes from the fact (perhaps implicit in these
> > textbooks, or perhaps they are not really texts on formal type theory)
> > that types are assigned to expressions,
>
> That doesn't *define* what's a type or what isn't!
>
I'm s
[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 formally define.
>
>
> That language is not a subset, if at all, it's the other
1 - 100 of 462 matches
Mail list logo
