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. -- flippa@flippac.org Society does not owe people jobs. Society owes it to itself to find people jobs.
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... 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: * does _ only work for types, or also for class contexts? * how would the exact syntax be? * 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"? * are there any interactions with typechecking of rank-n types or GADTs? Cheers, Andres
On 23.01 18:41, Andres Loeh wrote:
* 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"?
I think this can be done: type IdApp a = a -> a foo :: IdApp _ foo = ... would then be translated as foo :: exists a. IdApp a that is foo :: exists a. a -> a - Einar Karttunen
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.
On 1/21/06, Philippa Cowderoy
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?
If one had a type annotation, say:
f :: a -> _ -> Constr a Int _
would this be unification-equivalent to:
f :: exists b c. a -> b -> Constr a Int c
--
Taral
note that this is subsumed by my existential type synonyms proposal type Any = exists a . a so Any is any type. at least, I think that works. I didn't get a whole lot of feedback on the proposal. John -- John Meacham - ⑆repetae.net⑆john⑈
note that this is subsumed by my existential type synonyms proposal
type Any = exists a . a
so Any is any type.
at least, I think that works. I didn't get a whole lot of feedback on the proposal.
I haven't looked at your proposal yet, but existential types are not the same as partial type signatures.
x :: Any x = 2
Here, "x" would be essentially unusable, i.e., only applicable to polymorphic functions.
x :: _ x = 2
The above, however, would be the same as giving no type signature for "x" at all ... Cheers, Andres
On Mon, 23 Jan 2006, John Meacham wrote:
Ah, you are right. silly me. John
I imagine we'll all have shown ourselves to be silly by the time we have a standard... -- flippa@flippac.org "My religion says so" explains your beliefs. But it doesn't explain why I should hold them as well, let alone be restricted by them.
On Mon, 23 Jan 2006, John Meacham wrote:
note that this is subsumed by my existential type synonyms proposal
Hate to go netcop, but I suspect there's at least one person reading whose mailreader doesn't do threads and thus who'll have a fun time working out whether you're responding to my first or second post (it's the first, btw).
type Any = exists a . a
so Any is any type.
at least, I think that works. I didn't get a whole lot of feedback on the proposal.
It's on the wiki, right? Will look later. -- flippa@flippac.org There is no magic bullet. There are, however, plenty of bullets that magically home in on feet when not used in exactly the right circumstances.
participants (5)
-
Andres Loeh -
Einar Karttunen -
John Meacham -
Philippa Cowderoy -
Taral