Talk:Type system/Archive 3

Archive 1

Archive 2

Archive 3

GADT

I removed the sentence

Recent enhancements to statically typed languages (e.g. Haskell Generalized algebraic data types) have allowed eval functions to be written in a statically type checked way.

which confuses the example in the GADT paper with the traditional Lisp notion of an eval function, which is basically a function of type (forall a. String -> a). The example in the paper operates at the typed term level. Maybe the sentence can be rewritten somehow. 66.127.55.192 (talk) 19:13, 2 February 2010 (UTC)

References

CACM article

The following article is not very good but maybe it has a useful quote or two:

http://cacm.acm.org/magazines/2010/2/69367-type-theory-comes-of-age/fulltext

66.127.55.192 (talk) 20:41, 2 February 2010 (UTC)

Remove Intro Tag

The introductory style, I think, has been fixed now? --AnAbsolutelyOriginalUsername42 (talk) 19:41, 9 January 2010 (UTC)

The current intro really needs a rewrite. The tag said that it wasn't introductory enough, but IMO somebody went overboard in trying to correct this. 66.127.55.192 (talk) 20:52, 2 February 2010 (UTC)

Go is also a dynamically typed language

Go is not only statically type, it can also be used as a dynamically typed language and of course you can write this: var x = 12 x is not typed and therefore can take another type of value. x = "hello". —Preceding unsigned comment added by 109.193.2.62 (talk) 21:25, 28 May 2010 (UTC)

Associations; subtype; ∃X

• "Types usually have associations either with values in memory or with objects such as variables. "
  • What's meant with associations here?

• "A program typically associates each value with one particular type (although a type may have more than one subtype)."
  • Does the last statement mean that it's always the case that a type is a subtype of itself?

• "For example, the type "T = ∃X { a: X; f: (X → int); }" describes a module interface that has a data member of type X and a function that takes a parameter of the same type X and returns an integer."
  • Why is there an "∃X" existential quantification in this expression?

Thanks, --Abdull (talk) 21:00, 8 September 2010 (UTC)

Is duck typing implicit typing?

Why is Duck typing explained at the section about Polymorphism? If use an object in a duck-like manner because it looks and quacks like a duck, I don't mind what it actually is. It may be nothing but a plain old duck, so no polymorphism needs to be involved. As far as I understand, duck typing is much more related to type inference: type inference used at compile time, and duck typing is used used at running time. In both cases the programmer states what he does with an object and the type is infered. -- JakobVoss (talk) 08:39, 16 September 2010 (UTC)

According to Type polymorphism, "polymorphism is a programming language feature that allows values of different data types to be handled using a uniform interface", which makes it similar (in its effects) to duck typing. However, I wouldn't say that duck typing is related to type inference: no type is/has to be infered at runtime. After all, with duck typing, the type of an object does not matter when an method is called, it only matters whether it provides the requested method. – Adrian Willenbücher (talk) 13:04, 16 September 2010 (UTC)

