Implementation -------------- Max's environment or table of definitions has four entries for each name: tag: single lower case character name. ldef: lambda representation. cdef: combinator representation type: type of definition. Definitions are maintained in both lambda and combinator form. The former is more convenient for merging the equations which constitute definitions, while the latter allows simpler reduction and much simpler type checking. In common with Min, the implementation of Max uses no variables. That is to say that once a name is assigned, its value is not thereafter changed. The only ex- ception to this is the name '_' which is used as a sink. It may be specified more than once, but its value is never referenced. '_' is a good name for a sink because it is arguably the APL name with the lowest connotative overhead (most boring). The symbol is used in the functional language "Hope" for approximately the same purpose. Function [show] is used to display the first ⎕pw characters of a possibly infin- ite list. [show] outputs list items as a side-effect of calculating the number of session columns remaining. This approach was adopted so that with unbuffered ⍞← output, leftmost items of a list are displayed early. This provides an indic- ation that something is happening if reduction of successive items takes prog- ressively longer, as for example, in the case of the Fibonacci sequence. To help show what's going on, the APL code is occasionally commented using an informal notation to indicate function type. The scheme mirrors APL's header syntax, with '::' in place of the function name. For example: tex env ← tex :: exp env means the function is dyadic; takes a left argument of type "tex" (type express- ion); a 2-item right argument of "exp" (expression) and "env" (environment); and returns a 2-item result. The following D-functions implement Max: max process input stream, returning {shy} environment. parse parse tree from char vector source. lambda lambda expression from parse tree. local local definitions replaced with simple lambda expressions. equn argument patterns replaced with simple lambda expressions. show display of reduced expression. defn environment extended with new definition. compile compilation of lambda, into combinator form. typex type statement (::) processing. type deduction (inference) of expression type. unify unification of type expressions. reduce expression reduction. extend environment extended with primitive types and definitions. const implementation constants. trees graphical display of tree structures. In addition to these relatively substantial functions, which are described be- low, there are a number of small utilities which are defined dynamically in several places. This repetition is justified on the grounds that being able to see the definition in context outweighs any reluctance to replicate code. Dref: "Lookup Tables" are used in several places. These take the form of a vec- tor of names (tags) followed by a corresponding vector of values (vals). For ex- ample: tab←'abc'(1 2 3) ⍝ table of values for 'a', 'b', 'c'. A function to "dereference" a name from the table could be coded: dref←{ ⍝ Dereference from table. tags vals←⍺ ⍝ left arg: look-up table. name←⍵ ⍝ right arg: name to look up. (tags⍳name)⊃vals,⊂name ⍝ value corresponding to name. } The phrase ,⊂name in the last line supplies a default value if the name is un- known to the table. In this coding, the tag itself is returned: tab∘dref¨'a+b×c' ⍝ translate operands, preserve operators. 1 + 2 × 3 The above coding can be changed to use a reduction ↑{..}/ to split the left arg- ument, thus avoiding the allocation of explicit names for parts of the table. Then, within the reduction operand function, tags and vals are referenced as ⍺ and ⍵ respectively. dref←{ ⍝ Dereference from table. name←⍵ ⍝ right arg: name to look up. ↑{(⍺⍳name)⊃⍵,⊂name}/⍺ ⍝ value corresponding to name. } As a final step, we can make this a "one-liner" by turning the inner function into a monadic operator, and passing [name] as its operand. [name] is then ref- erenced as ⍺⍺. dref←{↑⍵{(⍺⍳⍺⍺)⊃⍵,⊂⍺⍺}/⍺} ⍝ Dereference from table. Another idiom worthy of note is "fold from the left". APL's primitive reduction operator '/' is applied "from the right", so to reverse this, we must commute the function operand and reverse the arguments. To build a "cons" tree, where cons (⊂) associates right, we can use primitive reduction: trees ↑{'⊂'⍺ ⍵}/ 'abcd' ⍝ tree from right. ┌⊂─┐ a ┌⊂─┐ b ┌⊂┐ c d but to build an "apply" tree, where apply associates left, we must use the com- muted form: trees ↑{'@'⍺ ⍵}⍨/⌽ 'abcd' ⍝ tree from left. ┌─@┐ ┌─@┐ d ┌@┐ c a b app←{↑{'@'⍺ ⍵}⍨/⌽⍵} ⍝ function application. Max --- Max's right argument is a script for processing prior to keyboard input. This can be a character matrix; a character vector with embedded new-lines; or a vec- tor of character vectors. Max returns as a shy result, an environment which may be re-input via its left argument as a starting point for a later session. The environment is a 4-column matrix: Name, lambda definition, combinator definition, type. Local functions in max: Stream: Takes the next complete input line. If this starts with ')', exit max, returning the environment as a shy result. Otherwise, process each line segment and then the rest of the script. Next: Returns a complete source line from the input stream. Input: Returns the next line from the script or keyboard. Prompt: Assembles the input prompt. Retract: Retracts primitive definitions from the environment leaving only user defined definitions. The environment is returned as a four-column matrix. Alph: A vector of valid names for definitions. Chars: A vector of valid input characters. The boolean argument to the unnamed function which generates chars, indicates the admission of language extensions. For pure Max, change this to 0. Parse ----- The number of operators in Max makes it just complex enough to merit a parser more general than Min's very specific one. Parse's left argument is a vector of operators in binding strength order, and its right argument, a source expression to be parsed. The result is a "parse tree": trees'+×'parse'a×b+c×d' ┌─+─┐ ┌×┐ ┌×┐ a b c d Parse has three phases: prep, post, and tree. Prep: Preprocess the source string performing simple lexical tasks that make the following pass easier. Firstly, it replaces lambda expressions of the form "\abc.X" with an infix equivalent "a\b\c\X". Secondly, it substitutes negative integers for local definition dot sequences: 'a.b...c..d' becomes 'a' ¯1 'b' ¯3 'c' ¯2 'd'. Lastly, the type digraph :: is replaced by a single character equi- valent '⊤'. Post: Converts the preprocessed source into postfix or reverse polish form. Input tokens are taken from the right argument and appended to one of two output arrays: 'ac', an accumulator for output tokens and 'sk', a stack for operators whose binding strength is less than that of those already output. The state of the process and current bracket appear in 'st' and 'bk'. State is one of: '-' initial; '∇' operator processed, expecting operand; or '⍵' operand processed. A dummy operand '?' is inserted between adjacent operators, and an explicit ap- ply operator '@' is inserted between adjacent operands. Parentheses and brackets are processed by a recursive call on post for a left (lb) one, and returning current sub-expression and remaining source tokens for a right (rb) one. Tree: Converts postfix form to the final nested array tree structure. The list separator ',' and cons operator ':' which have been kept distinct until now be- cause they have differing binding strengths are both translated to an applicat- ion of the primitive prefix function '⊂'. For example, 'ht:' → '@'('@' '⊂' h)t. Lambda ------ This function returns a lambda expression or definition from a parse tree. Two substantial subtasks are: - local definition resolution. - see function local. - pattern matching in equations - see function equn. Local ----- This function replaces local definitions using "where dots" with their lambda abstraction equivalent. In general: X.a=A → (\a.X)A Subfunction [lexp] tries to push the lambda abstraction as far down the tree as possible. For example, if X above is a function application: fx, then the trans- formation above becomes: fx.a=A → (\a.fx)A However, if variable "a" is free only in x (say) then the following is prefer- able: fx.a=A → f(x.a=A) → f((\a.x)A) If variable "a" occurs only once (or not at all) in expression X, then the lamb- da abstraction can be replaced directly with value A: fa.a=A → fA / "a" occurs once. f0.a=A → f0 / "a" does not occur. This optimisation is beneficial in its own right, and corresponds to the idea of localising names "as tightly as possible". However, the real reason for doing it, is to push name localisation below any pattern matching code, making it eas- ier to merge equations such as: p 0 j = 0 / product in terms of sum. p (+i) j = s j (p i j) . s 0 j = j / local defn of sum. . s (+i) j = +(s i j) Lambda trees for the two equations and final definition of p are: ┌=─┐ ┌=─┐ =merge=> ┌=─┐ p ┌\───┐ p ┌\──┐ p ┌\────┐ _ ┌──@┐ _ ┌─@───────┐ _ ┌───@───────┐ ┌─@─┐ ? ┌─@┐ ┌─────@─┐ ┌─@─┐ ┌─────@─┐ ┌@┐ ┌\┐ ┌@┐ ? ┌\─┐ ┌@┐ ┌@┐ ┌\┐ ┌\─┐ ┌@┐ ! _ j 0 ! _ i ┌\──┐ - _ ! _ j 0 i ┌\──┐ - _ j ··· j ··· As the local definition code is pushed below the pattern matching code, the '?' subtrees line up nicely, and the equations are easily merged. Equn ---- This function replaces a complex equation using argument patterns with its simple lambda equivalent. The pattern matching appears as explicit function calls on ! (test for zero) and ∘ (test for null). The dummy bound variable '_' may be used in the generated lambda abstractions. For example: n0=1 → n=\_.!_1? n(+i)=0 → n=\_.!_?((\i.0)(-i)) h(x:y)=x → h=\_.∘_?(\xy.x)(↑_)(↓_) The first lambda expression reads: "n is a function of _, where if _ is 0, the result is 1, otherwise it's an error". The second one reads: "n is a function of _ where if _ is zero then error, otherwise the result is the application of function (\i.0) to the predecessor of i. This last mechanism is how pattern variables assume their inverse values in the body of the expression. For example, a function f(+i)= ..i.. given an argu- ment of 4, has i with a value of 3 in its body. The third expression reads "h is a function of _, where if _ is null, then error, otherwise the result is the application function (\xy.x) to the head and tail of _". Typically, as in the first two examples above, a function definition is compris- ed of complementary equations where the error cases cancel out. Show ---- Show continually reduces an expression until either it reaches normal form, or ⎕PW characters of output have been displayed. Defn ---- The global environment is extended with a new definition, or a refinement of an existing definition. Compile ------- Compile translates an expression containing lambda abstractions into one con- sisting only of function applications. It is possible to represent any lambda expression using only the S,K and I combinators, but for non-trivial express- ions, unmanageably large expressions result. The optimisations employ additional combinators to reduce the size of the resulting tree. Max's compile is essent- ially the same as Min's, except that the table of optimisations is passed as a left argument. This is in order to restrict which optimisations are applied dur- ing the "bootstrap" process in function 'extend'. Typex ----- Typex processes Max's :: operator. The parser translates type expressions into: ⊤ exp ? / for a type query such as [0] :: ⊤ name type / for a type specification such as s :: #→#→# Typex returns a possibly updated environment and the number of output columns remaining. Type ---- Type deduces (infers) the type of a compiled expression. The expression may con- tain references to other objects in the environment which is passed as a left argument. There are two cases: If the expression is an atom, its type is referenced from the environment. Otherwise, the type is a function application: fun arg. The type of each of fun and arg is deduced recursively and the type of the resulting function applicat- ion produced by unifying function type, argument type, and a wild card type var- iable with the template for function application: func argt rslt ⍺→⍵ ⍺ ⍵ Unify ----- The unification algorithm is interesting in its own right, independent of Max. Its arguments are a pair of expressions to be unified. For example, if 'a+a' and 'b+(c×d)' are expressions with variables a, b, c and d, then we can deduce that the expressions can be unified (are equivalent) if and only if a=b=(c×d), in which case they are both equivalent to '(c×d)+(c×d)'. Internally, type var- iables: ⍺, ∊, ⍵, ··· are represented by natural numbers 0, 1, 2, ···. 1 '+' 1 unify 2 '+' (3 '×' 4) ⍝ a+a <≡> b+(c×d) ≡> (c×d)+(c×d). 3 × 4 + 3 × 4 See also: dfns.dws/notes.unify. Local functions in unify: Dist: The two expression are allocated distinct type variables. Subs: The expressions are traversed in parallel building a substitution table. For example if ⍺ on one side, matches #→# on the other, the substitution table is extended with a new entry: (⍺,#→#). Merge: Substitutions are merged into the table. For example, if (⍺,⍵→⍵) and (⍵,[#]), then (⍺,[#]→[#]). Fix: The fixpoint or power-limit operator applies its function operand repeat- edly until there is no difference between argument and result. The simplest form of this operator is {⍵≡z←⍺⍺ ⍵:⍵ ⋄ ∇ z}. However, in this case, an extra phrase aborts the process if an infinite cycle is detected. Such a cycle would occur trying to merge, for example: (⍺,[⍵]) and (⍵,[⍺]) which represents an expression with a non-finite type. Trying to infer the type of the primitive Y combinator leads to such a cycle. For this reason, Y is included in the primitive combin- ators at "boot" time because its type cannot be inferred by this method. Reduce ------ Max can accommodate expressions which represent infinite lists. Consequently, the process can't be allowed to attempt to reduce the expression to its simplest or "normal" form, as this might not terminate. The reduction proceeds to a less- er form called "weak head normal form". In this context, an expression is in WHNF if it is: - An atomic value, such as '0', or '+', - A function applied to fewer than its defined number of arguments, - A list construction of the form head:tail. Local functions in reduce: Eval: Takes a combinator expression and returns a reduced expression. There are three cases: If the expression is a function application, apply the (reduced) function to its argument. If the expression is a number or an error, return the value unchanged. Otherwise, the expression represents a function. In this case return a function suspension 4-tuple: The name of the function. An empty vector of function arguments (none so far). The argument template or function header. Definition if the function is a combinator. Apply: Takes a function suspension and an argument and returns either an extend- ed suspension or if the argument vector is complete, the result of the applicat- ion. In this case the function is either primitive, and is evaluated by [numb] or [list], or it's a combinator and so values are substituted from the argument vector into the combinator definition and the resulting expression returned. Numb: Applies a numeric function to its argument(s). All numeric primitive func- tions are "strict" in their first argument which means that this must be reduced to a number before the evaluation can proceed. List: Applies a list function to its argument(s). List primitives require that their first argument be in WHNF. Whnf: Iteratively reduces an expression to weak head normal form. Extend ------ Extend takes the initial environment input through Max's left argument and comp- lements it with definitions for each of the primitive functions and combinators. The types of the primitive functions and the definitions of the combinators are supplied by: const'ptypes' and const'cdefs'. Combinator types are inferred from their definitions; a process which is satis- fyingly circular: type: Deduces the type of the expression from the known types of its con- stituent combinators. Therefore it needs the combinator form of the definit- ion provided by 'compile'. compile: Produces the combinator form of an expression from the lambda equi- valent. Unfortunately, the optimised result may contain combinators whose type has not yet been inferred, so the process will fail. Avoiding the opt- imisation would produce excessively large combinator definitions with a con- sequent delay in initialisation. The cycle is broken by restricting the optimisations available to the compiler to those employing combinators whose type has already been determined. The pro- cess is boot-strapped with a set of "primitive" combinator types: const'ptypes', for S, K, I, and Y. As typing proceeds, compile is able to use more optimisat- ions and thus produce smaller expressions and quicker typing. Each combinator name is displayed briefly during this process. To extend Max's set of combinators, we need only add definitions to the const- 'cdefs' table. The new definitions will be typed at "boot" time. Const ----- Const produces tables of all of the constants used in the implementation. Alph: Alphabet of names that can be used in definitions. Vars: Alphabet of type variable names. Cdefs: Table of combinator definitions, each entry comprising: name, argument template, definition in terms of arguments. Ptypes: Table of types of primitive functions and combinators. Opts: Table of Curry/Turner combinator optimisations. Temps: Table of pattern matching templates. Trees ----- Trees is a utility, borrowed from Min, which is not used directly in the imple- mentation. It is handy for displaying intermediate expression trees that occur during the processing of a Max script. An example is: trees parse's0j=j, s(+i)j=+(sij), s::, ~s' ┌⋄───────────┐ ┌─=┐ ┌──────⋄───┐ ┌─@┐ j ┌─=─┐ ┌─⋄─┐ ┌@┐ j ┌──@┐ ┌@──┐ ┌⊤┐ ┌~┐ s 0 ┌@─┐ j + ┌─@┐ s ? ? s s ┌@┐ ┌@┐ j + i s i Max syntax ---------- stmt := defn | expr | type | stmt , stmt / Statement defn := name argt* = expr / Definition. argt := name | npat | lpat / Function argument. name := alph / Single char name. npat := digt | ( + argt ) / Numeric pattern. lpat := null | ( argt : lpat ) / List pattern. expr := prim | expr expr | ( expr ) | / Expression. expr whex | list prim := name | digt | pfun / Primitive object. whex := ..* defn | whex whex / Where expression. type := tdef | tenq / Type statement. tdec := name :: texp / Type declaration. tenq := expr :: / Type enquiry. texp := tvar | [ texp ] | texp → texp | / Type expression. ( texp ) list := [] | [ elts ] | expr : list / List. elts := expr | expr , elts / List elts. alph := a | b | ··· | z / Name alphabet. digt := 0 | 1 | ··· | 9 / Numeric digits. tvar := ⍺ | ⍵ | ∊ | ⍳ | ⍴ | ··· / Type variable. pfun := + / Primitive function. Where: ⍺* means 0 or more ⍺s. ⍺⍺* means 1 or more ⍺s. Binding strengths and associativity ----------------------------------- [6] (a b) c / Function application. [5] a:(b:c) / List construction. [4] a\(b\c) / Lambda abstraction. [3] a=(b=c) / Definition. [2] a.(b.c) / Localisation. [1] a,(b,c) / Item separation. [0] (a,b),c / Statement separation. Bugs ---- 1. The example using the Sieve of Eratosthenes appears to go to sleep after the promising start: [2,3,5,7,11,. This came as a bit of a blow to the author who had hoped to get rich by selling large primes to encryption agencies :-). The fault is due to the reduction engine's using call-by-name as opposed to call- by-need semantics, which leads to the repeated evaluation of arguments. The number of reductions grows rapidly with each term: 131, 835, 11,509, 117,745, 4,881,653, 38,063,959, 1,416,888,935, ... We could ameliorate this problem to some extent by using "memoization" tech- niques (see dfns.dws/notes.memo). The above example goes significantly faster if we add a simple linear cache to function [reduce]. This requires adding just two extra lines: keys vals←⍬ ⍬ ⍝ initial cache. | cache←{⊃⌽keys vals,∘⊂←⍺ ⍵} ⍝ !extend cache! | and modifying two others: eval←{ ⍝ Value of @exp. (⊂⍵)∊keys:(keys⍳⊂⍵)⊃vals ⍝ value in cache: done. | ⍴⍴⍵:⍵ cache(∇ 1⊃⍵)apply 2⊃⍵ ⍝ function application. | ~⍵∊tags:⍵ ⍝ number, null or error. ⍵'',(tags⍳⍵)⊃defs ⍝ function suspension. } ⍝ exp ← :: exp Note however, that adding the "!extend cache!" line above would violate the claim that "the implementation of Max uses no variables". 2. The type checker currently refuses to infer the type of \h.h[h], whereas it's perfectly happy with ↑[↑]. For this reason, the multi-line example in the In- troduction starting: p 2 [ / Pick 2th function from list. f . f x = h x, / head, f . f x = h (t x), / head of tail, ··· doesn't yet work, although it appears to be a correct Max expression. This may be due to the following bug: 3. Max assigns a local name (say "i") either: as a function ⍺rgument: f i = (i +)(i 0) [⍺] ¯¯¯¯¯¯¯¯ or as an expression ⍵here clause: (i +)(i 0) . i x = x [⍵] ¯¯¯¯¯ In case [⍺], the type-checker must infer the type of "i" solely from the con- text in which it is used within the body of the function. To have any chance of winding up with a reasonable typing and to catch any type errors, the checker refines its notion of a name's type using unification. In [⍺] above, the leftmost occurrence of "i" (i +) implies a type of (#→#)→⍺ and the right- most (i 0), a type of #→⍵. As these types cannot be unified, the expression as a whole fails. Note that if the checker had been more lax and assigned a type of ⍺→⍵ in both cases, the unification would have worked but the type implied by the expression (i +)(i 0) as a whole would be just ⍵, which tells us nothing. In case [⍵], the type-checker has a considerably easier job. The type of "i" can be deduced directly from its definition to be ⍺→⍺. If the checker acknow- ledges this distinction and _preserves_ rather than _refines_ this type as- signment while checking the body of the function, we wind up with (i +)(i 0) typed as #, which is spot-on. Unfortunately, this implementation of Max is unable to distinguish [⍺] from [⍵] as it converts both to lambda expressions and then to combinators _prior_ to type checking. This means that case [⍵], which should work, reports a type error. In the literature, definition "i" in [⍺] and [⍵] is termed "lambda-bound" and "let-bound" (or "where-bound") respectively. In the latter case, the type- checker should mark "i" as "generic" and refrain fom refining its type on en- countering references within the expression. Notice that a _global_ defition retains its generic type and so the following statement is accepted by the type-checker: ix=x, i+(i0) // global i::⍺→⍺ 1 Deficiencies ------------ 1. For no better reason than to explore a different technique, the original in- tention was to give Max a reduction mechanism distinct from Min's. The plan was to dispense with combinators altogether and reduce lambda expressions directly. Extended Max would expose these together with the set of internal primitive functions and a tracer would show the reduction of lambda, rather than combinator, expressions. z.z=0:z ; ∇(\z.0⊂z) ¯¯¯¯¯¯¯¯¯ (\z.0⊂z)(∇(\z.0⊂z)) ¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯ 0⊂∇(\z.0⊂z) ¯¯¯¯¯¯¯¯¯ 0⊂(\z.0⊂z)(∇(\z.0⊂z)) ¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯¯ 0⊂0⊂∇(\z.0⊂z) ¯¯¯¯¯¯¯¯¯ ··· A simple eval-apply lambda reducer ran into trouble with successive list items forcing the accumulation of multiple environments. This extra baggage seemed to slow reduction to an unacceptable degree and any attempt to "factor out" common environments didn't seem to pay off. A version powered by a lazy (call-by-name) SECD machine (Landin 1964) worked surprisingly well and a call-by-need version would certainly be worth re- visiting. However, while at first showing promise, these attempts foundered on the difficulty of inferring the type of lambda abstractions. Ways of achieving this are well understood, but sadly not by this author. An overriding bene- fit of the combinator implementation is that expressions are comprised ex- clusively of primitive objects of known type and function applications. Such constructs can be typed in a single recursive pass. No attempt has yet been made to implement a more modern engine such as STG (The Spineless Tagless G-Machine - Peyton Jones 1992) or TIM (The Three In- struction Machine - Peyton Jones and Lester 1992). 2. An earlier draft of Max supported "tuples". A tuple is Max's equivalent of a structure or record and is distinguished from a list by being enclosed in parentheses: (+,0,[]). A tuple is in some sense the dual of a list: a list of a particular type may have a varying number of items but each must be of the same type; a tuple has a fixed number of items but each may be of a distinct type. The type of the above example is denoted:: (#→#,#,[⍺]). The construct was later removed because the extra facility it provided to the language didn't quite seem to justify the additional complexity its imple- mentation incurred. An example of the distinction between lists and tuples is the old APL favour- ite, the "inverted" file. A "regular" component file where each component contains many fields is analogous to a list-of-tuples, whereas an inverted file (one component per field type), is a tuple-of-lists. 3. At present there is no tracer, but if one were added, it might be pleasing to watch the type inference process. It's not clear what this should look like for lambda abstractions, but for simple applicative expressions, perhaps something along the lines of: ↑[↑][↑] :: ; ([⍺]→⍺)[[⍺]→⍺][[⍺]→⍺] ¯¯¯¯¯¯¯¯¯¯¯¯¯¯ ([⍺]→⍺)[[⍺]→⍺] ¯¯¯¯¯¯¯¯¯¯¯¯¯¯ [⍺]→⍺ Starting Over ------------- In summary, a rewrite of Max might: - Reintroduce tuples; - Have the type-checker distinguish where-bound from lambda-bound definitions; - Reduce compiled lambda expressions directly using a call-by-need machine; - Implement a tracer; - Perhaps implement some sort of optional tracing of the type inference process. Background ---------- Local definitions using indentation appeared in Landin's language ISWIM (If you See What I Mean) in 1966. He used the term "off-side rule" (borrowed from Socc- er) to describe the scheme. The off-side rule is employed in a number of modern functional languages including Haskell (1999). In his paper "Basic Polymorphic Typechecking" (1987), Luca Cardelli gives the following "bit of history": "Polymorphic typing of programs was envisioned by Strachey; his lecture notes on fundamental concepts of programming languages [Strachey 1967] already contain much of the notation and terminology used today. Polymorphic types were already known as "type schemas" in combinatory logic [Curry 1958]. Extending Curry's work, and collaborating with him, Hindley introduced the idea of a principal type schema, which is the most general polymorphic type of an expression, and showed that if a combinatorial term has a type, then it has a principal type [Hindley 1969]. In doing so, he used a result by Robinson about the existence of most general unifiers in the unification algorithm [Robinson 1965]. These results contained all the germs of polymorphic typechecking, including the basic algorithms. The ex- istence of principal types means that a type inference algorithm will always compute a unique "best" type for a program; moreover, unification can be used to perform this computation. However, these results did not immediately influence the programming language community, because of their theoretical setting. Influenced by Strachey, and independently from Hindley, Milner rediscovered many of these ideas in the context of the LCF proof generation system [Gord- on 1979], which included the first version of the ML language [Milner 1984]. He introduced a crucial extension to Hindley's work: the notion of generic and non-generic type variables, which is essential for handling declarations of polymorphic functions. Milner implemented the first practical polymorphic typechecker, and showed that the type system is sound [Milner 1978]. More recently, Milner and Damas proved the principal-type property for the ex- tended system [Damas 1982] which implies that the type system is decidable." References ---------- 1. Cardelli, L., (1987) Basic Polymorphic Typechecking. Science of Computer Programming 8/2. http://research.microsoft.com/Users/luca/Papers/BasicTypechecking.A4.ps 2. Curry, H.B., Feys, R. (1958) Combinatory Logic, North-Holland, Amsterdam. 3. Damas, L., Milner, R., (1982) Principal type-schemes for functional pro- grams, Proc. POPL 82, pp. 207-212. 4. Gordon, M.J., Milner, R., Wadsworth, C.P., Edinburgh LCF, Lecture Notes in Computer Science, No 78, Springer-Verlag. 5. Hindley, R., (1969) The principal type scheme of an object in combinatory logic, Transactions of the American Mathematical Society, Vol. 146. 6. Landin, P.J., (1964) The Mechanical Evaluation of Expressions. Computer Journal, 6. pp 308-320. 7. Landin, P.J., (1966). The Next 700 Programming Languages. Communications of the ACM 9, 3. pp 153-403. 8. Milner, R., (1978). A Theory of type polymorphism in programming. Journal of Computer and System Science. Vol. 17, pp.348-75. 9. Milner, R., (1984) A proposal for Standard ML, Proc. of the 1984 ACM Sym- posium on Lisp and Functional Programming. 10. Peyton Jones, S.L., (1992). Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine. Journal of Functional Programm- ing 2(2), July 1992, pp. 127-202 11. Peyton Jones, S.L. and Lester, D.R., (1992). Implementing functional lang- uages: a tutorial, Prentice Hall, 1992. Now out of print, but try: ftp://ftp.dcs.glasgow.ac.uk/pub/pj-lester-book/ 12. Peyton Jones, S. and Hughes, J. (editors) (1999) Haskell 98 - A non-strict, purely functional language. http://www.haskell.org/definition 13. Robinson, J.A., (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM. Vol. 12, No. 1, pp. 23-41. 14. Strachey, C. (1967) Fundamental concepts in programming languages, lecture notes for the International Summer School in Computer Programming, Copen- hagen, 1967. Back to: contents