A Practical Subt yping System F or Erlang Simon Marlo w Philip W adler simonmdcsglaacuk wadlerresearchbellla bs com Univ ersit y of Glasgo w Bell Labs Lucen t T ec hnologies Abstract W e presen t a t yp e system for the programming language Er lang The t yp e system supp orts subt yping and declaration free recursiv e t yp es using subt yping constrain ts Our sys tem is similar to one explored b y Aik en and Wimmers though it sacrices expressiv e p o w er in fa v our of simplicit y W e co v er our tec hniques for t yp e inference t yp e simplic ation and c hec king when an inferred t yp e conforms to a usersupplied t yp e signature and rep ort on early exp erience with our protot yp e In tro duction W e can stop w aiting for functional languages to b e used in practicethat da y is here Erlang is a strict un t yp ed func tional language with supp ort for concurrency comm unica tion distribution faulttolerance onthey co de reloading and m ultiple platforms A VW Applications exist that consist of up w ards of half a million lines of co de This pap er do cumen ts our exp erience in designing and building a t yp e system for Erlang Our t yp e system pro vides t yp e inference with subt yping declarationfree recursiv e t yp es t yp e signature c hec king and data abstraction So far w e ha v e successfully applied our protot yp e to ab out of the lines of co de in the Erlang standard library and an ticipate no diculties in applying it to the remainder W e exp ect that adding a t yp e system to Erlang will impro v e do cumen tation main tenance and reliabilit y Our t yp e system had t w o goals First it should t yp e existing Er lang co de with little or no mo dication Second it should b e easy to comprehend Whereas man y t yp e systems striv e to maximise expressiv e p o w er our aim is to maximise sim plicit y consisten t with ha ving sucien t p o w er to describ e Erlang as it is t ypically used in practice Our rst goal rules out the p opular t yp e system devised b y Hindley and Milner Hin Mil DM The dicult y is that with HindleyMilner eac h t yp e m ust in v olv e a set of constructors distinct from those used in an y other t yp es a con v en tion not adhered to b y Erlang programmers So w e need a t yp e system that allo ws one constructor to b elong to sev eral dieren t t yp es One p ossibilit y is t yp es App ears in the In ternational Conference on F unctional Programming Amsterdam June based on ro w v ariables as in tro duced b y W and W an and used as the basis of the soft t yp e system for Sc heme b y Cart wrigh t F agan and W righ t CF W C It turns out that the ro w v ariable system rejects some programs that seem quite natural to us and the circumlo cutions w e had to go through to construct an equiv alen t program that w as w ell t yp ed struc k us as hard to explain This isnt a prob lem for soft t yping systems where the goal is to impro v e p er formance b y remo ving runtime t yp e c hec king and therefore maxim um information is of greater b enet than a natural notion of t yping The alternativ e that w e adopted is to build a t yp e system based on subt yping T yp e systems with subt yping ha v e b een studied b y sev eral researc hers Mit FM MR Rey and are based on solving systems of t yping constrain ts of the form U V where U and V are t yp es HindleyMilner systems b y con trast are based around equalit y constrain ts of the form U V whic h can b e solv ed b y unication Subt yping systems are strictly more general than Hindley Milner systems eac h program that can b e t yp ed b y Hindley Milner has a t yping in a subt yping system but not vice v ersa Our t yp e system is based around the system dev elop ed b y Aik en and Wimmers A W except sacrice express iv e p o w er in fa v our of simplicit y W e c hose the smallest t yp e language consisten t with describing t ypical Erlang pro grams w e supp ort disjoin t unions a limited form of com plemen t and recursiv e t yp es but not general unions or in tersections or conditional t yp es A WL Our exp ectation w as that these additional features w ould not help program mers but w ould mak e inferred t yp es less readable W e ha v e succeeded in that our simplied inferred t yp es are usually readable On the other hand w e ha v e encoun tered at least one situation where conditional t yp es w ould b e useful as discussed in Section The t yp e system presen ted here do es not include func tion t yp es since rstclass functions are not a feature of the curren t v ersion of Erlang Ho w ev er the so ontob ereleased Erlang supp orts rstclass functions and w e ha v e suc cessfully extended our protot yp e implemen tation to include function t yp es While w e conjecture that our t yp e c hec k ing algorithm without function t yp es is complete the w ork of T rifono v and Smith TS sho ws a similar system with function t yp es is incomplete although they claim this is not a serious problem in practice W e discuss this in Section W e demonstrate our system with a small program to manipulate sorted binary trees of k eys and v alues Figure sho ws a t yp e declaration and three Erlang functions with deftype treeAB T when T empty branchABTT type new tree new empty type insertABtreeAB treeAB insertKVempty branchKVemptyempty insertKVbranchKVLR if K K branchKVinsertKVLR K K branchKVLR true branchKVLinsertKVR end type lookupAtreeAB B error when B error lookupKempty error lookupKbranchKVLR if K K lookupKL K K V true lookupKR end Figure Binary T ree Example t yp e signatures All t yp e information is treated as annota tions whic h in Erlang are prefaced with a dash The basic data structures in Erlang are in tegers oats atoms suc h as empty and tuples suc h as branchKVLR where branch is an atom and K V L R are structures In our system the t yp es of these are resp ectiv ely written integer float empty and branchABTT where K has t yp e A V has t yp e B and L and R ha v e t yp e T Wh y w e write branchABTT in stead of branchABTT will b e explained in Section The empt y t yp e con taining no v alues is written and the univ ersal t yp e con taining all v alues is written In Erlang atoms and functions b egin with a small letter while v ariables b egin with a capital letter functions ma y b e distinguished from atoms b ecause they are follo w ed b y paren theses The same thing w orks at the t yp e lev el where empty is the t yp e of an atom integer is a builtin t yp e returning the t yp e of all in tegers and A is a t yp e v ariable The deftype annotation denes the t yp e treeAB while the three type annotations sp ecify t yp e signatures for the functions new insert and lookup These annotations allo w the user to do cumen t the program and the t yp e to ol c hec ks that the program conforms to that do cumen tation When m ultiple mo dules are pro cessed one ma y sp ecify that the name of a t yp e is exp orted without exp orting its den ition thereb y supp orting t yp e abstraction F or instance if this mo dule exp orts the t yp e tree without exp orting its denition then the t yp e system will ensure that only the three functions dened in it ha v e access to the represen ta tion of trees The function empty tak es no argumen ts and returns a tree the function insert tak es a k ey a v alue and a tree new A when empty A insertB C D A when branchEFGA A branchBCGH A branchEFAH A branchBCemptyempty A D empty branchEFGH G empty branchEFGH H empty branchEFGH H D G D lookupB C A when error A C empty branchDEFG F empty branchDEFG G empty branchDEFG E A F C G C Figure Inferred T yp es new empty insertD E F A when empty branchDEAA A F empty branchDEFF lookup B error A when B empty branch error A B B A error Figure Simplied T yp es and returns a new tree with the k ey and v alue inserted and the function lookup tak es a tree and a k ey and returns the v alue corresp onding to that k ey or the atom error if the k ey is not found T o a v oid an y p ossibilit y of confusing a success and failure the t yp e sp ecied for lookup adds the constrain t that the v alue t yp e B cannot include the atom error written B error In general the form of a t yp e signature is U when C where U is a t yp e and C is a set of constrain ts One problem with using a t yp e system built around sub t yping is that the set of constrain ts can b e arbitrarily large and inferred t yp es can b e dicult to read if they are not simplied This is one reason for fa v ouring simplicit y o v er expressiv eness the more expressiv e the t yp e language the more dicult it is to simplify t yp es Exp erimen ts with our protot yp e ha v e b een promising as for most functions w e can deriv e a natural and readable v ersion of its inferred t yp e Figure sho ws the t yp es deriv ed b y our inference al gorithm for the three tree op erations and Figure sho ws the same t yp es after simplication The userpro vided t yp e signatures dier considerably from the inferred and simpli ed t yp es First userpro vided t yp es ma y refer to t yp e denitions whic h do not app ear in inferred or simplied t yp es F or instance signature for new declares the function to ha v e t yp e tree where is the empt y t yp e whereas the simplied inferred t yp e is simply empty the empt y tree Second the userpro vided t yp es ma y b e more sp ecic than the inferred t yp e F or instance the signature for lookup restricts the t yp e A of the lo okup k ey to b e the same as the k ey elds in the tree and the t yp e B of the v alue elds in the tree not to con tain error whereas in the simplied inferred t yp e B is the t yp e of the tree and A is the t yp e of nonerror v alue elds but v alue elds ma y sp ecically include error Inferred t yp es are principal in that the inferred t yp e of a function has all other p ossible t yp es of that function as instances Ho w ev er as simplication demonstrates the same t yp e ma y b e written in man y forms Simplied t yp es are equiv alen t to the original in that they represen t the same set of v alues in the seman tic domain T o c hec k usersupplied t yp e signatures w e need to de termine when a one t yp e is an instance of another t yp e This problem turns out to b e surprisingly tric ky The prob lem has b een analysed b y T rifono v and Smith TS for a t yp e language con taining function t yp es but no t yp e union con v ersely ours con tains t yp e union but no function t yp es and they pro vide an algorithm whic h is sound but not com plete and lea v e the question of decidabilit y op en In this pap er w e giv e an algorithm whic h w e b eliev e is b oth sound and complete for our t yp e language but so far w e ha v e b een unable to nd a pro of The pap er is organised as follo ws Section in tro duces the syn tax of expressions and t yp es Section describ es the t yping rules for expressions Section presen ts a t yp e recon struction algorithm Section sho ws ho w to solv e systems of t yping constrain ts Section explains ho w to simplify t yp es Section describ es our algorithm for t yp e signature matc hing Section sk etc hes extensions to the t yp e system for pro cesses and higherorder functions Section relates our exp erience with the protot yp e implemen tation Section concludes Expressions and T yp es The syn tax of expressions w e will b e using is giv en in Figure The language is a small subset of Erlang con taining v ariables constructor applications called tagged tuples in Erlang function calls and simple case expressions W e use the o v erbar to indicate a sequence of ob jects for example E E 1 ;:::; E n The length of the sequence is normally discernable from the con text Eac h constructor has a xed arit y so in c f E g the length of the sequence of expressions E is equal to the arit y of the constructor c When there is no lengthxing con text the length of the sequence is arbitrary Standard Erlang do esnt ha v e constructor applications It has atoms whic h w e represen t as n ullary constructor ap plications and it has arbitrary tuples written f E 1 ;:::; E n g In our t yp e system w e use the con v en tion that if the rst elemen t of a tuple in an Erlang program is an atom then w e con v ert the tuple to a tagged tuple using the atom name as the constructor If the rst elemen t is some other expres sion then the tuple is an anon ymous tuple and w e assign the constructor tuple n where n is its arit y There are sev eral other dierences b et w een Erlang and our small subset All pattern matc hing is compiled in to simple case f ; g function names c ; d constructors X ; Y ; Z v ariables E X expression j c f E 1 ;:::; E n g j f E 1 ;:::; E n j case E 0 of c 1 f X 1 g E 1 c n f X n g E n X E n +1 end pr o g f 1 X 1 E 1 f n X n E n program Figure Expressions c ; d constructors ; t yp e v ariables U ; V P j U union t yp e j R P ; Q c f U g prime t yp e R cs remainder j cs j Figure T yp es expressions Algorithms to do this are w ell kno wn Aug W ad Case expressions alw a ys ha v e a default alternativ e of the form X E A sp ecial form of this is used to indicate that the alternativ e should nev er b e tak en X empty X where empty is a builtin function whic h alw a ys fails In terpro cess comm unication is omitted for no w W e discuss an extension to handle this in Section Programs consist of a set of toplev el function declara tions whic h ma y b e recursiv e Our t yp e system will assign p olymorphic t yp es to these function declarations The seman tics of our language is strict ie function argu men ts are alw a ys ev aluated b efore the function is called and constructor argumen ts are ev aluated b efore the structure is built The syn tax of t yp es is giv en in Figure Prime t yp es are written c f U 1 ;:::; U n g and represen t the t yp e of a tagged tuple with tag c arit y n and eld t yp es U 1 ::: U n The general form of a union t yp e U is c 1 f U 1 g j ::: j c n f U n g j R where R represen ts a r emainder A remainder is either a t yp e v ariable cs the univ ersal t yp e cs or the empt y t yp e The syn tax cs for a t yp e v ariable means that ranges o v er all t yp es not con taining elemen ts with the tags c 1 ;:::; c n cs The tags cs are called the exclude d tags on the t yp e v ariable Similarly the syn tax cs represen ts the univ ersal t yp e excluding t yp es with tags c 1 ;:::; c n If the list cs is empt y it is normally omitted When the remainder is or cs the t yp e is called a monot yp e The op erator j is a disjoin t union This means that in the t yp e expression P j U the t yp es P and U cannot o v erlap under an y legal substitution for the free v ariables of either t yp e This implies t w o further restrictions on the form of the general union t yp e c 1 f U 1 g j ::: j c n f U n g j R the tags cs m ust b e distinct and if R is of the form ds or ds then cs ds where cs is c 1 ;:::; c n This syn tax of t yp es pro vides exactly the lev el of gen eralit y w e require for t yping Erlang The main dierences b et w een this system and that of Aik en and Wimmers A W are the lac k of a general in tersection instead w e only al lo w excluded tags whic h w ould b e represen ted with in tersection in the Aik enWimmers system the lac k of function t yp es As men tioned in the in tro duction w e lea v e out function t yp es b ecause the curren t v ersion of Erlang do esnt supp ort them Our union op erator is equiv alen t to that used in the Aik enWimmers system except that w e do not allo w general nondisjoin t union on the left of a constrain t Ho w ev er general union on the left of a constrain t can alw a ys b e re placed b y sev eral constrain ts without union op erators The presence of the univ ersal t yp e is in teresting in fact w e nev er infer t yp es con taining the univ ersal t yp e although some t yp es are simplied b y replacing t yp e v ariables in neg ativ e p ositions 1 b y the univ ersal t yp e Exp erimen tation with the protot yp e p ersuaded us that the univ ersal t yp e in a p ositiv e p osition is useful for expressing the t yp e of certain Erlang builtin functions for whic h our t yp e system cannot pro vide precise t yp es F or example the function element selects the n th elemen t of an arbitrary tuple The b est t yp e for this function in our system is int ; tuple where int and tuple are builtin t yp es represen ting in tegers and tuples resp ectiv ely Without the univ ersal t yp e it w ould not b e p ossible to giv e a sound t yp e to this function Subt yping Constrain ts Subt yping constrain ts are written U V A constrain t is v alid if all v alues of the t yp e U are also v alues of the t yp e V W e use the iden tiers C and D to refer to sets of subt yping constrain ts where a constrain t set is v alid if and only if all the individual constrain ts are v alid If the t yp es in a constrain t set con tain t yp e v ariables the v alidit y of the set dep ends on a substitution from t yp e 1 A t yp e is in a negativ e p osition if it app ears in an argumen t p osi tion of a function t yp e or on the righ t hand side of a constrain t Result t yp es and the left hand sides of constrain ts are p ositiv e p ositions v ariables to typ e values A t yp e v alue is a certain p ortion of the seman tic domain for example in teger list of c har acters and tree of in teger pairs are all t yp e v alues a set of v alues is another w a y of thinking of it An ideal mo del similar to that in MPS or recursiv e t yp e equations as used b y T rifono v and Smith TS w ould pro vide a suitable framew ork for dening t yp e v alues A substitution is a solution of a constrain t set i its application renders the constrain t set v alid W e use some shorthand forms for sequences of similar subt yping constrain ts U V U 1 V 1 ;:::; U n V n U V U V 1 ;:::; U V n U V U 1 V ;:::; U n V En tailmen t W e also in tro duce an en tailmen t op erator o v er constrain t sets written as follo ws C D whic h is true if all solutions of C are also solutions of D En tailmen t is reexiv e and transitiv e W e will also use another form of en tailmen t : : C D whic h is true if ev ery substitution mapping to t yp e v alues that solv es C can b e extended to a solution of D b y adding mappings for It follo ws from this denition that m ust con tain at least the free t yp e v ariables of C If the free t yp e v ariables of D are a subset of those of C then the t w o op erators ab o v e are equiv alen t The latter op erator is used to dene t yp e instance in Section F unction T yp es Although our t yp e language do es not ha v e a general func tion space op erator w e assign t yp e sc hemes to toplev el functions in the source program T oplev el function t yp e sc hemes are p olymorphic and constrained They tak e the follo wing form : U V when C F unction t yp e sc hemes cannot ha v e an y free t yp e v ariables that is FTV U V when C T yping Rules W e giv e the t yping rules for expressions in t w o forms This section describ es a traditional set of t yping rules for subt yp ing and the follo wing t w o sections describ e our algorithm to determine the most general t yping of an expression The t yping rules in traditional format are giv en in Figure The form of a judgemen t is F A C E U Elemen ts of F ha v e the form f : U V when C Elemen ts of A ha v e the form x U The judgemen t asserts that under function assumption F and v ariable assumption V ar F A ; X U C X U Sub F A C E U C U V F A C E V F un F ; f : U V when D A C ; D V = f U V V = Con F A C E U F A C c f E g c f U g Call F A C f U V F A C E U F A C f E V Case F A C E 0 c 1 f U 1 g j ::: j c n f U n g j U F A ; X 1 U 1 C E 1 V ::: F A ; X n U n C E n V F A ; X U C E n +1 V F A C case E 0 of c 1 f X 1 g E 1 ::: c n f X n g E n X E n +1 end V Multi F A C E 1 U 1 ::: F A C E n U n F A C E U Def F ; f U V when C X U C E V FTV U V when C F C f X E : U V when C Figure T yping Rules A expression E has t yp e U whenev er the constrain t set C is satised The t yping rule for function names F un instan tiates the quan tied v ariables with arbitrary t yp es It also copies the constrain ts D from the function t yp e in to the curren t con strain t set C ensuring that the constrain ts on the function t yp e are satised eac h time the function is called As men tioned in Section w e assume one builtin func tion empty with t yp e empty The empt y function is the only means b y whic h a func tion ma y fail if empt y is ev er called at run time the program exits The rules allo w an y expression to b e assigned a t yping but only t ypings in whic h C has at least one solution are useful these are called v alid t ypings If an y v alid t yping exists then it is guaran teed that the program will nev er call empty at run time Subt yping is in tro duced with the subsumption rule Sub whic h allo ws the t yp e U of an expression to b e re placed with an y larger t yp e V pro vided the en tailmen t re lation C U V holds the en tailmen t op erator w as de scrib ed in Section The simplest w a y for this relation to hold is if C con tains U V F or case expressions the t yp e of the selector E 0 is re quired to b e smaller than the union of the t yp es of the pat tern alternativ es and the t yp e of the v ariable X b ound in the default alternativ e c 1 f U 1 g j ::: j c n f U n g j U where eac h t yp e c i f U i g is the t yp e of a pattern and U is the t yp e of X By the rules of the disjoin t union op erator this implies that the t yp e U cannot con tain an y elemen ts with the tags c 1 ;:::; c n Compare this with traditional HindleyMilner t yp e c hec king where there is no w a y of represen ting or ex ploiting the fact that the t yp e of the default v ariable ma y exclude t yp es handled b y earlier case branc hes In order to t yp e an arbitrary expression w e need to kno w t w o things whether a v alid t yping exists and the most general form of that t yping Note that in general there is no unique mostgeneral t yp e for a giv en function in this system Indeed the t yp e simpli cation pro cess that w e will describ e in Section attempts to replace a t yp e with an equiv alen t simpler t yp e Tw o t yp es are equiv alen t if they are instances of eac h other w e will discuss subt yp e instance in Section In our implemen tation t ypings are deriv ed in t w o stages Firstly t yp e reconstruction deriv es a t yp e and a set of t yping constrain ts for the expression This is the most general t yping of the expression if the constrain ts are satisable The second stage constrain t set reduction determines the solv abilit y of the constrain t set If the set is solv able then w e ha v e a t yp e for the expression These t w o stages are describ ed in the next t w o sections T yp e reconstruction The t yping rules can b e used in a syn taxdirected w a y to generate a constrained t yp e as follo ws Assign a fresh t yp e v ariable to eac h new b ound v ari able Th us the assumption A binds v ariables to unique t yp e v ariables Assign a fresh t yp e v ariable for the t yp e of eac h case expression Use subsumption in the follo wing places to promote the t yp e of eac h function argumen t in a function call to promote the t yp e of eac h branc h in a case expres sion to a common sup ert yp e whic h is a fresh t yp e v ariable and to promote the t yp e of the selector in a case expression to the union of the pattern t yp es F or eac h use of subsumption place the required con strain t in C so that the en tailmen t relation is trivially satised P j U V P V ; U V U none cs fail cs c f U g j U U ; cs U if c = cs cs U otherwise cs ds none if ds cs fail otherwise cs ds cs ds if ds cs fail otherwise c f U g fail c f U g c f U g j U U U if c c c f U g U otherwise c f U g cs none if c = cs fail otherwise c f U g cs c f U g cs if c = cs fail otherwise U cs ; cs V U V ; U cs ; cs V Figure Reduction Rules Prop osition principal t yp e prop ert y Ev ery t yp e deriv able for a function using the t yping rules is an instance of the t yp e deriv ed b y the t yp e reconstruction algorithm The pro of of this prop osition is similar to Mitc hells pro of of principal t yp es for his subt yping system Mit Constrain t Set Reduction Constrain t Reduction is the pro cess of determining whether a system of constrain ts is solv able If a constrain t system generated b y the t yp e reconstruction algorithm is not solv able it indicates that the program has a t yp e error W e do not ha v e to disco v er an actual solution to the set merely pro v e that one or more solutions exist This is done b y rep eatedly transforming the constrain t system while main taining transitiv e closure and c hec king for t yp e errors The transformation system is giv en in Figure Eac h rule applies to one or more constrain ts from the curren t set and yields one of the follo wing results fail indicating that the constrain t system has no solu tions and the original function therefore con tains a t yp e error none indicating that the constrain t should b e re mo v ed from the system one or more transformed constrain ts The original con strain ts are to b e remo v ed from the set A constrain t set is only fully reduced when b oth of the follo wing conditions apply Eac h constrain t in the set is of the form cs U or U cs and An y rule that can b e applied w ould tak e the constrain t set in to a state that has o ccurred b efore If the reduction pro cess terminates without failure the resulting constrain t set is said to b e c onsistent F or reasons of eciency w e ignore the strictness of con structors for t yp e inference purp oses In other w ords the t yp e of c fg in our system is c f g not A similar situation is found in A W where some solutions to the constrain t set are discarded for eciency Prop osition When applied to an arbitrary constrain t set the reduction pro cess either fails or terminates yield ing a consisten t constrain t set Pro of sk etc h Observ e that all rules in the transform ation algorithm except the last transitivit y either fail or split a constrain t in to zero or more constrain ts on subterms of the originals un til all the constrain ts ha v e a v ariable on one side or the other All the cases are co v ered so an y con strain t set can b e reduced to a state where all constrain ts are of the form cs U or U cs The transitivit y rule forms a new constrain t from exist ing t yp es This rule cannot b e applied indenitely without reac hing a xed p oin t b ecause there are only a nite n um b er of p ossible constrain ts to add W e m ust therefore reac h a state where all constrain ts are on v ariables and the only rule whic h can b e applied to c hange the set is transit ivit y and all p ossible constrain ts ha v e already b een added to the set Prop osition A consisten t constrain t set is solv able Pro of sk etc h W e pro v e this prop ert y b y relation with the inductiv e constrain t system of Aik en and Wim mers A W A consisten t constrain t set in our system can b e transformed in to an inductiv e constrain t set and the pro cess cannot fail Inductiv e constrain t sets w ere sho wn to b e solv able b y Aik en and Wimmers The sub ject of inductiv e form and the algorithm for con v erting a consisten t constrain t set in to an inductiv e con strain t set are discussed in Section T yp e Simplication The t yp e assigned to a function b y the t yp e inference al gorithm can b e large and un wieldy making it dicult for a user to in terpret and exp ensiv e for an implemen tation to deal with Therefore w e apply a n um b er of simplifying trans formations to the t yp e in an attempt to deriv e an equiv alen t t yp e that con tains few er t yping constrain ts Our simplication transformations are similar to those of F ahndric h and Aik en F A who use t yp e simplication amongst other tec hniques to sho w that setconstrain tbased analyses are scalable to large examples W e ha v e not found a suitable normal form for a con strained t yp e nor ha v e other researc hers in this area W e cannot therefore hop e for a simplication pro cedure that is complete There are sometimes t yping constrain ts whic h cannot b e eliminated one example is when the constrain ts are b eing used to represen t a recursiv e t yp e Ho w ev er the transformations giv en in this section are based on heurist ics that w e ha v e found to b e eectiv e In man y cases the deriv ed t yp e can b e simplied to the t yp e that one w ould normally assign to the function The constrain t set generated b y the t yp e inference al gorithm satises three imp ortan t prop erties that w e can mak e use of during simplication Eac h constrain t in the system is of the form cs U or U cs termed upp er and lo w er b ounds on resp ectiv ely F or an implemen tation this means that w e can represen t the constrain t set as a mapping from v ariables to sets of upp er and lo w er b ounds This prop ert y will hold throughout simplication Separate o ccurrences of the same v ariable will ha v e iden tical excluded tag lists This prop ert y will hold throughout simplication The constrain t set is transitiv ely closed That is for eac h constrain t pair cs ds and ds U the set con tains the constrain t cs U and for eac h pair U ds and ds cs the set con tains U cs W e will not retain this prop ert y during simplication although the transitiv e closure can alw a ys b e reco v ered b y adding the necessary constrain ts to the system General Simplications The follo wing transformations are applied whenev er the op p ortunit y arises during the simplication pro cess cs cs none cs none cs ds none if ds cs Eliminating Cycles Our implemen tation eliminates cycles in the constrain t set as a rst step since it has a dramatic eect on the e ciency of the rest of the simplication pro cess and is relat iv ely c heap to p erform The idea is to rst iden tify all cycles b et w een v ariables Since in an y solution of this constrain t set the v alues of these v ariables m ust b e iden tical w e can replace all o ccurrences of the v ariables with a new v ariable The transformation is giv en in Figure a If the constrain t set is treated as a graph with the v ari ables as no des then cycles can b e found in linear time using standard algorithms and remo v ed in linear time using the ab o v e substitution The result is a directed acyclic graph A constrain t set in this form is called c ontr active TS Com bining Upp er and Lo w er Bounds In general a v ariable ma y ha v e sev eral upp er and lo w er b ounds The purp ose of this simplication stage is to reduce the n um b er of upp er and lo w er b ounds on eac h v ariable b y com bining them where p ossible Com bining Lo w er Bounds It is alw a ys p ossible to com bine the lo w er b ounds on a v ari able suc h that w e ac hiev e a normal form 1 ds n ds c 1 f U 1 g j ::: j c n f U n g j ds After com bination the lo w er b ounds on a v ariable will consist of zero or more v ariableonly lo w er b ounds and at most one constructed lo w er b ound a union t yp e where the remainder is This is ac hiev ed b y applying the transform ation rules of Figure b and collecting the no w distinct prime t yp e lo w er b ounds on eac h v ariable in to a singe union t yp e F or example if w e ha v e the follo wing constrain t set c f U g ; c f V g then w e can replace this with c f g ; U ; V where there is no w only a single lo w er b ound on the v ariable There are no w t w o lo w er b ounds on the v ariable whic h can b e com bined in the same w a y Com bining Upp er Bounds Unlik e lo w er b ounds w e ha v e found no useful normal form for upp er b ounds b ecause w e cannot compute the in tersec tion of sev eral union t yp es and represen t the result in our t yp e syn tax Instead w e use some heuristics to com bine upp er b ounds where p ossible An example of one of the transformations used is giv en in Figure c where t w o upp er b ounds are com bined if they are monot yp es This is an imp ortan t transformation for our t yp e c hec king algorithm in Section T ransitiv e Kernel During the simplication pro cess w e w ork with the tr ans itive kernel of the constrain t set The transitiv e k ernel of a transitiv ely closed constrain t set C is dened as the smal lest constrain t set D suc h that the transitiv e closure of D is C If C is con tractiv e Section then there is a single unique D computed b y applying the transformation rule in Figure d as man y times as p ossible to the constrain t set The adv an tages of w orking with the transitiv e k ernel are The set is smaller but con tains the same information The original constrain t set can b e reco v ered b y forming the transitiv e closure Our simplifying transformations are equally v alid when applied to the transitiv e k ernel In fact remo v ing the transitiv e constrain ts can enable some trans formations that w ere not previously p ossible As an example of the second p oin t the v ariable elimin ation transformation is only applicable when a v ariable has a single upp er or lo w er b ound if there are other constrain ts on the v ariable that are presen t due to transitivit y then the transformation cannot b e applied W e could tak e in to ac coun t these transitiv e constrain ts during the transformation but it is simpler to compute the transitiv e k ernel once and main tain it throughout simplication Eliminating V ariables The transformation describ ed in this section is simple and y et remark ably eectiv e in simplifying t yp es The basic idea is to nd a v ariable with a single upp er b ound or a single cs 1 1 cs 2 2 ; : : : ; cs n n cs 1 1 ; C C ds = cs n 1 ; : : : ; ds = cs n n where fresh ; ds cs 1 ::: cs n a Eliminating Cycles c f U g j U cs c f U g cs ; U cs c f U g cs ; c f U g cs c f g cs ; U ; U where fresh b Com bining Lo w er Bounds cs c 1 f U 1 g j ::: j c n f U n g j a 1 f V 1 g j ::: j a m f V m g j R 1 cs c 1 f U 1 g j ::: j c n f U n g j b 1 f V 1 g j ::: j b l f V l g j R 2 cs c 1 f 1 g j ::: j c n f n g j f a i f V i g j in a i ; R 2 g j f b i f V i g j in b i ; R 1 g U i i i n U i i i n where i fresh i n in c ; cs c = cs in c ; false c Com bining Upp er Bounds U 1 U 2 ;:::; U n 1 U n ; U 1 U n U 1 U 2 ;:::; U n 1 U n d T ransitiv e Kernel Figure Simplifying T ransformations lo w er b ound and replace it with this b ound when it is legal to do so F or example the t yp e when c fg is equi v alen t to simply c fg and the rst t yp e can b e simplied to the second b y replacing the v ariable with its single lo w er b ound c fg The rst transformation applies to v ariables with a single upp er b ound U when cs V ; C U when C V = cs There are some restrictions on this transformation There are no cycles in the constrain t set in v olving cs cs app ears only negativ ely in U and C cs m ust ha v e v ariableonly lo w er b ounds unless V is a v ariable This is to retain the in v arian t that all constrain ts are on v ariables The substitution U when C V = cs m ust b e legal with resp ect to the disjoin t union op erator The rst restriction is to prev en t the transformation from b eing applied indenitely as w ould b e the case if the v ariable cs w ere part of the denition of a recursiv e t yp e in the constrain t set The dual of this transformation applies to single lo w er b ounds U when V cs ; C U when C V = cs The restrictions are similar to the upp erb ound case There are no cycles in the constrain t set in v olving cs cs app ears only p ositiv ely in U and C cs m ust ha v e v ariableonly upp er b ounds unless V is a v ariable There is no need for a restriction equiv alen t to the fourth restriction for upp er b ounds since it w ould alw a ys b e satis ed There are t w o subsidiary transformations whic h apply to v ariables with no upp er b ounds or no lo w er b ounds If cs has no upp er b ounds and app ears only negativ ely in U and C U when C U when C cs = cs And the dual case when cs has no lo w er b ounds and app ears only p ositiv ely in U and C U when C U when C = cs Eliminating lo w er b ounds The follo wing transformation has less restrictions than the v ariable elimination transformation but it is less b enecial in general since it do esnt eliminate an y t yp e v ariables only constrain ts W e generally use this transformation as the last stage of simplication U when c 1 f U 1 g j ::: j c n f U n g j ds ; C U when C c 1 f U 1 g j ::: j c n f U n g j ( ds cs ) = ds cs m ust ha v e no constructed upp er b ounds this is to retain the prop ert y that constrain ts are on v ariables There m ust b e no cycles in the constrain t set in v olving cs T yp e Chec king T yp e inference systems normally pro vide a w a y for the user to supply a t yp e for a function and ha v e that t yp e c hec k ed against the inferred one This serv es t w o purp oses The usersupplied t yp es serv e as do cumen tation for the function and the do cumen tation is alw a ys guaran teed to b e correct b ecause it is c hec k ed b y the t yp e system The usersupplied t yp e ma y b e more restrictiv e than the inferred t yp e This is useful in cases where the user wishes to place additional restrictions on the use of a function o v er those pro vided b y the inferred t yp e or to use a more general denition of a function when this w ould b e more ecien t A usersupplied t yp e is v alid if it is an instance of the in ferred t yp e In HindleyMilner t yp e systems an instance of a t yp e is formed b y replacing one or more of its univ ersally quan tied t yp e v ariables b y more sp ecic t yp es and it is straigh tforw ard to c hec k whether one t yp e is an instance of another When subt yping constrain ts are in v olv ed ho w ev er the problem is somewhat more dicult Determining when one constrained t yp e is an instance of another has so far receiv ed little atten tion in the literature TS FF In this sec tion w e outline an algorithm for determining this relation W e do not ha v e pro ofs of soundness or completeness but w e also ha v e not found an y coun ter examples to either prop ert y There do esnt seem to b e a straigh tforw ard extension of our algorithm to handle function t yp es since the ob vious exten sion suers from incompleteness Section In a subt yping system the instance relation is really a subt yp e relation w e are determining whether one t yp e rep resen ts a smaller p ortion of the seman tic domain than an other The term instanc e mak es sense in HindleyMilner st yle systems where the problem reduces to an instance re lation but in a subt yping system w e m ust b e more general The subt yping relation o v er quan tied constrained t yp es can b e dened using the en tailmen t op erator F or t w o t yp es : U when C and : V when D where the quan tied v ariables and are distinct : U when C : V when D i : : D U V ; C In the con text of t yp e c hec king the term on the left of the subt yp e relation is the inferred t yp e and the t yp e on the righ t is the usersupplied t yp e In brief the algorithm w orks as follo ws The constrain t sets on either side of the en tailmen t relation are con v erted to inductiv e form A W and canonical lo w er and upp er b ounds are computed for eac h t yp e v ariable in the set D The algorithm then pro ceeds in a similar w a y to that pro p osed b y T rifono vSmith TS the main dierence b eing that canonical upp er b ounds are more complicated to com pute since w e cannot form the in tersection of sev eral t yp es in general Inductiv e F orm Our en tailmen t algorithm mak es use of an inductiv e form for constrain t sets A W An inductiv e constrain t set can b e formed from a consisten t constrain t set ie one that has b een reduced Section b y rst c ho osing an ordering on v ariable names and then applying the transformations in Figure The transformation mak es use of a function TL V U whic h returns the toplev el v ariable the v ariable remainder of the t yp e U if it exists Th us > TL V U i TL V U exists and is smaller than in the c hosen v ariable ordering Tw o other op erations are used in the transformation The rst forms the union of a t yp e and a set of con structor applications whose elemen ts are all U cs c 1 f g j ::: j c n f g j U n cs The second op erator is n whic h excludes certain tags from a t yp e c f U gj U n cs U n cs if c cs c f U gj U n cs otherwise ds n cs ( ds cs ) ds n cs ( ds cs ) cs Once the transformations ha v e b een fully applied eac h constrain t in the set will b e of the form U or U where > TL V U In other w ords eac h constrain t is expressed as a b ound on a v ariable that only refers to v ariables lo w er than at the top lev el In the Aik en Wimmers system this allo ws the constrain t set to b e solv ed whereas w e use this form to calculate upp er b ounds for our en tailmen t algorithm One problem with using constrain ts in inductiv e form is that w e no longer ha v e the in v arian t that separate o ccur rences of the same v ariable ha v e iden tical sets of excluded tags Our en tailmen t algorithm needs to reduce constrain ts whic h do not satisfy this prop ert y so w e m ust alter the reduction algorithm accordingly The new reduction al gorithm is iden tical to Figure except that w e remo v e the transitivit y rule the last rule in the gure and add the follo wing t w o rules cs ds cs ds U cs ; ds V U V ds ; U cs ; ds V The second of the t w o new rules is a new transitivit y rule that tak es in to accoun t the diering excluded tags on the v ariable In the follo wing discussion of the en tailmen t algorithm w e will use the functions reduce C and induct C to refer to the new reduction and inductiv e transformations resp ect iv ely Computing Canonical Upp er and Lo w er Bounds W e ha v e already presen ted a canonicalisation of lo w er b ounds as part of t yp e simplication in Section W e use that transformation again here If C is an inductiv e constrain t set that has had the lo w erb ound transformation applied then the function lo w ers C ; returns a pair con sisting of a set of v ariables all less than in the inductiv e ordering and a union t yp e with a remainder of zero Canonicalising upp er b ounds is somewhat more dicult as w e cannot form the in tersection of sev eral union t yp es c f U g cs c f U g ds cs cs cs U U cs > TL V U as c 1 f U 1 g j ::: j c n f U n g j ds as c 1 f U 1 g j ::: j c n f U n g j ds ; ( as cs ) < cs ; U cs U Figure Inductiv e F orm in our t yp e language Ho w ev er the follo wing t w o sections describ e a metho d that allo ws us to com bine sev eral upp er b ounds in to a single t yp e for the purp oses of our en tailmen t algorithm The problem is to determine en tailmen ts of the follo wing form V 1 ; : : : ; V n ; C U whic h is true if and only if V 1 ; : : : ; V n ; C V 1 ::: V n U The problem is that w e cannot compute the v alue of the in tersection in general Ho w ev er for the purp oses of en tailmen t there are t w o metho ds that can b e used to pro v e this en tailmen t relation U is a monot yp e When U is a monot yp e w e can calculate the largest t yp e that eac h toplev el v ariable in the in tersection can tak e re ducing the in tersection to an in tersection b et w een mono t yp es whic h w e can reduce to a single t yp e Denition If V 1 ::: V n are the upp er b ounds of in the inductiv e constrain t set C then the absolute upp er b ound of the t yp e v ariable is calculated as follo ws for eac h top lev el v ariable cs in V 1 ::: V n replace cs with V n cs where V is the absolute upp er b ound of Then form the in tersection of the remaining monot yp es using the transformations from Section This denition is recursiv e but it is guaran teed to ter minate b ecause w e are w orking with inductiv e constrain ts The lo w est v ariable in the ordering cannot refer to an y top lev el v ariables in its upp er b ounds so its absolute upp er b ound can b e calculated the second v ariable in the order ing can only refer to the rst and so on Using the absolute upp er b ound w e can form the correct constrain t if U is a monot yp e for the en tailmen t to hold upp er C ; U where upp er C ; is the absolute upp er b ound of the t yp e v ariable in the inductiv e constrain t set C Absolute upp er b ounds can b e precalculated for an y giv en constrain t set U is not a monot yp e When the t yp e U is not a monot yp e using the absolute upp er b ound is not go o d enough it do esnt allo w us to pro v e the follo wing en tailmen t c fg j f c ; d g ; d fg j f c ; d g f c ; d g The absolute upp er b ound for is f c ; d g and it is not true that f c ; d g f c ; d g for all W e need to calculate the absolute upp er b ound with resp ect to a particular v ariable in this case In general the problem is ho w to pro v e the en tailmen t relation C V 1 ::: V n P 1 j ::: j P n j cs Firstly w e can split the inequation on the righ t as fol lo ws V 1 ::: V n P 1 j ::: j P n j cs V 1 ::: V n n ds where ds are the tags of P 1 ::: P n The rst inequation has a monot yp e on the righ t so w e can solv e it using the metho d ab o v e F or the second inequation w e can form the absolute upp er b ound with resp ect to for the t yp e on the left Denition If V 1 ::: V n are the upp er b ounds of in the inductiv e constrain t set C then the absolute upp er b ound of with resp ect to is calculated as follo ws for eac h top lev el v ariable cs in V 1 ::: V n where replace cs with V n cs where V is the absolute upp er b ound of with resp ect to Express the result as an in tersection of unions b y distributing j where necessary Com bine all in tersections of monot yp es in to a single monot yp e using the transformations of Section The absolute upp er b ound of with resp ect to lo oks lik e this U 1 j cs 1 ::: U n j cs n M where M is a monot yp e If w e m ultiply out the in tersec tion w e get U 1 j ::: U n j M ::: where the nal ::: represen ts the rest of the terms all of whic h are in tersections in v olving No w bac k to our original problem w e ha v e U 1 j ::: U n j M ::: n ds W e can discoun t all the terms represen ted b y ::: since they are all smaller than b y virtue of b eing in tersections in v olving The in tersection on the left can b e normalised to a single union t yp e and the problem is solv ed T o recap the en tailmen t C P 1 j ::: j P n j cs holds if and only if C upp er ; C P 1 j ::: j P n j cs and C upp er ; ; C n ds where upp er ; ; C is the absolute upp er b ound of with resp ect to in the constrain t set C and ds are the tags of P 1 ::: P n Algorithm to determine en tailmen t The follo wing algorithm determines whether the en tailmen t relation : : D U V ; C holds W e express the algorithm in an imp erativ e manner using global v ariables C D and Q where C is an ev olving constrain t set initialised from the inductiv e reduced form of C D is an ev olving constrain t set initialised from the inductiv e reduced form of D and Q is a queue of inequations left to pro v e The general strategy used is to attempt to pro v e that eac h constrain t on the righ t of the relation is implied b y D The pro of pro cess generates new constrain ts whic h m ust also b e sho wn to b e implied b y D along with an y constrain ts whic h are required for the transitiv e closure of the constrain t set on the righ t Let D induct reduce D If this fails then the en tailmen t is trivially satised since D has no solutions Compute lo w er and upp er b ounds for D Initialise C induct reduce f U V g C If the reduction fails then fail Initialise queue Q C Remo v e a constrain t from Q and analyse it using the follo wing table where con tin ue means rep eat step un til Q is empt y U con tin ue U con tin ue U let ; V lo w ers ; D if U V f g ; con tin ue else new V U ; con tin ue U analyse U P 1 j ::: j P n j cs V upp er ; D new V P 1 j ::: j P n j cs V upp er ; ; D new V ; con tin ue otherwise V upp er ; D new V U ; con tin ue where new U V F induct reduce U V F F F C T induct reducetrans F ; C T T T C C C F T Q Q F T where trans C ; D represen ts the set of constrain ts required to retain transitiv e closure of the set D when the constrain ts from set C are added The op erator stands for list ap p end If the algorithm completes then the sp ecied en tailmen t relation holds If an y of the reduce op erations fail the the en tailmen t relation is false Extensions Firstclass F unctions Plans are afo ot to extend Erlang to include rstclass func tions b y including lam b da expressions and application in the syn tax Our t yp e inference system extends in a straigh t forw ard w a y to include function t yp es as follo ws Add a new prime t yp e U 1 ;:::; U n V and a new tag to the t yp e syn tax and add lam b da expressions U 1 ;:::; U n V application E E 1 ;:::; E n and references to toplev el func tions f = n where n is the arit y of f to the expression syn tax Add the follo wing rules to the t yp e system Lam F A ; X U C E V F A C X E U V App F A C E U V F A C E U F A C E E V The reduction algorithm can b e extended to function t yp es with the addition of t w o rules U V U V j U U U ; V V U V c f U gj U U V Our algorithm for determining en tailmen t can b e exten ded to supp ort function t yp es but the resulting algorithm is kno wn to b e incomplete TS Decidabilit y of en tailmen t in the presence of function t yp es is not kno wn In terpro cess Comm unication One of the most imp ortan t features of Erlang is its supp ort for concurrency and transparen t distribution With some straigh tforw ard extensions w e can extend our t yp e system to c hec k the t yp es of messages passing b et w een pro cesses Erlang pro vides primitiv es for sending and receiving mes sages and spa wning new pro cesses T o t yp e c hec k message passing it is necessary to k eep trac k of the t yp es of messages receiv ed b y a giv en expression Therefore w e prop ose extending the t yping rules to pro vide t w o t yp es for an expression the t yp e of v alues it returns and the t yp e of messages it accepts T yping judgemen ts no w ha v e the form F X C E U receiv es R where R is the t yp e of messages receiv ed b y the expression Similarly function t yp es should b e written U R V where R is the t yp e of messages receiv ed b y the function b o dy In addition w e need to pro vide a new primitiv e data t yp e of the form pid U whic h is the t yp e of a pro cess that accepts messages of t yp e U W e can then supp ort t yp e c hec king of message sending with a primitiv e send pid U ; V when V U and pro cess spa wning with a primitiv e sp awn U R V ; U pid R This extension is a sp ecial case of eect t yp e systems TJ It w ould allo w the construction of p olymorphic serv er applications but it do esnt supp ort c hec king of pro to cols or detection of p ossible deadlo c ks Practical Exp erience The original goal of designing a t yp e system for Erlang w as for the resulting system to b e usable in a pro duction en vir onmen t b y Erlang programmers W e ha v e so far constructed a pro ofofconcept protot yp e implemen tation in Hask ell While lac king in p erformance in certain areas the protot yp e has pro vided v aluable insigh t in to ho w our t yp e system will coexist with the Erlang en vir onmen t and what c hanges are required to t yp ec hec k existing Erlang co de The protot yp e supp orts the follo wing features T yp e inference for the whole Erlang language T yp e simplication for deriv ed t yp es T yp e signature c hec king T yp e abbreviations for use in t yp e signatures for ex ample see the tree datat yp e in Figure Separate compilation through the use of in terface les whic h record the t yp es of exp orted functions in a mo d ule T yp e abstraction By default t yp e abbreviations are exp orted abstractly so the denition of a t yp e is hid den from external mo dules The programmer ma y op tionally request that certain t yp e denitions b e ex p orted in full The t yp e c hec k er detects abstraction violations and rep orts these to the programmer P artial t yp e c hec king On a functionb yfunction basis the programmer ma y pro vide t yp es that the t yp e system will assume without t yp e c hec king the function denition This is implemen ted with an unchecked directiv e in the co de This protot yp e has b een used to t yp ec hec k a large p or tion of the Erlang standard library and w e are curren tly us ing it to construct a pro duction v ersion of the t yp e c hec k er in Erlang The pro duction v ersion consists of lines of t yp ed Erlang P erformance W e ha v e found p erformance of the t yp e inference engine to b e adequate in most cases although due to the quadratic complexit y of constrain t reduction it can blo w up on large constrain t sets Programs that cause most problems are those in v olving large groups of m utually recursiv e functions whic h m ust b e t yp ec hec k ed together It is not un usual to nd t yp es with up w ards of ten thousand constrain ts P erformance of the t yp e simplication pro cess is p o or for large examples This is due to t w o factors simplic ation usually has to b e p erformed sev eral times b efore a xedp oin t is reac hed and our protot yp e implemen tation uses algorithms with w orse complexit y than is ac hiev able for some of the simplication transformations W e exp ect p erformance of the simplier to impro v e with the pro duction v ersion of the t yp e c hec k er There is a tradeo in v olving t yp e simplication and t yp e c hec king if the user supplies a t yp e signature should the inferred t yp e b e simplied b efore c hec king against the signa ture or should the original inferred t yp e b e used If the t yp e is simplied t yp e c hec king should b e faster but w e w ould pa y for simplication time instead By exp erimen tation w e ha v e found that t yp e c hec king is a relativ ely c heap op eration compared to simplication so w e opt not to simplify t yp es if the user has supplied a signature In practice w e ha v e found it con v enien t to use t yp e sig natures almost ev erywhere for t w o reasons supplying a t yp e signature a v oids the p o or p erform ance of the t yp e simplier and t yp e signatures ma y use abbreviations making them more readable than inferred t yp es T o pro vide some concrete n um b ers here are some of the timings for t yp ec hec king some mo dules from the pro duction v ersion of the t yp e c hec k er Mo dule Lines Times tctypesterl tctypeutilsterl tcreduceterl tcsynterl These times w ere pro duced b y the protot yp e t yp e c hec k er written in Hask ell on a Mhz P en tium Pro The mo d ule tctypesterl con tains a large n um b er of small unre lated functions and t yp e denitions whereas the mo dule tcreduceterl con tains a small n um b er of complicated m utually recursiv e functions hence the large t yp ec hec king time Diagnostics The usabilit y of a t yp e system is directly aected b y the qualit y of error messages generated for un t ypable expres sions It is p ossible to generate t yp e errors whic h include function and line n um b er information in our t yp e system us ing the follo wing tec hnique instead of generating the whole constrained t yp e for a function b efore reducing it w e can re duce constrain ts as they are generated and main tain a fully reduced constrain t set Using this metho d it is p ossible to iden tify the program construct that generated the constrain t that led to an incon sisten t t yping This tec hnique is not p erfect for example it is not p ossible to iden tify whether a t yp e error is caused b y an error in a function denition or in an application of that function In our system the error is alw a ys rep orted at the application site Errors in t yp e signatures are another matter when a signature is found not to b e an instance of the inferred t yp e w e simply rep ort the inferred t yp e and the constrain t that failed during the en tailmen t algorithm In most cases this information is insucien t to iden tify the cause of the error and matters are w orse when the inferred t yp e is large and complicated W e in tend to explore this problem as future w ork P attern Matc hing In order to t yp ec hec k the full Erlang language w e m ust compile the pattern matc hing in to simple case expressions Standard algorithms exist to p erform this transformation Aug W ad In most cases the use of pattern matc hing compilation in our t yp e c hec k er is transparen t to the pro grammer but there are cases where unexp ected t yp es are deriv ed F or example one p ossible w a y to write the b o olean and function is as follo ws andtruetrue true andfalseX false andXfalse false Giv en the t yp e declaration bool true false w e w ould exp ect to b e able to assign the t yp e type andboolbool bool as an instance of the inferred t yp e Ho w ev er in our system this is not the case P attern matc hing compilation trans forms the function as follo ws andXY let Z case Y of false false end in case X of true case Y of true true X Z end false false X Z end whic h yields the t yp e false false true The second argumen t is restricted to b eing false due to the rst case expression on Y in the transformed co de The t yp e is unexp ected since it do es not ha v e the t yp e boolbool bool as an instance This example displa ys a dierence b et w een our system and HindleyMilner since in that system the declaration of bool w ould enable the t yp e system to deriv e the exp ected t yp e Our system do es not require a t yp e declaration and assumes the w orst namely that in order to ensure that the function can nev er fail it is necessary to restrict the second argumen t to b eing false only A generalisation of our t yp e system suc h as con ditional t yp es A WL w ould b e necessary to de riv e a more accurate t yp e whic h w ould ha v e the t yp e boolbool bool as an instance Ho w ev er suc h an extension w ould also increase the complexit y of t yp e c hec king and decrease the readabilit y of t yp es Changes to existing co de W e w ere pleasan tly surprised that v ery little existing co de needed to b e c hanged to get through the t yp ec hec k er The c hanges w e ha v e had to mak e fall in to the follo wing categor ies Actual programming errors or more commonly cases where the original programmer had delib erately left out a failure case Our t yp e system guaran tees that t yp ec hec k ed co de will nev er fail except where the pro grammer has used an explicit exit call This means that all failure cases m ust b e explicitly c hec k ed for in t yp ed co de Clashes b et w een tagged tuples and anon ymous tuples In our t yp e system it is not the case that for instance a although some Erlang co de assumes this P attern matc hing o ddities as describ ed in Section Conclusion While m uc h has b een ac hiev ed in our T yp ed Erlang pro ject sev eral areas remain to b e explored Our principle ac hiev e men ts to date are the t yp e system itself sev eral heuristics for simplifying inferred t yp es the en tailmen t algorithm for determining t yp e instance and our exp erience with a pro tot yp e implemen tation whic h supp orts man y of the features one w ould exp ect from a t yp ed programming language Sev eral gaps remain in the theory most notably is a pro of of completeness for our en tailmen t algorithm without function t yp es Once this pro of is complete w e in tend to use the en tailmen t algorithm to pro v e the correctness of our t yp e simplications The pro duction v ersion of our t yp e c hec k er is curren tly under construction and will b e distributed along with a future v ersion of the Erlang system W e exp ect the nal v ersion to impro v e on the protot yp e in areas of p erformance robustness and the qualit y of diagnostics References Aug L Augustsson Compiling pattern matc hing In F unctional Pr o gr amming L anguages and Computer A r chite ctur e n um b er in Lecture Notes in Com puting Science pages Nancy Septem b er SpringerV erlag A VW J Armstrong R Virding and M Williams Con curr ent Pr o gr amming with Erlang Pren tice Hall A W A Aik en and E L Wimmers T yp e inclusion con strain ts and t yp e inference In F unctional Pr o gr am ming L anguages and Computer A r chite ctur e pages A WL A Aik en EL Wimmers and TK Lakshman Soft t yping with conditional t yp es In Symp osium on Principles of Pr o gr amming L anguages pages CF R Cart wrigh t and M F agan Soft t yping In A CM SIGPLAN Confer enc e on Pr o gr amming L anguage Design and Implementation pages June DM L Damas and R Milner Principal t yp e sc hemes for functional programs In Symp osium on Principles of Pr o gr amming L anguages F A M F ahndric h and A Aik en Making setconstrain t based program analyses scale T ec hnical Rep ort CSD UC Berk eley Also Workshop on Set Constr aints Cam bridge MA August FF C Flanagan and M F elleisen Mo dular and p oly morphic setbased analysis Theory and practice T ec hnical Rep ort TR Rice Univ ersit y FM YC F uh and P Mishra T yp e inference with sub t yp es In Eur op e an Symp osium on Pr o gr amming Hin R Hindley The principal t yp e sc heme of am ob ject in com binatory logic T r ansactions of the A meric an Mathematics So ciety Mil R Milner A theory of t yp e p olymorphism in pro gramming Journal of Computer and System Sci enc es Decem b er Mit J C Mitc hell T yp e inference with simple sub t yp es Journal of F unctional Pr o gr amming MPS D B MacQueen G Plotkin and R Sethi An ideal mo del for recursiv e p olymorphic t yp es In In formation and Contr ol v olume pages MR P Mishra and U Reddy Declarationfree t yp e c hec king In Symp osium on Principles of Pr o gr am ming L anguages pages P ey S L P eyton Jones The Implementation of F unc tional Pr o gr amming L anguages Pren tice Hall Rey J C Reynolds Three approac hes to t yp e struc ture In Pr o c T APSOFT A dvanc e d Seminar on the R ole of Semantics in Softwar e Development Lec ture Notes in Computing Science SpringerV erlag TJ JeanPierre T alpin and Pierre Jouv elot The t yp e and eect discipline Information and Computation TS V T rifono v and S Smith Subt yping constrained t yp es In Thir d International Static A nalysis Sym p osium Septem b er T o App ear W ad P W adler Ecien t compilation of pattern matc hing In P ey W an M W and Complete t yp e inference for simple ob jects In Pr o c nd IEEE Symp osium on L o gic in Computer Scienc e pages W C A K W righ t and R Cart wrigh t A practical soft t yp e system for sc heme In A CM Symp osium on Lisp and F unctional Pr o gr amming