Because the article is biased towards the dynamically challenged? If wanting to group type systems then it becomes the best of a bad set of groups to make it a member of? (Gosh I'm sniping today. Normal service will be resumed as soon as possible). --Paddy (talk) 13:11, 16 September 2010 (UTC)

I'm not sure what you want to express with the first two sentences. Do you mean that dynamic type systems are underrepresented in the article? Regarding the second sentence, are you saying that the duck typing section is at the wrong place? – Adrian Willenbücher (talk) 17:48, 16 September 2010 (UTC)

I'll address some of the questions Jakob has above. Talking about duck typing and polymorphism, there is polymorphism in a dynamic language. Polymorphism deals with abstraction, where the implementation of a method changes for different types in the system. I think the confusion is probably coming in that there's not necessarily an interface type change like in Java, but you can have the same behavior in Smalltalk (dynamically typed) without static typing. Consider an Animal object with an "makenoise" method that has some simple implementation (like returning "no noise"). Then there's 2 subclasses of Animal, Cat and Dog. Dog's makenoise method returns "bark" and Cat's makenoise returns "meow. Calling makenoise on a list of animals morphs from Cat to Dog etc, even with duck typing. There are different classes and as such the types are different. With regard to type inference. Type inference can be confusing because on the surface it looks very much like dynamic typing. Most people don't put types on objects and so it looks like duck typing. Here's the difference. Type inference, infers at compile time what type an object is based on the actions (method called) on that object. A good example of the difference is let's say we have a special integer type (i.e. a MyInteger class) that we create that has a special method addFrac method. The type inference case is easy, it sees addFrac at compile time, the compiler then knows, the only object that has an addFrac method is MyInteger. This is just like in Java if you had specifically declared that object as type MyInteger. In fact, I would say, depending on the language, might even be more strict (you can still cast an object to another type unsafely in Java). What I think illustrates this in duck typing, is let's say instead of the MyInteger class, we have a YourInteger class, and YourInteger does not have an addFrac method. There's no compiler error because this is a dynamic language. Now when addFrac is called on an instance of YourInteger, that method doesn't exist, so a "catch all" method is called. Let's say we define that method on YourInteger (doesNotUnderstand in Smalltalk, or method_missing in Ruby I think). The doesNotUnderstand method is called and maybe that method does the same thing as addFrac. So in that example, there actually is no addFrac method, but the class still responds to calls to addFrac (it's quacking like a duck) through it's catch all method "doesNotUnderstand" - Ryan Senior 23:35, 6 October 2010 (CST) —Preceding unsigned comment added by 99.183.215.173 (talk)

I would think it unlikely in your explanation that a default doesNotUnderstand method would do something you would want. It is more likely to just throw an exception. --Paddy (talk) 21:41, 8 October 2010 (UTC)

B-class? How did that happen?

Is there any report or discussion regarding the classification? I think the article is very confusing and there are a lot of things that are plainly wrong. I'd be interested to see what criteria were used to arrive at this rating. Ketil (talk) 13:10, 15 April 2011 (UTC)

This talk page needs archiving

Old and new discussion are too intertwined to follow. Pcap ping 09:57, 1 September 2009 (UTC)

I went ahead and archived a bunch of sections. I hope things are better now. :) -pinkgothic (talk) 21:30, 5 May 2011 (UTC)

link to a unified Weak and Strong typing article?

There's redundant info about Weak typing in Type system and Strong typing. In my opinion, Type system should have a brief explanation about both (possibly having the example table currently available in Strong typing), then link to an article that handles both Weak and Strong typing, since the explanation of each is brief and the concepts are compared everytime. This should make for a much cleaner way to organize this knowledge inside wikipedia. (I'm writing this opinion to all 3 current discussion pages) --Roberto.cr (talk) 09:13, 6 May 2011 (UTC)

Are you in fact advocating a weak versus strong typing article? --Paddy (talk) 14:46, 6 May 2011 (UTC)

Same thing really. The subject is really the axis of comparison, but I think "typing strength" would be a neologism. --Cybercobra (talk) 01:05, 7 May 2011 (UTC)

Possible Plagiarism in the Section on Static Typing

Because they evaluate type information during compilation and therefore lack type information that is only available at run-time, static type checkers are conservative. They will reject some programs that may be well-behaved at run-time, but that cannot be statically determined to be well-typed. For example, even if an expression <complex test> always evaluates to true at run-time, a program containing the code if <complex test> then 42 else <type error> will be rejected as ill-typed, because a static analysis cannot determine that the else branch won't be taken.

Seems awfully close to the text from the source:

Being static, type systems are necessarily also conservative: they can cate- gorically prove the absence of some bad program behaviors, but they cannot prove their presence, and hence they must also sometimes reject programs that actually behave well at run time. For example, a program like if <complex test> then 5 else <type error> will be rejected as ill-typed, even if it happens that the <complex test> will always evaluate to true, because a static analysis cannot determine that this is the case.

Danking00 (talk) 16:24, 25 August 2011 (UTC)

Type system vs type checking

Is that two ideas unnecessarily conflated in the introduction? --Paddy (talk) 19:50, 29 October 2011 (UTC)

