Changes between Version 17 and Version 18 of Holes

Apr 27, 2012 2:02:30 PM (2 years ago)

Deliberate type errors


  • Holes

    v17 v18  
    5454Deferring 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. 
     56== Inserting deliberate type errors == 
     58One technique for finding the type of a subterm that has been often seen on the mailing lists is deliberately inserting ill-typed terms, so that the type error reports the expected type of the term. 
     60Here is an example: 
     621 + () 
     64We get an error that there is no instance for {{{Num ()}}}. 
     66We can do this is a more refined manner by using {{{undefined}}} with a type annotation: 
     68test :: [Bool] 
     69test = undefined : ((undefined :: ()) ++ []) 
     71This gives the error: 
     74    Couldn't match expected type `[Bool]' with actual type `()' 
     75    In the first argument of `(++)', namely `(undefined :: ())' 
     76    In the second argument of `(:)', namely `((undefined :: ()) ++ [])' 
     77    In the expression: undefined : ((undefined :: ()) ++ []) 
     78Failed, modules loaded: none. 
     80The advantage of using {{{undefined}}} is that we can remove the type annotation, and the program will probably compile. 
     82The clear problem with deliberate type errors is that the program does not type-check. We cannot use this technique on multiple locations at one time. We also only get type errors and not other information. 
     84With '''deliberate errors and deferred type errors''', we do get a program that type-checks. This is actually a reasonable solution; however, it still has two problems: 
     85  * Deferring type errors is indiscriminate: you defer both the deliberate and unintended type errors. 
     86  * It does not provide useful information other than type errors. 
    5688= A proposed concrete design for Haskell = 
    83115First, two existing features that can be used as holes. 
    85 === {{{undefined}}} === 
    86 As stated before, {{{undefined}}} typechecks just like a hole: it has type {{{forall a.a}}}, so it can be used anywhere. However, it is not very easy to use in this way: it is impossible to find out what type the compiler found for the hole, and it's impossible to get a list of all the holes used in your source file(s). 
    88 A similar example: 
    89 {{{ 
    90 test :: [Bool] 
    91 test = undefined : (undefined ++ []) 
    92 }}} 
    94 Will 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. 
    96 To 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: 
    98 {{{ 
    99 test :: [Bool] 
    100 test = undefined : ((undefined :: ()) ++ []) 
    101 }}} 
    103 Gives: 
    105 {{{ 
    106 test.hs:2:22: 
    107     Couldn't match expected type `[Bool]' with actual type `()' 
    108     In the first argument of `(++)', namely `(undefined :: ())' 
    109     In the second argument of `(:)', namely `((undefined :: ()) ++ [])' 
    110     In the expression: undefined : ((undefined :: ()) ++ []) 
    111 Failed, modules loaded: none. 
    112 }}} 
    114 However, 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.  
    116117=== Implicit Parameters === 
    117118The GHC extension [ Implicit Parameters] comes closer to how holes are expected to work. This extension makes it possible to specify a term with a question mark, denoting a implicit variable, but this could also be seen as a hole.