Changes between Version 6 and Version 7 of PartialTypeSignatures


Ignore:
Timestamp:
Mar 14, 2014 2:38:47 PM (14 months ago)
Author:
thomasw
Comment:

Discuss the integration with the Holes proposal

Legend:

Unmodified
Added
Removed
Modified
  • PartialTypeSignatures

    v6 v7  
    2828more practical point of view in the hope to get some feedback from the 
    2929GHC developers community. 
     30 
     31 
     32'''NOTE''': [#holes a new section] about the integration of this 
     33proposal with the [wiki:Holes] proposal. 
    3034 
    3135== Motivation and discussion == 
     
    423427for more discussion. 
    424428 
    425 === Extension Flags === 
    426  
    427 Previously, underscores in types were disallowed and caused parse 
    428 errors. With this extension, underscores will be accepted by the 
    429 parser. To remain backwards compatible (also with Haskell 2010), we 
    430 require the user to enable our [[span(!PartialTypeSignatures, style=font-variant: small-caps)]] 
    431 extension. Using wildcards without this flag will trigger a parse 
    432 error with a suggestion to enable the flag. 
    433  
    434 Currently, GHC parses identifiers prefixed with an underscore in type 
    435 signatures, i.e. what we consider named wildcards, as type variables, 
    436 as prescribed in Haskell 2010. To also remain backwards compatible on 
    437 this front, we propose to only parse them as named wildcards when the 
    438 extension [[span(!NamedWildcards, style=font-variant: small-caps)]] is 
    439 enabled. This extension will be turned on automatically when the 
    440 [[span(!PartialTypeSignatures, style=font-variant: small-caps)]] 
    441 extension is turned on. 
    442  
    443 We opted for a separate flag because unnamed wildcards cause programs 
    444 previously rejected to be accepted, whereas named wildcards change the 
    445 behaviour of previously accepted programs. With this extra flag, the 
    446 user can still use (unnamed) wildcards with the 
    447 [[span((No)!NamedWildcards, style=font-variant: small-caps)]] 
    448 extension explicitly turned off, to maintain backwards compatibility. 
     429=== Holes === #holes 
     430 
     431'''NEW''': as suggested on the mailing list (by Austin Seipp, Richard 
     432Eisenberg, Edward Kmett, ...), it seems like a good idea to integrate 
     433this proposal with the [wiki:Holes] proposal (not to be confused with 
     434!TypedHoles, which actually occur in terms, whereas this proposal 
     435allows holes in types). Our idea is now the following. 
     436 
     437Previously, underscores in types were disallowed by GHC and Haskell 
     4382010, so to remain backwards compatible, wildcards or 'holes in types' 
     439should still result in errors. However, the generated error messages 
     440can now be much more informative, i.e. they should inform the user of 
     441the type each wildcard/hole was instantiated to. As this does not 
     442change the set of accepted programs nor the behaviour of accepted 
     443programs, this doesn't have to be an extension (similar to 
     444!TypedHoles). 
     445 
     446Furthermore, when the user enables the [[span(!PartialTypeSignatures, style=font-variant: small-caps)]] 
     447extension, the errors are not reported anymore, the inferred type is 
     448simply used. 
     449 
     450However, named wildcards (`_a`) are currently parsed as type 
     451variables. To also remain compatible on this front, we propose to 
     452introduce a separate extension, [[span(!NamedWildcards, style=font-variant: small-caps)]]. 
     453When this extension is enabled, a type variable like `_a` will be 
     454parsed as a named wildcard. 
     455 
     456To summarise, the four different cases, depending on the enabled 
     457extensions: 
     458 
     459||                                                                 ||= [[span(!PartialTypeSignatures, style=font-variant: small-caps)]] OFF =||= [[span(!PartialTypeSignatures, style=font-variant: small-caps)]] ON =|| 
     460||= [[span(!NamedWildcards, style=font-variant: small-caps)]] OFF =|| Informative errors are reported for hole instantiations, but only for unnamed wildcards. Named wildcards are still parsed as type variables, as before. || The types of unnamed wildcards are inferred and used. Named wildcards are still parsed as type variables. || 
     461||= [[span(!NamedWildcards, style=font-variant: small-caps)]] ON  =|| Informative errors are reported for hole instantiations, both for unnamed and named wildcards. || The types of both unnamed and named wildcards are inferred and used. || 
     462 
     463Along with informative errors, we can also suggest the user to turn on 
     464the [[span(!PartialTypeSignatures, style=font-variant: small-caps)]] 
     465extension. 
     466 
     467It would be nice to eventually have Agda-style hole/goal-driven 
     468development. In the future, we will look into extending the GHC API 
     469and we will try to hack together a prototype for Emacs. 
    449470 
    450471