Changes between Version 4 and Version 5 of Holes


Ignore:
Timestamp:
Feb 10, 2012 12:46:32 PM (2 years ago)
Author:
xnyhps
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v4 v5  
    1 = Holes = 
     1= Goals in Agda = 
    22 
    3 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 hole. After loading the file (which typechecks it), Agda gives an overview of the holes in the file and their types. 
     3One 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. 
    44 
    55For example: 
     
    2424}}} 
    2525 
    26 As can be seen here, holes are numbered, and the typechecker returns the inferred type for each of these holes. 
     26As can be seen here, goals are numbered, and the typechecker returns the inferred type for each of these goals. 
    2727 
    2828These 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. 
    2929 
    30 == In GHC == 
     30= How this can be used in GHC now = 
    3131GHC does not support holes in the way Agda does. It is possible to insert {{{undefined}}} in an expression to make it typecheck (which Agda doesn't have), but this is not very helpful when writing software. Inserting {{{undefined}}} only gives as information that the rest of the program typechecks, but will not help you find what you needed to use in its place. We propose to add an extension to GHC (and notably GHCi) to allow using holes, this page is meant to discuss the exact features and workflow of such an extension. 
    3232 
     
    4343 
    4444Will not help finding the types of the {{{undefined}}}s at all. One advantage is that the code can successfully run, except if one of the {{{undefined}}}s is actually evaluated. 
     45 
     46To find the type of the {{{undefined}}}, one can give it a type that is certainly wrong, and then check what the compiler says the right type is: 
     47 
     48{{{ 
     49test :: [Bool] 
     50test = undefined : ((undefined :: ()) ++ []) 
     51}}} 
     52 
     53Gives: 
     54 
     55{{{ 
     56test.hs:2:22: 
     57    Couldn't match expected type `[Bool]' with actual type `()' 
     58    In the first argument of `(++)', namely `(undefined :: ())' 
     59    In the second argument of `(:)', namely `((undefined :: ()) ++ [])' 
     60    In the expression: undefined : ((undefined :: ()) ++ []) 
     61Failed, modules loaded: none. 
     62}}} 
     63 
     64However, using multiple of these holes can cause the compiler to assume the error is in a different place than the hole. It also fails the compilation, causing other errors that might occur to not show up, and doesn't allow the rest of the code to still run.  
    4565 
    4666=== Implicit Parameters === 
     
    92112Another thing to keep in mind with implicit parameters is that implicit parameters with the same name in different functions are not assumed to be the same (i.e., required to be unifiable), ''except'' if some function has both implicit parameters in its constraints. Lastly, it's impossible to run code with unbound implicit parameters, even if the parameters are never actually used. 
    93113 
    94 ---- 
     114= How this could be implemented in GHC = 
    95115 
    96 Now for ways holes could be added to GHC(i). 
     116These two approaches are not ideal, they either don't give enough information, or they hinder using the code. 
    97117 
    98118=== Agda-style ===