More problematic is that it fails to distinguish between between the type theoretic definition (a formal deductive system from which a type checking algorithm usually follows trivially) versus the - by actual programmers more commonly used - definition, referring to features of a language's typing discipline (static vs. dynamic, weak vs. strong, ...). —Ruud 12:17, 31 October 2011 (UTC)

Intersection of Function Types

Due to contravariance, I'd expect the intersection between int->int and float->float to be float->int, instead of some sort of discriminated union as the article seems to imply.

A function of type float->int can safely be used where a function of type int->int is expected (because when used, it will accept the ints fed into it), and also where a function of type float->float is expected.

Is there a reference for this issue? — Preceding unsigned comment added by Zweije (talk • contribs) 18:52, 27 January 2012 (UTC)

Uh, are you talking about for some specific language here? It doesn't make much sense to me, and I think it would only work with some implicit conversion from floats to ints. Ketil (talk) 12:30, 9 March 2012 (UTC)

Gibberish

The Wikitext source is fine and the history seems normal, but when I view the article I see a bunch of gibberish. The gibberish is (unsurprisingly) visible in the HTML source. What is this madness? — Preceding unsigned comment added by 63.249.90.205 (talk) 16:44, 25 May 2012 (UTC)

Recent Fundamentals section edits

The Fundamentals section was edited almost entirely. I tried to copy what was there, trust me. It's laid out differently now, and while doing so there were so many sentences and phrases re-written. I'm asking that you'll just read it to get what I did. I want to break the eight paragraphs into two subsections named Richness evolves and either Advantages sustain or Advantages maintain as shown in the wikitext commented out. — CpiralCpiral 02:13, 2 September 2012 (UTC)

Objective C is also a dynamic language

As explained in the Objective C wikipedia article, Objective C, like smalltalk, can use dynamic typing and is considered as a dynamic language. So why put it as example in the static typing section ? — Preceding unsigned comment added by 194.147.254.37 (talk) 14:32, 5 November 2012 (UTC)

Type system

Hello. I do not believe your recent to Type system is completely accurate. See my comment left here. Could you try to improve the summary and perhaps expand a bit on the conditions of the experiment? Especially see the author's own conclusions and description in the abstract and the "Conclusions" section. Cheers, —Ruud 11:49, 16 December 2012 (UTC)

That is what it says, first paragraph of the conclusions: "first: development time until a minimal scanner has been implemented … In the first case, the use of the statically typed programming language had a significant negative impact." Please delete your little tag, or qualify the sentence as you see fit. Quoting the mentioned sentence could work.
As for duck typing not being mentioned: the study compares a dynamically typed language (naturally using duck typing) against a statically typed language. The study should be mentioned somewhere on the page. Feel free to move it around. 46.14.124.168 (talk) 15:42, 16 December 2012 (UTC)

Merger proposal

The following discussion is closed. Please do not modify it. Subsequent comments should be made in a new section. A summary of the conclusions reached follows.

The result of this discussion was no merge. — Dsimic (talk | contribs) 01:53, 23 December 2014 (UTC)

---

Gradual typing, as a very short article, should be merged into Type system § Combining static and dynamic type-checking section. It should fit there perfectly, allowing for both content deduplication and a broader picture at the same time. — Dsimic (talk | contribs) 00:43, 23 March 2014 (UTC)

On second thought, it would be much better to merge it into a new section, Type system § Gradual typing. Thoughts? — Dsimic (talk | contribs) 14:15, 24 March 2014 (UTC)

Don't Merge. I agree with the second thought and don't support a merge. The type system article is already long as it is. There also seems to be a section where Gradual typing could be included as a sub-section: Type_system#Specialized_type_systems I think the appropriate thing is to create a sub-section there for Gradual typing, put a short summary of gradual typing and then one of those main templates that points people to the Gradual typing article. --MadScientistX11 (talk) 15:58, 8 August 2014 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.

Undecidable Problem?

What does this sentence mean?

"Type safety contributes to program correctness, but cannot guarantee it unless the type checking itself becomes an undecidable problem. "

