On Mon, 23 Jan 2006, Andres Loeh wrote:
Hi Philippa,
Would it be possibly to support a 'wildcard' type (probably written "_" to match the pattern-matching syntax) that matched any inferred type without requiring any actual degree of polymorphism the way a type variable would? This would allow 'partial' annotations, making it easier to provide the type system with extra information without having to supply potentially complicated parameters that it can infer itself. Possibly the same thing could also be used in a type's constraint to indicate zero or more predicates other than those specified.
I like this idea. There's a Wiki page with not so much information yet about this feature:
http://haskell.galois.com/cgi-bin/haskell-prime/trac.cgi/wiki/PartialTypeSig...
As I understand it I don't have edit access to this as I'm not part of the committee. Given the intention of the wiki this may well just be the way things should be done, too - I certainly shouldn't be on the committee, I can't fairly make the commitment.
The disadvantage of the current Haskell solution is that it is so much "all or nothing". You cannot have the benefits of inference without losing the benefits of documentation. For complex class contexts (and even more for implicit parameters), it would be extremely helpful to have the possiblity to omit parts of a type signature, and even in normal situations it can be helpful.
I think what we need here is a real proposal, because it is a feature that currently isn't implemented (it might be in EHC, but I don't know the syntax there). In particular, I'm unclear about the following questions:
<rearranged bulletpoints for convenience of answering>
* does _ only work for types, or also for class contexts? * if you have multiple underscores, they're all different, I guess; but wouldn't you want also to be able to say that a type is "_a -> _a" for some "_a"?
Both of these I think boil down to "yes, assuming no good reason not to". Definitely I'd like to see it allowed in place of zero-or-more constraints, I figure it's probably a good idea within the individual predicates and more so given the use of _a for a metavariable. The only problem I can see with metavariables is that sooner or later someone's going to ask questions like "what scope should they have?" (I've talked about the possibility of module-level metavariables in #haskell before, so it's not a stupid question).
* are there any interactions with typechecking of rank-n types or GADTs?
I don't know about GADTs, though the intuition below should apply. Given a predicative type system (which rank-n types as implemented are currently) there may be some thinking to do about whether we want to allow wildcards to be instantiated impredicatively (which we can legitimately do as far as I'm aware as it's just a 'match' which should either fail or not generate any new information). If we don't allow that, _ only refers to a monotype. With an impredicative system (ala the "boxy types" paper) I don't see any problems at all - having seen the restriction on subsumption variance required by GHC (as mentioned in the latest version of the boxy types paper) I'm not quite as keen on impredicativity in Haskell' as before though. Knowing my luck, and given that I've never implemented a typechecker for anything more complicated than Hindley-Milner+subtyping+annotations, I'm probably about to be given a number of reasons why the proposal still falls through.
* how would the exact syntax be?
I'm going to pass on providing grammar extensions right now as it's late, I'm tired and I'd mess it up. If anyone wants to provide some for obvious variations of the above that'd be cool (I'm in two minds about _a or _a_ for metavariables, if we have them then _ is effectively just an 'anonymous metavariable'). Failing that I guess I should try to bash some out over the next few days. -- flippa@flippac.org The task of the academic is not to scale great intellectual mountains, but to flatten them.