Marshall wrote:
> Andreas Rossberg wrote:
> >
> > And note that even with second-class state you can still have aliasing
> > issues - you just need mutable arrays and pass around indices. Keys in
> > databases are a more general form of the same problem.
>
> So for
Darren New schrieb:
> 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 valu
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 talk of the "ty
Anton van Straaten wrote:
>
> Languages with latent type systems typically don't include type
> declarations in the source code of programs. The "static" type scheme
> of a given program in such a language is thus latent, in the English
> dictionary sense of the word, of something that is present
Rob Thorpe wrote:
>
> But it differs from latently typed languages like python, perl or lisp.
> In such a language there is no information about the type the variable
> stores. The programmer cannot write code to test it, and so can't
> write functions that issue errors if given arguments of the
Rob Thorpe write:
> >
> > Take one of these languages. You have a variable that is supposed to
> > store functions from int to int. Can you test that a given function
> > meets this requirement?
>
> The answer is no for python and perl AFAIK. Also no for lisp _aux
> naturelle_ (you can do it by mo
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 langua
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 c
Gabriel Dos Reis wrote:
> |
> | (Unfortunately, you can hardly write interesting programs in any safe
> | subset of C.)
>
> Fortunately, some people do, as living job.
I don't think so. Maybe the question is what a "safe subset" consists
of. In my book, it excludes all features that are potentiall
Gabriel Dos Reis wrote:
> [EMAIL PROTECTED] writes:
>
> | Gabriel Dos Reis wrote:
> | > |
> | > | (Unfortunately, you can hardly write interesting programs in any safe
> | > | subset of C.)
> | >
> | > Fortunately, some people do, as living job.
> |
> | I don't think so. Maybe the question is what
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 Java
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
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 th
On Jun 8, 6:28 am, "Ken T." wrote:
>
> > Let's not forget Elite for the 6502 exploiting predictable performance
> > in order to switch graphics modes partway down the vsync!
>
> That actually didn't require predictable timing. You could tell the
> video chip to send you an interrupt when it got t
David Hopwood wrote:
> George Neuner wrote:
>>
>>All of this presupposes that you have a high level of confidence in
>>the compiler. I've been in software development for going in 20 years
>>now and worked 10 years on high performance, high availability
>>systems. In all that time I have yet to m
Marshall wrote:
>
> Okay, sure. But for the problem you describe, both imperativeness
> and the presence of pointers is each necessary but not sufficient;
> it is the two together that causes the problem. So it strikes
> me (again, a very minor point) as inaccurate to describe this as
> a problem
ll imperative languages I know. :-)
- Andreas
--
Andreas Rossberg, [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Darren New wrote:
> Andreas Rossberg wrote:
>
>> Yes, technically you are right. But this makes a pretty weak notion of
>> mutability. All stateful data structures had to stay within their
>> lexical scope, and could never be passed to a function.
>
> Not reall
mming, usually based on deep unification, brings by far the worst
incarnation of aliasing issues to the table.
- Andreas
--
Andreas Rossberg, [EMAIL PROTECTED]
--
http://mail.python.org/mailman/listinfo/python-list
Chris F Clark wrote:
>
> A static
> type system eliminates some set of tags on values by syntactic
> analysis of annotations (types) written with or as part of the program
> and detects some of the disallowed compuatations (staticly) at compile
> time.
Explicit annotations are not a necessary ing
Rob Thorpe wrote:
>
> No, that isn't what I said. What I said was:
> "A language is latently typed if a value has a property - called it's
> type - attached to it, and given it's type it can only represent values
> defined by a certain class."
"it [= a value] [...] can [...] represent values"?
Rob Thorpe wrote:
>>
>>>No, that isn't what I said. What I said was:
>>>"A language is latently typed if a value has a property - called it's
>>>type - attached to it, and given it's type it can only represent values
>>>defined by a certain class."
>>
>>"it [= a value] [...] can [...] represent va
David Squire wrote:
> Andreas Rossberg wrote:
>
>> Rob Thorpe wrote:
>>
>>>>
>>>>> No, that isn't what I said. What I said was:
>>>>> "A language is latently typed if a value has a property - called it's
>>&
Rob Thorpe wrote:
>Andreas Rossberg wrote:
>>Rob Thorpe wrote:
>>
>>>>>"A language is latently typed if a value has a property - called it's
>>>>>type - attached to it, and given it's type it can only represent values
>>
David Hopwood wrote:
>
> Oh, but it *does* make sense to talk about dynamic tagging in a statically
> typed language.
It even makes perfect sense to talk about dynamic typing in a statically
typed language - but keeping the terminology straight, this rather
refers to something like described in
Rob Thorpe wrote:
>
> I think this should make it clear. If I have a "xyz" in lisp I know it
> is a string.
> If I have "xyz" in an untyped language like assembler it may be
> anything, two pointers in binary, an integer, a bitfield. There is no
> data at compile time or runtime to tell what it
Chris Uppal wrote:
>
> I have never been very happy with relating type to sets of values (objects,
> whatever).
Indeed, this view is much too narrow. In particular, it cannot explain
abstract types, which is *the* central aspect of decent type systems.
There were papers observing this as early
Marshall wrote:
>
> While we're on the topic of terminology, here's a pet peeve of
> mine: "immutable variable."
>
> immutable = can't change
> vary-able = can change
>
> Clearly a contradiction in terms.
>
> If you have a named value that cannot be updated, it makes
> no sense to call it "vari
Joachim Durchholz wrote:
>>
>>> It's worth noting, too, that (in some sense) the type of an object
>>> can change over time[*].
>>
>> No. Since a type expresses invariants, this is precisely what may
>> *not* happen.
>
> No. A type is a set of allowable values, allowable operations, and
> const
Darren New wrote:
>
> As far as I know, LOTOS is the only
> language that *actually* uses abstract data types
Maybe I don't understand what you mean with ADT here, but all languages
with a decent module system support ADTs in the sense it is usually
understood, see ML for a primary example. Cl
Vesa Karvonen wrote:
>
>>>Indeed, the ability to declare a new type that has the exact same
>>>underlying representation and isomorphically identical operations but
>>>not be the same type is something I find myself often missing in
>>>languages. It's nice to be able to say "this integer repres
Darren New wrote:
>
>> Maybe I don't understand what you mean with ADT here, but all
>> languages with a decent module system support ADTs in the sense it is
>> usually understood, see ML for a primary example.
>
> OK. Maybe some things like ML and Haskell and such that I'm not
> intimately f
Marshall wrote:
>Andreas Rossberg wrote:
>>Chris Uppal wrote:
>>
>>>I have never been very happy with relating type to sets of values (objects,
>>>whatever).
>>
>>Indeed, this view is much too narrow. In particular, it cannot explain
>>abstract
Rob Warnock wrote:
>
> Here's what the Scheme Standard has to say:
>
> http://www.schemers.org/Documents/Standards/R5RS/HTML/r5rs-Z-H-4.html
> 1.1 Semantics
> ...
> Scheme has latent as opposed to manifest types. Types are assoc-
> iated with values (also called objects) rath
Pascal Costanza wrote:
>
> Consider a simple expression like 'a + b': In a dynamically typed
> language, all I need to have in mind is that the program will attempt to
> add two numbers. In a statically typed language, I additionally need to
> know that there must a guarantee that a and b will
Chris Uppal wrote:
>
>>>It's worth noting, too, that (in some sense) the type of an object can
>>>change over time[*].
>>
>>No. Since a type expresses invariants, this is precisely what may *not*
>>happen. If certain properties of an object may change then the type of
>>the object has to reflect t
Pascal Bourguignon wrote:
>
> For example, sort doesn't need to know what type the objects it sorts
> are. It only needs to be given a function that is able to compare the
> objects.
Sure. That's why any decent type system supports polymorphism of this
sort. (And some of them can even infer whi
Marshall wrote:
>>
>>>What prohibits us from describing an abstract type as a set of values?
>>
>>If you identify an abstract type with the set of underlying values then
>>it is equivalent to the underlying representation type, i.e. there is no
>>abstraction.
>
> I don't follow. Are you saying tha
Rob Thorpe wrote:
>
> Its easy to create a reasonable framework.
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
---+
Marshall wrote:
>
> What we generally (in programming) call variables are locals
> and globals. If the languages supports an update operation
> on those variables, then calling them variables makes sense.
> But "variable" has become such a catch-all term that we call
>
> public static final int
David Hopwood wrote:
>>
>>"Values" refers to the concrete values existent in the semantics of a
>>programming language. This set is usually infinite, but basically fixed.
>>To describe the set of "values" of an abstract type you would need
>>"fresh" values that did not exist before (otherwise the a
Chris Uppal wrote:
>>>
>>>Well, it seems to me that you are /assuming/ a notion of what kinds of
>>>logic can be called type (theories), and I don't share your
>>>assumptions. No offence intended.
>>
>>OK, but can you point me to any literature on type theory that makes a
>>different assumption?
>
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
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
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
45 matches
Mail list logo
