Changes between Version 37 and Version 38 of Holes


Ignore:
Timestamp:
May 16, 2012 1:33:22 PM (3 years ago)
Author:
spl
Comment:

Update ambiguity section

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v37 v38  
    226226
    227227When using holes (i.e. {{{-XHoles}}} is set), we expect the following:
    228   1. The program should type-check as if every hole {{{_?h}}} is replaced with {{{undefined}}}. See [#Ambiguoustypes Ambiguous types] for an exception to this rule.
     228  1. The program should type-check as if every hole {{{_?h}}} is replaced with {{{undefined}}}. See [#Ambiguoustypes Ambiguous types] for more discussion.
    229229  1. If the program is well-typed (as above), then:
    230230    * The types of all holes should be reported.
     
    236236=== Ambiguous types ===
    237237
    238 Suppose that we replace every hole with {{{undefined}}} and type-check the program without {{{-XHoles}}}. Some programs would not type-check due to unsolved class constraints that result in ambiguous types. For example, {{{show _?h}}} becomes {{{show undefined}}}, and the {{{Show}}} constraint is not instantiated, so the program does not type-check.
    239 
    240 We think holes can be extremely useful with ambiguous types. We prefer that a program, in which there is a hole with unsolved constraints on the type of the hole, still be considered well-typed, assuming the rest of the program is well-typed. In the above example, we would expect {{{show _?h}}} to have the type {{{String}}} with the reported hole type {{{_?h :: Show a => a}}}.
    241 
    242 A hole with an ambiguous type should be treated as a hole runtime error (and not a deferred type error with {{{-fdefer-type-errors}}}). See [#Runtimeerror Runtime error] for an example.
     238Suppose that we replace every hole with {{{undefined}}} and type-check the program without {{{-XHoles}}}. Some programs would not type-check due to unsolved class constraints that result in ambiguous types. Consider this example:
     239{{{
     240f :: String
     241f = show _?h
     242}}}
     243If we view `_?h` as `undefined`, then this results in an error:
     244{{{
     245Main.hs:2:5:
     246    No instance for (Show a0) arising from a use of `show'
     247    The type variable `a0' is ambiguous
     248    ...
     249    In the expression: show _?h
     250    In an equation for `f': f = show _?h
     251Failed, modules loaded: none.
     252}}}
     253If we instead allow the program to type-check, we can find out what type the hole should have ({{{_?h :: Show a => a}}} in this case) and more information.
     254
     255A hole with an ambiguous type should probably be treated as a hole runtime error and not a deferred type error (see [#Runtimeerror Runtime error] for an example); however, not all holes are the immediate cause of ambiguity type errors. For example, consider:
     256{{{
     257data Foo a = Foo a {- no Show instance -}
     258main = putStrLn (show (Foo _?h))
     259}}}
     260Here, the ambiguity comes from having no `Show` instance for `Foo a` and not directly from the hole itself. In this case, we could defer the error (since it is related to a hole) or simply ignore the hole and allow for an error.
    243261
    244262==== Monomorphism restriction ====
    245263
    246 Some ambiguous types fall under the monomorphism restriction. That is, the following program will not type under Haskell2010 due to the restriction that {{{f}}} have a monomorphic type:
     264Some ambiguous types fall under the monomorphism restriction. That is, the following program will not type under Haskell2010 due to the restriction that `f` has a monomorphic type:
    247265{{{
    248266f = undefined >>= undefined
    249267}}}
    250 
    251 We also expect holes to be very useful in these cases, for example by replacing each {{{undefined}}} with a hole:
     268Replacing each {{{undefined}}} with a hole, we get:
    252269{{{
    253270f = _?h >>= _?i
    254271}}}
    255 Thus, we prefer that this program be considered well-typed with {{{f :: Monad m => m b}}} and the holes {{{_?h :: Monad m => m a}}} and {{{_?i :: Monad m => a -> m b}}}.
    256 
    257 If `-XNoMonomorphismRestriction` is used, we expect that the typing of the holes will not change.
     272This program could be considered well-typed with {{{f :: Monad m => m b}}} and the holes {{{_?h :: Monad m => m a}}} and {{{_?i :: Monad m => a -> m b}}}. As a result, if `-XNoMonomorphismRestriction` is used, the typing of the holes will not change.
     273
     274==== Useful? ====
     275
     276We think holes with ambiguous types can be useful, but it is unclear how they should be treated.
    258277
    259278=== Type of a hole ===