Changes between Version 12 and Version 13 of Holes

Apr 27, 2012 10:19:06 AM (3 years ago)



  • Holes

    v12 v13  
    3030These 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. 
     32= A proposed design = 
     34Here is a specification of the proposed user-level view of the design. 
     36A hole in a term is written `_?thing`.  Example: 
     38test : List Bool 
     39test = Cons _?x (Cons _?x Nil) 
     41If {{{-XHoles}}} is set, we want the following: 
     42  1. The program should be type-checked as if every hole {{{_?h}}} is replaced by {{{undefined}}}, except: 
     43    * If type-checking would fail due to unsolved constraints that could be solved by giving a type to a hole. 
     44  1. If the program is well-typed, then: 
     45    * The types of all holes should be reported. 
     46    * Reporting the hole types should not cause type-checking (or compiling in general) to stop (in error). 
     47  1. (optional) If the program is ill-typed, then: 
     48    * The types of all holes should be reported. 
     50The above should hold true with and without the monomorphism restriction. In particular, if an {{{undefined}}} somewhere in a program type-checked with the monomorphism restriction would cause type-checking to fail, then a hole in that same position should also cause type-checking to fail. 
     52The type of a hole should be the resolved type with minimum constraints. That is, the type of a hole should only have constraints that have not be solved but are either inferred from the context (e.g. {{{show _?h}}}) or given in a type annotation/signature (e.g. {{{_?h :: Show a => a}}}. 
     54'''Stuff below here might be out of date; please edit''' 
    3256= How we can almost do this in GHC now =