Talk:Type inference

From Wikipedia, the free encyclopedia

This is the discussion/talk page for: Type inference.

Contents

[edit] Question

This is a quote from the article
The ability to infer types automatically makes many programming tasks easier, leaving the programmer free to omit type annotations while maintaining some level of type safety

Why does it say "SOME" and not "A COMPLETE LEVEL OF SAFETY"? Are there downsides that someone would like to discuss? —Preceding unsigned comment added by 194.73.67.254 (talk) 18:16, 4 December 2007 (UTC)

Type inference protects against errors such as using a Double as a Char, but cannot usually detect the difference between runtime values of the same type. More advanced dependent type systems can embed more kinds of safety in the type system, such as static array index bounds checking, but these systems do not have complete type inference and may require annotations or even interactive theorem proving. Of course getting more out of type systems and type inference is ongoing cutting-edge research, but there are also genuinely undecidable questions. --Ørjan (talk) 07:02, 5 December 2007 (UTC)

[edit] Explain notation

Please explain the notations, e.g. \tau.e,\,\Gamma - I can't understand the article as-is. I do understand the notations a \to b \to c, e\,e but I still think it warrants explanation. 68.145.106.92 04:16, 15 November 2006 (UTC)

[edit] Rule

f\, \Gamma\, (\lambda v:\tau. e) = \tau_e \to \tau where \tau_e = f\, \Gamma'\, e and Γ' is Γ extended by the binding  v \,:\,\tau.

Should be

f\, \Gamma\, (\lambda v:\tau. e) = \tau \to \tau_e where \tau_e = f\, \Gamma'\, e and Γ' is Γ extended by the binding  v \,:\,\tau.

right?

[edit] Scope

Type inference is historically linked to funbctional language but I don't think it is limited to them.

Quite right. It's actually just part of lambda calculus, which isn't even mentioned here. That it happens to find good use in programming languages is nice, but not the most important thing. However, properly rewriting this article takes more time than I have available—sorry, Wikipedia. --131.155.69.144 12:21, 8 Mar 2005 (UTC)
You make me sad. So be it.
But what I want to know is whether the adumbrated algorithm is also used in dynamic typing systems. --Maru (talk) Contribs 01:06, 14 November 2005 (UTC)
So-called 'dynamic typing systems' are not actually type systems per-se (in the classical theoretical sense), but are rather a method for 'tagging' (sometimes primitive) memory-resident data structures in such a way as to influence their runtime evaluation (e.g., execute nominally or throw an error if something 'bad' is done with the structure). Type inference and the unification algorithm are not used here. There are some systems which propose to combine elements from static type system with these dynamic tagging approaches to achieve some sort of hybrid system though, and in those cases you may see some elements from static type inference arise. 70.36.29.121 08:23, 30 January 2006 (UTC)
I've added a little more to the article and corrected the statement regarding type inference only being used in functional languages. However, there's a whole lot that needs to be fleshed out to make things clearer than they are now. In particular, it would be good to explain more thoroughly the role type inference plays in programming languages by providing reference to the process of program compilation by describing the process of creating an AST, annotating it through type inference, possibly performing type erasure, then converting to an IR for optimization, translation to the target platform, etc. For now, I just mentioned all of that as "compiler," and although it's not technically incorrect, and it's easier to understand without all the additional information, it's not strictly the most accurate account. 70.36.29.121 12:16, 17 December 2005 (UTC)

[edit] External link

There's a thread in the archive of the Haskell mailing list with contributions by Philip Wadler and others explaining the history of the Hindley-Milner algorithm, but I'm not sure if this is important enough to be incorporated into the article as long as the article doesn't explain the algorithm itself. The tread also contains detailed references to the original publications of Curry, Feys, Hindley, Milner and Damas. --Tobias Bergemann 08:12, 2004 Nov 16 (UTC)

[edit] what has operator overloading to do with this?

Since there are no ad-hoc polymorphic subfunctions in the function definition, we can declare the function to be parametric polymorphic.

I followed the links trying to understand this sentence but it didn't work. Could somebody explain it? --euyyn 22:52, 2 July 2006 (UTC)

It is simply wrong, as is the current example even with the comment removed, because the length definition given is ad hoc overloaded, as in Haskell, 0, 1 and + are all affiliated not with Int, but with the overloaded type class Num (which includes Ints, unbounded Integers, floats, and even complex numbers). The standard length definition in Haskell is given an explicit type annotation to avoid this overloading. There is a genericLength function, but even that is explicitly restricted to a subclass, Integral, thus disallowing floating numbers.
If we wish to avoid the complication of ad-hoc overloading in the example, but still retain correct Haskell, I think we need to avoid using numerical expressions at all. I will try to use the map function instead. An alternative might be to use a language without numerical overloading, such as Ocaml. --Ørjan 21:03, 23 November 2006 (UTC)
Well, we have no Haskell lessons here in ULPGC.... I havent understood a word (nearly). --euyyn 17:24, 18 December 2006 (UTC)
That was sort of the point: The Haskell type system is quite advanced/complicated, so to get an example of type inference in it that is simple enough for the article, we need to be a bit careful and avoid the type classes. --Ørjan 01:26, 20 December 2006 (UTC)

80.7.195.184 Yes but computer Reals are not Real Reals, Real Reals would have Length INFINITY, the Reals are rational and what does that make the complex but imagined?

Could we call this Run Time Binding or Real Time Binding?

Also is it because atomics are not objects that we can type inference?

i.e. An Object must be made of something, another object Or something which is part of an object (eg an atomic)

Something must be mass or else its energy? So 3 is energy, t=3 means t is an integer, but could become a simulated real, either way we don't mean t as in the letter between s & u, for that we would say t="t" or t='t'

so its syntax and how to chew it

[edit] too technical

Is it just me, does this article dive right into the deep end with technical jargon and mark-up? Perhaps at least some pointers to articles which might explain some of the notation as well as terminology would be in order...?

(P.S., isn't there a template to mark an article as too technical?) —The preceding unsigned comment was added by 71.70.210.188 (talk) 04:49, 11 December 2006 (UTC).

27-Oct-2007: The article was expanded with a non-technical explanation (on 22-Feb-2007), showing a simple coding example. In October 2007, I expanded the example to also show what won't work for type inference. I think that is enough simplification, because the detailed technical issues are numerous and deserve more space in the article to encourage a full treatment of the subject. We must balance a novice view, against the right of technical readers to present and read full details. I have removed tag "{{technical}}" and suggested writing a more detailed analysis if the article still seems troublesome. -Wikid77 18:49, 27 October 2007 (UTC)

[edit] Math notation is confusing

Notation such as f\, \Gamma\, v = \tau is confusing if you don't specify you're using Haskell notation or if you don't know Haskell notation. I suggest using the typical f(x, y, ...) = ... notation instead. --indil 00:59, 12 March 2007 (UTC)

[edit] bad description

This article states that "Type inference is a feature present in some strongly statically typed programming languages." However, python implements type inference but is dynamically typed. The opening statement should be clarified that type inference is not only a feature of "strongly statically typed programming languages." mbecker 13:57, 23 August 2007 (UTC)

Python definitely does not implement any sort of type inferencing. Python is interpreted, not compiled. Type inferencing is something you do at compile time to assert all objects are correctly typed. Dynamically typed languages like Python only do runtime type checking, and thus, type errors can only be caught when executing the code. Tac-Tics 07:13, 9 September 2007 (UTC)

Nevertheless note that PyPy uses type inference for RPython source code which is a subset of the Python language. 77.8.158.253 (talk) 17:34, 20 April 2008 (UTC)