Changes between Version 15 and Version 16 of Holes


Ignore:
Timestamp:
Apr 27, 2012 1:29:51 PM (3 years ago)
Author:
spl
Comment:

Introduction

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v15 v16  
    1 This page describes the design and potential implementation of "holes" in GHC. The intention of holes is to support debugging types in Haskell programs. We have observed that programmers often want to find the type of an expression somewhere in the depths of a program. There are ways of doing this now, but none of them are satisfactory. 
    2  
    3 = Goals in Agda = 
    4  
    5 One of the features of the Emacs mode for [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda] is the ability to add goals, as a placeholder for code that is yet to be written. By inserting a {{{?}}} in an expression, the compiler will introduce a goal. After loading the file (which typechecks it), Agda gives an overview of the goals in the file and their types. 
     1''This page discusses the design and potential implementation of "holes" in GHC.'' 
     2 
     3= Introduction = 
     4 
     5Informally, a "hole" is something to be filled. A hole in the ground can cause an injury if you stepped into it, but you can also build a house around it without a problem. You can easily measure a hole to determine how much material (e.g. dirt or concrete) is needed to fill it. 
     6 
     7The 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. 
     8 
     9These are the primary aspects of the problem that holes solve: 
     10  1. Extract information about subterms in a program. 
     11  1. Do not interrupt compilation. 
     12 
     13We 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. 
     14 
     15= Related Work = 
     16 
     17== Goals in Agda == 
     18 
     19One of the features of the Emacs mode for [http://wiki.portal.chalmers.se/agda/pmwiki.php Agda] is the ability to insert a goal, a placeholder for code that is yet to be written. By inserting a {{{?}}} in an expression, the compiler will introduce a goal. After loading the file (which typechecks it), Agda gives an overview of the goals in the file and their types. 
    620 
    721For example: 
     
    1226}}} 
    1327 
    14 Gets turned into: 
     28gets turned into 
    1529 
    1630{{{ 
     
    1933}}} 
    2034 
    21 With extra output: 
     35with the output 
    2236 
    2337{{{ 
     
    2842As can be seen here, goals are numbered, and the typechecker returns the inferred type for each of these goals. 
    2943 
    30 These goals can make it a lot easier to write code. They allow typechecking to continue although certain parts of code are missing and they work as a TODO list. 
     44Goals 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. 
    3145 
    3246= A proposed concrete design for Haskell =