Talk:Type inference

From Wikipedia, the free encyclopedia

Contents

[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)

[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).