Wildcard type annotations

[Philippa Cowderoy]

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/PartialTypeSigs
> 

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 at flippac.org

The task of the academic is not to scale great 
intellectual mountains, but to flatten them.