Changes between Version 2 and Version 3 of Ticket #86


Ignore:
Timestamp:
Feb 3, 2006 2:25:29 AM (9 years ago)
Author:
flippa
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #86 – Description

    v2 v3  
    1 Short idea: _ in place of a type is "match anything". This is /not/ the type (exists a.a), contrary to suggestions on the mailing list, as a) we wish to end up with a more specific type via inference and b) the existential type would have issues with predicativity and/or impredicativity.
     1Short idea: _ in place of a type is "match anything" (by analogy to the wildcard pattern). This is /not/ the type (exists a.a), contrary to suggestions on the mailing list, as a) we wish to end up with a more specific type via inference and b) the existential type would have issues in a predicative type system (which includes the current rank-n implementations). Essentially, in checking the annotation we infer as normal for the _ and accept whatever is inferred.
    22
    33Note that _ *is not a type*. It's part of the type annotation, but should never be propagated "upwards" by the typechecker - only the type inferred for its position.
     4
     5There are some further possible extensions to this idea:
     6
     7 1. Allow _ in class contexts to mean one or both of "and additional constraints" or "some type variable that will be inferred".
     8 1. Allow "metavariables" (no longer actually meta due to being in the type system, of course) which might be written _a and appear multiple times in the same annotation always meaning the same type.
     9  * Add some kind of binder for metavariables and give them lexical scope much as can be done with ordinary type variables. If we do this, top-level bindings would also make sense and allow us to name types we'd like inferred for us before using them as part of type declarations
     10  * Allow some kind of constraints between metavariables (Frank Atanassow mentioned this to me on #haskell-blah)