Show simple item record

dc.rights.licenseCC-BY-NC-ND
dc.contributor.advisorSwierstra, W.
dc.contributor.advisorHage, J.
dc.contributor.authorEremondi, J.S.
dc.date.accessioned2016-09-01T17:00:37Z
dc.date.available2016-09-01T17:00:37Z
dc.date.issued2016
dc.identifier.urihttps://studenttheses.uu.nl/handle/20.500.12932/23979
dc.description.abstractDependently typed programming languages provide a powerful tool for proving code correct. However, these languages are complex, and programming in them is often difficult. Certain features, such as pattern matching or inferring values using metavariables, rely on a unification procedure performed during type-checking. When this process fails, the error messages provided are often confusing, and do not accurately indicate which programmer error caused the failure. For functional languages with simple typing, error messages have been improved by expressing type-checking as a constraint-solving problem, performing global analysis on a constraint-graph. While these attempts have been successful, there are a number of differences between dependent and simple types. Parametric polymorphism is expressed using implicit parameters, rather than polymorphic types. Moreover, since there is no distinction between types and terms, typechecking may require code to be evaluated. This means that the existing techniques for error generation do not directly apply to dependent-types. This thesis presents background information on dependent-type checking, functional error-message reporting, constraint-based typechecking, and higher-order unification. We frame some of the challenges for adapting existing techniques to more advanced languages. In an initial attempt to improve error messages, this thesis proposes a dependently-typed system with replay-graphs, for combining higher-order unification with type graphs. Additionally, a system of counter-factual constraint-solving is proposed, which finds multiple solutions for various subsets of unification constraints. The results of implementing these techniques is presented, with examples both of where they produce improved error messages on type-incorrect programs, and where they produce poor messages.
dc.description.sponsorshipUtrecht University
dc.format.extent470949
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.titleImproving Error Messages for Dependent Types with Constraint-based Unification
dc.type.contentMaster Thesis
dc.rights.accessrightsOpen Access
dc.subject.keywordsdependent-types, functional-programming, computer-science, types, error-messages, typechecking
dc.subject.courseuuComputing Science


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record