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 =