Changes between Version 6 and Version 7 of PartialTypeSignatures

Mar 14, 2014 2:38:47 PM (19 months ago)

Discuss the integration with the Holes proposal


  • PartialTypeSignatures

    v6 v7  
    2828more practical point of view in the hope to get some feedback from the
    2929GHC developers community.
     32'''NOTE''': [#holes a new section] about the integration of this
     33proposal with the [wiki:Holes] proposal.
    3135== Motivation and discussion ==
    423427for more discussion.
    425 === Extension Flags ===
    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.
    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.
    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
     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.
     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
     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.
     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.
     456To summarise, the four different cases, depending on the enabled
     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. ||
     463Along with informative errors, we can also suggest the user to turn on
     464the [[span(!PartialTypeSignatures, style=font-variant: small-caps)]]
     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.