If type safety becomes undecidable, doesn't the notion of asserting correctness based on type safety become decidedly nondeterministic (run-time errors notwithstanding)? Robertwharvey (talk) 18:31, 24 June 2010 (UTC)

This sentence means that when a type system is so powerful that it can show every desired property of a program (for example termination), then the type checking becomes undecidable, meaning that there will be programs for which the type checker will never be able to disprove a property even though the property does not hold (for example that there are inputs for which the program does not terminate). To put this another way: if a type checker should for every program after a finite time either prove that a property holds or does not hold, then you either have to constrain the properties in question or the types of programs allowed in your language. Does this answer your question? – Adrianwn (talk) 20:37, 24 June 2010 (UTC)

@Adrianwn: I'm sure it does, but I'm going to have to mull it over for awhile before I fully understand it. :P Offhand, what you described sounds like a variation of the halting problem.

Yes, in fact the halting problem is the reason why no decidable type system can check for termination; if such a system provides a type "total function with signature A -> B", then the programming language will have to place syntactic constraints on such functions, or reject some functions that are actually total. Let's look at another example:

P(x):

 var a: array[0 ... 1000];
 i := f(x);
 return a[i];

In the general case, a type system can not check whether the array access will always be valid (i.e. prove whether 0 <= i <= 1000 for all x), since proving first-order logic is semidecidable. – Adrianwn (talk) 06:58, 26 June 2010 (UTC)

I don't think this argument is valid. The operation a[i] is valid only for a small set of values i. Thus in a strongly-typed language, this would throw a type error. Say f:: a -> Int then i := f(x) has the wrong type for the access. — Preceding unsigned comment added by 129.138.26.151 (talk) 23:13, 29 January 2015 (UTC)

Unclear phasing Fundamentals section paragraph 2

I find the opening sentence of paragraph two of the Fundamentals section somewhat confusing and awkward to read.

It currently reads:

Assigning a data type, what is called typing, gives meaning to a sequences of bits such as a value in memory or some object such as a variable.

My suggested edit is:

The act of assigning a data type, called typing, gives meaning to a sequences of bits such as a value in memory or some object such as a variable.

Any objections?

Bekroogle (talk) 07:47, 30 January 2015 (UTC)

No objection here. But to be honest while grammatically your version is IMO clearly better it isn't much of an improvement. Just saying "gives meaning" is so generic. I think a better improvement (I'm not suggesting these exact words this is just off the top of my head) would be something like "provides information to programmers and systems that manipulate the program such as compilers that define and restrict the allowable operations on a sequence of bits defined as data". But in any case I agree your version is definitely an improvement. --MadScientistX11 (talk) 13:36, 30 January 2015 (UTC)

Wording of initial sentence

I came to this page to learn about a subject which I have no knowledge of. The opening sentence is

"In computer science, a type system may be defined as "a tractable syntactic framework for classifying phrases according to the kinds of values they compute"."

I did not understand it. Could it perhaps be written in plainer language? Mark.camp (talk) 01:58, 27 December 2010 (UTC)

The type system of a programming language classifies expressions in that language (such as variables, arithmetic expressions, or functions) in terms of the kinds of values they compute. Clear enough? --FOo (talk) 08:22, 27 December 2010 (UTC)

Sorry, still not clear. Could you put it in layman's language? Thanks!

Mark.camp (talk) 00:50, 4 January 2011 (UTC)

It's an article about a technical concept. A person who does not know what a "programming language" is, nor what an "expression" or "variable" or "function" is, is not equipped to understand the rest of the article either. Not everything in the world can be expressed in "layman's language" without loss of accuracy or usefulness.

A type system describes the sort of values (e.g. numbers, strings, data structures) that particular expressions might mean. This includes literals: 42 is an integer; [1.3, 2.4, 3.5] is a list of floating point numbers; "monkeybutt" is a string. But it also includes expressions, such as arithmetic expressions or function applications, e.g. 40 + 2 will evaluate to an integer; concat("monkey", "butt") will evaluate to a string, and so on. (In some made-up language, anyway.)

