Re: ExplicitForAll complete
On Fri, Dec 24, 2010 at 11:31:17PM +0100, Lennart Augustsson wrote: > I think they are equally feasible, but as Simon says, we have avoided > introducing new global keywords. > And I think we should avoid it this time too. Why break programs when we > don't have to. I've added an alternative delta to the page, where forall is only a keyword in types. The committee can choose which they prefer. Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
I think they are equally feasible, but as Simon says, we have avoided introducing new global keywords. And I think we should avoid it this time too. Why break programs when we don't have to. -- Lennart On Fri, Dec 24, 2010 at 9:31 PM, Ian Lynagh wrote: > On Thu, Dec 23, 2010 at 09:46:29AM +, Simon Marlow wrote: > > > > I don't think it's feasible to allow 'case' as a type > > variable, but it's certainly feasible to allow 'forall' as a term > > variable. > > Why is 'case'-only-in-expression harder than 'forall'-only-in-type? > > > On the other hand, it makes life difficult for syntax highlighters. > > Yup. > > > Thanks > Ian > > > ___ > Haskell-prime mailing list > Haskell-prime@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-prime > ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
On Thu, Dec 23, 2010 at 09:46:29AM +, Simon Marlow wrote: > > I don't think it's feasible to allow 'case' as a type > variable, but it's certainly feasible to allow 'forall' as a term > variable. Why is 'case'-only-in-expression harder than 'forall'-only-in-type? > On the other hand, it makes life difficult for syntax highlighters. Yup. Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
On 22/11/10 11:41, Ian Lynagh wrote: Hi Iavor, Thanks for your comments. On Sun, Nov 21, 2010 at 06:25:38PM -0800, Iavor Diatchki wrote: * Why is "forall" promoted to a keyword, rather then just being special in types as is in all implementations? I like the current status quo where "forall" can still be used in value expressions. You can't use "case" as a type variable, so I don't see why you should be able to use "forall" as an expression variable. I imagine that the reason implementations currently allow it is to minimise the chance of an extension breaking existing programs, but I believe that when making new versions of the standard we should, where feasible, write them in the way that they would have been written if the previous versions had never existed. We tend not to make new global keywords when we can avoid doing so. 'hiding', 'qualified', 'as', 'safe', 'unsafe', 'dynamic' etc. are all examples of identifiers interpreted as keywords only in certain contexts. I don't think it's feasible to allow 'case' as a type variable, but it's certainly feasible to allow 'forall' as a term variable. On the other hand, it makes life difficult for syntax highlighters. Cheers, Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
On Mon, Nov 22, 2010 at 02:36:51PM -0500, Isaac Dupree wrote: > > P.S. IMHO capitalization, ExplicitForAll vs ExplicitForall, let's stick > to one. The extension is written ExplicitForall. GHC only knows about ExplicitForAll. I think this was a mistake, but I don't think it's worth changing now (assuming the proposal is accepted), as shortly after it is part of H' it won't be necessary to refer to it by name in new code anyway. Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
On 11/22/10 06:41, Ian Lynagh wrote: On Sun, Nov 21, 2010 at 06:25:38PM -0800, Iavor Diatchki wrote: * It seems that allowing "superflous" values in "foralls" could be useful for some future extensions. For example, if we had scoped type variables and explicit type application, then it may make sense to have quantified variables that do not appear in the rest of the type (but do appear in the definition of the function). I guess, we could revise things again if that was to ever happen but still, it seems to me that this might be more appropriate as an "unused variable" warning, rather then an error? "Eq a => Int" isn't a valid type, so I don't think "forall a . Int" should be either. As you say, it's possible that future extensions will generalise this. In functions with typeclass overloading, the typeclass must be picked in order to call the function, even if this means resorting to defaulting. In functions with parametric polymorphism (no (context)=>), it never needs to be decided. For example, "exitFailure :: IO a" can be called on a line where the return value is never used (besides being unified with (>>=) types and stuff); it can remain "a". So I don't think that analogy works for me. Still not sure whether we should allow "forall a . Int" or not (no strong opinions either way). I think it would compile and type-inference fine (although GHC experts may correct me.. and/or people familiar with other compiler implementations too). * Is there any case where an empty "forall" is useful, and if not, why allow it? I guess it is a way to make it explicit that a value is monomorphic but i think that types like "forall. Int" look odd. I don't mind either way. It looks odd, but it would be annoying (to tools and otherwise) to exclude it from being allowed, even if it's not used much. P.S. IMHO capitalization, ExplicitForAll vs ExplicitForall, let's stick to one. The extension is written ExplicitForall. -Isaac ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
Hi Iavor, Thanks for your comments. On Sun, Nov 21, 2010 at 06:25:38PM -0800, Iavor Diatchki wrote: > > * Why is "forall" promoted to a keyword, rather then just being > special in types as is in all implementations? I like the current > status quo where "forall" can still be used in value expressions. You can't use "case" as a type variable, so I don't see why you should be able to use "forall" as an expression variable. I imagine that the reason implementations currently allow it is to minimise the chance of an extension breaking existing programs, but I believe that when making new versions of the standard we should, where feasible, write them in the way that they would have been written if the previous versions had never existed. > * It seems that allowing "superflous" values in "foralls" could be > useful for some future extensions. For example, if we had scoped type > variables and explicit type application, then it may make sense to > have quantified variables that do not appear > in the rest of the type (but do appear in the definition of the > function). I guess, we could revise things again if that was to ever > happen but still, it seems to me that this might be more appropriate > as an "unused variable" warning, rather then an error? "Eq a => Int" isn't a valid type, so I don't think "forall a . Int" should be either. As you say, it's possible that future extensions will generalise this. > * Is there any case where an empty "forall" is useful, and if not, > why allow it? I guess it is a way to make it explicit that a value is > monomorphic but i think that types like "forall. Int" look odd. I don't mind either way. Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ExplicitForAll complete
Hello, I have no strong feelings for or against allowing explicit foralls in types but I have a few questions/suggestions on the proposal in its current form (21 Nov 2010): * Why is "forall" promoted to a keyword, rather then just being special in types as is in all implementations? I like the current status quo where "forall" can still be used in value expressions. * It seems that allowing "superflous" values in "foralls" could be useful for some future extensions. For example, if we had scoped type variables and explicit type application, then it may make sense to have quantified variables that do not appear in the rest of the type (but do appear in the definition of the function). I guess, we could revise things again if that was to ever happen but still, it seems to me that this might be more appropriate as an "unused variable" warning, rather then an error? * Is there any case where an empty "forall" is useful, and if not, why allow it? I guess it is a way to make it explicit that a value is monomorphic but i think that types like "forall. Int" look odd. -Iavor On Fri, Nov 19, 2010 at 5:08 PM, Ian Lynagh wrote: > > Hi all, > > I've completed the ExplicitForAll proposal, started by Niklas Broberg > (but any errors are doubtless mine!): > > http://hackage.haskell.org/trac/haskell-prime/wiki/ExplicitForall > http://hackage.haskell.org/trac/haskell-prime/ticket/133 > > I imagine this is too late for H2011 (if that will actually be > happening?), but there wasn't an H2012 milestone, so I put it in H2011 > anyway. Please feel free to remilestone. > > > Thanks > Ian > > ___ > Haskell-prime mailing list > Haskell-prime@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-prime > ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
ExplicitForAll complete
Hi all, I've completed the ExplicitForAll proposal, started by Niklas Broberg (but any errors are doubtless mine!): http://hackage.haskell.org/trac/haskell-prime/wiki/ExplicitForall http://hackage.haskell.org/trac/haskell-prime/ticket/133 I imagine this is too late for H2011 (if that will actually be happening?), but there wasn't an H2012 milestone, so I put it in H2011 anyway. Please feel free to remilestone. Thanks Ian ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
ExplicitForall
Hi all, Per request I've made a ticket and proposal page for adding ExplicitForall to Haskell'2010: http://hackage.haskell.org/trac/haskell-prime/ticket/133 http://hackage.haskell.org/trac/haskell-prime/wiki/ExplicitForall Cheers, /Niklas ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: ExplicitForall
On Thu, Jul 23, 2009 at 7:36 AM, Niklas Broberg wrote: >> Alright, let's set an actual discussion period of 2 weeks for >> ExplicitForall. If there is no opposition by then, we can add >> ExplicitForall to the registered extensions in cabal as a first step. > > Slightly more than two weeks later, there has been no voices against > and at least a few in favor. Huh. I guess I forgot I could reply? In favour I am. (Even if I do live in the US. ) ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: ExplicitForall
> Alright, let's set an actual discussion period of 2 weeks for > ExplicitForall. If there is no opposition by then, we can add > ExplicitForall to the registered extensions in cabal as a first step. Slightly more than two weeks later, there has been no voices against and at least a few in favor. The attached patch for Cabal adds ExplicitForall to the Extension datatype, with documentation, and adds it to knownExtensions. Cheers, /Niklas ExplicitForall.dpatch Description: Binary data ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal: ExplicitForall
> What you suggest would be fine with me. Presumably ExplicitForall would be > implied by RankNTypes and the other extensions? Yes, that's the idea. Rank2Types, RankNTypes, PolymorphicComponents, ScopedTypeVariables and LiberalTypeSynonyms would all imply ExplicitForall. > There is a danger of having too *many* choices. > (http://www.joelonsoftware.com/items/2006/11/21.html) In particular, you > might consider making ScopedTypeVariables synonymous with ExplicitForAll. > Once you have given up the keyword, it seems a shame not to allow lexically > scoped type variables! While I agree with you (and Joel) in principle, I think this is the wrong level to hold that discussion. I think the long-term solution should be to keep the registered extensions cleanly separated, and instead supply extension *groups* as a way to limit choice. -fglasgow-exts has fit that niche admirably for a long time, I think a lot of people just use that without thinking twice about what particular extensions they actually use, and nothing wrong with that. I think the move towards LANGUAGE pragmas instead of compiler options is a good one from a standardisation and implementation point of view, but to avoid tedium and unnecessary choice for the programmer I strongly feel that extension groups need to be introduced at this level too. But as I said, that's for a different discussion... > On ExistentialQuantification, I personally think we should deprecate the > entire construct, suggesting GADT-style syntax instead. +1, though I was afraid to suggest something that radical. I might write a separate proposal for that then, to keep the discussion here focused on ExplicitForall. > If you can form a consensus, go for it. Alright, let's set an actual discussion period of 2 weeks for ExplicitForall. If there is no opposition by then, we can add ExplicitForall to the registered extensions in cabal as a first step. Cheers, /Niklas ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re[2]: Proposal: ExplicitForall
Hello Brandon, Wednesday, June 24, 2009, 8:56:30 AM, you wrote: > but also e.g. if you are actually compiling Haskell98, hierarchical > modules should be illegal. afaik, HM and FFI are just considered to be included in H98 later, so these are part of (revised) standard -- Best regards, Bulatmailto:bulat.zigans...@gmail.com ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: Proposal: ExplicitForall
| I would thus like to propose the following formalisation of the | ExplicitForall extension: What you suggest would be fine with me. Presumably ExplicitForall would be implied by RankNTypes and the other extensions? There is a danger of having too *many* choices. (http://www.joelonsoftware.com/items/2006/11/21.html) In particular, you might consider making ScopedTypeVariables synonymous with ExplicitForAll. Once you have given up the keyword, it seems a shame not to allow lexically scoped type variables! On ExistentialQuantification, I personally think we should deprecate the entire construct, suggesting GADT-style syntax instead. If you can form a consensus, go for it. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Proposal: ExplicitForall
Hi all, (I'm writing this to several lists since it involves GHC (implementation of extensions), cabal (registration of extensions) and some future Haskell standard (formalisation of extensions).) In my quest to implement all known syntactic extensions to Haskell in my haskell-src-exts package, I've become painfully aware of the sometimes ad-hoc nature that these extensions have been added to GHC. This should not be taken as criticism per se, GHC is awesome and I'm sure a lot of thought and research has gone into all of these extensions. I think the problem (from my point of view) is rather that most of the extensions are only really "interesting" on a type system level, whereas the syntactic level is rather trivial, and thus the latter has (rightly) gotten far less formal attention. I hope my putting the light on these issues will be a help and a kickoff towards improving the state of formalisation of the known and registered (with Cabal) extensions. One of the most blatant and (to me) problematic such issues is the matter of using 'forall'. GHC has a number of extensions relating to the use of forall-quantified types in various interesting ways. With none of these extensions on, forall is not considered a keyword, so the syntax with explicit forall quantification cannot be used at all ('forall' is considered a varid). However, with *any* extension on that relates to forall-quantified types, forall is a keyword, and can syntactically be used in types *anywhere*. This doesn't mean all such types will pass the type checker, most of them won't in fact, but syntactically there is really no (or at least very little) difference. Conceptually, all of these extensions (specifically PolymorphicComponents, Rank2Types, RankNTypes, LiberalTypeSynonyms and ScopedTypeVariables (and strangely also ExistentialQuantification)) thus have one thing in common. They all enable syntactically forall-quantified types. They allow different uses of these types as far as the type system is concerned, but syntactically there is no difference between type and type (in fact there cannot be, as I discussed in a recent blog post [1]). Funnily enough there are also some uses of forall-quantified types that are common to all of these extensions - using a forall just to make polymorphism explicit in a type doesn't change anything as far as the type system is concerned, so e.g. the types '(Eq a) => a -> Bool' and 'forall a . (Eq a) => a -> Bool' are equivalent. The latter type can be given to a function when any of the listed six extensions are given, even if most of them have nothing to do with this at all! So, what I'm getting at is an idea that Isaac Dupree gave as a comment to my blog post. He said: "I wish there was a plain old ExplicitForall extension that enabled the keyword in types (without extending the type checker -- only like (id :: forall a. a -> a) would be allowed)". I think this is a really great idea. I find it conceptually appealing, since I think it covers exactly that blind spot that is the seemingly unintended intersection between all these extensions. And it also makes the separation of concern between the syntactic level and the type system more clear. Any formalisation of any of the type system extensions would not need to bother with syntactic details, but can simply be said to imply ExplicitForall. I would thus like to propose the following formalisation of the ExplicitForall extension: = ExplicitForall enables the use of the keyword 'forall' to make a type explicitly polymorphic. Syntactically, it would mean the following change to Haskell 98: * 'forall' becomes a reserved word. * '.' (dot) becomes a special (not reserved) operator. * The following syntactic rule changes: type -> 'forall' tyvars '.' type | context '=>' type | ftype ftype -> btype '->' type | btype gendecl -> vars '::' type It does not allow the use of explicitly polymorphic types in any way not already allowed by Haskell 98 for implicitly polymorphic types. = One thing to note is that I haven't touched the matter of ExistentialQuantification in the above. Syntactically this is a different beast entirely, and could well be handled separately, though it's really an artifact of the way we (by default) write our data type declarations. Using GADT-style declarations, existential quantification goes nicely along with the others by following the same syntactic rules for types, even though from a type system it is of course still quite different from the rest. But with the ordinary Haskell 98 declaration style, we could define the syntactic part of the ExistentialQuantification extension as the foll