Principal type schemes for functional programs wit

PrincipalTypeSchemesforFunctionalProgramswithOverloadingandSubtypingGeoreyS.SmithCornellUniversityyDecember1994AbstractWeshowhowtheHindley/Milnerpolymorphictypesystemcanbeextendedtoincorporateoverloadingandsubtyping.Ourapproachistoattachconstraintstoquantiedtypesinordertorestricttheallowedin-stantiationsoftypevariables.Wepresentanalgorithmforinferringprin-cipaltypesandproveitssoundnessandcompleteness.Wendthatitisnecessaryinpracticetosimplifytheinferredtypes,andwedescribetechniquesfortypesimplicationthatinvolveshapeunication,stronglyconnectedcomponents,transitivereduction,andthemonotonicitiesoftypeformulas.1IntroductionManyalgorithmshavethepropertythattheyworkcorrectlyonmanydierenttypesofinput;suchalgorithmsarecalledpolymorphic.Apolymorphictypesystemsupportspolymorphismbyallowingsomeprogramstohavemultipletypes,therebyallowingthemtobeusedwithgreatergenerality.ThepopularpolymorphictypesystemduetoHindleyandMilner[7,10,3]usesuniversallyquantiedtypeformulastodescribethetypesofpolymorphicprograms.Eachprogramhasabesttype,calledtheprincipaltype,thatcap-turesallpossibletypesfortheprogram.Forexample,theprogramf:x:f(fx)hasprincipaltype8:(!)!(!);anyothertypeforthisprogramcanbeobtainedbyinstantiatingtheuniversallyquantiedtypevariableap-propriately.AnotherpleasantfeatureoftheHindley/Milnertypesystemisthepossibilityofperformingtypeinference|principaltypescanbeinferredauto-matically,withouttheaidoftypedeclarations.However,therearetwousefulkindsofpolymorphismthatcannotbehan-dledbytheHindley/Milnertypesystem:overloadingandsubtyping.IntheThisworkwassupportedjointlybytheNSFandDARPAundergrantASC-88-00465.yAuthor’scurrentaddress:SchoolofComputerScience,FloridaInternationalUniversity,Miami,FL33199;[e-mail]1Hindley/Milnertypesystem,anassumptionsetmaycontainatmostonetyp-ingassumptionforanyidentier;thismakesitimpossibletoexpressthetypesofanoverloadedoperationlikemultiplication.Forhastypesint!int!int1andreal!real!real(andperhapsothers),butitdoesnothavetype8:!!.Soanysingletyping:iseithertoonarrowortoobroad.Asforsubtyping,theHindley/Milnersystemdoesnotprovideforsubtypein-clusionssuchasintreal.ThispaperextendstheHindley/Milnersystemtoincorporateoverloadingandsubtyping,whilepreservingtheexistenceofprincipaltypesandtheabilitytodotypeinference.Inordertopreserveprincipaltypes,weneedarichersetoftypeformulas.Thekeydeviceneededisconstrained(universal)quantication,inwhichquantiedvariablesareallowedonlythoseinstantiationsthatsatisfyasetofconstraints.Todealwithoverloading,werequiretypingconstraintsoftheformx:,wherexisanoverloadedidentier.Toseetheneedforsuchconstraints,considerafunctionexpon(x;n)thatcalculatesxn,andthatiswrittenintermsofand1,whichareoverloaded.Thenthetypesofexponshouldbealltypesoftheform!int!,providedthat:!!and1:;thesetypesaredescribedbytheformula8with:!!;1::!int!.Todealwithsubtyping,werequireinclusionconstraintsoftheform0.Consider,forexample,thefunctionf:x:f(fx).IntheHindley/Milnersys-tem,thisfunctionhasprincipaltype8:(!)!(!).Butinthepresenceofsubtyping,thistypeisnolongerprincipal|ifintreal,thenf:x:f(fx)hastype(real!int)!(real!int),butthistypeisnotde-duciblefrom8:(!)!(!).Theprincipaltypeturnsouttobe8;with:(!)!(!).Asubtleissuethatariseswiththeuseofconstrainedquanticationisthesatisabilityofconstraintsets.Atypewithanunsatisableconstraintsetisvacuous;ithasnoinstances.Wemusttakecare,therefore,nottocallaprogramwelltypedunlesswecangiveitatypewithasatisableconstraintset.1.1RelatedWorkOverloading(withoutsubtyping)hasalsobeeninvestigatedbyKaes[8]andbyWadlerandBlott[19].Kaes’workrestrictsoverloadingquiteseverely;forexamplehedoesnotpermitconstantstobeoverloaded.BothKaes’andWadler/Blott’ssystemsignorethequestionofwhetheraconstraintsetissatis-able,withtheconsequencethatcertainnonsensicalexpressionsareregardedaswelltyped.Forexample,inWadler/Blott’ssystemtheexpressiontrue+trueiswelltyped,eventhough+doesnotworkonbooleans.Kaes’systemhassimilardiculties.Subtyping(withoutoverloading)hasbeeninvestigatedby(amongmanyoth-ers)Mitchell[11],Stansifer[15],FuhandMishra[4,5],andCurtis[2].Mitchell,Stansifer,andFuhandMishraconsidertypeinferencewithsubtyping,buttheir1Throughoutthispaper,wewritefunctionsincurriedform.2languagesdonotincludealetexpression;wewillseethatthepresenceofletmakesitmuchhardertoprovethecompletenessofourtypeinferencealgorithm.Curtisstudiesaveryrichtypesystemthatisnotrestrictedtoshallowtypes.Therichnessofhissystemmakesithardtocharacterizemuchofhiswork;forexamplehedoesnotaddressthecompletenessofhisinferencealgorithm.FuhandMishraandCurtisalsoexploretypesimplication.1.2OutlineoftheRestofthePaperInSection2,wegivetherulesofthetypesystem.InSection3,wepresentalgorithmWosforinferringprincipaltypes.Section4containstheproofsthatWosissoundandcomplete.Section5describestechniquesforsimplifyingthetypesproducedbyWos.Section6brieydiscussestheproblemoftestingthesatisabilityofaconstraintset.Finally,Section7concludeswithanumberofexamplesoftypeinference.2TheTypeSystemThelangu