Changes between Version 16 and Version 17 of Holes

Apr 27, 2012 1:44:50 PM (2 years ago)

Deferring type errors


  • Holes

    v16 v17  
    77The analogy of a hole in the ground can be transferred to a hole in a program. If you run the program and encounter a hole, the runtime will halt (e.g. as if you encountered {{{undefined}}}). But you can still compile a program with holes. The compiler reports information about the hole, so that the programmer knows what code should replace the hole. 
    9 These are the primary aspects of the problem that holes solve: 
     9These are the requirements of the problem that holes solve: 
    1010  1. Extract information about subterms in a program. 
    1111  1. Do not interrupt compilation. 
     13The extracted information from a hole can include, among other things: 
     14  * The expected type of the hole 
     15  * The local bindings (and their types) in the scope of the hole 
    1317We first describe related work, including concepts that are similar in other languages as well as other approaches to solving the problem proposed. Then, we discuss the proposal in detail. 
    4448Goals can make it a lot easier to write code. They allow typechecking to continue although certain parts of code are missing. They also work as a to-do list for incomplete programs. 
     50== Deferring type errors to runtime == 
     52The proposal DeferErrorsToRuntime implements a flag that turns every type error into a warning with an associated bit of code that is run when the offending ill-typed term is encountered at runtime. At the time of writing, this is implemented in GHC as {{{-fdefer-type-errors}}}. 
     54Deferring type errors alone is not a solution that fits the problem description; however, it can be used in conjunction with other things to solve the problem. 
    4656= A proposed concrete design for Haskell =