On Effects, Inference, and Type Flow

Much of the technology we use today involves software expressed as code in some programming language.It is important, then, that we develop methods to support the writing of efficient and maintainable code, while reducing the prevalence of errors.Type systems are a classic means to this end, used for decades to increase developer productivity and prevent bugs in programs.A type system restricts the set of valid programs while providing information to the programmer about the structure of their program, such as by indicating that a particular variable is an integer or string.The challenges of type system design lie in balancing the ergonomics of a type system with its complexity and with the guarantees it makes to the programmer: A more precise type system may closely describe the guarantees a programmer desires, but may be unwieldy, while a lax type system, though easy to satisfy, may not prevent many errors.In this dissertation, we consider several type systems.We begin with a look at type-and-effect systems, which track not only the types of values used in computation, but also the effects of the computation, such as writing to the console or modifying memory.We describe a novel system in which specific effects can be explicitly forbidden, a feature inexpressible in most effect systems yet desired by many programmers.We also describe a system in which effects can be integrated with type classes, an abstraction mechanism commonly found in functional programming languages.Next, we consider two contributions related to the idea of type flow.First, we develop a type system for restrictable variants, a sum type indexed by a set formula describing an "active" subset of the sum type.This feature enables precise typing of nonexhaustive pattern match expressions as variants are transformed across chains of function calls.Second, we develop a simple monomorphization technique supporting higher-rank and existential types, and identify the class of programs for which monomorphization is impossible.The technique is guided by the flow of types throughout a program.Finally, we consider programming languages as they are actually used, with a small study on scientists and their programming methods.From here we draw some conclusions about scientists' style of programming, specifically identifying a result-oriented approach.We formalized and implemented each of the type systems as an extension of the Flix programming language, with an evaluation of the extension's impact on the standard library where appropriate.We formalized and implemented the monomorphization technique on a sample language.i Resumé En stor del af teknologien, vi bruger i dag, involverer software udtrykt som kode i et programmeringssprog.Det er derfor vigtigt, at vi udvikler måder at skrive effektiv og vedligeholdelsesvenlig kode, samtidig med at vi reducerer udbredelsen af fejl.Typesystemer er et klassisk virkemiddel for dette mål, brugt i årtier for at øge udvikleres produktivitet og at forhindre fejl i programmer.Et typesystem begrænser mængden af gyldige programmer, mens det skaffer information til programmøren om programmets struktur, så som at vise at en bestemt variabel er et heltal eller en streng.Udfordringerne ved typesystemdesign ligger i at balancere et typesystems ergonomi med dets kompleksitet og de garantier, det tilbyder programmøren: Et mere nøjagtigt typesystem kan præcist beskrive de garantier, programmøren ønsker, men det kan være besværligt, mens et lempeligt typesystem, om end det er nemt at tilfredsstille, forhindrer måske ikke mange fejl.I denne afhandling, overvejer vi flere typesystemer.Vi begynder med et kig på type-og-effektsystemer, som sporer både typer af de værdier, der bruges i beregningen, og beregningens effekter, såsom at udskrive på konsollen eller at ændre hukommelse.Vi beskriver et nyt system hvor særlige effekter kan forbydes, et træk som ikke kan udtrykkes i de fleste systemer, men som er ønsket af mange programmøre.Vi beskriver også et system, hvor effekter kan integreres med typeklasser, et abstraktionsmiddel som ofte findes i funktionelprogrammeringssprog.Dernæst, overvejer vi to bidrag, der er beslægtet med ideen om typestrøm.For det første, udvikler vi et typesystem for begrænsebare varianter, en sumtype indekseret af en mængdeformel, der beskriver sumtypens "aktive" delmængde.Dette træk muliggør præcist typebestemmelse af ikke-udtømmende mønstergenkendelse-udtryk, mens varianter bliver forvandlet på tværs af funktionskald.For det andet, udvikler vi en simpel monomorfiseringsteknik, der håndterer højere-rang og eksistentielle typer, og vi identificerer programklassen som ikke kan monomorfiseres.Teknikken styres af programmens typestrøm.Til sidst, overvejer vi programmeringssprog som de bruges i virkeligheden, med et lille studium af forskere og deres programmeringsmetoder.Herfra trækker vi konklusioner om forskernes programmeringsstil og identificerer en resultatorienteret tilgang.Vi formaliserede og implementerede hvert af typesystemerne som udvidelser af programmeringssproget Flix, med en vurdering af udvidelsernes indvirkning på standardbibliotekket, hvor relevant.Vi formaliserede og implementerede monomorfiseringsteknikken med et eksperimentsprog.iii I owe a great deal to a great number who have supported my academic and personal development both before and during my doctoral studies.I thank the following: Jonathan Lindegaard Starup and other coauthors and colleagues, for many productive and unproductive discussions; Magnus Madsen, for his encouragement and guidance well before and throughout my studies; Giuseppe Castagna, for leading my first foray into research; Aparna Raman, for her support of my academic career even as I worked in industry; Louis Lei Yu, for helping me find a passion for computer science; Doug Uehling, for inspiring confidence in my thinking and writing; Nathan Bouman, for sharing with me the joys of programming; Tim Becker, for introducing me to recreational mathematics; and Bill Ickstadt, for instilling an early sense of self-discipline.I am grateful to Flora Lecoeur for her love, patience, and companionship throughout the complications of academic life, and to my family,