It also lets us talk about the types that are expected as function arguments, and that are returned as function results. We can talk about a function that takes a list of integers as an argument, and returns an integer as a result. (Perhaps the sum function, for instance.) We would say that sum itself has a type: Its type is function from lists of integers, to integers. (In Haskell we'd write this type as [Int] -> Int.)

Does any of this clear it up? Still isn't obvious to me how this could be condensed into the lede, though. Technical articles will be technical. --FOo (talk) 04:31, 5 January 2011 (UTC)

Thanks, this is exactly what I was looking for. Could some of this text be incorporated into the article? I think it would make the article understandable to many more readers.

Mark.camp (talk) 01:48, 11 January 2011 (UTC)

Or perhaps the bits of the article that is in direct contradiction could be removed? Like "Assigning data types (typing) gives meaning to sequences of bits. Types usually have associations either with values in memory or with objects such as variables." Ketil (talk) 13:15, 15 April 2011 (UTC)

Seanhalle (talk) 12:53, 10 December 2012 (UTC) I went ahead and added an intro that should be clear. It gives the value of a type system, the basic elements of a type system, and how those elements relate to a program, a compiler, and each other.

The main description assigns to much to the term type system. Some of it belongs to the translater of a program. A type system I believe is a concept independent of language translation. It is of course part of the specifications of a language. I do not see it as directly applying to expressions. An expressions type is determined by its atomic elements and the target use. The type of a variable it is assigned to or its use such as an index etc. Relational expressions comparing values of different types. These functions are the compilers domain. Data objects may carry their type and the combinatorial type must be determined on the fly. It just seams a bit unclear as to exactly what a type system is and where it fits in. Is it during language translation. Part of the language specification. Informally or formally defined?

The article talks about compilers typing etc. That's all well and good. I and others I know use the term independent of compiler operation. The a language' type system determined it's capabilities. We can compare type systems of various languages. In this context a type system is the availability if types implemented and how they can be used in the language. A languages type system determines the algorithms that can be expressed in the language. This article goes into implementation which I think is a separate subject belonging to symantecs.

Steamerandy (talk) 23:21, 27 February 2015 (UTC)

That kind of wording doesn't quite apply to a functional language, which is a kind of language that stays away from algorithm until more fundamental semantics than algorithms are defined. The term 'Algorithm' has an imperative language history which gets in the way. It's not helpful to prematurely map 'algorithm' until more fundamental objects are defined. Best to read type theory first. And it's best not to use the terminology here elsewhere. It confuses any communication with others who have studied type systems and type theory.

My apologies for talking past your points.

If you are talking about computer systems like the Burroughs series or even the IPL series, that indeed is a world apart, both in viewpoint and in history, from the functional languages discussed in the article.

But it appears, just from the Burroughs sample code, these are single user systems, just to keep recursive jobs from killing other programs which might also reside in memory. True? --Ancheta Wis   (talk | contribs) 03:40, 28 February 2015 (UTC)

Type safety and memory safety

In this example z will point to a memory address five characters beyond y, equivalent to three characters after the terminating zero character of the string pointed to by y.
Shouldn't it be two?
--Volker Alexander (talk) 12:10, 28 February 2014 (UTC)

No, if y[] = "123456", y+5 would point to the 6. QuentinUK (talk) 16:50, 8 March 2015 (UTC)

Newest inline tags

Addressing the newest inline tags is going to take some work. I am listing some resources which may help us fix the tags.

• Stack overflow evolution from Strongly typed (2009) to strictly typed (2014)
• languages that compile to javascript
• Brian Kernighan (1981), Why Pascal is Not My Favorite Programming Language
• Jeff Atwood, Effective Programming: More Than Writing Code
• Jon Bentley Programming Pearls (2nd Edition)

One issue is that Type systems have grown in scope, and the technology post-dates some popular languages. It may be more productive to rewrite the article from the POV of the newer languages.

Type inference would help here. --Ancheta Wis   (talk | contribs) 15:14, 29 November 2015 (UTC)

Propose a better example of type system usage: a URL-unaware application

Suppose we are looking on the Web for a house to buy: we enter the search criteria in a browser and receive a list of addresses, each with a URI for a house which matches our criteria.

We pass the list to an app, a C program. But suppose that C program is merely echoing a string of bytes, without understanding where the specific type, the URI starts/stops. If the app does not understand the URI, the user of that app will know, intuitively, that something is wrong in the app. So if an open-source utility such as http-parser.h is used, the app has a way to handle errors from the POV of the user.

Now the C program has a head start in decoding the rest of the items in that list of search results. Of course, just as we need code for parsing URLs, we need code to help us start processing other Types, such as pictures of the exterior, the rooms in the interior, street views, planting, lawn, driveway, bathrooms, bedrooms, kitchen appliances, windows and family rooms. We need code which handles Types for schools, neighborhood safety, and so forth.

I propose patching in these statements just before the simple C example. --Ancheta Wis   (talk | contribs) 02:34, 1 July 2016 (UTC)

Soundness

Remy's critique appears to be a defense of poor typing. Compare to Milner's slogan "well-typed programs cannot go wrong" Remy p.7. Rather than getting stuck in a discussion of soundness, perhaps we might consider another approach; see the Hindley–Milner type system used in Haskell. In addition, the Haskell type system is lifted, to include non-termination. --Ancheta Wis   (talk | contribs) 01:46, 5 July 2017 (UTC)

This contribution appears to be about typewriter keystroking, not type systems

The concept in this contribution appears to be about indentation style rather than a type system. --Ancheta Wis   (talk | contribs) 15:08, 4 August 2018 (UTC)

@Stan0033: Please see the indentation style, off-side rule, and whitespace articles, which already cover your contribution. Rather than typing in the sense of whitespace this article covers the word used as in type theory, data type, abstract data type, and its application in type systems --Ancheta Wis   (talk | contribs) 19:27, 4 August 2018 (UTC)

Units of Measurement/Dimensional analysis as types.

I have an incomplete bibliography at User:RDBrown/Prog Lang Dimensions on Units of Measure (Dimensional Analysis) being added to programming languages. Griffioen's thesis, building on Kennedy's work and Hart's dimensioned linear algebra seems to be state of the art for functional languages. I'm not sure where a precis of some of these should go in the main article — should it be in one of the linked articles? RDBrown (talk) 04:37, 19 February 2020 (UTC)
I've added a See Also Programming Languages section to Dimensional Analysis. RDBrown (talk) 13:10, 30 March 2020 (UTC)

There is a related stream at Scientific method:"Donald M. MacKay has analyzed these elements in terms of limits to the accuracy of measurement and has related them to instrumental elements in a category of measurement.".-- 09:20, 19 February 2020 (UTC)

Re-reading the quote, 'the first group' (calculable a priori from a specification) corresponds to 'type'. The 'second group' (calculated a posteriori from what was done), corresponds to 'application', as we would say nowadays. -- 09:20, 19 February 2020 (UTC)

But there are now languages that discriminate 'evaluation' from 'application'. -- 09:31, 19 February 2020 (UTC)

Griffioen's usage of a unit as a modifier to selected quantities in an array (or better, in a tuple) corresponds to a type. --Ancheta Wis   (talk | contribs) 09:41, 19 February 2020 (UTC)

This goes a bit further: McBride, Conor; Nordvall-Forsberg, Fredrik (2022). "Type systems for programs respecting dimensions" (PDF). Advanced Mathematical and Computational Tools in Metrology and Testing XII. Advances in Mathematics for Applied Sciences. World Scientific. pp. 331–345. doi:10.1142/9789811242380_0020. ISBN 9789811242380.

--added sig of User:RDBrown 05:03, 23 April 2022

References

Spelling - "type checking"

What should the spelling be? The following?

type checking (verb)

typechecking (noun)

type-checking (adjective)

Wiktionary only has typechecking (noun).

--Mortense (talk) 21:54, 19 December 2020 (UTC)