=Paper=
{{Paper
|id=Vol-2707/oopslepaper3
|storemode=property
|title=Solved and Open Problems in Type Error Diagnosis
|pdfUrl=https://ceur-ws.org/Vol-2707/oopslepaper3.pdf
|volume=Vol-2707
|authors=Jurriaan Hage
|dblpUrl=https://dblp.org/rec/conf/staf/Hage20
}}
==Solved and Open Problems in Type Error Diagnosis==
https://ceur-ws.org/Vol-2707/oopslepaper3.pdf
Solved and Open Problems in Type Error
Diagnosis ?
Jurriaan Hage
Dept. of Information and Computing Sciences, Utrecht University The Netherlands
j.hage@uu.nl
Abstract. The purpose of this paper is to present a number of directions
for future research in type error diagnosis. To be able to position these
open problems, we first discuss accomplishments in the field without
trying to be exhaustive.
Keywords: programming languages, type error diagnosis, functional program-
ming paradigm, open problems
1 Introduction
Individual lives as well as entire economies now depend on the reliability of
software. However, it is a major challenge to ensure that software is safe and
correct: it is estimated that programmers make, on average, 15 to 50 errors
per 1,000 lines of code [35], and these errors may lead to bugs, system failures,
security leaks, or even major catastrophes [8, 15, 18, 45, 52]. There are many
approaches to increase the reliability of software, ranging from manual code
inspection, via testing, to formal methods such as program verification, model
checking, and static typing. In this paper we only consider the light-weight formal
method of static typing.
A static type-based approach integrates the verification of program properties
tightly with the program source. A program type is effectively an automatically
and independently verifiable certificate that the stated property holds for a spe-
cific program fragment, module, or the complete program. These properties can
then be verified efficiently and effectively by a compiler using mathematically
verified techniques, thereby improving the quality of software during its produc-
tion. Compared to other formal methods it is lightweight, and can therefore be
easily embedded into the software development loop. It is not surprising then
that most of the recent developments in industrial cutting-edge programming
languages draw heavily on types, e.g. Facebook’s Hack [5], Google’s Go [4], and
Mozilla’s Rust [7].
The guarantees that types provide are typically not complete: the type of the
sorting function may guarantee that it returns a list, but not that the output
?
Copyright c 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
Solved and Open Problems in Type Error Diagnosis 63
list is indeed sorted, or even that the input and output list are of the same
length. What can and cannot be verified depends on the expressiveness of the
type system that is part of the programming language definition. Along this
dimension dependently-typed languages such as Agda [1], Coq [2] and Idris [6]
are considered to be the most expressive.
Expressiveness and power do come at a price. It seems that the more ad-
vanced type level features a language and its implementations support, the more
incomprehensible type error messages become, decreasing programmer produc-
tivity and hindering the uptake of these features, features that were intended by
their designers to increase the number and precision of the guarantees that the
compiler can provide for a given application. Martin Odersky, in private com-
munication, called this problem the “type wall”, and not addressing the issue
may well lead to developers turning their backs on statically typed languages,
and flocking to dynamic languages instead.
In this paper, we want to propose a number of challenges within the field of
type error diagnosis, embedding these challenges in discussions of the state of
the art. We do not try to be comprehensive; there seems to be enough interesting
work to be done. Note that the earlier sections consider concrete challenges in
rather specific contexts, while later sections are more speculative.
Before we go on: in the literature, some researchers explicitly distinguish
between two theoretical extremes: type checking (all types are given and we
only need to check these) and type inference (no types are given, the process
discovers all types on the go). In practical settings, the distinction is less extreme.
Certainly, we do not expect in any programming language that the programmer
annotates every single part of his/her program with types, so there will always be
some amount of inference (note that inference goes beyond choosing the types of
identifiers and also includes coming up with inferred types for all expressions and
statements in the program). The extent to which types can be omitted depends
intimately on the language and its implementation. Below, we do not distinguish
between the two, and use type inferencing to refer to this combined process.
2 Type error diagnosis for functional languages
Although it is hard to say why, languages in the functional programming paradigm
have received much more attention when it comes to type error diagnosis. Possi-
bly this is because it is much easier to make mistakes when higher-order functions
and parametric polymorphism are used on a daily basis. Some researchers in the
field have published a manifest that details what properties one may want type
error messages to have [58].
The earliest work on type error diagnosis aimed at improving the now classic
algorithm W [16]. Researchers quickly discovered that any implementation that
solves unifications during the traversal of the abstract syntax tree was bound to
have some form of bias, derived from the particular traversal. For example, the
folklore algorithm M was known to discover mistakes “sooner”, that is, having
looked at fewer unifications [32]. From an efficiency point of view, this may well
64 Jurriaan Hage
be good, but not for type error diagnosis. The reason is that when you look at the
type error diagnosis that can be provided, comparing algorithms M and W, the
latter can provide more context about the error, having seen more unifications.
As it happens, when all unifications are equality constraints, the order of
solving is irrelevant, and we are in fact free to choose the order in which con-
straints are solved. This is why algorithm G was defined [32], providing external
control of the various orderings it supports. However, whatever the chosen or-
dering, there will always be programs for which that ordering leads to a type
error message that has some bias. If only the solving order could in some ways
be dictated by the program itself.
A different way of implementing the type inference process was proposed
by various authors [27, 28, 43]: as a constraint solving problem. This implies
that type inference consists of an abstract syntax tree traversal that maps the
program to some kind of constraint program (some use a constraint set, others
a constraint tree, again others a single constraint in a more elaborate constraint
language), which is later “interpreted” by a solver. If the solver succeeds, it
returns a substitution as evidence that it did, and otherwise it typically returns
a (set of) constraint(s), the solver deems responsible for the error. This separation
of concerns has been followed by many others and may now be considered the
standard approach 1 . In the case of the Helium compiler [21,22,25,28], constraints
were used to decouple the type system from the solving order by mapping the
program to a constraint tree. That constraint tree could then be flattened into a
list of constraints that were then fed to a solver. The benefits were that when you
were unsatisfied with the type error message, you could (1) choose a different
ordering, and/or (2) choose a different solver. Various orders were predefined
(including the orders of W and M) as well as various solvers. Typically, the
compiler uses a fast greedy solver for equality constraints as long as no error
occurs, but when a type error does occur, it starts a more complicated solving
process for the binding group where the type inconsistency arises. Such a binding
group is typically small compared to the size of the program, and using a more
complicated solver did not harm performance very much. In the case of Helium,
heuristics were developed to provide tailormade error messages. Helium does
this by means of a special datastructure called the type graph that can model
inconsistent constraint sets over which heuristics, looking for clues, have been
defined [21]. For example, we may define a heuristic that depending on how a
literal is used, will provide a suggestion to use a different literal (examples taken
from [11]).
Given the following simple Haskell program
shout :: Show a ⇒ a → String
shout x = show x + + 0 !0
a recent version of Helium that is based on OutsideIn(X) [55] returns the fol-
lowing message
1
The approach is also followed in implementations of realistic functional languages
such as Haskell [3,20], in the case of ghc, a constrain-based formulation also became
necessary to be able to deal with complexity of the language and its many variations.
Solved and Open Problems in Type Error Diagnosis 65
(2,21): Type error in literal
expression : '!'
type : Char
expected type : String
probable fix : use a string literal instead
In this case, the character literal should be a string literal since it is passed
to the (++) append operator that expects two lists (in Haskell lists of characters
are synonymous with strings).
Another example is a heuristic that addresses faulty function applications by
suggesting to rearrange, insert or delete arguments. For example,
g :: [Int ] → [Int ]
g xs = map (+1)
leads to the following type error message:
(2,8): Type error in application
expression : map (+ 1)
term : map
type : (Int -> Int) -> [Int]
does not match : (a -> b ) -> [a] -> [b]
probable fix : insert a second argument
In this case, the type signature provides evidence that xs has type [Int ] and
that the type of the right-hand side should also be [Int ]. Alas, map takes two
arguments, a function and a list, of which only one is provided. Therefore the type
of the right-hand side is [Int ] → [Int ]. The heuristics detects this, and suggest
to add a second argument. It does not suggest to use xs for that argument,
however. Another way to fix the issue is to remove xs as an argument, so writing
g = map (+1), but that would assume that xs is in fact the missing argument
to map. This is not unlikely in this particular case, but what if we add another
argument of type [Int ]?
Other research approaches to type error diagnosis are possible too, however,
and it makes sense to discuss these at this point before we move on.
The idea of type error slicing is inspired by that of program slicing [57]. In
program slicing, a slicing criterion is chosen, e.g., a variable used at a particular
line in the program, and then the (backward) slicing removes parts of the pro-
gram that cannot affect the value of the variable at that program point. This
can be used to simplify programs while debugging. In the case of type error
slicing, programmers are provided with a program in which all the parts that
may contribute to a type error are highlighted; all other parts of the program
can be ignored when trying to resolve the inconsistency. Skalpel [44] (a con-
tinuation of [19]) implements type error slicers for Standard ML, supporting
advanced SML features like modules, which are somewhat related to GADTs in
Haskell. [46] adapts this idea to Haskell 98. The advantage of slicing is that the
actual location that causes the problem is highlighted, a disadvantage is that
many other locations are highlighted as well.
Because type error slices can be large, many researchers prefer to blame one
or maybe a few constraints. For example, SHErrLoc [59] uses a graph-based
66 Jurriaan Hage
structure to encode the solving process, and then ranks the likeness of a con-
straint being to blame using a Bayesian model. Their work considers type error
reporting for modern Haskell, including local hypotheses. [12] explains type er-
rors in Haskell programs using counter-factual typing, a version of variational
typing in which they keep track of the different types that an expression may
take. Although computationally somewhat costly, they can propagate type in-
consistencies from one binding group to another. [38] achieves something similar
by using an iterative deepening approach, in which the body of a binding is
inlined in its usage site if a conflict is detected between both. This allows the
inferencer to blame a location in the body of a (type correct) function if an ap-
plication of that function is type incorrect, at the expense of repeatedly calling
an SM solver with a growing set of constraints. These papers only address the
problem of error localization, and they can do little to explain what went wrong,
and how to fix the error (by suggesting changes to the source code). This infor-
mation is available when type graphs are used. Work, beyond Helium, that uses
type graphs includes [39] and [56]. In the former type graphs were extended with
type classes and row types in the setting of Elm; in the latter heuristics were
defined to explain confidentality errors. Type graphs were extended recently to
OutsideIn(X), so that existential types and GADTs could be modeled [11].
Some authors use a more complicated structure to diagnose type errors: [40]
and [53] expose the trace of the type checker to the programmer (for Scala
and OCaml, respectively), and [13] defines an explanation graph for Hindley-
Miler type systems, which summarizes the information involved in type checking.
LiquidHaskell [54] uses SMT solving as part of type checking. In those cases,
reverse interpolation [36] can be used to derive a simpler explanation.
From a didactic point of view, some researchers thought it a good idea to let
the type inference process, for a type incorrect program, to be best modeled as
an interaction between programmer and compiler. The most important research
line in this direction is that of Chameleon, although it seems work has been at
a standstill for quite some time [50, 51].
For the case that we have no control over the compiler infrastructure, [33]
presents an approach in which the compiler is iteratively queried for the well-
typedness of modified versions of the programmer input, which are then ranked
to present a solution to the type error. A big advantage of this approach is it
treats the type inference process as a black box.
Now that the reader should have some idea of the work that has been done
in this area, we can now list some challenges within this (narrow) field, including
some reflections on the problems at hand.
Open Problem: advanced type level features and their interactions
The Haskell implementation ghc contains many type system features that have
never been considered from the type error diagnosis perspective. The only excep-
tion seems to be GADTs and existential types [11]. Although others have made
implementations that can work in the presence of some of Haskell’s advanced
features, as far as this author knows, the benchmarks they employed did not
Solved and Open Problems in Type Error Diagnosis 67
include any programs that used such features. It has not yet been established
that good solutions to error diagnosis for these advanced features exist, and even
more so what happens when a given programmer selects a particular set of ex-
tensions to use within a single application. Does this change the error diagnosis
at all? Does this depend strongly on the particular combination of extensions?
This is a wide open area with many unanswered questions.
Open Problem: proof assistance In dependently typed languages, such as
Agda, Idris, and Coq, type correctness corresponds to functional correctness.
These languages are usually not used to implement applications, but as proof
tools. This means that “error diagnosis” can take on two forms: the usual type
error messages we also see come up in everyday functional programming (e.g.,
you pass the arguments to this function in the wrong order), and the problem
of proof assistance (e.g., you need to strenghten this lemma for the theorem to
go through). In the former case we can look at research on plain functional lan-
guages, in the latter case we find a pretty completely open field of investigation.
Only a few works have addressed the problem of error diagnosis at all in this
setting [14, 17].
Open Problem: error explanation and repair As the above historical
overview suggests, most work in this area is on error localization. The advantage
of work in that direction is that it is relatively easily to validate: the output is
a simple location, not the way a type error message is formulated.
But localization also means we can only point at a location, and not diagnose
the mistake, or make suggestions on how to fix the problem. This does not mean
localization is altogether useless, and in fact such localizers can also be used
in a setting that employs heuristics. Consider a compiler that has any number
of implementations of localizing errors. In addition, we implement a heuristic
approach in which many different heuristics are asked to come up with both a
location and a diagnosis or fix based on that location. A problem when using
heuristics is you may have multiple heuristics, each choosing a particular location
and explanation. Which heuristic is the right one? Well, maybe that is simply
the one that agrees best with the localizers. In other words, the localizers provide
more confidence when choosing the right message (or, if we can have multiple
messages, which one to put at the top).
Open Problem: benchmarks A major problem in all type error diagnosis
endeavors is the absence of suitable benchmarks. The author of this paper has
collected a “large” number (around 50,000) of programs written by students,
that have also been used by others. However, these were collected from second
year undergraduate students and they do not employ any advanced features, just
plain old Haskell 98. There are not many places where students, in sufficiently
large numbers, program using the more advanced features we now will want to
be considering, and for publishing about research on these features, benchmarks
are indispensable.
68 Jurriaan Hage
Open Problem: aspects of domain-specific type error diagnosis There
is a strand of work by the author that addresses the problem of type error
diagnosis for embedded domain-specific languages, again within the context of
Haskell, and mostly within Helium [24,26,48]; a PhD has been published that has
similar aims but works on Scala [41]. In these works, domain-specific type error
diagnosis is implemented as an external DSL that uses type error specifications
to control the solving order and the delivered diagnosis. The specifications are
automatically checked for soundness with respect to type system.
Some of the ideas of these works have also been implemented in ghc [47].
In this case, we are limited by what can be grafted onto ghc’s type inference
engine. But this approach also has significant advantages: changes to the com-
piler were minimal, and soundness of the type rules is verified by the compiler
as part of its type system. Moreover, since the rules are written using the type
level programming facilities of Haskell, the methods of abstraction that Haskell
provides there are all available to us. A disadvantage is that the diagnosis of type
level programming itself is not a solved problem (see earlier), and the control we
can exert is less than reported in other work. It is unclear at this time how far
the idea can be taken without having to completely redesign the type inference
engine of ghc.
In a setting with external DSLs, it may well be possible to approach the
problem of type error diagnosis as we do in defining the intrinsic type system of
a general purpose language. In [49], an architecture for such an implementation
is defined and motivated. The full architecture is not something that has been
exhaustively tested, but generally it does seem to be the case that decoupling the
specification of the type system in terms of constraints from the solving process
is a good idea for two reasons: it simplifies the type system implementation, and
it simplifies diagnosis.
3 Beyond type error diagnosis in functional languages
The type system that comes with statically typed languages as part of their
definition is not the only one of its kind. One can implement various extensions
to such type systems. Typical examples include dimension analysis [29, 30], type
based security analysis [42, 56] and pattern match analysis [31, 37]. In the latter
case, we want the compiler to verify that pattern match failures cannot crash the
program, in dimension analysis type are refined by having “floats that represent
meters” and “floats that represent kilograms” and preventing the programmer
from, say, adding two such floats together. Such types have been implemented
in F#. Since we now want to reject more programs, the problem of type error
diagnosis will come up sooner or later, although it will depend somewhat on the
richness of the dimension types.
In the case of security type systems, the type system prevents values of high
confidentiality to end up in variables of low confidentiality. As far as this author
knows, this is the only validating analysis for which type error diagnosis has
been considered [56].
Solved and Open Problems in Type Error Diagnosis 69
Much more speculatively, optimising analyses for functional languages are
often designed as annotated type systems [34]. Examples are too numerous to
mention, and include control-flow analysis, sharing analysis, escape analysis,
binding-time analysis. In such a system, annotations, that describe additional
properties of the type, are attached to types, and the type system implementation
will try to infer the best properties. The above validating analyses actually use
the same approach.
The difference is that an optimising analysis typically will accept exactly all
programs accepted by the underlying intrinsic type system. At this point, error
diagnosis does not play a role. But what if we want to allow the programmer
to express certain properties about his/her programs to communicate to the
programmer that certain optimisations should be made, and to have the compiler
verify that these properties make sense? Then, if the analysis fails, we may want
the compiler to explain to the programmer why this is not the case. This is
currently a wide open field of investigation.
4 Type error diagnosis, elsewhere
What is most striking about type error diagnosis beyond the functional pro-
gramming languages is that there is almost nothing to report on. A few papers
exist that deal with generic method invocations in Java [9,10], and a PhD thesis
within the context of Scala [41] that tries to achieve something like the special-
ized type rules of Helium [26], but with much more control over the process by
providing the ability to inspect type inference traces. This increased control does
come at the price of more complexity.
Type error diagnosis in this setting may well be harder, because the type
systems themselves typically combine higher-order functions, parametric poly-
morphism and some form of subtyping. Therefore, type inference is algorith-
mically already quite hard, and diagnosis will typically not make it any easier.
Another aspect is that multi-paradigm languages like Scala tend to draw people
from different paradigms, and their needs are likely to be different. For example,
a Haskell programmer may be surprised that types do not propagate as easily
under local type inference in Scala, while Java programmers will not always be
that familiar with type variables. Another complication is that a language like
Java started from an object-oriented core and had various extensions added to
it while having to remain backwards compatible. These grafts on top the lan-
guage tend to be quite ad hoc, complicating type error diagnosis. To be fair,
Haskell seems to have a similar problem as compared to full dependently typed
languages.
5 What about SLE?
The talk that led to this paper was presented at OOPSLE, which may lead to
the question: how is this topic relevant to SLE? Clearly, the problem is related
to the implementation of programming languages.
70 Jurriaan Hage
In [49], an architecture is presented for a (Haskell) compiler that has type
error diagnosis as part of its design, not as an afterthought. Although it remains
to be seen whether the architecture is sufficiently rich to be used in all situations,
and whether its features are relevant in every setting, it does tell us that things
aren’t so simple as they may seem at first. The relevance to SLE is that the work
tells us how to organize/structure a compiler to deal with various kinds of tasks
in type error diagnosis.
5.1 Open Problem: analysis of compilation behavior
A paper published at the first SLE in Toulouse presented Neon [23], a library
for analyzing interactions with the compiler in the context of Helium. Helium
has built-in log facilities that could communicate compiled programs to a server.
Programs, collected during class hours while students were working on their
practical assignments, have been used by various authors in the field. The first
attempt with Helium to extract information from these compiles is hampered by
the fact that the programs were collected in vivo. For example, when someone
fixes a mistake after 10 minutes is that because they went for coffee and checked
their phones for messages, or were they working on solving the problem? And
when after a type error the program compiles correctly is that because a teaching
assistant told them how to fix it, did they fix it themselves, or did they delete the
definition altgother? And if we perform these experiments with students, either
in vivo or in vitro, does that tell us anything about professional developers?
Every answer seems to raise only more questions.
5.2 Open Problem: everyone is different
Type error diagnosis is to some extent a matter of taste. The thing is that
depending on where you come from, your level of expertise, your programming
style even, you will be wanting different things from error diagnosis. Maybe, all a
seasoned programmer needs is to get the approximate location of a mistake, but
what if these seasoned programmers start to uses type system extensions they
are not yet familiar with? Do their needs change over time, as they do become
more familiar? Everyone seems to have different needs, and at this time we are
not yet at the level that we can satisfy the needs themselves. The problem to
decide what someone needs and when is likely to be even harder. Some process in
which programming becomes an interaction with a compilation system, so that
that system can accrue some kind of operational profile is likely to be essential
in that case.
Of course, there is a field in computer science that excels at modeling the
ad-hocness of human nature: machine learning. But that will only work if we
have enough data to learn from. And as we explained above, that data is at this
time simply not available.
Solved and Open Problems in Type Error Diagnosis 71
6 Conclusion
The conclusion is simple: there is still an immense amount of work to do.
References
1. The Agda programming language. http://wiki.portal.chalmers.se/agda/
pmwiki.php, accessed: 2020-03-20
2. The Coq proof assistant. https://coq.inria.fr/, accessed: 2020-09-11
3. The Glasgow Haskell Compiler, GHC. https://www.haskell.org/ghc/, accessed:
2020-03-27
4. The Go programming language. https://golang.org/, accessed: 2020-03-27
5. The Hack programming language. https://hacklang.org/, accessed: 2020-03-27
6. The Idris programming language. https://www.idris-lang.org/, accessed: 2020-
09-11
7. The Rust programming language. https://www.rust-lang.org/, accessed: 2020-
03-27
8. When code can kill or care, tech. Quarterly (Economist), Q2.2012
9. el Boustani, N., Hage, J.: Corrective hints for type incorrect Generic Java programs.
In: Gallagher, J., Voigtländer, J. (eds.) Proceedings of the ACM SIGPLAN 2010
Workshop on Partial Evaluation and Program Manipulation (PEPM ’10). pp. 5–14.
ACM Press (2010)
10. el Boustani, N., Hage, J.: Improving type error messages for generic java. Higher-
Order and Symbolic Computation 24(1), 3–39 (2012), http://dx.doi.org/10.
1007/s10990-011-9070-3, 10.1007/s10990-011-9070-3
11. Burgers, J.: Type error diagnosis for OutsideIn(X) in Helium (2019), https://
dspace.library.uu.nl/handle/1874/382127
12. Chen, S., Erwig, M.: Counter-factual Typing for Debugging Type Errors. In:
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages. pp. 583–594. POPL ’14, ACM, New York, NY, USA
(2014). https://doi.org/10.1145/2535838.2535863, http://doi.acm.org/10.1145/
2535838.2535863
13. Chitil, O.: Compositional explanation of types and algorithmic debugging of
type errors. In: Proceedings of the Sixth ACM SIGPLAN International Con-
ference on Functional Programming. pp. 193–204. ICFP ’01, ACM, New York,
NY, USA (2001). https://doi.org/10.1145/507635.507659, http://doi.acm.org/
10.1145/507635.507659
14. Christiansen, D.R.: Reflect on your mistakes ! lightweight domain-specific error
messages (2014)
15. Cipra, B.: How number theory got the best of the pentium chip, science, 267:5195,
pp.170-175, 1995
16. Damas, L., Milner, R.: Principal Type-schemes for Functional Programs. In:
Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages. pp. 207–212. POPL ’82, ACM, New York, NY,
USA (1982). https://doi.org/10.1145/582153.582176, http://doi.acm.org/10.
1145/582153.582176
17. Eremondi, J., Swierstra, W., Hage, J.: A framework for improving er-
ror messages in dependently-typed languages. Open Comput. Sci. 9(1), 1–
32 (2019). https://doi.org/10.1515/comp-2019-0001, https://doi.org/10.1515/
comp-2019-0001
72 Jurriaan Hage
18. Gleick, J.: A bug and a crash (1996), http://www.around.com/ariane.html
19. Haack, C., Wells, J.B.: Type Error Slicing in Implicitly Typed Higher-
order Languages. Sci. Comput. Program. 50(1-3), 189–224 (Mar 2004).
https://doi.org/10.1016/j.scico.2004.01.004, http://dx.doi.org/10.1016/j.
scico.2004.01.004
20. Hage, J.: The Helium homepage (2020), https://github.com/Helium4Haskell/
21. Hage, J., Heeren, B.: Heuristics for type error discovery and recovery. In: Horváth,
Z., Zsók, V., Butterfield, A. (eds.) Implementation of Functional Languages – IFL
2006. vol. 4449, pp. 199 – 216. Springer Verlag, Heidelberg (2007)
22. Hage, J., Heeren, B.: Strategies for solving constraints in type and effect sys-
tems. Electronic Notes in Theoretical Computer Science 236, 163 – 183 (2009),
proceedings of the 3rd International Workshop on Views On Designing Complex
Architectures (VODCA 2008)
23. Hage, J., van Keeken, P.: Neon: A library for language usage analysis. In: Gasevic,
D., Lämmel, R., Wyk, E.V. (eds.) Proceedings of the 1st Conference on Software
Language Engineering (SLE ’08). Lecture Notes in Computer Science, vol. 5452,
pp. 35 – 53. Springer (2009), revised selected papers
24. Heeren, B., Hage, J.: Type class directives. In: Seventh International Symposium
on Practical Aspects of Declarative Languages. pp. 253 – 267. Springer Verlag,
Berlin (2005)
25. Heeren, B., Hage, J., Swierstra, S.D.: Constraint based type inferencing in He-
lium. In: Silaghi, M.C., Zanker, M. (eds.) Workshop Proceedings of Immediate
Applications of Constraint Programming. pp. 59 – 80. Cork (September 2003)
26. Heeren, B., Hage, J., Swierstra, S.D.: Scripting the type inference process. In:
Eighth International Conference on Functional Programming. pp. 3 – 13. ACM
Press, New York (2003)
27. Heeren, B., Hage, J., Swierstra, S.D.: Constraint based type inferencing in He-
lium. In: Silaghi, M.C., Zanker, M. (eds.) Workshop Proceedings of Immediate
Applications of Constraint Programming. pp. 59 – 80. Cork (September 2003)
28. Heeren, B.J.: Top Quality Type Error Messages. Ph.D. thesis, Universiteit Utrecht,
The Netherlands (Sep 2005)
29. Kennedy, A.: Types for units-of-measure: Theory and practice. In: Horváth, Z.,
Plasmeijer, R., Zsók, V. (eds.) Central European Functional Programming School
(CEFP), Lecture Notes in Computer Science, vol. 6299, pp. 268 – 305. Springer
Verlag (2010)
30. Kennedy, A.J.: Programming Languages and Dimensions. Ph.D. thesis, Computer
Laboratory, University of Cambridge (1995), available as Technical Report No. 391
31. Koot, R., Hage, J.: Type-based exception analysis for non-strict higher-order func-
tional languages with imprecise exception semantics. In: Proceedings of the 2015
Workshop on Partial Evaluation and Program Manipulation. pp. 127–138. PEPM
’15, ACM, New York, NY, USA (2015). https://doi.org/10.1145/2678015.2682542,
http://doi.acm.org/10.1145/2678015.2682542
32. Lee, O., Yi, K.: A generalization of hybrid let-polymorphic type inference algo-
rithms. In: Proceedings of the First Asian Workshop on Programming Languages
and Systems. pp. 79–88. National university of Singapore, Singapore (December
2000)
33. Lerner, B.S., Flower, M., Grossman, D., Chambers, C.: Searching for Type-error
Messages. In: Proceedings of the 28th ACM SIGPLAN Conference on Program-
ming Language Design and Implementation. pp. 425–434. PLDI ’07, ACM, New
York, NY, USA (2007). https://doi.org/10.1145/1250734.1250783, http://doi.
acm.org/10.1145/1250734.1250783
Solved and Open Problems in Type Error Diagnosis 73
34. Lucassen, J.M., Gifford, D.K.: Polymorphic effect systems. In: POPL ’88:
Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles
of programming languages. pp. 47–57. ACM, New York, NY, USA (1988).
https://doi.org/http://doi.acm.org/10.1145/73560.73564
35. McConnell, S.: Code Complete. A Practical Handbook of Software Construction.
2nd edn. (2015)
36. McMillan, K.L.: An interpolating theorem prover. In: Jensen, K., Podelski, A.
(eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp.
16–30. Springer Berlin Heidelberg, Berlin, Heidelberg (2004)
37. Mitchell, N., Runciman, C.: Not all patterns, but enough: an automatic verifier for
partial but sufficient pattern matching. In: Proceedings of the first ACM SIGPLAN
symposium on Haskell. pp. 49–60. Haskell ’08, ACM, New York, NY, USA (2008)
38. Pavlinovic, Z., King, T., Wies, T.: Practical SMT-based Type Error Localiza-
tion. In: Proceedings of the 20th ACM SIGPLAN International Conference on
Functional Programming. pp. 412–423. ICFP 2015, ACM, New York, NY, USA
(2015). https://doi.org/10.1145/2784731.2784765, http://doi.acm.org/10.1145/
2784731.2784765
39. Peijnenburg, F., Hage, J., Serrano, A.: Type directives and type graphs in elm.
In: Proceedings of the 28th Symposium on the Implementation and Application
of Functional Programming Languages, IFL 2016, Leuven, Belgium, August 31 -
September 2, 2016. pp. 2:1–2:12 (2016). https://doi.org/10.1145/3064899.3064907,
https://doi.org/10.1145/3064899.3064907
40. Plociniczak, H.: Scalad: An Interactive Type-level Debugger. In: Proceedings of
the 4th Workshop on Scala. pp. 8:1–8:4. SCALA ’13, ACM, New York, NY, USA
(2013). https://doi.org/10.1145/2489837.2489845, http://doi.acm.org/10.1145/
2489837.2489845
41. Plociniczak, H.: Decrypting Local Type Inference. Ph.D. thesis, IC, Lausanne
(2016). https://doi.org/10.5075/epfl-thesis-6741
42. Pottier, F., Simonet, V.: Information flow inference for ml. In: POPL ’02:
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles
of programming languages. pp. 319–330. ACM, New York, NY, USA (2002).
https://doi.org/http://doi.acm.org/10.1145/503272.503302
43. Pottier, F., Rémy, D.: he Essence of ML Type Inference. In: Pierce, B.C. (ed.)
Advanced Topics in Types and Programming Languages, chap. 10, pp. 389–489.
MIT Press (2005), http://cristal.inria.fr/attapl/
44. Rahli, V., Wells, J., Pirie, J., Kamareddine, F.: Skalpel: A constraint-based
type error slicer for Standard ML. J. Symb. Comput. 80(P1), 164–208 (May
2017). https://doi.org/10.1016/j.jsc.2016.07.013, https://doi.org/10.1016/j.
jsc.2016.07.013
45. Reuters: Toyota to recall 436,000 hybrids globally, feb. 2010
46. Schilling, T.: Constraint-free Type Error Slicing. In: Proceedings of the 12th Inter-
national Conference on Trends in Functional Programming. pp. 1–16. TFP’11,
Springer-Verlag, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-
32037-8 1, http://dx.doi.org/10.1007/978-3-642-32037-8_1
47. Serrano, A., Hage, J.: Type error customization in ghc: Controlling expression-
level type errors by type-level programming. In: Proceedings of the 29th
Symposium on the Implementation and Application of Functional Program-
ming Languages. pp. 2:1–2:15. IFL 2017, ACM, New York, NY, USA
(2017). https://doi.org/10.1145/3205368.3205370, http://doi.acm.org/10.1145/
3205368.3205370
74 Jurriaan Hage
48. Serrano, A., Hage, J.: Type error diagnosis for embedded dsls by two-stage spe-
cialized type rules. In: Programming Languages and Systems - 25th European
Symposium on Programming, ESOP 2016, Proceedings. pp. 672–698 (2016)
49. Serrano, A., Hage, J.: A compiler architecture for domain-specific type error diag-
nosis. Open Comput. Sci. 9(1), 33–51 (2019). https://doi.org/10.1515/comp-2019-
0002, https://doi.org/10.1515/comp-2019-0002
50. Stuckey, P.J., Sulzmann, M., Wazny, J.: Interactive type debugging in Haskell. pp.
72–83. New York (2003)
51. Stuckey, P.J., Sulzmann, M., Wazny, J.: Improving type error diagnosis. pp. 80–91
(2004)
52. Technica, A.: Airbus confirms software configuration error caused plane crash, 2015
53. Tsushima, K., Asai, K.: An embedded type debugger. In: Hinze, R. (ed.) Imple-
mentation and Application of Functional Languages. pp. 190–206. Springer Berlin
Heidelberg, Berlin, Heidelberg (2013)
54. Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton Jones, S.: Refinement
Types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Con-
ference on Functional Programming. pp. 269–282. ICFP ’14, ACM, New York, NY,
USA (2014). https://doi.org/10.1145/2628136.2628161, http://doi.acm.org/10.
1145/2628136.2628161
55. Vytiniotis, D., Peyton Jones, S., Schrijvers, T., Sulzmann, M.: OutsideIn(x):
Modular Type Inference with Local Assumptions. J. Funct. Program. 21(4-
5), 333–412 (Sep 2011). https://doi.org/10.1017/S0956796811000098, http://dx.
doi.org/10.1017/S0956796811000098
56. Weijers, J., Hage, J., Holdermans, S.: Security type error diagnosis for higher-
order, polymorphic languages. Science of Computer Programming 95, 200 – 218
(2014). https://doi.org/https://doi.org/10.1016/j.scico.2014.03.011, http://www.
sciencedirect.com/science/article/pii/S0167642314001518, selected and ex-
tended papers from Partial Evaluation and Program Manipulation 2013
57. Weiser, M.: Program slicing. In: Proceedings of the 5th International Conference
on Software Engineering. pp. 439–449. ICSE ’81, IEEE Press (1981)
58. Yang, J., Michaelson, G., Trinder, P.: Explaining polymorphic types. The Com-
puter Journal 45(4), 436–452 (2002)
59. Zhang, D., Myers, A.C., Vytiniotis, D., Peyton Jones, S.: Diagnosing Type Er-
rors with Class. In: Proceedings of the 36th ACM SIGPLAN Conference on Pro-
gramming Language Design and Implementation. pp. 12–21. PLDI ’15, ACM,
New York, NY, USA (2015). https://doi.org/10.1145/2737924.2738009, http:
//doi.acm.org/10.1145/2737924.2738009