Re: Why aren't classes like "Num" levity polymorphic?
Another, weaker version of this is to just require default signatures that assume r has type LiftedRep for each of the defaults, but then instantiating things at obscure kinds becomes _much_ harder. -Edward On Mon, May 9, 2022 at 12:30 PM Edward Kmett wrote: > Also, if you do want to experiment with this in ghci you need to set some > flags in .ghci: > > -- ghci binds 'it' to the last expression by default, but it assumes it > lives in Type. this blocks overloaded printing > :set -fno-it > > -- replace System.IO.print with whatever 'print' is in scope. You'll need > a RuntimeRep polymorphic 'print' function, though. > :set -interactive-print print > > -- we don't want standard Prelude definitions. The above Lev trick for > ifThenElse was required because turning on RebindableSyntax broke if. > :set -XRebindableSyntax -XNoImplicitPrelude > > etc. > > With that you can get surprisingly far. It is rather nice being able to > use (+) and a Show and the like on primitive Int#s and what have you. > > For me the main win is that I can do things like install Eq on > (MutableByteArray# s) and the like and stop having to use random function > names to access that functionality. > > You can also use the new UnliftedDataTypes and/or UnliftedNewtypes to do > things like pass around a Natural# that is stored in a couple of registers > and then build support for it. This is also included in that repo above. > > > -Edward > > On Mon, May 9, 2022 at 12:24 PM Edward Kmett wrote: > >> It is rather shockingly difficult to get it to work out because of the >> default definitions in each class. >> >> Consider just >> >> class Eq (a :: TYPE r) where >> (==), (/=) :: a -> a -> Bool >> >> That looks good until you remember that >> >> x == y = not (x /= y) >> x /= y = not (x == y) >> >> are also included in the class, and cannot be written in a RuntimeRep >> polymorphic form! >> >> The problem is that x has unknown rep and is an argument. We can only be >> levity polymorphic in results. >> >> So you then have to do something like >> >> default (==) :: EqRep r => a -> a -> Bool >> (==) = eqDef >> default (/=) :: EqRep r => a -> a -> Bool >> (/=) = neDef >> >> >> class EqRep (r :: RuntimeRep) where >> eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool >> >> and then bury them in a class that actually knows about the RuntimeRep. >> >> We can lift the Prelude.Eq into the modified Eq above pointwise inside >> kind Type. >> >> instance Prelude.Eq a => Eq (a :: Type) where >> (==) = (Prelude.==) >> (/=) = (Prelude./=) >> >> and/or we can instantiate EqRep at _all_ the RuntimeReps. >> >> That is where we run into a problem. You could use a compiler plugin to >> discharge the constraint (which is something I'm actively looking into) or >> you can do something like write out a few hand-written instances that are >> all completely syntactically equal: >> >> instance EqRep LiftedRep where >> eqDef x y = not (x /= y) >> neDef x y = not (x == y) >> >> instance EqRep ... where >>... >> >> The approach I'm taking today is to use backpack to generate these EqRep >> instances in a canonical location. It unfortunately breaks GHC when used in >> sufficient anger to handle TupleRep's of degree 2 in full generality, >> because command line lengths for each GHC invocation starts crossing 2 >> megabytes(!) and we break operating system limits on command line lengths, >> because we don't have full support for passing arguments in files from >> cabal to ghc. >> >> The approach I'd like to take in the future is to discharge those >> obligations via plugin. >> >> >> There are more tricks that you wind up needing when you go to progress to >> handle things like Functor in a polymorphic enough way. >> >> type Lev (a :: TYPE r) = () => a >> >> is another very useful tool in this toolbox, because it is needed when >> you want to delay a computation on an argument in a runtime-rep polymorphic >> way. >> >> Why? Even though a has kind TYPE r. Lev a always has kind Type! >> >> So I can pass it in argument position independent of RuntimeRep. >> >> ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a >> ifThenElse True x _ = x >> ifThenElse False _ y = y >> >> Note this function didn't need any fancy Foo
Re: Why aren't classes like "Num" levity polymorphic?
Also, if you do want to experiment with this in ghci you need to set some flags in .ghci: -- ghci binds 'it' to the last expression by default, but it assumes it lives in Type. this blocks overloaded printing :set -fno-it -- replace System.IO.print with whatever 'print' is in scope. You'll need a RuntimeRep polymorphic 'print' function, though. :set -interactive-print print -- we don't want standard Prelude definitions. The above Lev trick for ifThenElse was required because turning on RebindableSyntax broke if. :set -XRebindableSyntax -XNoImplicitPrelude etc. With that you can get surprisingly far. It is rather nice being able to use (+) and a Show and the like on primitive Int#s and what have you. For me the main win is that I can do things like install Eq on (MutableByteArray# s) and the like and stop having to use random function names to access that functionality. You can also use the new UnliftedDataTypes and/or UnliftedNewtypes to do things like pass around a Natural# that is stored in a couple of registers and then build support for it. This is also included in that repo above. -Edward On Mon, May 9, 2022 at 12:24 PM Edward Kmett wrote: > It is rather shockingly difficult to get it to work out because of the > default definitions in each class. > > Consider just > > class Eq (a :: TYPE r) where > (==), (/=) :: a -> a -> Bool > > That looks good until you remember that > > x == y = not (x /= y) > x /= y = not (x == y) > > are also included in the class, and cannot be written in a RuntimeRep > polymorphic form! > > The problem is that x has unknown rep and is an argument. We can only be > levity polymorphic in results. > > So you then have to do something like > > default (==) :: EqRep r => a -> a -> Bool > (==) = eqDef > default (/=) :: EqRep r => a -> a -> Bool > (/=) = neDef > > > class EqRep (r :: RuntimeRep) where > eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool > > and then bury them in a class that actually knows about the RuntimeRep. > > We can lift the Prelude.Eq into the modified Eq above pointwise inside > kind Type. > > instance Prelude.Eq a => Eq (a :: Type) where > (==) = (Prelude.==) > (/=) = (Prelude./=) > > and/or we can instantiate EqRep at _all_ the RuntimeReps. > > That is where we run into a problem. You could use a compiler plugin to > discharge the constraint (which is something I'm actively looking into) or > you can do something like write out a few hand-written instances that are > all completely syntactically equal: > > instance EqRep LiftedRep where > eqDef x y = not (x /= y) > neDef x y = not (x == y) > > instance EqRep ... where >... > > The approach I'm taking today is to use backpack to generate these EqRep > instances in a canonical location. It unfortunately breaks GHC when used in > sufficient anger to handle TupleRep's of degree 2 in full generality, > because command line lengths for each GHC invocation starts crossing 2 > megabytes(!) and we break operating system limits on command line lengths, > because we don't have full support for passing arguments in files from > cabal to ghc. > > The approach I'd like to take in the future is to discharge those > obligations via plugin. > > > There are more tricks that you wind up needing when you go to progress to > handle things like Functor in a polymorphic enough way. > > type Lev (a :: TYPE r) = () => a > > is another very useful tool in this toolbox, because it is needed when you > want to delay a computation on an argument in a runtime-rep polymorphic way. > > Why? Even though a has kind TYPE r. Lev a always has kind Type! > > So I can pass it in argument position independent of RuntimeRep. > > ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a > ifThenElse True x _ = x > ifThenElse False _ y = y > > Note this function didn't need any fancy FooRep machinery and it has the > right semantics in that it doesn't evaluate the arguments prematurely! This > trick is needed when you want to go convert some kind of RuntimeRep > polymorphic Maybe or List for one RuntimeRep to one for another RuntimeRep > unless you want to deal with an explosive number of instances parameterized > on pairs of RuntimeReps. > > https://github.com/ekmett/unboxed is a repo of me experimenting with this > from last year some time. > > I'm also giving a talk at Yow! LambdaJam in a week or so on this! > > -Edward > > > On Mon, May 9, 2022 at 11:27 AM Clinton Mead > wrote: > >> Hi All >> >> It seems to me to be a free win just to replace: >
Re: Why aren't classes like "Num" levity polymorphic?
It is rather shockingly difficult to get it to work out because of the default definitions in each class. Consider just class Eq (a :: TYPE r) where (==), (/=) :: a -> a -> Bool That looks good until you remember that x == y = not (x /= y) x /= y = not (x == y) are also included in the class, and cannot be written in a RuntimeRep polymorphic form! The problem is that x has unknown rep and is an argument. We can only be levity polymorphic in results. So you then have to do something like default (==) :: EqRep r => a -> a -> Bool (==) = eqDef default (/=) :: EqRep r => a -> a -> Bool (/=) = neDef class EqRep (r :: RuntimeRep) where eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool and then bury them in a class that actually knows about the RuntimeRep. We can lift the Prelude.Eq into the modified Eq above pointwise inside kind Type. instance Prelude.Eq a => Eq (a :: Type) where (==) = (Prelude.==) (/=) = (Prelude./=) and/or we can instantiate EqRep at _all_ the RuntimeReps. That is where we run into a problem. You could use a compiler plugin to discharge the constraint (which is something I'm actively looking into) or you can do something like write out a few hand-written instances that are all completely syntactically equal: instance EqRep LiftedRep where eqDef x y = not (x /= y) neDef x y = not (x == y) instance EqRep ... where ... The approach I'm taking today is to use backpack to generate these EqRep instances in a canonical location. It unfortunately breaks GHC when used in sufficient anger to handle TupleRep's of degree 2 in full generality, because command line lengths for each GHC invocation starts crossing 2 megabytes(!) and we break operating system limits on command line lengths, because we don't have full support for passing arguments in files from cabal to ghc. The approach I'd like to take in the future is to discharge those obligations via plugin. There are more tricks that you wind up needing when you go to progress to handle things like Functor in a polymorphic enough way. type Lev (a :: TYPE r) = () => a is another very useful tool in this toolbox, because it is needed when you want to delay a computation on an argument in a runtime-rep polymorphic way. Why? Even though a has kind TYPE r. Lev a always has kind Type! So I can pass it in argument position independent of RuntimeRep. ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a ifThenElse True x _ = x ifThenElse False _ y = y Note this function didn't need any fancy FooRep machinery and it has the right semantics in that it doesn't evaluate the arguments prematurely! This trick is needed when you want to go convert some kind of RuntimeRep polymorphic Maybe or List for one RuntimeRep to one for another RuntimeRep unless you want to deal with an explosive number of instances parameterized on pairs of RuntimeReps. https://github.com/ekmett/unboxed is a repo of me experimenting with this from last year some time. I'm also giving a talk at Yow! LambdaJam in a week or so on this! -Edward On Mon, May 9, 2022 at 11:27 AM Clinton Mead wrote: > Hi All > > It seems to me to be a free win just to replace: > > `class Num a where` > > with > > `class Num (a :: (r :: RuntimeRep)) where` > > And then one could define `Num` instances for unlifted types. > > This would make it possible to avoid using the ugly `+#` etc syntax for > operations on unlifted types. > > `Int#` and `Word#` could have `Num` instances defined just as `Int` and > `Word` already have. > > I presume there's a reason why this hasn't been done, but I was wondering > why? > > Thanks, > Clinton > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Pattern synonym constraints :: Ord a => () => ...
On Tue, Oct 5, 2021 at 12:39 PM David Feuer wrote: > To be clear, the proposal to allow different constraints was accepted, but > integrating it into the current, incredibly complex, code was well beyond > the limited abilities of the one person who made an attempt. Totally > severing pattern synonyms from constructor synonyms (giving them separate > namespaces) would be a much simpler design. > It might be simpler in some ways, despite needing yet another syntactic marker, etc. but also would make them a lot less useful for a lot of places where they are used today, e.g. to provide backwards compatibility for old constructors as an API changes, and the like. Before I left MIRI, Cale had started work on these for us. Is that the work you are thinking of, or are you thinking of an earlier effort? -Edward > On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg > wrote: > >> >> >> On Oct 3, 2021, at 5:38 AM, Anthony Clayden >> wrote: >> >> >pattern SmartConstr :: Ord a => () => ... >> >> Seems to mean: >> >> * Required constraint is Ord a -- fine, for building >> >> >> Yes. >> >> * Provided constraint is Ord a -- why? for matching/consuming >> >> >> No. Your signature specified that there are no provided constraints: >> that's your (). >> >> >> I'm using `SmartConstr` with some logic inside it to validate/build a >> well-behaved data structure. But this is an ordinary H98 datatype, not a >> GADT. >> >> >> I believe there is no way to have provided constraints in Haskell98. You >> would need either GADTs or higher-rank types. >> >> >> This feels a lot like one of the things that's wrong with 'stupid theta' >> datatype contexts. >> >> >> You're onto something here. Required constraints are very much like the >> stupid theta datatype contexts. But, unlike the stupid thetas, required >> constraints are sometimes useful: they might be needed in order to, say, >> call a function in a view pattern. >> >> For example: >> >> checkLT5AndReturn :: (Ord a, Num a) => a -> (Bool, a) >> checkLT5AndReturn x = (x < 5, x) >> >> pattern LessThan5 :: (Ord a, Num a) => a -> a >> pattern LessThan5 x <- ( checkLT5AndReturn -> (True, x) ) >> >> >> My view pattern requires (Ord a, Num a), and so I must declare these as >> required constraints in the pattern synonym type. Because vanilla data >> constructors never do computation, any required constraints for data >> constructors are always useless. >> >> >> For definiteness, the use case is a underlying non-GADT constructor for a >> BST >> >> > Node :: Tree a -> a -> Tree a -> Tree a >> > >> >pattern SmartNode :: Ord a => () => Tree a -> a -> Tree a -> Tree a >> >> with the usual semantics that the left Tree holds elements less than this >> node. Note it's the same `a` with the same `Ord a` 'all the way down' the >> Tree. >> >> >> Does SmartNode need Ord a to match? Or just to produce a node? It seems >> that Ord a is used only for production, not for matching. This suggests >> that you want a separate smartNode function (not a pattern synonym) and to >> have no constraints on the pattern synonym, which can be unidirectional >> (that is, work only as a pattern, not as an expression). >> >> It has been mooted to allow pattern synonyms to have two types: one when >> used as a pattern and a different one when used as an expression. That >> might work for you here: you want SmartNode to have no constraints as a >> pattern, but an Ord a constraint as an expression. At the time, the design >> with two types was considered too complicated and abandoned. >> >> Does this help? >> >> Richard >> ___ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >> > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Rewrite rules involving LHS lambda?
I don't knw of a formal writeup anywhere. But does that actually mean what you are trying to write? With the effective placement of "forall" quantifiers on the outside for u and v I'd assume that x didn't occur in either u or v. Effectively you have some scope like forall u v. exists x. ... Under that view, the warnings are accurate, and the rewrite is pretty purely syntactic. I don't see how we could write using our current vocabulary that which you want. On Sun, Dec 3, 2017 at 4:50 AM, Conal Elliott wrote: > Is there a written explanation and/or examples of rewrite rules involving > a LHS lambda? Since rule matching is first-order, I'm wondering how terms > with lambda are matched on the LHS and substituted into on the RHS. For > instance, I want to restructure a lambda term as follows: > > > foo (\ x -> fmap u v) = bar (\ x -> u) (\ x -> v) > > My intent is that the terms `u` and `v` may contain `x` and that whatever > variable name is actually used in a term being rewritten is preserved so as > to re-capture its occurrences on the RHS. > > When I write this sort of rule, I get warnings about `x` being defined but > not used. > > Thanks, -- Conal > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: DeriveFoldable treatment of tuples is surprising
As I recall, Richard Eisenberg has been pushing, off and on, for us to get a better vocabulary to specify "how" something is derived, via DeriveAnyClass, generalized newtype deriving, DeriveFoldable, etc. In general I think the current behavior is the least surprising as it "walks all the a's it can" and is the only definition compatible with further extension with Traversable. Right now there are no instances provided by base that violate the "walk all the a's" intuition and there is a fair bit of user code for things like vector types that do things like newtype V3 a = V3 (a,a,a,a) replacing that with a data type isn't without cost because now converting back and forth between that and a tuple could no longer be done for zero cost with coercions. This style of code is more common among the ML-turned-haskeller crowd, whom -- in my experience -- tend to think of it as just giving the constructor paren around its arguments rather than as a tuple. Destroying Foldable for that and making working code not work just for users to have to manually specify multiple tedious instances that should be easily derivable shouldn't be a thing we do lightly. DeriveFunctor doesn't consider that functors involved may be contravariant either. DeriveFoo generally does something that is a best effort. I'm more inclined to leave it on the list of things that DeriveFoo does differently than GND, and as yet another argument pushing us to find a better vocabulary for talking about deriving. -Edward On Tue, Mar 21, 2017 at 5:11 PM, David Feuer wrote: > The point is that there are two reasonable ways to do it, and the > deriving mechanism, as a rule, does not make choices between > reasonable alternatives. > > On Tue, Mar 21, 2017 at 5:05 PM, Jake McArthur > wrote: > > I think it's a question of what one considers consistent. Is it more > > consistent to treat tuples as transparent and consider every component > with > > type `a`, or is it more consistent to treat tuples as opaque and reuse > the > > existing Foldable instance for tuples even if it might cause a compile > time > > error? > > > > > > On Tue, Mar 21, 2017, 4:34 PM David Feuer wrote: > >> > >> This seems much too weird: > >> > >> *> :set -XDeriveFoldable > >> *> data Foo a = Foo ((a,a),a) deriving Foldable > >> *> length ((1,1),1) > >> 1 > >> *> length $ Foo ((1,1),1) > >> 3 > >> > >> I've opened Trac #13465 [*] for this. As I write there, I think the > >> right thing is to refuse to derive Foldable for a type whose Foldable > >> instance would currently fold over components of a tuple other than > >> the last one. > >> > >> I could go either way on Traversable instances. One could argue that > >> since all relevant components *must* be traversed, we should just go > >> ahead and do that. Or one could argue that we should be consistent > >> with Foldable and refuse to derive it. > >> > >> What do you all think? > >> > >> [*] https://ghc.haskell.org/trac/ghc/ticket/13465 > >> ___ > >> Glasgow-haskell-users mailing list > >> Glasgow-haskell-users@haskell.org > >> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Derived Functor instance for void types
"Preserving user bottoms" was found to be better behavior for us with Void as well back in the day. Evaluating such a term to get the bottom out is better than making up one that loses information for the user about precisely what bottom it is they had. We do so with absurd and the like for Void. This way if you map over a structure with errors at the leaves you get a new structure with those same errors at the leaves. *tl;dr* +1 from me. -Edward On Sun, Jan 15, 2017 at 11:00 PM, Kevin Cotrone wrote: > That seems to have a surprising strictness. > > I'm not sure if it would be the best idea to try and evaluate a type with > no inhabitants. > > On Sun, Jan 15, 2017 at 2:37 PM, David Feuer > wrote: > >> Currently, if you write >> >> data V a deriving Functor >> >> GHC generates >> >> fmap _ _ = error "Void fmap" >> >> This seems quite unfortunate, because it loses potentially useful error >> information: >> >> fmap (+ 3) (error "Too many snozzcumbers!") >> >> throws "Void fmap", rather than the much more precise "Too many >> snozzcumbers!" I've opened Trac #13117 to fix this, but I figured I should >> double check that no one is opposed. >> >> David Feuer >> >> ___ >> Libraries mailing list >> librar...@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> >> > > ___ > Libraries mailing list > librar...@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Retro-Haskell: can we get seq somewhat under control?
Actually, if you go back to the original form of Seq it would translate to data Seq a => Foo a = Foo !Int !a which requires resurrecting DatatypeContexts, and not data Foo a = Seq a => Foo !Int !a The former requires Seq to call the constructor, but doesn't pack the dictionary into the constructor. The latter lets you get the dictionary out when you pattern match on it. meaning it has to carry the dictionary around! Unfortunately, non-trivial functionality is lost. With the old DatatypeContext translation you can't always unpack and repack a constructor. Whereas with a change to an existential encoding you're carrying around a lot of dictionaries in precisely the structures that least want to carry extra weight. Both of these options suck relative to the status quo for different reasons. -Edward On Wed, Dec 21, 2016 at 2:14 PM, Index Int wrote: > There's a related GHC Proposal: > https://github.com/ghc-proposals/ghc-proposals/pull/27 > > On Wed, Dec 21, 2016 at 10:04 PM, David Feuer > wrote: > > In the Old Days (some time before Haskell 98), `seq` wasn't fully > > polymorphic. It could only be applied to instances of a certain class. > > I don't know the name that class had, but let's say Seq. Apparently, > > some people didn't like that, and now it's gone. I'd love to be able > > to turn on a language extension, use an alternate Prelude, and get it > > back. I'm not ready to put up a full-scale proposal yet; I'm hoping > > some people may have suggestions for details. Some thoughts: > > > > 1. Why do you want that crazy thing, David? > > > > When implementing general-purpose lazy data structures, a *lot* of > > things need to be done strictly for efficiency. Often, the easiest way > > to do this is using either bang patterns or strict data constructors. > > Care is necessary to only ever force pieces of the data structure, and > > not the polymorphic data a user has stored in it. > > > > 2. Why does it need GHC support? > > > > It would certainly be possible to write alternative versions of `seq`, > > `$!`, and `evaluate` to use a user-supplied Seq class. It should even > > be possible to deal with strict data constructors by hand or > > (probably) using Template Haskell. For instance, > > > > data Foo a = Foo !Int !a > > > > would translate to normal GHC Haskell as > > > > data Foo a = Seq a => Foo !Int !a > > > > But only GHC can extend this to bang patterns, deal with the > > interactions with coercions, and optimize it thoroughly. > > > > 3. How does Seq interact with coercions and roles? > > > > I believe we'd probably want a special rule that > > > > (Seq a, Coercible a b) => Seq b > > > > Thanks to this rule, a Seq constraint on a type variable shouldn't > > prevent it from having a representational role. > > > > The downside of this rule is that if something *can* be forced, but we > > don't *want* it to be, then we have to hide it a little more carefully > > than we might like. This shouldn't be too hard, however, using a > > newtype defined in a separate module that exports a pattern synonym > > instead of a constructor, to hide the coercibility. > > > > 4. Optimize? What? > > > > Nobody wants Seq constraints blocking up specialization. Today, a > function > > > > foo :: (Seq a, Foldable f) => f a -> () > > > > won't specialize to the Foldable instance if the Seq instance is > > unknown. This is lousy. Furthermore, all Seq instances are the same. > > The RTS doesn't actually need a dictionary to force something to WHNF. > > The situation is somewhat similar to that of Coercible, *but more so*. > > Coercible sometimes needs to pass evidence at runtime to maintain type > > safety. But Seq carries no type safety hazard whatsoever--when > > compiling in "production mode", we can just *assume* that Seq evidence > > is valid, and erase it immediately after type checking; the worst > > thing that could possibly happen is that someone will force a function > > and get weird semantics. Further, we should *unconditionally* erase > > Seq evidence from datatypes; this is necessary to maintain > > compatibility with the usual data representations. I don't know if > > this unconditional erasure could cause "laziness safety" issues, but > > the system would be essentially unusable without it. > > > > 4. What would the language extension do, exactly? > > > > a. Automatically satisfy Seq for data types and families. > > b. Propagate Seq constraints using the usual rules and the special > > Coercible rule. > > c. Modify the translation of strict fields to add Seq constraints as > required. > > > > David Feuer > > ___ > > ghc-devs mailing list > > ghc-d...@haskell.org > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ > ghc-devs mailing list > ghc-d...@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ Glasgow-haskell-users mailin
Re: Looking for GHC compile-time performance tests
vector-algorithms has gotten slower to both compile and for users rather consistently during each release throughout the 7.x lifecycle. That may serve as a good torture test as well. > On May 6, 2016, at 6:22 AM, Erik de Castro Lopo wrote: > > Ben Gamari wrote: > >> So, if you would like to see your program's compilation time improve >> in GHC 8.2, put some time into reducing it to something minimal, submit >> it to us via a Trac ticket, and let us know in this thread. > > The vector package is probably a good candidate. Compling vector slowed > down signicantly between 7.8 and 7.10, only to speed up again with 8.0. > > Erik > -- > -- > Erik de Castro Lopo > http://www.mega-nerd.com/ > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0
Moreover those _'d type variables would infect all of our haddocks. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0
No, the type instance must match the class heading. I *can* use instance Foo [_a] where type Bar [_a] = Int whatever = ... where bar :: _a -> Int bar = ... but that is a needlessly messy thing to request of every package everywhere. The arguments being pattern matched in a class associated type aren't really just bindings, they reference the surrounding context and so shouldn't be treated the same as the basic type family case. It isn't just the class associated type being mangled, it is every type variable that comes from the instance head in the entire body of every instance that happens to have a class associated type in it. Note that in the example above I added another ScopedTypeVariables reference to the same parameter, but it _also_ must be mangled despite having absolutely nothing to do with the class associated type. The existing convention has worked since 6.10 or so, when all of this stuff was invented in the first place, and the new state of affairs is clearly worse. -Edward On Sun, Jan 17, 2016 at 3:16 AM, Andrew Farmer wrote: > Can't you just: > > instance Foo [a] where > type Bar [_a] = Int > > (At least I think I did that somewhere...) > On Jan 16, 2016 9:24 PM, "Edward Kmett" wrote: > >> As a data point I now get thousands of occurrences of this warning across >> my packages. >> >> It is quite annoying. >> >> class Foo a where >> type Bar a >> >> instance Foo [a] where >> type Bar [a] = Int >> >> is enough to trigger it. >> >> And you can't turn it off by using _ as >> >> instance Foo [_] where >> type Bar [_] = Int >> >> isn't legal. >> >> I've been avoiding it for now by using >> >> if impl(ghc >= 8) >> >> ghc-options: -fno-warn-unused-matches >> >> but this is a pretty awful addition to this warning as it stands. >> -Edward >> >> On Mon, Jan 11, 2016 at 2:12 PM, Henning Thielemann < >> lemm...@henning-thielemann.de> wrote: >> >>> >>> On Mon, 11 Jan 2016, Richard Eisenberg wrote: >>> >>> On Jan 9, 2016, at 6:44 PM, Henning Thielemann < >>>> lemm...@henning-thielemann.de> wrote: >>>> >>>>> >>>>> instance (Natural n) => Num.Integer (Un n) where >>>>>type Repr (Un _n) = Unary >>>>> >>>>> >>>>> GHC-7.6.3 and GHC-7.4.2 complain: >>>>>Type indexes must match class instance head >>>>>Found `Un _n' but expected `Un n' >>>>>In the type synonym instance declaration for `Num.Repr' >>>>>In the instance declaration for `Num.Integer (Un n)' >>>>> >>>>> >>>>> GHC-7.8.4, GHC-7.10.3 and GHC-8.0 are happy with the difference. >>>>> >>>> >>>> I'm surprised this is accepted at all. Looks like hogwash to me. I >>>> think you should post a bug report. >>>> >>> >>> Ok, but then GHC must not warn about the unused argument of Repr. >>> >>> ___ >>> Glasgow-haskell-users mailing list >>> Glasgow-haskell-users@haskell.org >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >>> >> >> >> ___ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users >> >> ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0
As a data point I now get thousands of occurrences of this warning across my packages. It is quite annoying. class Foo a where type Bar a instance Foo [a] where type Bar [a] = Int is enough to trigger it. And you can't turn it off by using _ as instance Foo [_] where type Bar [_] = Int isn't legal. I've been avoiding it for now by using if impl(ghc >= 8) ghc-options: -fno-warn-unused-matches but this is a pretty awful addition to this warning as it stands. -Edward On Mon, Jan 11, 2016 at 2:12 PM, Henning Thielemann < lemm...@henning-thielemann.de> wrote: > > On Mon, 11 Jan 2016, Richard Eisenberg wrote: > > On Jan 9, 2016, at 6:44 PM, Henning Thielemann < >> lemm...@henning-thielemann.de> wrote: >> >>> >>> instance (Natural n) => Num.Integer (Un n) where >>>type Repr (Un _n) = Unary >>> >>> >>> GHC-7.6.3 and GHC-7.4.2 complain: >>>Type indexes must match class instance head >>>Found `Un _n' but expected `Un n' >>>In the type synonym instance declaration for `Num.Repr' >>>In the instance declaration for `Num.Integer (Un n)' >>> >>> >>> GHC-7.8.4, GHC-7.10.3 and GHC-8.0 are happy with the difference. >>> >> >> I'm surprised this is accepted at all. Looks like hogwash to me. I think >> you should post a bug report. >> > > Ok, but then GHC must not warn about the unused argument of Repr. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Arithmetic overflow in rem and mod
We went round and round on this back in August. The ultimate decision was to leave the existing behavior for quot and div as sufficient consensus for changing it was not reached. I've updated the ticket in question to reflect that resolution. -Edward On Mon, Jun 1, 2015 at 6:40 PM, Nikita Karetnikov wrote: > According to the documentation, rem and mod must satisfy the following > laws: > > -- > (x `quot` y)*y + (x `rem` y) == x > rem > > -- > (x `div` y)*y + (x `mod` y) == x > mod > > https://hackage.haskell.org/package/base-4.8.0.0/docs/src/GHC-Real.html > > Note, however, that there is a case when quot and div result in an > arithmetic overflow: > > Prelude> (minBound :: Int) `quot` (-1) > *** Exception: arithmetic overflow > Prelude> (minBound :: Int) `div` (-1) > *** Exception: arithmetic overflow > > while rem and mod don't: > > Prelude> (minBound :: Int) `rem` (-1) > 0 > Prelude> (minBound :: Int) `mod` (-1) > 0 > > Is this a mistake? > > For the record, I'm aware of the safeint package, which raises the error > for rem and mod, and this ticket: > > https://ghc.haskell.org/trac/ghc/ticket/8695 > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: -Wall and the fail method
It probably doesn't belong in -Wall, as it is a fairly common idiom to use fail intentionally this way, but it could pretty easily be added to the 'do' and list/monad comprehension desugaring to issue a separate warning that we don't turn on by default. Making it possible to see where you use 'fail' explicitly might be a nice step on the road towards splitting out MonadFail though. Herbert has been working up a plan we can put forth to the community for how to proceed on that front. It may make sense to roll any such warnings into that effort. -Edward On Fri, May 22, 2015 at 8:06 PM, Nikita Karetnikov wrote: > Can -Wall be extended to report pattern match failures in do > expressions, like it does for case expressions? > > Prelude> :set -Wall > Prelude> let f = do Just x <- return Nothing; return x > Prelude> let g = case Nothing of Just x -> x > > :9:9: Warning: > Pattern match(es) are non-exhaustive > In a case alternative: Patterns not matched: Nothing > > One can argue that it's similar to undefined, error, and various > unsafeSomething functions, which I think should be reported as well, if > possible. But these things can be found already with a simple grep > while a pattern match cannot. > > I bet it has been discussed already, but "fail" is a terrible search > term, so I cannot find anything relevant in the archives nor in the bug > tracker. > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Qualified names in TH?
Using {-# LANGUAGE TemplateHaskell #-} you can use 'foo and ''Foo to get
access to the names in scope in the module that is building the splice,
rather than worrying about what names are in scope in the module the code
gets spliced into.
-Edward
On Mon, Mar 16, 2015 at 10:54 PM, J. Garrett Morris wrote:
> I'm trying to write some Template Haskell code that (among other
> things) manipulates IntSets. So, for example, I'd like a splice to
> generate a call to Data.IntSet.fromList. However, I'm not sure how
> IntSet will be imported in the target module. Is there a way to
> resolve the fully qualified name (or similar) to a TH Name, without
> having to know how it's imported in the splicing module? (The obvious
> approach---mkName "Data.IntSet.fromList"---seems not to work in GHC
> 7.8.)
>
> Thanks!
>
> /g
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: GHC 7.10 regression when using foldr
I was assuming that the list was generated by doing more or less the same check we do now. I haven't looked at the code for it. If so, then it seems it wouldn't flag a now-unnecessary Data.Traversable dependency for instance. At least not without rather significant retooling. I might be off in my understanding of how it works, though. -Edward On Tue, Jan 20, 2015 at 7:40 PM, Edward Z. Yang wrote: > I don't see why that would be the case: we haven't *excluded* any > old import lists, so -ddump-minimal-imports could still > take advantage of Prelude in a warning-free way. > > Edward > > Excerpts from Edward Kmett's message of 2015-01-20 16:36:53 -0800: > > It isn't without a cost. On the down-side, the results of > > -ddump-minimal-imports would be er.. less minimal. > > > > On Tue, Jan 20, 2015 at 6:47 PM, Edward Z. Yang wrote: > > > > > I like this proposal: if you're explicit about an import that > > > would otherwise be implicit by Prelude, you shouldn't get a > > > warning for it. If it is not already the case, we also need to > > > make sure the implicit Prelude import never causes "unused import" > > > errors. > > > > > > Edward > > > > > > Excerpts from Edward Kmett's message of 2015-01-20 15:41:13 -0800: > > > > Sure. > > > > > > > > Adding it to the CHANGELOG makes a lot of sense. I first found out > about > > > it > > > > only a few weeks ago when Herbert mentioned it in passing. > > > > > > > > Of course, the geek in me definitely prefers technical fixes to human > > > ones. > > > > Humans are messy. =) > > > > > > > > I'd be curious how much of the current suite of warnings could be > fixed > > > > just by switching the implicit Prelude import to the end of the > import > > > list > > > > inside GHC. > > > > > > > > Now that Herbert has all of his crazy tooling to build stuff with > 7.10 > > > and > > > > with HEAD, it might be worth trying out such a change to see how > much it > > > > reduces the warning volume and if it somehow manages to introduce > any new > > > > warnings. > > > > > > > > I hesitate to make such a proposal this late in the release candidate > > > game, > > > > but if it worked it'd be pretty damn compelling. > > > > > > > > -Edward > > > > > > > > On Tue, Jan 20, 2015 at 6:27 PM, Edward Z. Yang > wrote: > > > > > > > > > Hello Edward, > > > > > > > > > > Shouldn't we publicize this trick? Perhaps in the changelog? > > > > > > > > > > Edward > > > > > > > > > > Excerpts from Edward Kmett's message of 2015-01-20 15:22:57 -0800: > > > > > > Building -Wall clean across this change-over has a big of a > trick to > > > it. > > > > > > > > > > > > The easiest way I know of when folks already had lots of > > > > > > > > > > > > import Data.Foldable > > > > > > import Data.Traversable > > > > > > > > > > > > stuff > > > > > > > > > > > > is to just add > > > > > > > > > > > > import Prelude > > > > > > > > > > > > explicitly to the bottom of your import list rather than > > > painstakingly > > > > > > exclude the imports with CPP. > > > > > > > > > > > > This has the benefit of not needing a bunch of CPP to manage what > > > names > > > > > > come from where. > > > > > > > > > > > > Why? GHC checks that the imports provide something 'new' that is > > > used by > > > > > > the module in a top-down fashion, and you are almost suredly > using > > > > > > something from Prelude that didn't come from one of the modules > > > above. > > > > > > > > > > > > On the other hand the implicit import of Prelude effectively > would > > > come > > > > > > first in the list. > > > > > > > > > > > > It is a dirty trick, but it does neatly side-step this problem > for > > > folks > > > > > in > > > > > > your situation. > > > > > > > > > > > > -Edward > > > > > > > > > > > > On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan < > > > b...@serpentine.com> > > > > > > wrote: > > > > > > > > > > > > > > > > > > > > On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel < > > > h...@gnu.org> > > > > > > > wrote: > > > > > > > > > > > > > >> I'm a bit confused, several past attoparsec versions seem to > build > > > > > just > > > > > > >> fine with GHC 7.10: > > > > > > >> > > > > > > >> https://ghc.haskell.org/~hvr/buildreports/attoparsec.html > > > > > > >> > > > > > > >> were there hidden breakages not resulting in compile errors? > > > > > > >> Or are the fixes you mention about restoring -Wall hygiene? > > > > > > >> > > > > > > > > > > > > > > I build with -Wall -Werror, and also have to maintain the test > and > > > > > > > benchmark suites. > > > > > > > > > > > > > > > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHC 7.10 regression when using foldr
It isn't without a cost. On the down-side, the results of -ddump-minimal-imports would be er.. less minimal. On Tue, Jan 20, 2015 at 6:47 PM, Edward Z. Yang wrote: > I like this proposal: if you're explicit about an import that > would otherwise be implicit by Prelude, you shouldn't get a > warning for it. If it is not already the case, we also need to > make sure the implicit Prelude import never causes "unused import" > errors. > > Edward > > Excerpts from Edward Kmett's message of 2015-01-20 15:41:13 -0800: > > Sure. > > > > Adding it to the CHANGELOG makes a lot of sense. I first found out about > it > > only a few weeks ago when Herbert mentioned it in passing. > > > > Of course, the geek in me definitely prefers technical fixes to human > ones. > > Humans are messy. =) > > > > I'd be curious how much of the current suite of warnings could be fixed > > just by switching the implicit Prelude import to the end of the import > list > > inside GHC. > > > > Now that Herbert has all of his crazy tooling to build stuff with 7.10 > and > > with HEAD, it might be worth trying out such a change to see how much it > > reduces the warning volume and if it somehow manages to introduce any new > > warnings. > > > > I hesitate to make such a proposal this late in the release candidate > game, > > but if it worked it'd be pretty damn compelling. > > > > -Edward > > > > On Tue, Jan 20, 2015 at 6:27 PM, Edward Z. Yang wrote: > > > > > Hello Edward, > > > > > > Shouldn't we publicize this trick? Perhaps in the changelog? > > > > > > Edward > > > > > > Excerpts from Edward Kmett's message of 2015-01-20 15:22:57 -0800: > > > > Building -Wall clean across this change-over has a big of a trick to > it. > > > > > > > > The easiest way I know of when folks already had lots of > > > > > > > > import Data.Foldable > > > > import Data.Traversable > > > > > > > > stuff > > > > > > > > is to just add > > > > > > > > import Prelude > > > > > > > > explicitly to the bottom of your import list rather than > painstakingly > > > > exclude the imports with CPP. > > > > > > > > This has the benefit of not needing a bunch of CPP to manage what > names > > > > come from where. > > > > > > > > Why? GHC checks that the imports provide something 'new' that is > used by > > > > the module in a top-down fashion, and you are almost suredly using > > > > something from Prelude that didn't come from one of the modules > above. > > > > > > > > On the other hand the implicit import of Prelude effectively would > come > > > > first in the list. > > > > > > > > It is a dirty trick, but it does neatly side-step this problem for > folks > > > in > > > > your situation. > > > > > > > > -Edward > > > > > > > > On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan < > b...@serpentine.com> > > > > wrote: > > > > > > > > > > > > > > On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel < > h...@gnu.org> > > > > > wrote: > > > > > > > > > >> I'm a bit confused, several past attoparsec versions seem to build > > > just > > > > >> fine with GHC 7.10: > > > > >> > > > > >> https://ghc.haskell.org/~hvr/buildreports/attoparsec.html > > > > >> > > > > >> were there hidden breakages not resulting in compile errors? > > > > >> Or are the fixes you mention about restoring -Wall hygiene? > > > > >> > > > > > > > > > > I build with -Wall -Werror, and also have to maintain the test and > > > > > benchmark suites. > > > > > > > > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: "Found hole"
FWIW- you can think of a 'hole' as a "not in scope" error with a ton of useful information about the type such a term would have to have in order to go in the location you referenced it. This promotes a very useful style of type-driven development that is common in Agda, where you write out your program and then leave holes that start with _'s to fill in later. Since no new programs are accepted or rejected, GHC turned on "holes" support by default. Users have historically faked this style with ImplicitParams by labeling their holes ?foo, but that approach doesn't give any information on what local stuff could be used to plug the hole. The only thing that changed is the nature of the error message, which carefully track what variables are in scope, how they are instantiated, and what type the missing term is used at. Since libraries like lens were already making heavy use of the _'d namespace this only happens if the name isn't already in use. This is why you can define _'d things just fine. The main thing that happened is if you typo the name of a lens, well, your error messages got even worse. ;) -Edward On Tue, Jan 20, 2015 at 1:36 PM, Volker Wysk wrote: > Hello! > > What is a "hole"? > > This program fails to compile: > > main = _exit 0 > > I get this error message: > > ex.hs:1:8: > Found hole ‘_exit’ with type: t > Where: ‘t’ is a rigid type variable bound by >the inferred type of main :: t at ex.hs:1:1 > Relevant bindings include main :: t (bound at ex.hs:1:1) > In the expression: _exit > In an equation for ‘main’: main = _exit > > When I replace "_exit" with "foo", it produces a "not in scope" error, as > expected. What is special about "_exit"? It doesn't occur in the Haskell > Hierarchical Libraries. > > Bye > Volker > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHC 7.10 regression when using foldr
Sure. Adding it to the CHANGELOG makes a lot of sense. I first found out about it only a few weeks ago when Herbert mentioned it in passing. Of course, the geek in me definitely prefers technical fixes to human ones. Humans are messy. =) I'd be curious how much of the current suite of warnings could be fixed just by switching the implicit Prelude import to the end of the import list inside GHC. Now that Herbert has all of his crazy tooling to build stuff with 7.10 and with HEAD, it might be worth trying out such a change to see how much it reduces the warning volume and if it somehow manages to introduce any new warnings. I hesitate to make such a proposal this late in the release candidate game, but if it worked it'd be pretty damn compelling. -Edward On Tue, Jan 20, 2015 at 6:27 PM, Edward Z. Yang wrote: > Hello Edward, > > Shouldn't we publicize this trick? Perhaps in the changelog? > > Edward > > Excerpts from Edward Kmett's message of 2015-01-20 15:22:57 -0800: > > Building -Wall clean across this change-over has a big of a trick to it. > > > > The easiest way I know of when folks already had lots of > > > > import Data.Foldable > > import Data.Traversable > > > > stuff > > > > is to just add > > > > import Prelude > > > > explicitly to the bottom of your import list rather than painstakingly > > exclude the imports with CPP. > > > > This has the benefit of not needing a bunch of CPP to manage what names > > come from where. > > > > Why? GHC checks that the imports provide something 'new' that is used by > > the module in a top-down fashion, and you are almost suredly using > > something from Prelude that didn't come from one of the modules above. > > > > On the other hand the implicit import of Prelude effectively would come > > first in the list. > > > > It is a dirty trick, but it does neatly side-step this problem for folks > in > > your situation. > > > > -Edward > > > > On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan > > wrote: > > > > > > > > On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel > > > wrote: > > > > > >> I'm a bit confused, several past attoparsec versions seem to build > just > > >> fine with GHC 7.10: > > >> > > >> https://ghc.haskell.org/~hvr/buildreports/attoparsec.html > > >> > > >> were there hidden breakages not resulting in compile errors? > > >> Or are the fixes you mention about restoring -Wall hygiene? > > >> > > > > > > I build with -Wall -Werror, and also have to maintain the test and > > > benchmark suites. > > > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHC 7.10 regression when using foldr
Building -Wall clean across this change-over has a big of a trick to it. The easiest way I know of when folks already had lots of import Data.Foldable import Data.Traversable stuff is to just add import Prelude explicitly to the bottom of your import list rather than painstakingly exclude the imports with CPP. This has the benefit of not needing a bunch of CPP to manage what names come from where. Why? GHC checks that the imports provide something 'new' that is used by the module in a top-down fashion, and you are almost suredly using something from Prelude that didn't come from one of the modules above. On the other hand the implicit import of Prelude effectively would come first in the list. It is a dirty trick, but it does neatly side-step this problem for folks in your situation. -Edward On Tue, Jan 20, 2015 at 6:12 PM, Bryan O'Sullivan wrote: > > On Tue, Jan 20, 2015 at 3:02 PM, Herbert Valerio Riedel > wrote: > >> I'm a bit confused, several past attoparsec versions seem to build just >> fine with GHC 7.10: >> >> https://ghc.haskell.org/~hvr/buildreports/attoparsec.html >> >> were there hidden breakages not resulting in compile errors? >> Or are the fixes you mention about restoring -Wall hygiene? >> > > I build with -Wall -Werror, and also have to maintain the test and > benchmark suites. > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHC 7.10 regression when using foldr
On Tue, Jan 20, 2015 at 9:00 AM, Kim-Ee Yeoh wrote: > > There are few reports because the change hasn't affected the dark majority > yet. RC builds are used by a tiny fraction. There's a long tail of users > still on 7.6, 7.4, 7.2, and 6.x. > We've been actively testing since the first time we had a usable implementation of both the Foldable/Traversable proposal and AMP. Very large chunks of hackage have been built in house with hand-patched upstreams to maximize how much of it we can build and we've been using that to try to minimize impact. Herbert has been hard at work on this for six months now. It was known going in that there'd be some broken eggs, and that there'd be a large number of details to figure out, so Simon formed the core libraries committee in part to have someone responsible for making decisions around situations like this. Far and away the greatest contributing factor to build failures in 7.10 is the AMP. More code is broken by the import of (<*>) in Applicative alone. As in, going into the same release, the Foldable/Traversable changes barely blip the build-failure radar, by a factor of 50 compared to AMP-induced failures. The whack-a-mole game needs only to be played once and the results shared > among those relying on the abstractions. Was that route ever explored? > Yes. You could say that this is precisely what we've been doing since 2008. We've had a dozen or so alternate preludes. Nobody wants the extra build dependency or per module setup cost. We've had a proposal to eliminate the Prelude entirely by Igloo, to make it so if you import Prelude.Foo you'd get that Prelude and not the other. I also spent much of 2014 going around to every Haskell meetup I could make it to around the world looking for more direct feedback from folks. The list goes on of options that have been put on the table. It does nothing to stem the tide of users who reinvent these abstractions, or who by dint of the undiscoverability of the current API never find out about it. The classy-prelude for instance when it was first released didn't know that there was any pre-existing relationship between virtually all the combinators it offered and split things up into dozens of classes. A separate Prelude doesn't address the fact that the limited versions of these functions are re-exported over and over across dozens of other modules within base and without. To that end we had a proposal. It had the most feedback of any proposal ever put forth on the libraries mailing list, but it went through with something like 90% approval. I'm not one to speak of "mandates from the people", but if anything ever came close, that sounds like one to me. The FTP discussion needs to be re-opened. And it will be, eventually. > That statement needs some seriously sinister music. ;) -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GHC 7.10 regression when using foldr
There is a limited set of situations where the new signatures can fail to infer, where it would infer before. This can happen when you construct a Foldable/Traversable value using polymorphic tools (like Read) that were previously instantiated for list, but where since foldr et al. are now polymorphic, this doesn't give enough information for it to know that [] is the instance you wanted. Ultimately, there is, of course, a balancing act between flexibility and inference. I can at least say that the incident rate for cases seems to be very low, especially when it is contrasted against the pain users have had with using the existing Foldable/Traversable imports where virtually everything in them collided with less useful versions of the same combinator (e.g. mapM) from the Prelude that a dozen other modules (e.g. Control.Monad and virtually every module in mtl) insisted on re-exporting, making it a game of whack-a-mole to try to hide them. The fix here is to supply a manual type signature on the helper. -Edward On Tue, Jan 20, 2015 at 6:20 AM, Björn Peemöller wrote: > I just discovered that the following program compiled fine using GHC > 7.8.4 but was rejected by GHC 7.10.1-rc1: > > ~~~ > data List a = Nil | Cons a (List a) > > instance Read a => Read (List a) where > readsPrec d s = map convert (readsPrec d s) > where > convert (xs, s2) = (foldr Cons Nil xs, s2) > ~~~ > > GHC 7.10 now complains: > > ~~~ > Read.hs:5:23: > Could not deduce (Foldable t0) arising from a use of ‘convert’ > from the context (Read a) > bound by the instance declaration at Read.hs:4:10-32 > The type variable ‘t0’ is ambiguous > Note: there are several potential instances: > instance Foldable (Either a) -- Defined in ‘Data.Foldable’ > instance Foldable Data.Proxy.Proxy -- Defined in ‘Data.Foldable’ > instance GHC.Arr.Ix i => Foldable (GHC.Arr.Array i) > -- Defined in ‘Data.Foldable’ > ...plus three others > In the first argument of ‘map’, namely ‘convert’ > In the expression: map convert (readsPrec d s) > In an equation for ‘readsPrec’: > readsPrec d s > = map convert (readsPrec d s) > where > convert (xs, s2) = (foldr Cons Nil xs, s2) > > Read.hs:5:32: > Could not deduce (Read (t0 a)) arising from a use of ‘readsPrec’ > from the context (Read a) > bound by the instance declaration at Read.hs:4:10-32 > The type variable ‘t0’ is ambiguous > Relevant bindings include > readsPrec :: Int -> ReadS (List a) (bound at Read.hs:5:3) > Note: there are several potential instances: > instance (Read a, Read b) => Read (Either a b) > -- Defined in ‘Data.Either’ > instance forall (k :: BOX) (s :: k). Read (Data.Proxy.Proxy s) > -- Defined in ‘Data.Proxy’ > instance (GHC.Arr.Ix a, Read a, Read b) => Read (GHC.Arr.Array a b) > -- Defined in ‘GHC.Read’ > ...plus 18 others > In the second argument of ‘map’, namely ‘(readsPrec d s)’ > In the expression: map convert (readsPrec d s) > In an equation for ‘readsPrec’: > readsPrec d s > = map convert (readsPrec d s) > where > convert (xs, s2) = (foldr Cons Nil xs, s2) > ~~~ > > The reason is the usage of foldr, which changed its type from > > foldr :: (a -> b -> b) -> b -> [a] -> b -- GHC 7.8.4 > > to > > foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b -- GHC 7.10.1 > > Thus, the use of foldr is now ambiguous. I can fix this by providing a > type signature > > convert :: ([a], String) -> (List a, String) > > However, is this breaking change intended? > > Regards, > Björn > > > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Equality Constraints (a ~ b)
They were introduced as part of the System Fc rewrite. The Fc approach has the benefit of unifying a lot of the work on GADTs, functional dependencies, type and data families, etc. all behind the scenes. Every once in a while, (~) constraints can leak into the surface language and it can be useful to be able to talk about them in the surface language of Haskell, because otherwise it isn't clear how to talk about F a ~ G b style constraints, which arise in practice when you work with type families. -Edward On Sun, Jan 11, 2015 at 6:04 PM, Dominic Steinitz wrote: > Hi, > > I am trying to find more background on these. They don’t exist in the > Haskell 2010 Language Report, they didn’t exist in ghc 6.8.2 but make an > appearance in 7.0.1. The documentation in the manual is rather sparse and > doesn’t contain a reference: > https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf section > 7.11. Folk on #ghc referred me to > http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/. I > can find papers that refer to ~ in F_C (aka FC?) but as far as I can tell > not in the Haskell language itself. > > Many thanks > > Dominic Steinitz > domi...@steinitz.org > http://idontgetoutmuch.wordpress.com > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Permitting trailing commas for record syntax ADT declarations
Not a concrete suggestion, but just a related data point / nod to the sanity of the suggestion: I'm not sure I'd remove them entirely either, but FWIW, we don't require commas in fixity declarations in Ermine and it works well. On the other hand, our import lists are rather more complicated than Haskell's due to a need for extensive renaming on import though, so we don't shed the commas, but wind up using layout-based separation there, instead, avoiding conflicts by another means. That ship, however, has sailed for Haskell. ;) -Edward On Mon, Sep 29, 2014 at 9:27 AM, Richard Eisenberg wrote: > To be fair, I'm not sure I like the make-commas-optional approach either. > But, the solution occurred to me as possible, so I thought it was worth > considering as we're exploring the design space. > > And, yes, I was suggesting only to make them optional, not to require > everyone remove them. > > Richard > > On Sep 26, 2014, at 5:34 PM, Brandon Allbery wrote: > > On Fri, Sep 26, 2014 at 5:21 PM, Johan Tibell > wrote: > >> I don't think that's necessarily is good style. I don't think we want two >> different ways of doing import lists. > > > Yes; I kinda hate the idea myself, it encourages an unreadable programming > style. But it's not the wholesale breaking change you were suggesting, > either. > > -- > brandon s allbery kf8nh sine nomine > associates > allber...@gmail.com > ballb...@sinenomine.net > unix, openafs, kerberos, infrastructure, xmonad > http://sinenomine.net > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Old code broken by new Typeable class
If you can't change the definition you can use the syntax Björn Bringert
added back in 2006 or so for StandaloneDeriving.
Just turn on
{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable #-}
and then you can use
deriving instance Typeable Foo
-Edward
On Tue, Aug 5, 2014 at 1:47 PM, Volker Wysk
wrote:
> Am Dienstag, 5. August 2014, 12:46:23 schrieb Carter Schonwald:
> > i assume 7.6 and 7.8, if we're talking GHC rather than GCC :)
> >
> > in 7.8 you can't define userland typeable instances, you need only write
> > deriving (Typeable) and you're all set.
> > add some CPP to select the instances suitable
>
> So you need to be able to change the definition of the data type, in order
> to
> add deriving (Typeable). It's not possible to add a Typeable instance
> declaration later.
>
> When you can't change the definition, you're out of luck.
>
> Okay,
> V.W.
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Overlapping and incoherent instances
Now if only we could somehow find a way to do the same thing for
AllowAmbiguousTypes. :)
I have a 2500 line file that I'm forced to turn on AllowAmbiguousTypes in
for 3 definitions, and checking that I didn't accidentally make something
else ambiguous to GHC's eyes is a rather brutal affair. (I can't break up
the file without inducing orphans)
This is just a passing comment, while I'm thinking about it, not a serious
attempt to derail the topic!
-Edward
On Thu, Jul 31, 2014 at 4:13 AM, Simon Peyton Jones
wrote:
> Andreas, remember that GHC 7.8 already implements (essentially) the same
> algorithm. The difference is that 7.8 offers only the brutal
> -XOverlappingInstances to control it. In your example of the decision you
> make when writing
>instance Bla a => Bla [a]
> vs
>instance {-# OVERLAPPABLE #-} Bla a => Bla [a]
> you are, with GHC 7.8, making precisely the same decision when you decide
> whether or not to add {-# LANGUAGE OverlappingInstances #-} to that module.
> Perhaps that wasn't clear in what I wrote; apologies.
>
> So your proposal seems to be this
>
> don't remove -XOverlappingInstances, because that will prevent
> programmers from "flipping on/off pragmas until their program
> goes through".
>
> It's hard to argue AGAINST providing the opportunity for more careful
> programmers to express their intentions more precisely, which is what the
> OVERLAP/OVERLAPPABLE pragmas do.
>
> Concerning deprecating OverlappingInstances, my gut feel is that it is
> positively a good thing to guide programmers towards a more robust
> programming style. But my reason for starting this thread was to see
> whether or not others' gut feel is similar.
>
> Simon
>
> | -Original Message-
> | From: Libraries [mailto:libraries-boun...@haskell.org] On Behalf Of
> | Andreas Abel
> | Sent: 31 July 2014 08:59
> | To: Simon Peyton Jones; ghc-devs; GHC users; Haskell Libraries
> | (librar...@haskell.org)
> | Subject: Re: Overlapping and incoherent instances
> |
> | On 31.07.2014 09:20, Simon Peyton Jones wrote:
> | > Friends, in sending my message below, I should also have sent a link
> | > to
> | >
> | > https://ghc.haskell.org/trac/ghc/ticket/9242#comment:25
> |
> | Indeed.
> |
> | Quoting from the spec:
> |
> | * Eliminate any candidate IX for which both of the following hold:
> | * There is another candidate IY that is strictly more specific;
> | that is, IY is a substitution instance of IX but not vice versa.
> |
> | * Either IX is overlappable or IY is overlapping.
> |
> | Mathematically, this makes a lot of sense. But put on the hat of
> | library writers, and users, and users that don't rtfm. Looking out
> | from under this hat, the one may always wonder whether one should make
> | one's generic instances OVERLAPPABLE or not.
> |
> | If I create a library with type class Bla and
> |
> |instance Bla a => Bla [a]
> |
> | I could be a nice library writer and spare my users from declaring
> | their Bla String instances as OVERLAPPING, so I'd write
> |
> |instance {-# OVERLAPPABLE #-} Bla a => Bla [a]
> |
> | Or maybe that would be malicious?
> |
> | I think the current proposal is too sophisticated. There are no
> | convincing examples given in the discussion so far that demonstrate
> | where this sophistication pays off in practice.
> |
> | Keep in mind that 99% of the Haskell users will never study the
> | instance resolution algorithm or its specification, but just flip
> | on/off pragmas until their code goes through. [At least that was my
> | approach: whenever GHC asks for one more LANGUAGE pragma, just throw it
> | in.]
> |
> | Cheers,
> | Andreas
> |
> |
> | > Comment 25 describes the semantics of OVERLAPPING/OVERLAPPABLE etc,
> | > which I signally failed to do in my message below, leading to
> | > confusion in the follow up messages. My apologies for that.
> | >
> | > Some key points:
> | >
> | > *There is a useful distinction between /overlapping/ and
> | > /overlappable/, but if you don't want to be bothered with it you can
> | > just say OVERLAPS (which means both).
> | >
> | > *Overlap between two candidate instances is allowed if /either/ has
> | > the relevant property. This is a bit sloppy, but reduces the
> | > annotation burden. Actually, with this per-instance stuff I think
> | > it'd be perfectly defensible to require both to be annotated, but
> | > that's a different discussion.
> | >
> | > I hope that helps clarify.
> | >
> | > I'm really pretty certain that the basic proposal here is good: it
> | > implements the current semantics in a more fine-grained manner. My
> | > main motivation was to signal the proposed deprecation of the global
> | > per-module flag -XoverlappingInstances. Happily people generally
> | seem
> | > fine with this. It is, after all, precisely what deprecations are
> | for
> | > ("the old thing still works for now, but it won't do so for ever, and
> | > you should change as soon as is conv
Re: Why no `instance (Monoid a, Applicative f)=> Monoid (f a)` for IO?
There are monads for which you want another Monoid, e.g. Maybe provides a different unit, because it pretends to lift a Semigroup into a Monoid. There are also monoids that take a parameter of kind * that would overlap with this instance. So we can't (and shouldn't) have the global Monoid instance like you give there first. As for the particular case of IO a, lifting may be a reasonable option there. A case could be made for adding an `instance Monoid a => Monoid (IO a)`, but for such a ubiquitously used type, expect that this wouldn't be an easy sell. You'd possibly have to deal with everyone and their brother coming out of the woodwork offering up every other Monoid they happened to use on IO. Why? IO provides a notion of failing action you could use for zero and you can build an (<|>) like construction on it as well, so the 'multiplicative' structure isn't the _only_ option for your monoid. Even within the multiplicative structure using the monoid isn't necessarily ideal as you might leak more memory with an IO a monoid that lifts () than you would with working specifically on IO (). You can argue the case that the choice you made is a sensible default instance by instance, but when there isn't a real canonical choice we do tend to err on the side of leaving things open as orphans are at least possible, but once the choice is made it is very very hard to unmake. I say this mostly so you know the kinds of objections proposals like this usually see, not to flat out reject the idea of the particular case of this instance for IO. I will say the global 'instance (Applicative f, Monoid m) => Monoid (f m)' won't fly for overlap reasons though. -Edward On Mon, Jul 14, 2014 at 6:55 PM, Brandon Simmons < brandon.m.simm...@gmail.com> wrote: > It seems to me that this should be true for all `f a` like: > > instance (Monoid a, Applicative f)=> Monoid (f a) where > mappend = liftA2 mappend > mempty = pure mempty > > But I can't seem to find the particular `instance (Monoid a)=> Monoid > (IO a)` anywhere. Would that instance be incorrect, or does it live > somewhere else? > > FWIW I noticed this when I started thinking about an instance I wanted > for 'contravariant': > > instance (Monoid a, Applicative f)=> Monoid (Op (f a) b) where > mempty = Op $ const $ pure mempty > mappend (Op f) (Op g) = Op (\b-> liftA2 mappend (f b) (g b)) > > at which point I realized (I think) all `f a` are monoidal, and so we > ought to be able to get the instance above with just a deriving > Monoid. > > Brandon > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Monomorphizing GHC Core?
I think the first time I saw a connection to polymorphic recursion was in Neil Mitchell's supero, which used it as a catch-all fallback plan. http://community.haskell.org/~ndm/downloads/slides-haskell_with_go_faster_stripes-30_nov_2006.pdf -Edward On Thu, Jun 19, 2014 at 4:49 PM, Conal Elliott wrote: > Thanks, Ed. It hadn't occurred to me that defunctionalization might be > useful for monomorphization. Do you know of a connection? > > I'm using a perfect leaf tree type similar to the one you mentioned but > indexed by depth: > > > data Tree :: (* -> *) -> Nat -> * -> * where > > L :: a -> Tree k 0 a > > B :: Tree k n (k a) -> Tree k (1+n) a > > Similarly for "top-down" perfect leaf trees: > > > data Tree :: (* -> *) -> Nat -> * -> * where > > L :: a -> Tree k 0 a > > B :: k (Tree k n a) -> Tree k (1+n) a > > This way, after monomorphization, there won't be any sums remaining. > > -- Conal > > > > On Thu, Jun 19, 2014 at 1:22 PM, Edward Kmett wrote: > >> Might you have more success with a Reynolds style defunctionalization >> pass for the polymorphic recursion you can't eliminate? >> >> Then you wouldn't have to rule out things like >> >> data Complete a = S (Complete (a,a)) | Z a >> >> which don't pass that test. >> >> -Edward >> >> >> On Thu, Jun 19, 2014 at 3:28 PM, Conal Elliott wrote: >> >>> Has anyone worked on a monomorphizing transformation for GHC Core? I >>> understand that polymorphic recursion presents a challenge, and I do indeed >>> want to work with polymorphic recursion but only on types for which the >>> recursion bottoms out statically (i.e., each recursive call is on a smaller >>> type). I'm aiming at writing high-level polymorphic code and generating >>> monomorphic code on unboxed values. This work is part of a project for >>> compiling Haskell to hardware, described on my blog (http://conal.net). >>> >>> Thanks, - Conal >>> >>> ___ >>> Glasgow-haskell-users mailing list >>> Glasgow-haskell-users@haskell.org >>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>> >>> >> > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Monomorphizing GHC Core?
Might you have more success with a Reynolds style defunctionalization pass for the polymorphic recursion you can't eliminate? Then you wouldn't have to rule out things like data Complete a = S (Complete (a,a)) | Z a which don't pass that test. -Edward On Thu, Jun 19, 2014 at 3:28 PM, Conal Elliott wrote: > Has anyone worked on a monomorphizing transformation for GHC Core? I > understand that polymorphic recursion presents a challenge, and I do indeed > want to work with polymorphic recursion but only on types for which the > recursion bottoms out statically (i.e., each recursive call is on a smaller > type). I'm aiming at writing high-level polymorphic code and generating > monomorphic code on unboxed values. This work is part of a project for > compiling Haskell to hardware, described on my blog (http://conal.net). > > Thanks, - Conal > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [core libraries] Re: Tightening up on inferred type signatures
Er.. my mistake. Control.Applicative. That is what it is we don't re-export that is used in Traversal. =) On Wed, Apr 30, 2014 at 2:47 AM, Edward Kmett wrote: > Not sure. > > An even simpler case is something like exporting a Traversal but not > exporting Data.Traversable, which appears in the expansion, etc. > > These sorts of things happen in code using lens. Older versions of lens > didn't export all of the types needed to write out the type signature long > hand without extra imports, just to avoid cluttering the namespace. > > -Edward > > > On Wed, Apr 30, 2014 at 2:10 AM, Ganesh Sittampalam wrote: > >> On 23/04/2014 20:04, dm-list-haskell-librar...@scs.stanford.edu wrote: >> > Edward Kmett writes: >> > >> >> You can wind up in perfectly legitimate situations where the name for >> the >> >> type you are working with isn't in scope, but where you can write a >> >> combinator that would infer to have that type. I'd hate to lose that. >> >> >> >> It is admittedly of marginal utility at first glance, but there are >> some >> >> tricks that actually need it, and it can also arise if a type synonym >> >> expands to a type that isn't exported or brought into scope, so trying >> to >> >> push this line of reasoning too far I is possibly not too productive. >> > >> > Good point. In particular, it's not weird at all want to export type >> > synonyms on their own, particularly where ghost type parameters are used >> > to select between only a few cases. Consider something like this >> > (inspired by postgresql-orm): >> >> Is there an abstraction being protected by only exporting the type >> synonym in cases like this? >> >> Cheers, >> >> Ganesh >> > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [core libraries] Re: Tightening up on inferred type signatures
Not sure. An even simpler case is something like exporting a Traversal but not exporting Data.Traversable, which appears in the expansion, etc. These sorts of things happen in code using lens. Older versions of lens didn't export all of the types needed to write out the type signature long hand without extra imports, just to avoid cluttering the namespace. -Edward On Wed, Apr 30, 2014 at 2:10 AM, Ganesh Sittampalam wrote: > On 23/04/2014 20:04, dm-list-haskell-librar...@scs.stanford.edu wrote: > > Edward Kmett writes: > > > >> You can wind up in perfectly legitimate situations where the name for > the > >> type you are working with isn't in scope, but where you can write a > >> combinator that would infer to have that type. I'd hate to lose that. > >> > >> It is admittedly of marginal utility at first glance, but there are some > >> tricks that actually need it, and it can also arise if a type synonym > >> expands to a type that isn't exported or brought into scope, so trying > to > >> push this line of reasoning too far I is possibly not too productive. > > > > Good point. In particular, it's not weird at all want to export type > > synonyms on their own, particularly where ghost type parameters are used > > to select between only a few cases. Consider something like this > > (inspired by postgresql-orm): > > Is there an abstraction being protected by only exporting the type > synonym in cases like this? > > Cheers, > > Ganesh > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: RFC: changes to -i flag for finding source files
You can actually make symbolic links (as well as hard links and "directory junctions") on windows. -Edward > On Apr 25, 2014, at 12:51 PM, Roman Cheplyaka wrote: > > * Felipe Lessa [2014-04-25 13:01:43-0300] >> Em 25-04-2014 12:22, Edward Kmett escreveu: >>> +1 from me. I have a lot of projects that suffer with 4 levels of vacuous >>> subdirectories just for this. >>> >>> In theory cabal could support this on older GHC versions by copying all of >>> the files to a working dir in dist with the expected layout on older GHCs. >>> >>> That would enable this to get much greater penetration more quickly. >> >> What if you had a "real-src" directory with all your files as they are >> now, and a "src" symlink pointing inside your directory tree? > > I don't think Windows users can enjoy this, but it's a neat idea. > > Roman > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: RFC: changes to -i flag for finding source files
I check out and work on projects on a bunch of machines, so it is important that I can just pull with git and go. AFAIK, git doesn't understand them won't build symlinks for me, so it'd just become another setup step for very marginal benefit, and another thing to .gitignore. -Edward > On Apr 25, 2014, at 12:01 PM, Felipe Lessa wrote: > > Em 25-04-2014 12:22, Edward Kmett escreveu: >> +1 from me. I have a lot of projects that suffer with 4 levels of vacuous >> subdirectories just for this. >> >> In theory cabal could support this on older GHC versions by copying all of >> the files to a working dir in dist with the expected layout on older GHCs. >> >> That would enable this to get much greater penetration more quickly. > > What if you had a "real-src" directory with all your files as they are > now, and a "src" symlink pointing inside your directory tree? > > Cheers, > > -- > Felipe. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: RFC: changes to -i flag for finding source files
+1 from me. I have a lot of projects that suffer with 4 levels of vacuous subdirectories just for this. In theory cabal could support this on older GHC versions by copying all of the files to a working dir in dist with the expected layout on older GHCs. That would enable this to get much greater penetration more quickly. -Edward > On Apr 25, 2014, at 9:17 AM, Simon Marlow wrote: > > I want to propose a simple change to the -i flag for finding source files. > The problem we often have is that when you're writing code for a library that > lives deep in the module hierarchy, you end up needing a deep directory > structure, e.g. > > src/ > Graphics/ > UI/ > Gtk/ >Button.hs >Label.h >... > > where the top few layers are all empty. There have been proposals of > elaborate solutions for this in the past (module grafting etc.), but I want > to propose something really simple that would avoid this problem with minimal > additional complexity: > > ghc -iGraphics.UI.Gtk=src > > the meaning of this flag is that when searching for modules, ghc will look > for the module Graphics.UI.Gtk.Button in src/Button.hs, rather than > src/Graphics/UI/Gtk/Button.hs. The source file itself is unchanged: it still > begins with "module Graphics.UI.Gtk.Button ...". > > The implementation is only a few lines in the Finder (and probably rather > more in the manual and testsuite), but I wanted to get a sense of whether > people thought this would be a good idea, or if there's a better alternative > before I push it. > > Pros: > > - simple implementation (but Cabal needs mods, see below) > - solves the deep directory problem > > Cons: > > - It makes the rules about finding files a bit more complicated. >People need to find source files too, not just compilers. > - packages that want to be compatible with older compilers can't >use it yet. > - you can't use '=' in a source directory name (but we could pick >a different syntax if necessary) > - It won't work for Cabal packages until Cabal is modified to >support it (PreProcess and SrcDist and perhaps Haddock are the only >places affected, I think) > - Hackage will need to reject packages that use this feature without >also specifying ghc >= 7.10 and some cabal-version too. > - Are there other tools/libraries that will need changes? Leksah? > > Cheers, > Simon > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [core libraries] Re: Tightening up on inferred type signatures
You can wind up in perfectly legitimate situations where the name for the type you are working with isn't in scope, but where you can write a combinator that would infer to have that type. I'd hate to lose that. It is admittedly of marginal utility at first glance, but there are some tricks that actually need it, and it can also arise if a type synonym expands to a type that isn't exported or brought into scope, so trying to push this line of reasoning too far I is possibly not too productive. Parts of lens, constraints and probably a few other packages I maintain would break as hard data points. -Edward On Tue, Apr 22, 2014 at 2:44 AM, Simon Peyton Jones wrote: > | Independent of language extensions, what about types and classes whose > | names are not in scope. Is there an implicit "... if you import all > | the relevant symbols" and the end of the rule? > > Good point. I'm honestly unsure how far to push this one! (It'd be > relatively easy to check whether they were in scope and complain if not, > but ...) > > Simon > > | -Original Message- > | From: haskell-core-librar...@googlegroups.com [mailto:haskell-core- > | librar...@googlegroups.com] On Behalf Of David Mazieres > | Sent: 22 April 2014 00:41 > | To: Simon Peyton Jones; Haskell Libraries (librar...@haskell.org); > | core-libraries-commit...@haskell.org; GHC users > | Subject: [core libraries] Re: Tightening up on inferred type signatures > | > | Simon Peyton Jones writes: > | > | > GHC generally obeys this rule > | > > | > * If GHC infers a type f::type, then it's OK for you to add a type > | > signature saying exactly that. > | > | Independent of language extensions, what about types and classes whose > | names are not in scope. Is there an implicit "... if you import all > | the relevant symbols" and the end of the rule? > | > | David > | > | -- > | You received this message because you are subscribed to the Google > | Groups "haskell-core-libraries" group. > | To unsubscribe from this group and stop receiving emails from it, send > | an email to haskell-core-libraries+unsubscr...@googlegroups.com. > | For more options, visit https://groups.google.com/d/optout. > > -- > You received this message because you are subscribed to the Google Groups > "haskell-core-libraries" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to haskell-core-libraries+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [core libraries] Tightening up on inferred type signatures
No objections here. The types involved really *do* have FlexibleContexts in them, so it makes sense to require the extension. The upgrade path for library authors is also clear. It'll complain to add the extension, and they'll fix it by adding the line of code suggested and perhaps realize something about their code in the process. -Edward On Mon, Apr 21, 2014 at 4:30 AM, Simon Peyton Jones wrote: > Friends > > GHC generally obeys this rule > > · If GHC infers a type *f::type*, then it’s OK for you to add a > type signature saying exactly that. > > For example, it rejects inferred types that are ambiguous. I think this > is a good property; it was certainly the source of many bug reports before > inferred ambiguous types were rejected. > > However, up to now (including in 7.8) GHC hasn’t followed this rule > consistently. In particular, it will infer types like > >fold :: (Functor (PF a), Regular a) => (PF a b -> b) -> a -> b > > (where PF is a type family). If you write this as a type signature, GHC > will insist on FlexibleContexts and TypeFamilies. > > So in https://ghc.haskell.org/trac/ghc/ticket/8883, Jan has made GHC > check inferred types in the same way that it checks declared types, thus > rejecting the above inferred type unless you give the language extensions. > > This makes the compiler more consistent. > > But it does mean that some code may be rejected that 7.8 accepts. This > email is just a heads-up that you might want to compile your library with > 7.10 (i.e. a snapshot of HEAD) well in advance. There will be other > breaking changes of course; e.g Applicative will finally be a superclass of > Monad, for example. > > Simon > > > > -- > You received this message because you are subscribed to the Google Groups > "haskell-core-libraries" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to haskell-core-libraries+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] Eta Reduction
Unfortunately the old class based solution also carries other baggage, like the old data type contexts being needed in the language for bang patterns. :( -Edward > On Apr 1, 2014, at 5:26 PM, John Lato wrote: > > Hi Edward, > > Yes, I'm aware of that. However, I thought Dan's proposal especially droll > given that changing seq to a class-based function would be sufficient to make > eta-reduction sound, given appropriate instances (or lack thereof). Meaning > we could leave the rest of the proposal unevaluated (lazily!). > > And if somebody were to suggest that on a different day, +1 from me. > > John > >> On Apr 1, 2014 10:32 AM, "Edward Kmett" wrote: >> John, >> >> Check the date and consider the process necessary to "enumerate all Haskell >> programs and check their types". >> >> -Edward >> >> >>> On Tue, Apr 1, 2014 at 9:17 AM, John Lato wrote: >>> I think this is a great idea and should become a top priority. I would >>> probably start by switching to a type-class-based seq, after which perhaps >>> the next step forward would become more clear. >>> >>> John L. >>> >>>> On Apr 1, 2014 2:54 AM, "Dan Doel" wrote: >>>> In the past year or two, there have been multiple performance problems in >>>> various areas related to the fact that lambda abstraction is not free, >>>> though we >>>> tend to think of it as so. A major example of this was deriving of >>>> Functor. If we >>>> were to derive Functor for lists, we would end up with something like: >>>> >>>> instance Functor [] where >>>> fmap _ [] = [] >>>> fmap f (x:xs) = f x : fmap (\y -> f y) xs >>>> >>>> This definition is O(n^2) when fully evaluated,, because it causes O(n) eta >>>> expansions of f, so we spend time following indirections proportional to >>>> the >>>> depth of the element in the list. This has been fixed in 7.8, but there are >>>> other examples. I believe lens, [1] for instance, has some stuff in it that >>>> works very hard to avoid this sort of cost; and it's not always as easy to >>>> avoid >>>> as the above example. Composing with a newtype wrapper, for instance, >>>> causes an >>>> eta expansion that can only be seen as such at the core level. >>>> >>>> The obvious solution is: do eta reduction. However, this is not >>>> operationally >>>> sound currently. The problem is that seq is capable of telling the >>>> difference >>>> between the following two expressions: >>>> >>>> undefined >>>> \x -> undefined x >>>> >>>> The former causes seq to throw an exception, while the latter is considered >>>> defined enough to not do so. So, if we eta reduce, we can cause terminating >>>> programs to diverge if they make use of this feature. >>>> >>>> Luckily, there is a solution. >>>> >>>> Semantically one would usually identify the above two expressions. While I >>>> do >>>> believe one could construct a semantics that does distinguish them, it is >>>> not >>>> the usual practice. This suggests that there is a way to not distinguish >>>> them, >>>> perhaps even including seq. After all, the specification of seq is >>>> monotone and >>>> continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an >>>> extra >>>> element for the latter. >>>> >>>> The currently problematic case is function spaces, so I'll focus on it. How >>>> should: >>>> >>>> seq : (a -> b) -> c -> c >>>> >>>> act? Well, other than an obvious bottom, we need to emit bottom whenever >>>> our >>>> given function is itself bottom at every input. This may first seem like a >>>> problem, but it is actually quite simple. Without loss of generality, let >>>> us >>>> assume that we can enumerate the type a. Then, we can feed these values to >>>> the >>>> function, and check their results for bottom. Conal Elliot has prior art >>>> for >>>> this sort of thing with his unamb [2] package. For each value x :: a, >>>> simply >>>> compute 'f x `seq` ()' in parallel, and look for
Re: [Haskell-cafe] Eta Reduction
John, Check the date and consider the process necessary to "enumerate all Haskell programs and check their types". -Edward On Tue, Apr 1, 2014 at 9:17 AM, John Lato wrote: > I think this is a great idea and should become a top priority. I would > probably start by switching to a type-class-based seq, after which perhaps > the next step forward would become more clear. > > John L. > On Apr 1, 2014 2:54 AM, "Dan Doel" wrote: > >> In the past year or two, there have been multiple performance problems in >> various areas related to the fact that lambda abstraction is not free, >> though we >> tend to think of it as so. A major example of this was deriving of >> Functor. If we >> were to derive Functor for lists, we would end up with something like: >> >> instance Functor [] where >> fmap _ [] = [] >> fmap f (x:xs) = f x : fmap (\y -> f y) xs >> >> This definition is O(n^2) when fully evaluated,, because it causes O(n) >> eta >> expansions of f, so we spend time following indirections proportional to >> the >> depth of the element in the list. This has been fixed in 7.8, but there >> are >> other examples. I believe lens, [1] for instance, has some stuff in it >> that >> works very hard to avoid this sort of cost; and it's not always as easy >> to avoid >> as the above example. Composing with a newtype wrapper, for instance, >> causes an >> eta expansion that can only be seen as such at the core level. >> >> The obvious solution is: do eta reduction. However, this is not >> operationally >> sound currently. The problem is that seq is capable of telling the >> difference >> between the following two expressions: >> >> undefined >> \x -> undefined x >> >> The former causes seq to throw an exception, while the latter is >> considered >> defined enough to not do so. So, if we eta reduce, we can cause >> terminating >> programs to diverge if they make use of this feature. >> >> Luckily, there is a solution. >> >> Semantically one would usually identify the above two expressions. While >> I do >> believe one could construct a semantics that does distinguish them, it is >> not >> the usual practice. This suggests that there is a way to not distinguish >> them, >> perhaps even including seq. After all, the specification of seq is >> monotone and >> continuous regardless of whether we unify ⊥ with \x -> ⊥ x or insert an >> extra >> element for the latter. >> >> The currently problematic case is function spaces, so I'll focus on it. >> How >> should: >> >> seq : (a -> b) -> c -> c >> >> act? Well, other than an obvious bottom, we need to emit bottom whenever >> our >> given function is itself bottom at every input. This may first seem like a >> problem, but it is actually quite simple. Without loss of generality, let >> us >> assume that we can enumerate the type a. Then, we can feed these values >> to the >> function, and check their results for bottom. Conal Elliot has prior art >> for >> this sort of thing with his unamb [2] package. For each value x :: a, >> simply >> compute 'f x `seq` ()' in parallel, and look for any successes. If we >> ever find >> one, we know the function is non-bottom, and we can return our value of >> c. If we >> never finish searching, then the function must be bottom, and seq should >> not >> terminate, so we have satisfied the specification. >> >> Now, some may complain about the enumeration above. But this, too, is a >> simple >> matter. It is well known that Haskell programs are denumerable. So it is >> quite >> easy to enumerate all Haskell programs that produce a value, check >> whether that >> value has the type we're interested in, and compute said value. All of >> this can >> be done in Haskell. Thus, every Haskell type is programatically >> enumerable in >> Haskell, and we can use said enumeration in our implementation of seq for >> function types. I have discussed this with Russell O'Connor [3], and he >> assures >> me that this argument should be sufficient even if we consider semantic >> models >> of Haskell that contain values not denoted by any Haskell program, so we >> should >> be safe there. >> >> The one possible caveat is that this implementation of seq is not >> operationally >> uniform across all types, so the current fully polymorphic type of seq >> may not >> make sense. But moving back to a type class based approach isn't so bad, >> and >> this time we will have a semantically sound backing, instead of just >> having a >> class with the equivalent of the current magic function in it. >> >> Once this machinery is in place, we can eta reduce to our hearts' >> content, and >> not have to worry about breaking semantics. We'd no longer put the burden >> on >> programmers to use potentially unsafe hacks to avoid eta expansions. I >> apologize >> for not sketching an implementation of the above algorithm, but I'm sure >> it >> should be elementary enough to make it into GHC in the next couple >> versions. >> Everyone learns about this type
Re: PROPOSAL: Literate haskell and module file names
Foo+rst.lhs does nicely dodge the collision with jhc. How does ghc do the search now? By trying each alternative in turn? On Sun, Mar 16, 2014 at 1:14 PM, Merijn Verstraaten wrote: > I agree that this could collide, see my beginning remark that I believe > that the report should provide a minimal specification how to map modules > to filenames and vice versa. > > Anyhoo, I'm not married to this specific suggestion. Carter suggested > "Foo+rst.lhs" on IRC, other options would be "Foo.rst+lhs" or > "Foo.lhs+rst", I don't particularly care what as long as we pick something. > Patching tools to support whatever solution we pick should be trivial. > > Cheers, > Merijn > > On Mar 16, 2014, at 16:41 , Edward Kmett wrote: > > One problem with Foo.*.hs or even Foo.md.hs mapping to the module name Foois > that as I recall JHC will look for > Data.Vector in Data.Vector.hs as well as Data/Vector.hs > > This means that on a case insensitive file system Foo.MD.hs matches both > conventions. > > Do I want to block an change to GHC because of an incompatible change in > another compiler? Not sure, but I at least want to raise the issue so it > can be discussed. > > Another small issue is that this means you need to actually scan the > directory rather than look for particular file names, but off my head > really I don't expect directories to be full enough for that to be a > performance problem. > > -Edward > > > > On Sun, Mar 16, 2014 at 8:56 AM, Merijn Verstraaten < > mer...@inconsistent.nl> wrote: > >> Ola! >> >> I didn't know what the most appropriate venue for this proposal was so I >> crossposted to haskell-prime and glasgow-haskell-users, if this isn't the >> right venue I welcome advice where to take this proposal. >> >> Currently the report does not specify the mapping between filenames and >> module names (this is an issue in itself, it essentially makes writing >> haskell code that's interoperable between compilers impossible, as you >> can't know what directory layout each compiler expects). I believe that a >> minimal specification *should* go into the report (hence, haskell-prime). >> However, this is a separate issue from this proposal, so please start a new >> thread rather than sidetracking this one :) >> >> The report only mentions that "by convention" .hs extensions imply normal >> haskell and .lhs literate haskell (Section 10.4). In the absence of >> guidance from the report GHC's convention of mapping module Foo.Bar.Baz to >> Foo/Bar/Baz.hs or Foo/Bar/Baz.lhs seems the only sort of standard that >> exists. In general this standard is nice enough, but the mapping of >> literate haskell is a bit inconvenient, it leaves it completelyl ambiguous >> what the non-haskell content of said file is, which is annoying for tool >> authors. >> >> Pandoc has adopted the policy of checking for further file extensions for >> literate haskell source, e.g. Foo.rst.lhs and Foo.md.lhs. Here .rst.lhs >> gets interpreted as being reStructured Text with literate haskell and >> .md.lhs is Markdown with literate haskell. Unfortunately GHC currently maps >> filenames like this to the module names Foo.rst and Foo.md, breaking >> anything that wants to import the module Foo. >> >> I would like to propose allowing an optional extra extension in the >> pandoc style for literate haskell files, mapping Foo.rst.lhs to module name >> Foo. This is a backwards compatible change as there is no way for >> Foo.rst.lhs to be a valid module in the current GHC convention. Foo.rst.lhs >> would map to module name "Foo.rst" but module name "Foo.rst" maps to >> filename "Foo/rst.hs" which is not a valid haskell module anyway as the rst >> is lowercase and module names have to start with an uppercase letter. >> >> Pros: >> - Tool authors can more easily determine non-haskell content of literate >> haskell files >> - Currently valid module names will not break >> - Report doesn't specify behaviour, so GHC can do whatever it likes >> >> Cons: >> - Someone has to implement it >> - ?? >> >> Discussion: 4 weeks >> >> Cheers, >> Merijn >> >> >> ___ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> >> > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Safe Haskell trust
Not directly. You can, however, make a Trustworthy module that re-exports the (parts of) the Unsafe ones you want to allow yourself to use. -Edward On Sun, Mar 16, 2014 at 12:57 PM, Fabian Bergmark wrote: > Im using the Hint library in a project where users are able to upload > and run code. As I don't want them to do any IO, I run the interpreter > with -XSafe. However, some packages (in my case aeson) are needed and > I therefore tried marking them as trusted with ghc-pkg trust aeson. > This seems to have no effect however and the interpreter fails with: > > Data.Aeson: Can't be safely imported! The module itself isn't safe > > Is there any way to get XSafe-like guarantees with the ability of > allowing certain packages? > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PROPOSAL: Literate haskell and module file names
One problem with Foo.*.hs or even Foo.md.hs mapping to the module name Foois that as I recall JHC will look for Data.Vector in Data.Vector.hs as well as Data/Vector.hs This means that on a case insensitive file system Foo.MD.hs matches both conventions. Do I want to block an change to GHC because of an incompatible change in another compiler? Not sure, but I at least want to raise the issue so it can be discussed. Another small issue is that this means you need to actually scan the directory rather than look for particular file names, but off my head really I don't expect directories to be full enough for that to be a performance problem. -Edward On Sun, Mar 16, 2014 at 8:56 AM, Merijn Verstraaten wrote: > Ola! > > I didn't know what the most appropriate venue for this proposal was so I > crossposted to haskell-prime and glasgow-haskell-users, if this isn't the > right venue I welcome advice where to take this proposal. > > Currently the report does not specify the mapping between filenames and > module names (this is an issue in itself, it essentially makes writing > haskell code that's interoperable between compilers impossible, as you > can't know what directory layout each compiler expects). I believe that a > minimal specification *should* go into the report (hence, haskell-prime). > However, this is a separate issue from this proposal, so please start a new > thread rather than sidetracking this one :) > > The report only mentions that "by convention" .hs extensions imply normal > haskell and .lhs literate haskell (Section 10.4). In the absence of > guidance from the report GHC's convention of mapping module Foo.Bar.Baz to > Foo/Bar/Baz.hs or Foo/Bar/Baz.lhs seems the only sort of standard that > exists. In general this standard is nice enough, but the mapping of > literate haskell is a bit inconvenient, it leaves it completelyl ambiguous > what the non-haskell content of said file is, which is annoying for tool > authors. > > Pandoc has adopted the policy of checking for further file extensions for > literate haskell source, e.g. Foo.rst.lhs and Foo.md.lhs. Here .rst.lhs > gets interpreted as being reStructured Text with literate haskell and > .md.lhs is Markdown with literate haskell. Unfortunately GHC currently maps > filenames like this to the module names Foo.rst and Foo.md, breaking > anything that wants to import the module Foo. > > I would like to propose allowing an optional extra extension in the pandoc > style for literate haskell files, mapping Foo.rst.lhs to module name Foo. > This is a backwards compatible change as there is no way for Foo.rst.lhs to > be a valid module in the current GHC convention. Foo.rst.lhs would map to > module name "Foo.rst" but module name "Foo.rst" maps to filename > "Foo/rst.hs" which is not a valid haskell module anyway as the rst is > lowercase and module names have to start with an uppercase letter. > > Pros: > - Tool authors can more easily determine non-haskell content of literate > haskell files > - Currently valid module names will not break > - Report doesn't specify behaviour, so GHC can do whatever it likes > > Cons: > - Someone has to implement it > - ?? > > Discussion: 4 weeks > > Cheers, > Merijn > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Enabling TypeHoles by default
It actually can affect what code compiles with -fdefer-type-errors, but I don't feel terribly strongly about that. -Edward On Tue, Jan 14, 2014 at 12:23 PM, Joachim Breitner wrote: > Hi, > > heh, I wanted to throw in the same argument: If its just more elaborate > error messages, why do we need a flag for it? So count that as +1 from > me. > > Greetings, > Joachim > > > Am Dienstag, den 14.01.2014, 11:12 -0600 schrieb Austin Seipp: > > I'm actually more in favor of Richard's proposal of just removing the > > flag to be honest, now that he mentioned it. And it's not like it's > > much more code. > > > > In any case, as Duncan informed me we'll have a Cabal release anyway, > > so I'll work on sorting this out and enabling it. > > > > On Tue, Jan 14, 2014 at 10:54 AM, Duncan Coutts > wrote: > > > On Tue, 2014-01-14 at 17:44 +0100, Johan Tibell wrote: > > >> I can make another cabal release if needed, if someone submits a pull > > >> request with the right fix (i.e. add TypedHoles with TypeHoles as a > > >> synonym.) > > > > > > Thanks Johan, or I'm happy to do it. > > > > > > Duncan > > > > > >> On Tue, Jan 14, 2014 at 5:33 PM, Austin Seipp > wrote: > > >> > > >> > At the very least, Type(d)Holes would never appear explicitly since > it > > >> > would be enabled by default. But it might be turned off (but I don't > > >> > know who would do that for the most part.) Cabal at least might > still > > >> > need an update. > > >> > > > >> > In any case, Herbert basically summed it up: the time window is kind > > >> > of close, and we would need to re-release/redeploy a few things most > > >> > likely. I really think it mostly depends on the Cabal team and what > > >> > their priorities are. I've CC'd Duncan and Johan for their opinions. > > >> > > > >> > On Tue, Jan 14, 2014 at 10:27 AM, Herbert Valerio Riedel < > h...@gnu.org> > > >> > wrote: > > >> > > Hi, > > >> > > > > >> > > On 2014-01-14 at 17:14:51 +0100, David Luposchainsky wrote: > > >> > >> On 14.01.2014 17:07, Austin Seipp wrote: > > >> > >>> We probably won't change the name right now however. It's > already > > >> > >>> been put into Cabal (as a recognized extension,) so the name has > > >> > >>> propagated a slight bit. We can however give it a new name and > > >> > >>> deprecate the old -XTypeHoles in the future. Or, we could change > > >> > >>> it, but I'm afraid it's probably a bit too late in the cycle for > > >> > >>> other devs to change. > > >> > >> > > >> > >> Removing a name later on is more time-consuming, with or without > > >> > >> deprecation. People get used to the "wrong" name and stop > caring, but > > >> > >> I can already picture the "type holes are really typed holes" > > >> > >> discussions on IRC. I'm strongly in favour of introducing the > new name > > >> > >> (and the deprecation for the synonym) as early as possible. This > > >> > >> change should not be very extensive anyway, so why not slip it > in? > > >> > > > > >> > > Well, as Austin hinted at, this would also require a Cabal-1.18.x > > >> > > release in time for the final 7.8, and a recompile of Hackage to > pick it > > >> > > up so that people can start using the new 'TypedHoles' token in > their > > >> > > .cabal files... so there's a bit of coordination required to make > this > > >> > > happen in a timely manner... Or put differently, somebody has to > care > > >> > > enough to invest some time and pull this through :-) > > >> > > > > >> > > Cheers, > > >> > > hvr > > >> > > > > >> > > > >> > > > >> > > > >> > -- > > >> > Regards, > > >> > > > >> > Austin Seipp, Haskell Consultant > > >> > Well-Typed LLP, http://www.well-typed.com/ > > >> > > > > > > > > > > -- > > > Duncan Coutts, Haskell Consultant > > > Well-Typed LLP, http://www.well-typed.com/ > > > > > > > > > > > > > > -- > Joachim “nomeata” Breitner > m...@joachim-breitner.de • http://www.joachim-breitner.de/ > Jabber: nome...@joachim-breitner.de • GPG-Key: 0x4743206C > Debian Developer: nome...@debian.org > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Enabling TypeHoles by default
Heck if we wanted to bikeshed the name, even 'Holes' would do. ;) On Mon, Jan 13, 2014 at 4:30 PM, Daniil Frumin wrote: > On ghc-dev Dominique Devriese has actually proposed changing TypeHoles > to TypedHoles or to something similar, because "TypeHoles" sounds like > you can have holes in types, just like in your example. > > But what error message do you want to get if you have a hole in your > type? GHC won't be able to tell you much > > On Tue, Jan 14, 2014 at 12:54 AM, Mateusz Kowalczyk > wrote: > > On 13/01/14 18:42, Krzysztof Gogolewski wrote: > >> Hello, > >> > >> As discussed on ghc-devs, I propose to enable -XTypeHoles in GHC by > >> default. Rationale: > >> > >> (1) This way holes are far easier to use; just entering "_" allows to > check > >> type of a subexpression, no need of adding "-XTypeHoles". > >> > >> (2) This affects error messages only; i.e. the set of programs that > compile > >> stays the same - Haskell 2010. The only exception is that if you use > >> -fdefer-type-errors, then a program with a hole compiles, but this seems > >> fine with philosophy of -fdefer-type-errors. > >> > >> If so: would you like it to be in 7.8 or wait a cycle? My preference is > >> 7.8, two people (John and Richard) suggested 7.10. > >> > >> -KG > >> > > > > Sounds good. Are there plans to allow TypeHoles to actually sit in place > > of types? In the past I did > > > > ``` > > data Hole > > > > hole :: Hole > > hole = undefined > > > > foo :: Integer -> Integer > > foo x = hole > > > > bar :: Integer -> Hole > > bar x y = x + y > > ``` > > > > to cause type errors that could guide me. I now don't have to resort to > > the first use in ‘foo’ but I still have to define my own Hole type in > ‘bar’. > > > > > > -- > > Mateusz K. > > ___ > > Glasgow-haskell-users mailing list > > Glasgow-haskell-users@haskell.org > > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > > > -- > Sincerely yours, > -- Daniil > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Enabling TypeHoles by default
I have to admit, I rather like this suggestion. -Edward On Mon, Jan 13, 2014 at 1:42 PM, Krzysztof Gogolewski < krz.gogolew...@gmail.com> wrote: > Hello, > > As discussed on ghc-devs, I propose to enable -XTypeHoles in GHC by > default. Rationale: > > (1) This way holes are far easier to use; just entering "_" allows to > check type of a subexpression, no need of adding "-XTypeHoles". > > (2) This affects error messages only; i.e. the set of programs that > compile stays the same - Haskell 2010. The only exception is that if you > use -fdefer-type-errors, then a program with a hole compiles, but this > seems fine with philosophy of -fdefer-type-errors. > > If so: would you like it to be in 7.8 or wait a cycle? My preference is > 7.8, two people (John and Richard) suggested 7.10. > > -KG > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why cannot inferred type signatures restrict (potentially) ambiguous type variables?
AllowAmbiguousTypes at this point only extends to signatures that are
explicitly written.
This would need a new "AllowInferredAmbiguousTypes" or something.
On Sat, Oct 12, 2013 at 5:34 PM, adam vogt wrote:
> Hello,
>
> I have code:
>
> {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses,
> ScopedTypeVariables, TypeFamilies #-}
>
> class C a b where c :: a -> b
> instance (int ~ Integer) => C Integer int where c = (+1)
>
> c2 :: forall a b c. (C a b, C b c) => a -> c
> c2 x = c (c x :: b)
> c2 x = c ((c :: a -> b) x)
>
>
> Why are the type signatures needed? If I leave all of them off, I get:
>
> Could not deduce (C a1 a0)
> arising from the ambiguity check for ‛c2’
> from the context (C a b, C a1 a)
> bound by the inferred type for ‛c2’: (C a b, C a1 a) => a1 -> b
>
> from the line: c2 x = c (c x)
>
>
> From my perspective, it seems that the type signature ghc infers
> should be able to restrict the ambiguous types as the hand-written
> signature does.
>
> These concerns apply to HEAD (using -XAllowAmbiguousTypes) and ghc-7.6 too.
>
> Regards,
> Adam
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
On Fri, Oct 11, 2013 at 1:00 PM, Simon Peyton-Jones wrote: > First, in this case Set’s argument has nominal role, so the GND you give > would be rejected anyway. So Set’s sanctity stays unscathed. > Fair enough. I'm very happy to hear that avenue of attack doesn't work. =) > But beyond that, when you say > > newtype Bar = Bar Int deriving (Eq,Foo) > > the “deriving Foo” bit says > > “please implement all the Foo operations on Bar values in precisely the > same way that you implement Foo operations on Int.” > > Now that might be a stupid thing to say. There are many ways in which it > could be semantically wrong. One of them is that Ints are ordered one way > and Bars are ordered another. But there may be other ways too. Perhaps > Bars have properties that Ints don’t which mean that inserting should work > differently. A type system cannot hope to catch all of these. > My main concern is just making sure that we don't wind up with situations where you can get two instances of, say, Eq Bar that disagree under Safe Haskell depending on where you obtained it. So far Richard's proposed fix has handled every attack I've come up with. I'll go back to looking for other attack vectors. -Edward > *From:* Edward Kmett [mailto:ekm...@gmail.com] > *Sent:* 11 October 2013 03:09 > *To:* Richard Eisenberg > *Cc:* David Menendez; glasgow-haskell-users@haskell.org Mailing List; > Simon Peyton-Jones > *Subject:* Re: default roles > > ** ** > > Wait, that sounds like it induces bad semantics. > > ** ** > > Can't we use that as yet another way to attack the sanctity of Set? > > ** ** > > class Ord a => Foo a where > > badInsert :: a -> Set a -> Set a > > ** ** > > instance Foo Int where > > badInsert = insert > > ** ** > > newtype Bar = Bar Int deriving (Eq,Foo) > > ** ** > > instance Ord Bar where > > compare (Bar x) (Bar y) = compare y x > > ** ** > > Now you can badInsert into a Set. > > ** ** > > If that is still in play then even with all the roles machinery then GND > doesn't pass the restrictions of "SafeHaskell". =( > > ** ** > > -Edward > > ** ** > > On Thu, Oct 10, 2013 at 9:52 PM, Richard Eisenberg > wrote: > > > On Oct 10, 2013, at 1:14 PM, David Menendez wrote: > > Sure, but if op uses show internally, we get Int's show, not Age's, > right? That seems correct, in that it's doing what GND is supposed to do, > but I'll bet it will surprise people. > > Yes, you're right. If a method in a subclass uses a superclass method, it > uses the base type's instance's method, not the newtype's. Very weird, but > I guess it makes sense in its own way. This does show how GND can create > instance incoherence even without storing dictionaries in datatypes. > > > Richard > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ** ** > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
Wait, that sounds like it induces bad semantics. Can't we use that as yet another way to attack the sanctity of Set? class Ord a => Foo a where badInsert :: a -> Set a -> Set a instance Foo Int where badInsert = insert newtype Bar = Bar Int deriving (Eq,Foo) instance Ord Bar where compare (Bar x) (Bar y) = compare y x Now you can badInsert into a Set. If that is still in play then even with all the roles machinery then GND doesn't pass the restrictions of "SafeHaskell". =( -Edward On Thu, Oct 10, 2013 at 9:52 PM, Richard Eisenberg wrote: > > On Oct 10, 2013, at 1:14 PM, David Menendez wrote: > > Sure, but if op uses show internally, we get Int's show, not Age's, > right? That seems correct, in that it's doing what GND is supposed to do, > but I'll bet it will surprise people. > > Yes, you're right. If a method in a subclass uses a superclass method, it > uses the base type's instance's method, not the newtype's. Very weird, but > I guess it makes sense in its own way. This does show how GND can create > instance incoherence even without storing dictionaries in datatypes. > > Richard > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
The only class I'd want to preserve a representational roles for its arguments for would be Coercible. It does strike me as interesting to consider what it would mean to properly check other instances for overlap when the instances are defined only 'up to representation'. It also strikes me as quite a rabbit hole. ;) -Edward On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg wrote: > Now I think we're on the same page, and I *am* a little worried about the > sky falling because of this. (That's not a euphemism -- I'm only a little > worried.) > > Well, maybe I should be more worried. > > The whole idea of roles is to protect against type-unsoundness. They are > doing a great job of that here -- no problem that we've discussed in this > thread is a threat against type safety. > > The issue immediately at hand is about coherence (or perhaps you call it > confluence) of instances. Roles do not address the issue of coherence at > all, and thus they fail to protect against coherence attacks. It would take > More Thought to reformulate roles (or devise something else) to handle > coherence. > > It's worth pointing out that this isn't a new problem, exactly. Bug #8338 > shows a way to produce incoherence using only the GADTs extension. (It does > need 4 modules, though.) I conjecture that incoherence is also possible > through GeneralizedNewtypeDeriving, both as it existed in GHC 7.6.3 and in > 7.8, so it's not an issue with Coercible, exactly. It's just that Coercible > allows you to get incoherence with so much less fuss than before! > > Wait! I have an idea! > The way I've been describing GND all along has been an abbreviation. GHC > does not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC > mints a fresh dictionary for Ord Age where all the methods are implemented > as coerced versions of the methods for Ord Int. (I'm not sure why it's > implemented this way, which is why I've elided this detail in just about > every conversation on the topic.) With this in mind, I have a proposal: > > 1) All parameters of all classes have nominal role. > 2) Classes also store one extra bit per parameter, saying whether all uses > of that parameter are representational. Essentially, this bit says whether > that parameter is suitable for GND. (Currently, we could just store for the > last parameter, but we can imagine extensions to the GND mechanism for > other parameters.) > > Because GND is implemented using coercions on each piece instead of > wholesale, the nominal roles on classes won't get in the way of proper use > of GND. An experiment (see below for details) also confirms that even > superclasses work well with this idea -- the superclasses aren't coerced. > > Under this proposal, dictionaries can never be coerced, but GND would > still seem to work. > > Thoughts? > > Richard > > Experiment: > > newtype Age = MkAge Int > > instance Eq Age where > _ == _ = False > > deriving instance Ord Age > > useOrdInstance :: Ord a => a -> Bool > useOrdInstance x = (x == x) > > > What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD). > This means that the existing GND mechanism (I didn't change anything around > this part of the code) uses superclass instances for the *newtype*, not for > the *base type*. So, even with superclasses, class dictionaries don't need > to be coerced. > > On Oct 9, 2013, at 2:52 PM, Edward Kmett wrote: > > I'd be happy to be wrong. =) > > We do seem to have stumbled into a design paradox though. > > To make it so you can use roles in GeneralizedNewtypeDeriving hinges on > the parameter's role being representational, but making it representational > means users can also use coerce to turn dictionaries into other > dictionaries outside of GND. > > This is quite insidious, as another dictionary for Eq or Ord may exist for > that type, where it becomes unsound as the generated dictionary may be used > to destroy confluence. > > This means that even if something like Set has a nominal argument it isn't > safe, because you can attack the invariants of the structure via Ord. > > newtype Bad = Bad Int deriving Eq > instance Ord Bad where >compare (Bad a) (Bad b) = compare b a > > If Ord has a representational role then I can use coerce to convert a > dictonary Ord Bad to Ord Int, then work locally in a context where that is > the dictionary for Ord Int that I get when I go to do an insert or lookup. > > I don't mean to sound like the sky is falling, but I do worry that the > 'use of a constraint in a data type' may not be necessary or sufficient.
Re: default roles
On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg wrote: > Now I think we're on the same page, and I *am* a little worried about the > sky falling because of this. (That's not a euphemism -- I'm only a little > worried.) > =) > Wait! I have an idea! > The way I've been describing GND all along has been an abbreviation. GHC > does not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC > mints a fresh dictionary for Ord Age where all the methods are implemented > as coerced versions of the methods for Ord Int. (I'm not sure why it's > implemented this way, which is why I've elided this detail in just about > every conversation on the topic.) With this in mind, I have a proposal: > > 1) All parameters of all classes have nominal role. > 2) Classes also store one extra bit per parameter, saying whether all uses > of that parameter are representational. Essentially, this bit says whether > that parameter is suitable for GND. (Currently, we could just store for the > last parameter, but we can imagine extensions to the GND mechanism for > other parameters.) > > Because GND is implemented using coercions on each piece instead of > wholesale, the nominal roles on classes won't gehingt in the way of proper > use of GND. An experiment (see below for details) also confirms that even > superclasses work well with this idea -- the superclasses aren't coerced. > > Under this proposal, dictionaries can never be coerced, but GND would > still seem to work. > > Thoughts? > This strikes me as a remarkably straightforward solution. Does it strike you as something implementable in time for 7.8 though? > Richard > > Experiment: > > newtype Age = MkAge Int > > instance Eq Age where > _ == _ = False > > deriving instance Ord Age > > useOrdInstance :: Ord a => a -> Bool > useOrdInstance x = (x == x) > > > What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD). > This means that the existing GND mechanism (I didn't change anything around > this part of the code) uses superclass instances for the *newtype*, not for > the *base type*. So, even with superclasses, class dictionaries don't need > to be coerced. > Upon reflection it makes a lot of sense that GND has to mint a new dictionary, because the superclasses may differ, like you showed here. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
I'd be happy to be wrong. =) We do seem to have stumbled into a design paradox though. To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the parameter's role being representational, but making it representational means users can also use coerce to turn dictionaries into other dictionaries outside of GND. This is quite insidious, as another dictionary for Eq or Ord may exist for that type, where it becomes unsound as the generated dictionary may be used to destroy confluence. This means that even if something like Set has a nominal argument it isn't safe, because you can attack the invariants of the structure via Ord. newtype Bad = Bad Int deriving Eq instance Ord Bad where compare (Bad a) (Bad b) = compare b a If Ord has a representational role then I can use coerce to convert a dictonary Ord Bad to Ord Int, then work locally in a context where that is the dictionary for Ord Int that I get when I go to do an insert or lookup. I don't mean to sound like the sky is falling, but I do worry that the 'use of a constraint in a data type' may not be necessary or sufficient. That is a lot of surface area to defend against attack. I am not sure that I actually need a data type to coerce a dictionary. It seems likely that I could do it with just a well crafted function argument and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the moment to give it a try. -Edward On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg wrote: > I don't quite agree with your analysis, Edward. > > Eq can be auto-derived, so it makes for a confusing example. Let's replace > Eq in your example with this class: > > > class C a where > > c_meth :: a -> a -> Bool > > Then, your example leads to the same embarrassing state of affairs: > coercing a dictionary for (C Int) to one for (C Bar). > > But, I would argue that we still want C's parameter to have a > representational role. Why? Consider this: > > > data Blargh = ... > > instance C Blargh where ... > > > > newtype Baz = MkBaz Blargh deriving C > > We want that last line to work, using GeneralizedNewtypeDeriving. This > hinges on C's parameter's role being representational. > > I think that what you've witnessed is a case of bug #8338 ( > http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my > view, and it seems to touch on roles, but I'm not completely sure of their > relationship. > > So, I think that classes should keep their representational roles > (regardless of the decision on datatypes -- Haskell doesn't really support > "abstract" classes), but perhaps we have to find a way to stop these > incoherent instances from forming. Maybe the use of a constraint makes a > datatype's role be nominal? > > Richard > > On Oct 9, 2013, at 1:55 PM, Edward Kmett wrote: > > I just noticed there is a pretty big issue with the current default role > where typeclasses are concerned! > > When implementing Data.Type.Coercion I had to use the fact that I could > apply coerce to the arguments of > > data Coercion a b where > Coercion :: Coercible a b => Coercion a b > > This makes sense as Coercion itself has two representational arguments. > > This struck me as quite clever, so I went to test it further. > > data Foo a where >Foo :: Eq a => Foo a > > newtype Bar = Bar Int > instance Eq Bar where > _ == _ = False > > I fully expected the following to fail: > > coerce (Foo :: Foo Int) :: Foo Bar > > but instead it succeeded. > > This means I was able to convert a dictionary Eq Int into a dictionary > for Eq Bar! > > This indicates that Eq (actually all) of the typeclasses are currently > marked as having representational, when actually it strikes me that > (almost?) none of them should be. > > Coercible is the only case I can think of in base of a class with two > representational arguments, but this is only valid because we prevent users > from defining Coercible instances manually. > > If I try again with a new typeclass that has an explicit nominal role > > type role Eq nominal > class Eq a > instance Eq Int > instance Eq Bar > > then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd > expect. > > This indicates two big issues to me: > > 1.) At the very least the default role for type *classes* should be > nominal for each argument. The very point of an instance is to make a > nominal distinction after all. =) > > 2.) It also indicates that making any typeclass with a representational (/ > phantom?) argument shouldn't be possible in valid SafeHaskell, as you can > use it to subvert the current restrict
Re: default roles
I just noticed there is a pretty big issue with the current default role
where typeclasses are concerned!
When implementing Data.Type.Coercion I had to use the fact that I could
apply coerce to the arguments of
data Coercion a b where
Coercion :: Coercible a b => Coercion a b
This makes sense as Coercion itself has two representational arguments.
This struck me as quite clever, so I went to test it further.
data Foo a where
Foo :: Eq a => Foo a
newtype Bar = Bar Int
instance Eq Bar where
_ == _ = False
I fully expected the following to fail:
coerce (Foo :: Foo Int) :: Foo Bar
but instead it succeeded.
This means I was able to convert a dictionary Eq Int into a dictionary for Eq
Bar!
This indicates that Eq (actually all) of the typeclasses are currently
marked as having representational, when actually it strikes me that
(almost?) none of them should be.
Coercible is the only case I can think of in base of a class with two
representational arguments, but this is only valid because we prevent users
from defining Coercible instances manually.
If I try again with a new typeclass that has an explicit nominal role
type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar
then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd
expect.
This indicates two big issues to me:
1.) At the very least the default role for type *classes* should be nominal
for each argument. The very point of an instance is to make a nominal
distinction after all. =)
2.) It also indicates that making any typeclass with a representational (/
phantom?) argument shouldn't be possible in valid SafeHaskell, as you can
use it to subvert the current restrictions on OverlappingInstances.
-Edward
On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki wrote:
> Hello,
>
> My preference would be for the following design:
>
> 1. The default datatypes for roles are Nominal, but programmers can add
> annotations to relax this.
> 2. Generlized newtype deriving works as follows: we can coerce a
> dictionary for `C R` into `C T`, as long as we can coerce the types of all
> methods instantiated with `R`, into the corresponding types instantiated
> with `T`. In other words, we are pretending that we are implementing all
> methods by using `coerce`.
>
> As far as I can see this safe, and matches what I'd expect as a
> programmer. It also solves the problem with the `Set` example: because
> `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge`
> and, hence, we cannot derive an instance of `MyAge` for `HasSet`. An added
> benefit of this approach is that when newtype deriving fails, we can give a
> nicer error saying exactly which method causes the problem.
>
> -Iavor
>
>
>
>
>
>
> On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg wrote:
>
>> As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are
>> a mechanism to allow for safe 0-cost conversions between newtypes and their
>> base types. GeneralizedNewtypeDeriving (GND) already did this for class
>> instances, but in an unsafe way -- the feature has essentially been
>> retrofitted to work with roles. This means that some uses of GND that
>> appear to be unsafe will no longer work. See the wiki page [1] or slides
>> from a recent presentation [2] for more info.
>>
>> [1] : http://ghc.haskell.org/trac/ghc/wiki/Roles
>> [2] : http://www.cis.upenn.edu/~eir/papers/2013/roles/roles-slides.pdf
>>
>> I am writing because it's unclear what the *default* role should be --
>> that is, should GND be allowed by default? Examples follow, but the
>> critical issue is this:
>>
>> * If we allow GND by default anywhere it is type-safe, datatypes (even
>> those that don't export constructors) will not be abstract by default.
>> Library writers would have to use a role annotation everywhere they wish to
>> declare a datatype they do not want users to be able to inspect. (Roles
>> still keep type-*un*safe GND from happening.)
>>
>> * If we disallow GND by default, then perhaps lots of current uses of GND
>> will break. Library writers will have to explicitly declare when they wish
>> to permit GND involving a datatype.
>>
>> Which do we think is better?
>>
>> Examples: The chief example demonstrating the problem is (a hypothetical
>> implementation of) Set:
>>
>> > module Set (Set) where -- note: no constructors exported!
>> >
>> > data Set a = MkSet [a]
>> > insert :: Ord a => a -> Set a -> Set a
>> > ...
>>
>> > {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
>> > module Client where
>> >
>> > import Set
>> >
>> > newtype Age = MkAge Int deriving Eq
>> >
>> > instance Ord Age where
>> > (MkAge a) `compare` (MkAge b) = b `compare` a -- flip operands,
>> reversing the order
>> >
>> > class HasSet a where
>> > getSet :: Set a
>> >
>> > instance HasSet Int where
>> > getSet = insert 2 (insert 5 empty)
>> >
>> > deriving instance HasSet Age
>> >
>> > good :: Set Int
>> > good = getSet
>> >
>> > bad :: Set Age
>> > bad = getS
Re: Desugaring do-notation to Applicative
That is admittedly a pretty convincing example that we may want to provide either a LANGUAGE pragma or a different syntax to opt in. As a data point in this space, the version of the code I have in scheme calls the version of 'do' that permits applicative desugaring 'ado'. A port of it to Haskell with minor infelicities as a quasi-quoter can be found here: http://hackage.haskell.org/package/applicative-quoters-0.1.0.7/docs/Control-Applicative-QQ-ADo.html However, that version uses an awkward hack to permit pattern matches to fail. -Edward On Wed, Oct 2, 2013 at 12:24 PM, Reid Barton wrote: > On Wed, Oct 2, 2013 at 12:01 PM, Dag Odenhall wrote: > >> What about MonadComprehensions, by the way? The way I see it, it's an >> even better fit for Applicative because the return is implicit. >> > Yes, or ordinary list comprehensions for that matter. > > But there is a danger in desugaring to Applicative: it may introduce too > much sharing. Currently a program like "main = print $ length [ (x, y) | x > <- [1..3], y <- [1..1000] ]" (or the equivalent in do-notation) runs in > constant space with either -O0 or -O -fno-full-laziness. If you desugar it > to a form like "main = print $ length $ (,) <$> [1..3] <*> [1..1000]", > then no optimization flags will save you from a space leak. > > It might be better to require explicit opt-in to the Applicative > desugaring on a per-do-notation/comprehension basis. Of course, finding > good syntax is always such a bother... > > I'm definitely +1 on the overall idea though, I have a bunch of FRP code > (where I have to use Applicative) that looks just like Dan Doel's second > snippet and it's pretty horrid. > > Regards, > Reid Barton > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Liberalising IncoherentInstances
I'll probably never use it, but I can't see any real problems with the
proposal. In many ways it is what I always expected IncoherentInstances to
be.
One thing you might consider is that if you have to make an arbitrary
instance selection at the end during compile time, making that emit a
warning by default or at least under -Wall. That way it is clear when you
are leaning on underdetermined semantics.
-Edward
On Sat, Jul 27, 2013 at 4:16 PM, Simon Peyton-Jones
wrote:
> Friends
>
> I've realised that GHC's -XIncoherentInstances flag is, I think,
> over-conservative. I propose to liberalise it a bit. This email describes
> the issue. Please yell if you think this is a bad idea.
>
> Simon
>
> Suppose we have
>
> class C a where { op :: a -> String }
> instance C [a] where ...
> instance C [Char] where ...
>
> f :: [b] -> String
> f xs = "Result:" ++ op xs
>
> With -XOverlappingInstances, but without -XIncoherentInstances, f won't
> compile. Reason: if we call 'f' at Char (e.g. f "foo") then you might
> think we should use instance C [Char]. For example, if we inlined 'f' at
> the call site, to get ("Result:" ++ op "foo"), we certainly then would use
> the C [Char] instance, giving perhaps different results. If we accept the
> program as-is, we'll permanently commit 'f' to using the C [a] instance.
>
> The -XIncoherentInstances flag says "Go ahead and use an instance, even if
> another instance might become relevant if you were to specialise or inline
> the enclosing function." The GHC user manual gives a more precise spec [1].
>
> Now consider this
> class D a b where { opD :: a -> b -> String }
> instance D Int b where ...
> instance D a Int where ...
>
> g (x::Int) = opD x x
>
> Here 'g' gives rise to a constraint (D Int Int), and that matches two
> instance declarations. So this is rejected regardless of flags. We can
> fix it up by adding
> instance D Int Int where ...
> but this is pretty tiresome in cases where it really doesn't matter which
> instance you choose. (And I have a use-case where it's more than tiresome
> [2].)
>
> The underlying issue is similar to the previous example. Before, there
> was *potentially* more than one way to generate evidence for (C [b]); here
> there is *actually* more than one instance. In both cases the dynamic
> semantics of the language are potentially affected by the choice -- but
> -XIncoherentInstnaces says "I don't care".
>
>
> So the change I propose to make IncoherentInstances to pick arbitrarily
> among instances that match. More precisely, when trying to find an
> instance matching a target constraint (C tys),
>
> a) Find all instances matching (C tys); these are the candidates
>
> b) Eliminate any candidate X for which another candidate Y is
> strictly more specific (ie Y is a substitution instance of X),
> if either X or Y was complied with -XOverlappingInstances
>
> c) Check that any non-candidate instances that *unify* with (C tys)
>were compiled with -XIncoherentInstances
>
> d) If only one candidate remains, pick it.
> Otherwise if all remaining candidates were compiled with
> -XInccoherentInstances, pick an arbitrary candidate
>
> All of this is precisely as now, except for the "Otherwise" part of (d).
> One could imagine different flags for the test in (c) and (d) but I really
> don't think it's worth it.
>
>
> Incidentally, I think it'd be an improvement to localise the
> Overlapping/Incoherent flags to particular instance declarations, via
> pragmas, something like
> instance C [a] where
> {-# ALLOW_OVERLAP #-}
> op x =
>
> Similarly {-# ALLOW_INCOHERENT #-}. Having -XOverlappingInstances for
> the whole module is a bit crude., and might be missed when looking at an
> instance. How valuable would this be?
>
> [1]
> http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap
> [2] http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers
>
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: How to fix DatatypeContexts?
This is exactly what GADTs are for.
-Edward
On Thu, Jul 18, 2013 at 6:54 AM, harry wrote:
> data Eq a => Pair a = Pair {x::a, y::a}
>
> equal :: Pair a -> Bool
> equal pair = (x pair) == (y pair)
>
> This code will fail to compile, even with the deprecated DatatypeContexts
> extension, because equal must be given the Eq a => constraint, even though
> this has already been declared on the Pair type.
>
> Some of my code is littered with such redundant type constraints (although
> some of them could be replaced with a redundant pattern match). A proposal
> to enhance DatatypeContexts (#8026) in this way was rejected as unsound, as
> some nefarious uses of undefined would break the type system.
>
> Is there any way that the type system could be enhanced to avoid this
> redundancy?
>
>
>
> --
> View this message in context:
> http://haskell.1045720.n5.nabble.com/How-to-fix-DatatypeContexts-tp5733103.html
> Sent from the Haskell - Glasgow-haskell-users mailing list archive at
> Nabble.com.
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Field accessor type inference woes
On Tue, Jul 2, 2013 at 4:53 AM, AntC wrote: > > > > I was envisaging that we might well need a functional dependency > > > > Hi Adam, Edward, (Simon), > > I think we should be really careful before introducing FunDeps (or type > functions). > > Can we get to the needed type inference with UndecidableInstances? > Is that so bad? > That doesn't solve this problem. The issue isn't that the it is undecidable and that it could choose between two overlapping options. The issue is that there is no 'correct' instance to choose. > In the original SORF proposal, Simon deliberately avoided type functions, > and for closely argued reasons: > "But this approach fails for fields with higher rank types." > I guess the same would apply for FunDeps. > The approach still has issues with higher kinded types when extended to include setting. > FWIW in the DORF prototype, I did use type functions. > I was trying to cover a panoply of HR types, parametric polymorphic > records, type-changing update [**], and all sorts; > so probably too big a scope for this project. > > If you're interested, it's deep in the bowels of the Implementation notes, > so I could forgive anybody for tl;dr. See: > http://hackage.haskell.org/trac/ghc/wiki/Records/DeclaredOverloadedRecordFi > elds/ImplementorsView#Type-changingupdate > > In terms of the current Plan: > > class Has r fld t where > getFld :: r -> GetResult r fld t > > Of course where the record and field do determine the result, > the GetResult instance can simply ignore its third argument. > But for HR types, this allows the `Has` instance to > 'improve' `t` through Eq constraints, > _and_then_ pass that to GetResult. > > In the 'chained' accessors that Edward raises, > I think the presence of the type function 'fools' type inference into > thinking there's a dependency. > There really is a dependency. If the input record type doesn't determine the output value type that has to be passed to the next field accessor (or vice versa) then there is *no* known type for the intermediate value type. You can't punt it to the use site. > So (foo . bar) has type (and abusing notation): > > ( Has r "bar" t_bar, Has (GetResult r "bar" t_bar) "foo" t_foo ) > => r -> (GetResult (GetResult r "bar" t_bar) "foo" t_foo) The extra parameter actually makes coverage even harder to determine and it makes instance selection almost impossible as it will in almost all cases be under-determined, and since we're playing games with type application, not even manually able to be applied! > [**] Beware that the DORF approach didn't support type-changing update in > all cases, for reasons included in the notes for Adam's Plan page. > > Also beware that DORF used type families and some sugar around them. > That had the effect of generating overlapping family instances in some > cases -- which was OK, because they were confluent. > But if I understand correctly what Richard E is working on > http://hackage.haskell.org/trac/ghc/wiki/NewAxioms > overlapping stand-alone family instances are going to be banished > -- even if confluent. > Even with overlapping type families nothing changes. Coverage is still violated. > So today I would approach it by making them associated types, > and including the GetResult instance inside the `Has`, > so having a separate (non-overlapping) instance > for each combination of record and field (Symbol). > > HTH. Is Adam regretting taking up the challenge yet? ;-) > > AntC > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Field accessor type inference woes
On Mon, Jul 1, 2013 at 1:07 PM, Adam Gundry wrote: > Hi Edward, > > I was envisaging that we might well need a functional dependency > > class Has (r :: *) (x :: Symbol) (t :: *) | r x -> t > > and, as you point out, composition of polymorphic accessors certainly > motivates this. Isn't that enough, though? I think it works out more > neatly than the type family version, not least because evidence for a > Has constraint is still merely a projection function, and we can still > handle universally quantified fields. > My understanding from a recent interaction with Iavor was that the old difference between functional dependencies and type families where the fundep only chose the 'instance' rather than the actual meaning of the arguments has changed recently, to make the two approaches basically indistinguishable. This happened as part of the resolution to http://hackage.haskell.org/trac/ghc/ticket/2247 as I understand it. In particular this broke similar code that relied on this functionality in lens and forced a rather large number of patches that had made (ab)use of the old fundep behavior to be reverted in lens. Consequently, I don't think you'll find much of a difference between the type family and the functional depency, except that the latter is forced to infect more type signatures. Obviously it will still not allow determining the type of a record from > the type of one of its fields, but that doesn't seem unreasonable to me. > Have you any examples where this will be problematic? > Well, it does have the unfortunate consequence that it dooms the lifted instance we talked about that could make all field accessors automatically lift into lenses, as that required inference to flow backwards from the 'field' to the 'record'. Moreover, I suggest that Has constraints are only introduced when there > are multiple fields with the same name in scope, so existing code (with > no ambiguity) will work fine. > The awkward part about that is that it becomes impossible to write code that is polymorphic and have it get the more general signature without putting dummies in scope just to force conflict. -Edward > Thanks, > > Adam > > > On 01/07/13 15:48, Edward Kmett wrote: > > It strikes me that there is a fairly major issue with the record > > proposal as it stands. > > > > Right now the class > > > > class Has (r :: *) (x :: Symbol) (t :: *) > > > > can be viewed as morally equivalent to having several classes > > > > class Foo a b where > > foo :: a -> b > > > > class Bar a b where > > bar :: a -> b > > > > for different fields foo, bar, etc. > > > > I'll proceed with those instead because it makes it easier to show the > > issue today. > > > > When we go to compose those field accessors, you very quickly run into a > > problem due to a lack of functional dependencies: > > > > When you go to define > > > > fooBar = foo.bar > > > > which is perfectly cromulent with existing record field accessors you > > get a big problem. > > > > fooBar :: (Foo b c, Bar a b) => a -> c > > > > The b that should occur in the signature isn't on the right hand side, > > and isn't being forced by any fundeps, so fooBar simply can't be written. > > > > Could not deduce (Foo b0 c) arising from a use of `foo' from the context > > (Bar a b, Foo b c) > > > > If you leave off the signature you'll get an ambiguity check error: > > > > Could not deduce (Foo b0 c) > > arising from the ambiguity check for `fooBar' > > from the context (Bar a b, Foo b c) > > bound by the inferred type for `fooBar': > > (Bar a b, Foo b c) => a -> c > > > > It strikes me that punting all functional dependencies in the record > > types to the use of equality constraints has proven insufficient to > > tackle this problem. You may be able to bandaid over it by including a > > functional dependency/type family > > > > class Has (r :: *) (x :: Symbol) where > > type Got r x :: * > > getFld :: r -> Got r x > > > > (or to avoid the need for type applications in the first place!) > > > > class Has (r :: *) (x :: Symbol) where > > type Got r x :: * > > getFld :: p x -> r -> Got r x > > > > This has some annoying consequences though. Type inference can still > > only flow one way through it, unlike the existing record accessors, and > > it would cost the ability to 'cheat' and still define 'Has' for > > universally quantified fields that we might have been able to do with > > the proposal as it stands. > > > > -Edward > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Field accessor type inference woes
It strikes me that there is a fairly major issue with the record proposal as it stands. Right now the class class Has (r :: *) (x :: Symbol) (t :: *) can be viewed as morally equivalent to having several classes class Foo a b where foo :: a -> b class Bar a b where bar :: a -> b for different fields foo, bar, etc. I'll proceed with those instead because it makes it easier to show the issue today. When we go to compose those field accessors, you very quickly run into a problem due to a lack of functional dependencies: When you go to define fooBar = foo.bar which is perfectly cromulent with existing record field accessors you get a big problem. fooBar :: (Foo b c, Bar a b) => a -> c The b that should occur in the signature isn't on the right hand side, and isn't being forced by any fundeps, so fooBar simply can't be written. Could not deduce (Foo b0 c) arising from a use of `foo' from the context (Bar a b, Foo b c) If you leave off the signature you'll get an ambiguity check error: Could not deduce (Foo b0 c) arising from the ambiguity check for `fooBar' from the context (Bar a b, Foo b c) bound by the inferred type for `fooBar': (Bar a b, Foo b c) => a -> c It strikes me that punting all functional dependencies in the record types to the use of equality constraints has proven insufficient to tackle this problem. You may be able to bandaid over it by including a functional dependency/type family class Has (r :: *) (x :: Symbol) where type Got r x :: * getFld :: r -> Got r x (or to avoid the need for type applications in the first place!) class Has (r :: *) (x :: Symbol) where type Got r x :: * getFld :: p x -> r -> Got r x This has some annoying consequences though. Type inference can still only flow one way through it, unlike the existing record accessors, and it would cost the ability to 'cheat' and still define 'Has' for universally quantified fields that we might have been able to do with the proposal as it stands. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: A possible alternative to dot notation for record access
If you really want to hunt for unused syntax and we wind up needing a (.)
analogue then (->) is currently a reserved operator, so opening it up for
use at the term level could be made to work, and there is a precedent with
c/c++ pointer dereferencing.
-Edward
On Mon, Jul 1, 2013 at 1:10 AM, Edward Kmett wrote:
> (#) is a legal operator today and is used in a number of libraries.
>
>
> On Sun, Jun 30, 2013 at 11:38 PM, wrote:
>
>> As long as we're bikeshedding...
>>
>> Possibly '#' is unused syntax -- Erlang uses it for its records too, so
>> we wouldn't be pulling it out of thin air. E.g. "person#firstName"
>>
>> Tom
>>
>>
>> El Jun 30, 2013, a las 22:59, AntC
>> escribió:
>>
>> >> Carter Schonwald gmail.com> writes:
>> >>
>> >> indeed, this relates / augments record puns syntax already in
>> > GHC http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-
>> > extns.html#record-puns.
>> >
>> > Uh-oh. That documentation gives an example, and it exactly explains the
>> > weird type-level error I got when I tried to use the proposed syntax
>> > myself:
>> >
>> >Note that:
>> >
>> >* Record punning can also be used in an expression, writing, for
>> > example,
>> >
>> >let a = 1 in C {a}-- !!!
>> >
>> >instead of
>> >
>> >let a = 1 in C {a = a}
>> >
>> >The expansion is purely syntactic, so the expanded right-hand
>> side
>> > expression refers to the nearest enclosing variable that is spelled the
>> > same as the field name.
>> >
>> > IOW the proposal _does_ conflict with existing syntax. (And I guess I
>> can
>> > see a use for the example. Note that outside of that let binding, `a`
>> > would be a field selector function generated from the data decl in which
>> > field `a` appears -- that's the weirdity I got.)
>> >
>> > I suppose the existing syntax has a data constructor in front of the
>> > braces, whereas the proposal wants a term. But of course a data
>> > constructor is a term.
>> >
>> > So the proposal would be a breaking change. Rats! Is anybody using that
>> > feature?
>> >
>> >>
>> >> On Sun, Jun 30, 2013 at 2:59 AM, Judah Jacobson
>> > gmail.com> wrote:
>> >>
>> >> Unlike dot notation, this is unambiguous and doesn't conflict with any
>> > existing syntax (AFAIK). ...
>> >
>> >
>> > ___
>> > Glasgow-haskell-users mailing list
>> > Glasgow-haskell-users@haskell.org
>> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: A possible alternative to dot notation for record access
(#) is a legal operator today and is used in a number of libraries.
On Sun, Jun 30, 2013 at 11:38 PM, wrote:
> As long as we're bikeshedding...
>
> Possibly '#' is unused syntax -- Erlang uses it for its records too, so we
> wouldn't be pulling it out of thin air. E.g. "person#firstName"
>
> Tom
>
>
> El Jun 30, 2013, a las 22:59, AntC
> escribió:
>
> >> Carter Schonwald gmail.com> writes:
> >>
> >> indeed, this relates / augments record puns syntax already in
> > GHC http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-
> > extns.html#record-puns.
> >
> > Uh-oh. That documentation gives an example, and it exactly explains the
> > weird type-level error I got when I tried to use the proposed syntax
> > myself:
> >
> >Note that:
> >
> >* Record punning can also be used in an expression, writing, for
> > example,
> >
> >let a = 1 in C {a}-- !!!
> >
> >instead of
> >
> >let a = 1 in C {a = a}
> >
> >The expansion is purely syntactic, so the expanded right-hand side
> > expression refers to the nearest enclosing variable that is spelled the
> > same as the field name.
> >
> > IOW the proposal _does_ conflict with existing syntax. (And I guess I can
> > see a use for the example. Note that outside of that let binding, `a`
> > would be a field selector function generated from the data decl in which
> > field `a` appears -- that's the weirdity I got.)
> >
> > I suppose the existing syntax has a data constructor in front of the
> > braces, whereas the proposal wants a term. But of course a data
> > constructor is a term.
> >
> > So the proposal would be a breaking change. Rats! Is anybody using that
> > feature?
> >
> >>
> >> On Sun, Jun 30, 2013 at 2:59 AM, Judah Jacobson
> > gmail.com> wrote:
> >>
> >> Unlike dot notation, this is unambiguous and doesn't conflict with any
> > existing syntax (AFAIK). ...
> >
> >
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Overloaded record fields
On Thu, Jun 27, 2013 at 2:14 AM, AntC wrote:
> > Edward Kmett gmail.com> writes:
> >
> > Let me take a couple of minutes to summarize how the lens approach
> tackles the composition problem today without requiring confusing changes
> in the lexical structure of the language.
>
> Thank you Edward, I do find the lens approach absolutely formidable. And I
> have tried to read the (plentiful) documentation. But I haven't seen a
> really, really simple example that shows the correspondence with H98
> records and fields -- as simple as Adam's example in the wiki. (And this
> message from you doesn't achieve that either. Sorry, but tl;dr, and there
> isn't even a record decl in it.)
There was this one buried down near the bottom.
data Foo = Foo { _fooX, _fooY :: Int }
fooY f (Foo x y) = Foo x <$> f y
We could implement that lens more like:
fooY :: Lens' Foo Int
fooY f s = (\a -> r { _fooY = a }) <$> f (_fooY s)
if you really want to see more record sugar in there, but the code means
the same thing.
So let me show you exactly what you just asked for. The correspondence with
the getter and setter for the field:
The correspondence with the getter comes from choosing to use the
appropriate functor. With some thought it becomes obvious that it should be
Const. I won't explain why as that apparently triggers *tl;dr. *;)
s ^. l = getConst (l Const s)
Recall that fmap f (Const a) = Const a, so
s ^. fooY = getConst ((\a -> r { _fooY = a }) <$> Const (_fooY s)) =
getConst (Const (_fooY s)) = _fooY s
and we can recover the setter by choosing the Functor to be Identity.
modify l f s = runIdentity (l (Identity . f) s)
modify fooY f s = runIdentity (fooY (Identity . f) s) = runIdentity
((\a -> r { _fooY = a }) <$> (Identity . f) (_fooY s) )
if you remove the newtype noise thats the same as
modify fooY f s = s { _fooY = f (_fooY s) }
Similarly after expansion:
set fooY a s = s { _fooY = a }
I sought to give a feel for the derivation in the previous email rather
than specific examples, but to work through that and the laws takes a fair
bit of text. There isn't any getting around it.
With language support one could envision an option where record
declarations cause the generation of lenses using whatever scheme one was
going to use for the 'magic (.)' in the first place.
The only difference is you get something that can already be used as both
the getter and setter and which can be composed with other known
constructions as well, isomorphisms, getters, setters, traversals, prisms,
and indexed variants all fit this same mold and have a consistent
theoretical framework.
Does the lens approach meet SPJ's criteria of:
> * It is the smallest increment I can come up with that
>meaningfully addresses the #1 pain point (the inability to
>re-use the same field name in different records).
>
The lens approach is *orthogonal* to the SORF/DORF design issue. It simply
provides a way to make the field accessors compose together in a more
coherent way, and helps alleviate the need to conconct confusing semantics
around (.), by showing that the existing ones are enough.
* It is backward-compatible.
>
Lens already works today. So I'd dare say that the thing that works today
is compatible with what already works today, yes. ;)
[I note BTW that as the "Plan" currently stands, the '.field' postfix
> pseudo-operator doesn't rate too high on backward-compatible.]
>
> I do think that freeing up the name space by not auto-generating a record-
> type-bound field selector will help some of the naming work-rounds in the
> lens TH.
>
I'm going to risk going back into *tl;dr* territory in response to the
comment about lens TH:
Currently lens is pretty much non-commital about which strategy to use for
field naming / namespace management.
We do have three template-haskell combinators that provide lenses for
record types in lens, but they are more or less just 'what we can do in the
existing ecosystem'.
I am _not_ advocating any of these, merely describing what we already can
do today with no changes required to the language at all.
makeLenses - does the bare minimum to allow for type changing assignment
makeClassy - allows for easy 'nested record types'
makeFields - allows for highly ad hoc per field-name reuse
Consider
data Foo a = Foo { _fooBar :: Int, _fooBaz :: a }
and we can see what is generated by each.
*makeLenses ''Foo*
generates the minimum possible lens support
fooBar :: Lens' (Foo a) Int
fooBar f s = (\a -> s { _fooBar = a }) <$> f (_fooBar a)
fooBaz :: Lens (Foo a) (Foo b) a b
fooBaz f s = (\a -> s { _fooBaz = a }) <$> f (_fooBaz a)
*makeClassy ''Foo* generates
class HasFoo t a | t -> a where
foo :: Lens' t (Fo
Re: Overloaded record fields
Let me take a couple of minutes to summarize how the lens approach tackles
the composition problem today without requiring confusing changes in the
lexical structure of the language.
I'll digress a few times to showcase how this actually lets us make more
powerful tools than are available in standard OOP programming frameworks as
I go.
The API for lens was loosely inspired once upon a time by Erik Meijer's old
'the power is in the dot' paper, but the bits and pieces have nicely become
more orthogonal.
Lens unifies the notion of (.) from Haskell with the notion of (.) as a
field accessor by choosing an interesting form for the domain and codomain
of the functions it composes.
I did a far more coherent introduction at New York Haskell
http://www.youtube.com/watch?v=cefnmjtAolY&hd=1&t=75s that may be worth
sitting through if you have more time.
In particular in that talk I spend a lot of time talking about all of the
other lens-like constructions you can work with. More resources including
several blog posts, announcements, a tutorial, etc. are available on
http://lens.github.com/
A lens that knows how to get a part p out of a whole w looks like
type Lens' w p = forall f. Functor f => (p -> f p) -> w -> f w
In the talk I linked above, I show how this is equivalent to a
getter/setter pair.
Interestingly because the function is already CPSd, this composition is the
'reverse' composition you expect.
You can check that:
(.) :: Lens a b -> Lens b c -> Lens a c
The key here is that a lens is a function from a domain of (p -> f p) to
a codomain of (w -> f w) and therefore they compose with (.) from the
Prelude.
We can compose lenses that know how to access parts of a structure in a
manner analogous to writing a Traversable instance.
Lets consider the lens that accesses the second half of a tuple:
_2 f (a,b) = (,) a <$> f b
We can write a combinator that use these lenses to read and write their
respective parts:
import Control.Applicative
infixl 8 ^.
s ^. l = getConst (l Const s)
With that combinator in hand:
("hello","world")^._2 = "world"
(1,(3,4))^._2._2 = 4 -- notice the use of (.) not (^.) when chaining these.
Again this is already in the order an "OOP programmer" expects when you go
compose them!
_1 f (a,b) = (,b) <$> f a
(1,(3,4))^._2._1 = 3
The fixity of (^.) was chosen carefully so that the above parses as
(1,(3,4))^.(_2._1)
If you just write the definitions for the lenses I gave above and let type
inference give you their types they turn out to be more general than the
signature for Lens' above.
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
With that type you could choose to write the signatures above as:
_1 :: Lens (a,c) (b,c) a b
_2 :: Lens (c,a) (c,b) a b
(^.) :: s -> ((a -> Const a b) -> s -> Const a t) -> a
But we don't need the rank-2 aliases for anything other than clarity.
In particular the code above can be written and typechecked entirely
in Haskell 98.
We can also generate a 'getter' from a normal haskell function such
that it can be composed with lenses and other getters:
to :: (s -> a) -> (a -> Const r b) -> s -> Const r t
to sa acr = Const . getConst . acr . sa
x^.to f = getConst (to f Const s) = getConst ((Const . getConst .
Const . f) s) = f s
Then the examples where folks have asked to be able to just compose in
an arbitrary Haskell function become:
(1,"hello")^._2.to length = 5
We can also write back through a lens:
They take on the more general pattern that actually allows type
changing assignment.
modify :: ((a -> Identity b) -> s -> Identity t) -> (a -> b) -> s -> t
modify l ab = runIdentity . l (Identity . ab)
set l b = modify l (const b)
These can be written entirely using 'base' rather than with Identity
from transformers by replacing Identity with (->) ()
With that in hand we can state the 'Setter' laws:
modify l id = id
modify l f . modify l g = modify l (f . g)
These are just the Functor laws!
and we can of course make a 'Setter' for any Functor that you could
pass to modify:
mapped :: Functor f => (a -> Identity b) -> f a -> Identity (f b)
mapped aib = Identity . fmap (runIdentity . aib)
then you can verify that
modify mapped ab = runIdentity . Identity . fmap (Identity .
runIdentity ab) = fmap ab
modify (mapped.mapped) = fmap.fmap
'mapped' isn't a full lens. You can't read from 'mapped' with (^.).
Try it. Similarly 'to' gives you merely a 'Getter', not something
suitable to modify. You can't 'modify the output of 'to', the types
won't let you. (The lens type signatures are somewhat more complicated
here because they want the errors to be in instance resolution rather
than unification, for readability's sake)
But we can still use modify on any lens, because Identity is a
perfectly cromulent Functor.
modify _2 (+2) (1,2) = (1,4)
modify _2 length (1,"hello") = (1,5) -- notice the change of type!
modify (_2._1) (+1) (1,(2,3)) = (1,(3,3))
modify (_2.mapped) (+1) (1,[2,3,4]) = (
Re: Overloaded record fields
Note: the lens solution already gives you 'reverse function application'
with the existing (.) due to CPS in the lens type.
-Edward
On Wed, Jun 26, 2013 at 4:39 PM, Simon Peyton-Jones
wrote:
> | record projections. I would prefer to have dot notation for a
> | general, very tightly-binding reverse application, and the type of the
> record
> | selector for a field f changed to "forall r t. r { f :: t } => r -> t"
> | instead of "SomeRecordType -> t". Such a general reverse application
> dot would
> | allow things like "string.toUpper" and for me personally, it would
> | make a Haskell OO library that I'm working on more elegant...
>
> Actually I *hadn't* considered that. I'm sure it's been suggested before
> (there has been so much discussion), but I had not really thought about it
> in the context of our very modest proposal.
>
> We're proposing, in effect, that ".f" is a postfix function with type
> "forall r t. r { f :: t } => r -> t". You propose to decompose that idea
> further, into (a) reverse function application and (b) a first class
> function f.
>
> It is kind of weird that
> f . g means\x. f (g x)
> but f.gmeansg f
>
> but perhaps it is not *more* weird than our proposal.
>
> Your proposal also allows things like
>
> data T = MkT { f :: Int }
>
> foo :: [T] -> [Int]
> foo = map f xs
>
> because the field selector 'f' has the very general type you give, but the
> type signature would be enough to fix it. Or, if foo lacks a type
> signature, I suppose we'd infer
>
> foo :: (r { f::a }) => [r] -> [a]
>
> which is also fine.
>
> It also allows you to use record field names in prefix position, just as
> now, which is a good thing.
>
> In fact, your observation allows us to regard our proposal as consisting
> of two entirely orthogonal parts
> * Generalise the type of record field selectors
> * Introduce period as reverse function application
>
> Both have merit.
>
> Simon
>
> | -Original Message-
> | From: glasgow-haskell-users-boun...@haskell.org [mailto:
> glasgow-haskell-users-
> | boun...@haskell.org] On Behalf Of Dominique Devriese
> | Sent: 26 June 2013 13:16
> | To: Adam Gundry
> | Cc: glasgow-haskell-users@haskell.org
> | Subject: Re: Overloaded record fields
> |
> | I think it's a good idea to push forward on the records design because
> | it seems futile to hope for an ideal consensus proposal.
> |
> | The only thing I dislike though is that dot notation is special-cased to
> | record projections. I would prefer to have dot notation for a
> | general, very tightly-binding reverse application, and the type of the
> record
> | selector for a field f changed to "forall r t. r { f :: t } => r -> t"
> | instead of
> | "SomeRecordType -> t". Such a general reverse application dot would
> | allow things like "string.toUpper" and for me personally, it would
> | make a Haskell OO library that I'm working on more elegant...
> |
> | But I guess you've considered such a design and decided against it,
> | perhaps because of the stronger backward compatibility implications of
> | changing the selectors' types?
> |
> | Dominique
> |
> | 2013/6/24 Adam Gundry :
> | > Hi everyone,
> | >
> | > I am implementing an overloaded record fields extension for GHC as a
> | > GSoC project. Thanks to all those who gave their feedback on the
> | > original proposal! I've started to document the plan on the GHC wiki:
> | >
> | >
> http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Plan
> | >
> | > If you have any comments on the proposed changes, or anything is
> unclear
> | > about the design, I'd like to hear from you.
> | >
> | > Thanks,
> | >
> | > Adam Gundry
> | >
> | > ___
> | > Glasgow-haskell-users mailing list
> | > Glasgow-haskell-users@haskell.org
> | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> |
> | ___
> | Glasgow-haskell-users mailing list
> | Glasgow-haskell-users@haskell.org
> | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: base package (Was: GHC 7.8 release?)
Comparing hash, ptr, str gives you a pretty good acceptance/rejection test. hash for the quick rejection, ptr for quick acceptance, str for accuracy. Especially since the particular fingerprints for Typeable at least are usually made up of 3 bytestrings that were just stuffed in and forgotten about. That said, this would seem to bring ByteString or at least Ptr in at a pretty low level for the level of generality folks seem to be suddenly seeking. -Edward On Wed, Feb 20, 2013 at 12:12 PM, Ian Lynagh wrote: > On Fri, Feb 15, 2013 at 02:45:19PM +, Simon Marlow wrote: > > > > Remember that fingerprinting is not hashing. For fingerprinting we > > need to have a realistic expectation of no collisions. I don't > > think FNV is suitable. > > > > I'm sure it would be possible to replace the C md5 code with some > > Haskell. Performance *is* important here though - Typeable is in > > the inner loop of certain generic programming libraries, like SYB. > > We currently just compare > hash(str) > for equality, right? Could we instead compare > (hash str, str) > ? That would be even more correct, even if a bad/cheap hash function is > used, and would only be slower for the case where the types match > (unless you're unlucky and get a hash collision). > > In fact, we may be able to arrange it so that in the equal case the > strings are normally exactly the same string, so we can do a cheap > pointer equality test (like ByteString already does) to make the equal > case fast too (falling back to actually checking the strings are equal, > if they aren't the same string). > > > Thanks > Ian > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: data kinds
This has the problem that kind is currently a valid function name, so it would take a new keyword, or at least on conditional on the DataKinds extension. -Edward On Sun, Jan 27, 2013 at 3:02 AM, Erik Hesselink wrote: > When we discussed this last time (summarized by the link Pedro sent, I >> think) it came up that it might be nice to also >> have kind synonyms, which would be analogous to type synonyms, but one >> level up. The "natural" syntax for that would be to have a "type kind" >> declaration, but this seems a bit confusing... >> > > What about just 'kind'? It's symmetric with 'type'. > > Erik > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Newtype wrappers
No magic coercing is present in the proposal. You need to use explicit newtype wrap and newtype unwrap expressions. Sent from my iPad On Jan 14, 2013, at 6:42 PM, Johan Tibell wrote: > On Mon, Jan 14, 2013 at 3:40 PM, Evan Laforge wrote: >> Wait, what's the runtime error? Do you mean messing up Set's invariants? > > Yes. > >> If you as the library writer don't want to allow unsafe things, then >> don't export the constructor. Then no one can break your invariants, >> even with newtype malarky. If you as the the library user go and >> explicitly import the bare Set constructor from (theoretical) >> Data.Set.Unsafe, then you are in the position to break Set's internal >> invariants anyway, and have already accepted the great power / great >> responsibility tradeoff. > > If it's explicit that this is what you're doing I'm fine with it. I > just don't want magic coercing depending on what's in scope. > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Newtype wrappers
Actually upon reflection, this does appear to help with implementing some
things in my code with a much reduced unsafeCoerce count, though it remains
orthogonal to the issue of how to lift these things through third-party
types that I raised above.
-Edward
On Mon, Jan 14, 2013 at 5:40 PM, Edward Kmett wrote:
> It sounds like the solution you are proposing then is to an issue largely
> orthogonal to the one I'm talking about.
>
> As far as I can tell, I derive no immediate benefit from this version.
>
> -Edward
>
> On Mon, Jan 14, 2013 at 4:09 PM, Simon Peyton-Jones > wrote:
>
>> If you are worrying about #1496, don’t worry; we must fix that, and the
>> fix will apply to newtype wrappers.
>>
>>
>> If you are worrying about something else, can you articulate what the
>> something else is?
>>
>> ** **
>>
>> I don’t want to involve type classes, nor Functor. We don’t even have a
>> good way to say “is a functor of its second type argument” for a type
>> constructor of three arguments.
>>
>> ** **
>>
>> Simon
>>
>> ** **
>>
>> ** **
>>
>> ** **
>>
>> *From:* Edward Kmett [mailto:ekm...@gmail.com]
>> *Sent:* 14 January 2013 18:39
>> *To:* Simon Peyton-Jones
>> *Cc:* GHC users
>> *Subject:* Re: Newtype wrappers
>>
>> ** **
>>
>> Many of us definitely care. =)
>>
>> ** **
>>
>> The main concern that I would have is that the existing solutions to this
>> problem could be implemented while retaining SafeHaskell, and I don't see
>> how a library that uses this can ever recover its SafeHaskell guarantee.*
>> ***
>>
>> ** **
>>
>> Here is a straw man example of a solution that permits SafeHaskell in the
>> resulting code that may be useful in addition to or in lieu of your
>> proposed approach:
>>
>> ** **
>>
>> We could extend Data.Functor with an fmap# operation that was only, say,
>> exposed via Data.Functor.Unsafe:
>>
>> ** **
>>
>> {-# LANGUAGE Unsafe, MagicHash #-}
>>
>> module Data.Functor.Unsafe where
>>
>> class Functor f where
>>
>> fmap# :: (a -> b) -> f a -> f b
>>
>> fmap :: (a -> b) -> f a -> f b
>>
>> (<$) :: b -> f a -> f b
>>
>> fmap# = \f -> \fa -> fa `seq` fmap f p
>>
>> ** **
>>
>> Then we flag Data.Functor as Trustworthy and export just the safe subset:
>>
>>
>> ** **
>>
>> {-# LANGUAGE Trustworthy #-}
>>
>> module Data.Functor (Functor(fmap,(<$))) where
>>
>> import Data.Functor.Unsafe
>>
>> ** **
>>
>> then fmap# from Data.Functor.Unsafe is allowed to be fmap# _ =
>> unsafeCoerce for any Functor that doesn't perform GADT-like interrogation
>> of its argument (this could be assumed automatically in DeriveFunctor,
>> which can't handle those cases anyways!)
>>
>> ** **
>>
>> Then any user who wants to enable a more efficient fmap for fmapping over
>> his data type with a newtype instantiates fmap# for his Functor. They'd
>> have to claim Trustworthy (or use the enhanced DeriveFunctor), to discharge
>> the obligation that they aren't introducing an unsafeCoerce that is visible
>> to the user. (After all the user has to import another Unsafe module to get
>> access to fmap# to invoke it.)
>>
>> ** **
>>
>> Finally then code that is willing to trust other trustworthy code can
>> claim to be Trustworthy in turn, import Data.Functor.Unsafe and use fmap#
>> for newtypes and impossible arguments:
>>
>> ** **
>>
>> {-# LANGUAGE Trustworthy #-}
>>
>> module Data.Void where
>>
>> ** **
>>
>> import Data.Functor.Unsafe
>>
>> ** **
>>
>> newtype Void = Void Void deriving Functor
>>
>> ** **
>>
>> absurd :: Void -> a
>>
>> absurd (Void a) = absurd a
>>
>> ** **
>>
>> vacuous :: Functor f => f Void -> f a
>>
>> vacuous = fmap# absurd
>>
>> ** **
>>
>> This becomes valuable when data types like Void are used to mark the
>> absence of variables in a syntax tree, which could be quite large.
>>
>> ** **
>>
>> Currently we have to fmap absurd over the tree, paying an asymptotic cost
>> for not using (forall a. Expr a) or some newtype wrapped e
Re: Newtype wrappers
It sounds like the solution you are proposing then is to an issue largely
orthogonal to the one I'm talking about.
As far as I can tell, I derive no immediate benefit from this version.
-Edward
On Mon, Jan 14, 2013 at 4:09 PM, Simon Peyton-Jones
wrote:
> If you are worrying about #1496, don’t worry; we must fix that, and the
> fix will apply to newtype wrappers.
>
>
> If you are worrying about something else, can you articulate what the
> something else is?
>
> ** **
>
> I don’t want to involve type classes, nor Functor. We don’t even have a
> good way to say “is a functor of its second type argument” for a type
> constructor of three arguments.
>
> ** **
>
> Simon****
>
> ** **
>
> ** **
>
> ** **
>
> *From:* Edward Kmett [mailto:ekm...@gmail.com]
> *Sent:* 14 January 2013 18:39
> *To:* Simon Peyton-Jones
> *Cc:* GHC users
> *Subject:* Re: Newtype wrappers
>
> ** **
>
> Many of us definitely care. =)
>
> ** **
>
> The main concern that I would have is that the existing solutions to this
> problem could be implemented while retaining SafeHaskell, and I don't see
> how a library that uses this can ever recover its SafeHaskell guarantee.**
> **
>
> ** **
>
> Here is a straw man example of a solution that permits SafeHaskell in the
> resulting code that may be useful in addition to or in lieu of your
> proposed approach:
>
> ** **
>
> We could extend Data.Functor with an fmap# operation that was only, say,
> exposed via Data.Functor.Unsafe:
>
> ** **
>
> {-# LANGUAGE Unsafe, MagicHash #-}
>
> module Data.Functor.Unsafe where
>
> class Functor f where
>
> fmap# :: (a -> b) -> f a -> f b
>
> fmap :: (a -> b) -> f a -> f b
>
> (<$) :: b -> f a -> f b
>
> fmap# = \f -> \fa -> fa `seq` fmap f p
>
> ** **
>
> Then we flag Data.Functor as Trustworthy and export just the safe subset:*
> ***
>
> ** **
>
> {-# LANGUAGE Trustworthy #-}
>
> module Data.Functor (Functor(fmap,(<$))) where
>
> import Data.Functor.Unsafe
>
> ** **
>
> then fmap# from Data.Functor.Unsafe is allowed to be fmap# _ =
> unsafeCoerce for any Functor that doesn't perform GADT-like interrogation
> of its argument (this could be assumed automatically in DeriveFunctor,
> which can't handle those cases anyways!)
>
> ** **
>
> Then any user who wants to enable a more efficient fmap for fmapping over
> his data type with a newtype instantiates fmap# for his Functor. They'd
> have to claim Trustworthy (or use the enhanced DeriveFunctor), to discharge
> the obligation that they aren't introducing an unsafeCoerce that is visible
> to the user. (After all the user has to import another Unsafe module to get
> access to fmap# to invoke it.)
>
> ** **
>
> Finally then code that is willing to trust other trustworthy code can
> claim to be Trustworthy in turn, import Data.Functor.Unsafe and use fmap#
> for newtypes and impossible arguments:
>
> ** **
>
> {-# LANGUAGE Trustworthy #-}
>
> module Data.Void where
>
> ** **
>
> import Data.Functor.Unsafe
>
> ** **
>
> newtype Void = Void Void deriving Functor
>
> ** **
>
> absurd :: Void -> a
>
> absurd (Void a) = absurd a
>
> ** **
>
> vacuous :: Functor f => f Void -> f a
>
> vacuous = fmap# absurd
>
> ** **
>
> This becomes valuable when data types like Void are used to mark the
> absence of variables in a syntax tree, which could be quite large.
>
> ** **
>
> Currently we have to fmap absurd over the tree, paying an asymptotic cost
> for not using (forall a. Expr a) or some newtype wrapped equivalent as our
> empty-expression type.
>
> ** **
>
> This would dramatically improve the performance of libraries like bound
> which commonly use constructions like Expr Void.
>
> ** **
>
> Its safety could be built upon by making another class for tracking
> newtypes etc so we can know whats safe to pass to fmap#, and you might be
> able to spot opportunities to rewrite an explicit fmap of something that is
> a `cast` in the core to a call to fmap#.
>
> ** **
>
> -Edward
>
> ** **
>
> On Mon, Jan 14, 2013 at 1:09 PM, Simon Peyton-Jones
> wrote:
>
> Friends
>
>
>
> I’d like to propose a way to “promote” newtypes over their enclosing
> type. Here’s the writeup
>
> http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers
>
>
>
> Any comments? Below is the problem
Re: Newtype wrappers
Many of us definitely care. =)
The main concern that I would have is that the existing solutions to this
problem could be implemented while retaining SafeHaskell, and I don't see
how a library that uses this can ever recover its SafeHaskell guarantee.
Here is a straw man example of a solution that permits SafeHaskell in the
resulting code that may be useful in addition to or in lieu of your
proposed approach:
We could extend Data.Functor with an fmap# operation that was only, say,
exposed via Data.Functor.Unsafe:
{-# LANGUAGE Unsafe, MagicHash #-}
module Data.Functor.Unsafe where
class Functor f where
fmap# :: (a -> b) -> f a -> f b
fmap :: (a -> b) -> f a -> f b
(<$) :: b -> f a -> f b
fmap# = \f -> \fa -> fa `seq` fmap f p
Then we flag Data.Functor as Trustworthy and export just the safe subset:
{-# LANGUAGE Trustworthy #-}
module Data.Functor (Functor(fmap,(<$))) where
import Data.Functor.Unsafe
then fmap# from Data.Functor.Unsafe is allowed to be fmap# _ = unsafeCoerce
for any Functor that doesn't perform GADT-like interrogation of its
argument (this could be assumed automatically in DeriveFunctor, which can't
handle those cases anyways!)
Then any user who wants to enable a more efficient fmap for fmapping over
his data type with a newtype instantiates fmap# for his Functor. They'd
have to claim Trustworthy (or use the enhanced DeriveFunctor), to discharge
the obligation that they aren't introducing an unsafeCoerce that is visible
to the user. (After all the user has to import another Unsafe module to get
access to fmap# to invoke it.)
Finally then code that is willing to trust other trustworthy code can claim
to be Trustworthy in turn, import Data.Functor.Unsafe and use fmap# for
newtypes and impossible arguments:
{-# LANGUAGE Trustworthy #-}
module Data.Void where
import Data.Functor.Unsafe
newtype Void = Void Void deriving Functor
absurd :: Void -> a
absurd (Void a) = absurd a
vacuous :: Functor f => f Void -> f a
vacuous = fmap# absurd
This becomes valuable when data types like Void are used to mark the
absence of variables in a syntax tree, which could be quite large.
Currently we have to fmap absurd over the tree, paying an asymptotic cost
for not using (forall a. Expr a) or some newtype wrapped equivalent as our
empty-expression type.
This would dramatically improve the performance of libraries like bound
which commonly use constructions like Expr Void.
Its safety could be built upon by making another class for tracking
newtypes etc so we can know whats safe to pass to fmap#, and you might be
able to spot opportunities to rewrite an explicit fmap of something that is
a `cast` in the core to a call to fmap#.
-Edward
On Mon, Jan 14, 2013 at 1:09 PM, Simon Peyton-Jones
wrote:
> Friends
>
> ** **
>
> I’d like to propose a way to “promote” newtypes over their enclosing
> type. Here’s the writeup
>
> http://hackage.haskell.org/trac/ghc/wiki/NewtypeWrappers
>
> ** **
>
> Any comments? Below is the problem statement, taken from the above page.*
> ***
>
> ** **
>
> I’d appreciate
>
> **· **A sense of whether you care. Does this matter?
>
> **· **Improvements to the design I propose
>
> ** **
>
> Simon
>
> ** **
>
> ** **
>
> ** **
>
> *The problem*
>
> Suppose we have
>
> newtype Age = MkAge Int
>
> Then if n :: Int, we can convert n to an Age thus: MkAge n :: Age.
> Moreover, this conversion is a type conversion only, and involves no
> runtime instructions whatsoever. This cost model -- that newtypes are free
> -- is important to Haskell programmers, and encourages them to use newtypes
> freely to express type distinctions without introducing runtime overhead.
>
>
> Alas, the newtype cost model breaks down when we involve other data
> structures. Suppose we have these declarations
>
> data T a = TLeaf a | TNode (Tree a) (Tree a)
>
> data S m a = SLeaf (m a) | SNode (S m a) (S m a)
>
> and we have these variables in scope
>
> x1 :: [Int]
>
> x2 :: Char -> Int
>
> x3 :: T Int
>
> x4 :: S IO Int
>
> Can we convert these into the corresponding forms where the Int is
> replaced by Age? Alas, not easily, and certainly not without overhead. ***
> *
>
>- For x1 we can write map MkAge x1 :: [Age]. But this does not follow
>the newtype cost model: there will be runtime overhead from executing the
>map at runtime, and sharing will be lost too. Could GHC optimise the
>map somehow? This is hard; apart from anything else, how would GHC
>know that map was special? And it it gets worse.
>
>
>- For x2 we'd have to eta-expand: (\y -> MkAge (x2 y)) :: Char -> Age.
>But this isn't good either, because eta exapansion isn't semantically valid
>(if x2 was bottom, seq could distinguish the two). See
> #7542for a real life example.
>
>
>
>- For x3, we'd have to map over T, thus mapT MkAge x3.
Re: Generating random type-level naturals
; having dependent types in Haskell. The answer to this is also given in the >> paper, but I'll cut to the chase. The basic idea is that we just need to be >> able to hide our dependent types from the compiler. That is, we can't >> define: >> >> reifyInt :: (n::Int) -> ...n... >> >> but only because we're not allowed to see that pesky n. And the reason >> we're not allowed to see it is that it must be some particular fixed value >> only we don't know which one. But, if we can provide a function eliminating >> n, and that function works for all n, then it doesn't matter what the >> actual value is since we're capable of eliminating all of them: >> >> reifyInt :: Int -> (forall n. ReflectNum n => n -> a) -> a >> >> This is just the standard CPS trick we also use for dealing with >> existentials and other pesky types we're not allowed to see. Edward Kmett >> has a variation of this theme already on Hackage: >> >> >> http://hackage.haskell.org/**package/reflection<http://hackage.haskell.org/package/reflection> >> >> It doesn't include the implementation of type-level numbers, so you'll >> want to look at the paper to get an idea about that, but the reflection >> package does generalize to non-numeric types as well. >> >> -- >> Live well, >> ~wren >> >> >> __**_ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.**org >> http://www.haskell.org/**mailman/listinfo/glasgow-**haskell-users<http://www.haskell.org/mailman/listinfo/glasgow-haskell-users> >> > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: TypeHoles: unbound variables as named holes
On Fri, Oct 5, 2012 at 10:22 AM, Sean Leather wrote: > I also like the proposal; however, I think it only makes sense if the set > of unbound variables with the same name is treated as referring to the same > identifier. This was, after all, the main reason for named holes. Roman > expected this, and I think everybody who uses the feature will expect it. > I for one wasn't expecting it, so I guess that makes me fall outside of the scope of everybody. ;) The main thing I like about Simon's proposal is that I could just drop an _foo in my file, and when I open it back up with vim or what have you /_foo to find my way back to it. > Here's a thought that just occurred to me, though I'm not yet sure if it > makes sense. Treat all expression identifiers _x as unique but report them > as one hole with all possible types. Then, you can visually identify the > patterns between the types. So: > > > f x = _y > > g x = _y 'a' > > with some warning like this: > > Found hole `_y' in multiple locations with the possible types > File.hs:##:##: a0 > File.hs:##:##: Char -> b0 > > Now, I know by looking at it that `a0' and `b0' are universally quantified > per location, but I can do some mental unification myself. > There is the slight complication that the inscope variables shown for each location would be in different unification contexts as well, so your list gets a lot more cluttered, and the in scope variables probably should be grouped with each in turn, so I'm not sure this is any better than listing them separately by the time you factor in that clutter. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Comments on current TypeHoles implementation
I really like this proposal.
-Edward
On Thu, Oct 4, 2012 at 5:40 AM, Simon Peyton-Jones wrote:
> There is also the small matter, in this example, of distinguishing which
> `_' is which. The description works, but you have to think about it. I
> don't have an immediate and simple solution to this. Perhaps the addition
> of unique labels (e.g. _$1 _$2). But this is not a major problem. It can
> even wait until some future development/expansion on TypeHoles.
>
> ** **
>
> I have a proposal. Someone has already suggested on
> hackage.haskell.org/trac/ghc/ticket/5910 that an un-bound variable
> behaves like a hole. Thus, if you say
>
> ** **
>
> f x = y
>
> GHC says “Error: y is not in scope”. But (idea) with -XTypeHoles
>
> ** **
>
> f x = y
>
> might generate
>
> **1. **(renamer) *Warning*: y is not in scope
>
> **2. **(type) *Error*: Hole “y” has type
>
> So that’s like a named hole, in effect.
>
> ** **
>
> If you say
>
>f x = 4
>
> GHC warns about the unused binding for x. But if you say
>
>f _x = 4
>
> the unused-binding warning is suppressed. So (idea) if you say
>
> f x = _y
>
> maybe we can suppress warning (1). And, voila, named holes.
>
> ** **
>
> Moreover if you add –fdefer-type-errors you can keep going and run the
> program.
>
> ** **
>
> Any comments? This is pretty easy to do.
>
> ** **
>
> (I’m unhappy that –XTypeHoles is a language pragma while
> –fdefer-type-errors is a compiler flag. Maybe we should have
> –XDeferTypeErrors?)
>
> ** **
>
> Simon
>
> ** **
>
> ** **
>
> ** **
>
> *From:* sean.leat...@gmail.com [mailto:sean.leat...@gmail.com] *On Behalf
> Of *Sean Leather
> *Sent:* 03 October 2012 16:45
> *To:* Simon Peyton-Jones
> *Cc:* GHC Users List; Thijs Alkemade
> *Subject:* Comments on current TypeHoles implementation
>
> ** **
>
> Hi Simon,
>
> ** **
>
> Thanks for all your work in getting TypeHoles into HEAD. We really
> appreciate it.
>
> ** **
>
> I was playing around with HEAD today and wanted to share a few
> observations.
>
> ** **
>
> (1) One of the ideas we had was that a hole `_' would be like `undefined'
> but with information about the type and bindings. But in the current
> version, there doesn't appear to be that connection. This mainly applies
> to ambiguous type variables.
>
> ** **
>
> Consider:
>
> > f = show _
>
> The hole has type a0.
>
> ** **
>
> But with
>
> > f = show undefined
>
> there is a type error because a0 is ambiguous.
>
> ** **
>
> We were thinking that it would be better to report the ambiguous type
> variable first, rather than the hole. In that case, tou can use
> -fdefer-type-errors to defer the error. Currently, you don't have that
> option. I can see the argument either way, however, and I'm not sure which
> is better.
>
> ** **
>
> (2) There is a strange case where an error is not reported for a missing
> type class instance, even though there is no (apparent) relation between
> the missing instance and the hole. (This also relates to the connection
> to `undefined', but less directly.)
>
> ** **
>
> We have the following declaration:
>
> > data T = T Int {- no Show instance -}
>
> ** **
>
> With a hole in the field
>
> > g = show (T _)
>
> we get a message that the hole has type Int.
>
> ** **
>
> With
>
> > g = show (T undefined)
>
> we get an error for the missing instance of `Show T'.
>
> ** **
>
> (3) In GHCi, I see that the type of the hole now defaults. This is not
> necessarily bad, though it's maybe not as useful as it could be.
>
> ** **
>
> ghci> :t show _
>
> reports that the hole has type ().
>
> ** **
>
> (4) In GHCi, sometimes a hole throws an exception, and sometimes it does
> not.
>
> ** **
>
> ghci> show _
>
> throws an exception with the hole warning message
>
> ** **
>
> ghci> show (T _)
>
> and
>
> ghci> _ + 42
>
> cause GHCi to panic.
>
> ** **
>
> (5) There are some places where unnecessary parentheses are used when
> pretty-printing the code:
>
> ** **
>
> ghci> :t _ _
>
> ** **
>
> :1:1: Warning:
>
> Found hole `_' with type t0 -> t
>
> Where: `t0' is a free type variable
>
>`t' is a rigid type variable bound by
>
>the inferred type of it :: t at Top level
>
> In the expression: _
>
> In the expression: _ (_)
>
> ** **
>
> :1:3: Warning:
>
> Found hole `_' with type t0
>
> Where: `t0' is a free type variable
>
> In the first argument of `_', namely `_'
>
> In the expression: _ (_)
>
> _ _ :: t
>
> ** **
>
> The argument `_' does not need to be printed as `(_)'.
>
> ** **
>
> There is also the small matter, in this example, of distinguishing which
> `_' is which. The description works, but you have to think about it. I
> don't have an immediate and
Re: Comments on current TypeHoles implementation
On Wed, Oct 3, 2012 at 11:44 AM, Sean Leather wrote: > Hi Simon, > > Thanks for all your work in getting TypeHoles into HEAD. We really > appreciate it. > > I was playing around with HEAD today and wanted to share a few > observations. > > (1) One of the ideas we had was that a hole `_' would be like `undefined' > but with information about the type and bindings. But in the current > version, there doesn't appear to be that connection. This mainly applies > to ambiguous type variables. > > Consider: > > f = show _ > The hole has type a0. > > But with > > f = show undefined > there is a type error because a0 is ambiguous. > > We were thinking that it would be better to report the ambiguous type > variable first, rather than the hole. In that case, tou can use > -fdefer-type-errors to defer the error. Currently, you don't have that > option. I can see the argument either way, however, and I'm not sure which > is better. > At least in the first case I would actually prefer it not to complain about the ambiguity. The point of putting the hole in is to figure out the type that something going into that location should have and what information I have available to use to plug that hole. An 'undefined' _is_ ambiguous, but _ is a placeholder for code that presumably will be valid when it gets expanded. If I have to put a type annotation on it to avoid the compiler dumping out with an error about an ambiguous hole that would seem to me at least to largely defeat the very utility of holes. I would further suspect there are places where you'll be putting holes that have higher rank types, and where undefined might complain. I largely agree with but don't really have a deep opinion on the other issues you raised, though. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why is Bag's Data instance "broken"?
The missing dataCast1 is just a bug, yes. I suppose someone who uses Bag
and cares can submit something about fixing gunfold.
On Thu, Sep 20, 2012 at 7:22 AM, José Pedro Magalhães wrote:
> Right now I was just planning to fix the missing dataCast1 from Bag, and
> the rest from
> Data.Data (see http://hackage.haskell.org/trac/ghc/ticket/7256). I think
> those are just
> a bug, unrelated to the abstraction story, no?
>
>
> Cheers,
> Pedro
>
>
> On Thu, Sep 20, 2012 at 12:19 PM, Edward Kmett wrote:
>
>> Note: It was probably built with an eye towards how Data.Map and the like
>> performed abstraction. However, This isn't necessary to protect the
>> invariants of a bag.
>>
>> The constructors exposed via Data do not have to be the actual
>> constructors of the data type. With this you can quotient out the portions
>> of the structure you don't want the user to be able to inspect.
>>
>> See the libraries@ proposal that I put in 3-4 weeks ago (which will have
>> just passed) to fix all the broken Data instances for containers by using
>> virtual constructors such as 'fromList', (which incidentally led to Milan
>> finding huge space and time improvements in fromList).
>>
>> Effectively allowing the user to use the 'listToBag' as a "constructor"
>> loses no information violates no invariants, and prevents code written for
>> uniplate, SYB, etc. from having to crash, panic or give up upon the sight
>> of a mkNoRepType.
>>
>> My reaction for years to the sight of a mkNoRepType and undefined gunfold
>> has been to hang my head. Now I just fix them.
>>
>> -Edward
>>
>> On Wed, Aug 29, 2012 at 7:11 AM, José Pedro Magalhães wrote:
>>
>>> Hi Philip,
>>>
>>> On Wed, Aug 29, 2012 at 12:01 PM, Philip Holzenspies <
>>> p...@st-andrews.ac.uk> wrote:
>>>
>>>> Dear GHCers,
>>>>
>>>> I'm performing traversals over GHC-API results (HsSyn et al). For this
>>>> purpose, I'm using SYB generics.
>>>>
>>>> I found that I couldn't use "ext1Q" for a function with type "Data x =>
>>>> Bag x -> String", i.e. that this function was never applied. The source of
>>>> Bag's instance of the Data class seems to explain why:
>>>>
>>>>
>>>> instance Data a => Data (Bag a) where
>>>> gfoldl k z b = z listToBag `k` bagToList b -- traverse abstract type
>>>> abstractly
>>>> toConstr _ = abstractConstr $ "Bag("++show (typeOf
>>>> (undefined::a))++")"
>>>> gunfold _ _ = error "gunfold"
>>>> dataTypeOf _ = mkNoRepType "Bag"
>>>>
>>>>
>>>> Is there a rationale to not allow gunfolds and to keep toConstr
>>>> abstract?
>>>
>>>
>>> As far as I understand, this is to keep `Bag` itself abstract,
>>> preventing users from inspecting its internals.
>>>
>>>
>>>> More to the point for my needs, is there a reason to not allow
>>>> dataCast1 casting of Bags?
>>>>
>>>
>>> That is a separate issue; I believe this instance is just missing a
>>> `dataCast1 = gcast1` line.
>>> All datatypes of kind `* -> *` should have such a definition.
>>>
>>> (Having a look at Data.Data, I guess the same applies to `Ptr a` and
>>> `ForeignPtr a`.
>>> And `Array a b` seems to be missing the `dataCast2` method. I propose
>>> fixing all of these.)
>>>
>>>
>>> Cheers,
>>> Pedro
>>>
>>>
>>>>
>>>> Regards,
>>>> Philip
>>>> ___
>>>> Glasgow-haskell-users mailing list
>>>> Glasgow-haskell-users@haskell.org
>>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>>
>>>
>>>
>>> ___
>>> Glasgow-haskell-users mailing list
>>> Glasgow-haskell-users@haskell.org
>>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>>
>>>
>>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why is Bag's Data instance "broken"?
Note: It was probably built with an eye towards how Data.Map and the like
performed abstraction. However, This isn't necessary to protect the
invariants of a bag.
The constructors exposed via Data do not have to be the actual constructors
of the data type. With this you can quotient out the portions of the
structure you don't want the user to be able to inspect.
See the libraries@ proposal that I put in 3-4 weeks ago (which will have
just passed) to fix all the broken Data instances for containers by using
virtual constructors such as 'fromList', (which incidentally led to Milan
finding huge space and time improvements in fromList).
Effectively allowing the user to use the 'listToBag' as a "constructor"
loses no information violates no invariants, and prevents code written for
uniplate, SYB, etc. from having to crash, panic or give up upon the sight
of a mkNoRepType.
My reaction for years to the sight of a mkNoRepType and undefined gunfold
has been to hang my head. Now I just fix them.
-Edward
On Wed, Aug 29, 2012 at 7:11 AM, José Pedro Magalhães wrote:
> Hi Philip,
>
> On Wed, Aug 29, 2012 at 12:01 PM, Philip Holzenspies <
> p...@st-andrews.ac.uk> wrote:
>
>> Dear GHCers,
>>
>> I'm performing traversals over GHC-API results (HsSyn et al). For this
>> purpose, I'm using SYB generics.
>>
>> I found that I couldn't use "ext1Q" for a function with type "Data x =>
>> Bag x -> String", i.e. that this function was never applied. The source of
>> Bag's instance of the Data class seems to explain why:
>>
>>
>> instance Data a => Data (Bag a) where
>> gfoldl k z b = z listToBag `k` bagToList b -- traverse abstract type
>> abstractly
>> toConstr _ = abstractConstr $ "Bag("++show (typeOf
>> (undefined::a))++")"
>> gunfold _ _ = error "gunfold"
>> dataTypeOf _ = mkNoRepType "Bag"
>>
>>
>> Is there a rationale to not allow gunfolds and to keep toConstr abstract?
>
>
> As far as I understand, this is to keep `Bag` itself abstract, preventing
> users from inspecting its internals.
>
>
>> More to the point for my needs, is there a reason to not allow dataCast1
>> casting of Bags?
>>
>
> That is a separate issue; I believe this instance is just missing a
> `dataCast1 = gcast1` line.
> All datatypes of kind `* -> *` should have such a definition.
>
> (Having a look at Data.Data, I guess the same applies to `Ptr a` and
> `ForeignPtr a`.
> And `Array a b` seems to be missing the `dataCast2` method. I propose
> fixing all of these.)
>
>
> Cheers,
> Pedro
>
>
>>
>> Regards,
>> Philip
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher wrote: > Hi, > > Note that nobody was suggesting two pragmas with incompatible behaviors, > only to have just one symbol reserved to still be able to have type > operator variables. > An issue with reserving a symbol for type operator variables is it doesn't help you today. 7.6.1 is already released. This means that any change in behavior would have to be in 7.6.2 at the earliest. Assuming the bikeshedding could complete and Simon et al. frantically patched the code tomorrow, rushing to release a 7.6.2 before the platform release. Failing that, you'd have a whole release cycle to wait through, probably a platform, before you could go back to your old behavior, and then your code would have some strange gap of GHC version numbers over which it didn't work. Everyone would have to pretend 7.6.1 never happened, or and break anyone's code that was already written for 7.6, so instead of one breaking change, we'd now have two. For instance, I'm already using ~> in 'github.com/ekmett/indexed.git' for natural transformations and I am loving it, and would be sad to lose it to the choice of ~ as a herald, similarly it would make the >~c~> trick more verbose, and ~ is particularly terrible for operators like ~+~. Other herald choices lead to different issues, '.' is slightly better for the other operators, but makes kind of ugly arrows, plus some day i'd _really_ like to be able to use . as a type constructor for functor composition! It is currently reserved at the type level as an almost accidental consequence of the way forall gets parsed today. I really like Iavor's entirely-in-language way of addressing the issue, due in part to it providing even better associativity than the existing approach, and honestly, even if GHC HQ was somehow convinced to set aside an ad hoc herald for type variables, I'd probably start using it in my code. (probably sandwiching between something like :- and :> for old GHC compatibility). I really like that I can just call the Category c, and just get >~c~> or something similar as its arrows. This feels more notationally accurate to me. It also has two major benefits compared to any proposal for adding different heralds: 1.) It is compatible with old code, code written with 7.6.1 and I suppose future code, since (:) is such a remarkably awkward choice of herald for the reasons already documented that it seems an unlikely choice. 2.) I can program with it today. I just realized if you don't want to worry about collisions with the type naturals from GHC.TypeLits, and didn't care about pre-7.6 compatibility, you could strip the notation down all the way to cmap :: CFunctor f c d => (x -c> y) -> f x -d> f y This is even shorter than the conventional cmap :: CFunctor f (~>) (~~>) => (x ~> y) -> f x ~~> f y Which turns the "but it is longer" argument against it on its head. ;) -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
Iavor: Wow, I really like the >--c--> trick at the type level.
Note: we can shorten that somewhat and improve the fixity to associate
correctly, matching the associativity of (->), which fortunately associates
to the right. (associating to the left can be done with a similar trick,
based on the original version of this hack by Chung-Chieh Shan.)
{-# LANGUAGE TypeOperators, PolyKinds #-}
import Control.Category
infixr 0 >~
infixr 0 ~>
type (>~) a b = b a
type (~>) a b = a b
g :: Category c => (x >~c~> y) -> (y >~c~> z) -> x >~c~> z
g = undefined
Note, this also has the benefit of picking the correct associativity for
>~c~>. Unlike naively using a locally bound (~>) and avoids the headaches
of picking (-->) and (--->) or something equally hideous when working with
two categories.
class (Category c, Category d) => CFunctor f c d | f c -> d, f d -> c where
cmap :: (a >~c~> b) -> f a >~d~> f b
-Edward
On Mon, Sep 17, 2012 at 1:02 PM, Sjoerd Visscher wrote:
> Hi,
>
> Note that nobody was suggesting two pragmas with incompatible behaviors,
> only to have just one symbol reserved to still be able to have type
> operator variables.
>
> I do like your suggestion, although >--c--> is quite a bit longer than ~>.
>
> Sjoerd
>
> On Sep 17, 2012, at 6:28 PM, Iavor Diatchki wrote:
>
> Hello,
>
> I think that it would be a mistake to have two pragmas with incompatible
> behaviors: for example, we would not be able to write modules that use
> Conal's libraries and, say, the type nats I've been working on.
> If the main issue is the notation for arrows, has anoyone played with what
> can be done with the current (7.6) system? I just thought of two
> variations that seem to provide a decent notation for writing arrow-ish
> programs. The second one, in particular, mirrors the arrow notation at the
> value level, so perhaps that would be enough?
>
> -Iavor
>
>
> {-# LANGUAGE TypeOperators, KindSignatures #-}
> module Test where
>
> import Control.Category
>
> -- Variant 1: Post-fix annotation
>
> type (a ---> b) c = c a b
>
> f :: Category c => (x ---> y) c -> (y ---> z) c -> (x ---> z) c
> f = undefined
>
>
> -- Variant 2: Arrow notation
>
> type a >-- (c :: * -> * -> *) = c a
> type c --> b = c b
>
> infix 2 >--
> infix 1 -->
>
> g :: Category c => (x >--c--> y) -> (y >--c--> z) -> (x >--c--> z)
> g = undefined
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type operators in GHC
One issue with this proposal is it makes it *completely* impossible to pick
a type constructor operator that works with both older GHCs and 7.6.
It is a fairly elegant choice, but in practice it would force me and many
others to stop using them completely for the next couple of years, as I
wouldn't be able to support any users on older GHCs, or if I did I would
have to export completely different operator names, and then the users
would have to use conditional compilation to do different things with them.
=/
As it is, I can and do at least choose : prefixed names for any type
constructor I want to have be compatible with old GHCs.
Back when the change was initially proposed I think it was Igloo who
suggested that it might be possible to allow the use of symbols as type
variables if they were explicitly quantified by a forall.
Would that be a viable approach?
-Edward
On Fri, Sep 14, 2012 at 7:26 PM, Simon Peyton-Jones
wrote:
> Fair point. So you are saying it’d be ok to say
>
> ** **
>
> data T (.->) = MkT (Int .-> Int)
>
> ** **
>
> where (.+) is a type variable? Leaving ordinary (+) available for type
> constructors.
>
> ** **
>
> If we are inverting the convention I wonder whether we might invert it
> completely and use “:” as the “I’m different” herald as we do for **
> constructor** operators in terms. Thus
>
> ** **
>
> data T (:->) = MkT (Int :-> Int)
>
> ** **
>
> That seems symmetrical, and perhaps nicer than having a new notation. ***
> *
>
>
>
> In terms In types***
> *
>
> ---***
> *
>
> aTerm variable Type variable
>
> AData constructor Type constructor
>
> +Term variable operator Type constructor operator***
> *
>
> :+ Data constructor operator Type variable operator
>
> ** **
>
> Any other opinions?
>
> ** **
>
> Simon
>
> ** **
>
> *From:* conal.elli...@gmail.com [mailto:conal.elli...@gmail.com] *On
> Behalf Of *Conal Elliott
> *Sent:* 06 September 2012 23:59
>
> *To:* Simon Peyton-Jones
> *Cc:* GHC users
> *Subject:* Re: Type operators in GHC
>
> ** **
>
> Oh dear. I'm very sorry to have missed this discussion back in January.
> I'd be awfully sad to lose pretty infix notation for type variables of kind
> * -> * -> *. I use them extensively in my libraries and projects, and
> pretty notation matters.
>
>
> I'd be okay switching to some convention other than lack of leading ':'
> for signaling that a symbol is a type variable rather than constructor,
> e.g., the *presence* of a leading character such as '.'.
>
> Given the increasing use of arrow-ish techniques and of type-level
> programming, I would not classify the up-to-7.4 behavior as a "foolish
> consistency", especially going forward.
>
> -- Conal
>
>
>
> On Wed, Jan 18, 2012 at 6:27 AM, Simon Peyton-Jones <
> simo...@microsoft.com> wrote:
>
> Dear GHC users
>
> As part of beefing up the kind system, we plan to implement the "Type
> operators" proposal for Haskell Prime
> http://hackage.haskell.org/trac/haskell-prime/wiki/InfixTypeConstructors
>
> GHC has had type operators for some kind, so you can say
> data a :+: b = Left a | Right b
> but you can only do that for operators which start with ":".
>
> As part of the above wiki page you can see the proposal to broaden this to
> ALL operators, allowing
> data a + b = Left a | Right b
>
> Although this technically inconsistent the value page (as the wiki page
> discussed), I think the payoff is huge. (And "A foolish consistency is the
> hobgoblin of little minds", Emerson)
>
>
> This email is (a) to highlight the plan, and (b) to ask about flags. Our
> preferred approach is to *change* what -XTypeOperators does, to allow type
> operators that do not start with :. But that will mean that *some*
> (strange) programs will stop working. The only example I have seen in tc192
> of GHC's test suite
> {-# LANGUAGE TypeOperators #-}
> comp :: Arrow (~>) => (b~>c, c~>d)~>(b~>d)
> comp = arr (uncurry (>>>))
>
> Written more conventionally, the signature would look like
> comp :: Arrow arr => arr (arr b c, arr c d) (arr b d)
> comp = arr (uncurry (>>>))
> or, in infix notation
> {-# LANGUAGE TypeOperators #-}
> comp :: Arrow arr => (b `arr` c, c `arr` d) `arr` (b `arr` d)
> comp = arr (uncurry (>>>))
>
> But tc192 as it stands would become ILLEGAL, because (~>) would be a type
> *constructor* rather than (as now) a type *variable*. Of course it's
> easily fixed, as above, but still a breakage is a breakage.
>
> It would be possible to have two flags, so as to get
> - Haskell 98 behaviour
> - Current TypeOperator behaviuor
> - New TypeOperator behaviour
> but it turns out to be Quite Tiresome to
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I've come to think the culprit here is the fallacy that Any should inhabit
every kind.
I realize this is useful from an implementation perspective, but it has a
number of far reaching consequences:
This means that a product kind isn't truly a product of two kinds. x * y,
it winds up as a *distinguishable* x * y + 1, as Andrea has shown us
happens because you can write a type family or MPTC with fundep that can
match on Any.
A coproduct of two kinds x + y, isn't x + y, its x + y + 1.
Kind level naturals aren't kind nats, they are nats + 1, and not even the
one point compactification we get with lazy nats where you have an
indistinguishable infinity added to the domain, but rather there is a
distinguished atom to each kind under consideration.
I noticed that the polykindedness of Any is abused in the GHC.TypeLits to
make fundeps determining a kind, but where else is it exploited?
-Edward
On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg wrote:
> I retract my statement.
>
> My mistake was that I looked at the definition for consistency in FC --
> which correctly is agnostic to non-base-kind coercions -- and applied it
> only to the set of coercion assumptions, not to any coercion derivable from
> the assumptions. As Andrea's example shows, by assuming an eta coercion, it
> is possible to derive an inconsistent coercion.
>
> Examining the definition for FC consistency more closely, an eta coercion
> does not match to the form allowed for coercion assumptions used to prove
> consistency. The proof, in [1], requires all assumptions to have a type
> family application on the left-hand side. An eta coercion does not have a
> type family application on either side, and so the consistency proof in [1]
> does not apply.
>
> In light of this, it would seem that allowing eta coercions while
> retaining consistency would require some more work.
>
> Thanks for pointing out my mistake.
> Richard
>
> [1] S. Weirich et al. "Generative Type Abstraction and Type-level
> Computation."
> (http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)
>
> On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:
>
> > On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg
> wrote:
> >> [...]
> >> So, it seems possible to introduce eta coercions into FC for all kinds
> containing only one type constructor without sacrificing soundness. How the
> type inference engine/source Haskell triggers the use of these coercions is
> another matter, but there doesn't seem to be anything fundamentally wrong
> with the idea.
> >>
> >
> > A recent snapshot of ghc HEAD doesn't seem to agree:
> >
> > {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> > TypeFamilies, ScopedTypeVariables, TypeOperators #-}
> >
> > import GHC.Exts
> > import Unsafe.Coerce
> >
> > data (:=:) :: k -> k -> * where
> > Refl :: a :=: a
> >
> > trans :: a :=: b -> b :=: c -> a :=: c
> > trans Refl Refl = Refl
> >
> > type family Fst (x :: (a,b)) :: a
> > type family Snd (x :: (a,b)) :: b
> >
> > type instance Fst '(a,b) = a
> > type instance Snd '(a,b) = b
> >
> > eta :: x :=: '(Fst x, Snd x)
> > eta = unsafeCoerce Refl
> > -- ^^^ this is an acceptable way to simulate new coercions, i hope
> >
> > type family Bad s t (x :: (a,b)) :: *
> > type instance Bad s t '(a,b) = s
> > type instance Bad s t Any = t
> >
> > refl_Any :: Any :=: Any
> > refl_Any = Refl
> >
> > cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> > cong_Bad Refl = Refl
> >
> > s_eq_t :: forall (s :: *) (t :: *). s :=: t
> > s_eq_t = cong_Bad (trans refl_Any eta)
> >
> > subst :: x :=: y -> x -> y
> > subst Refl x = x
> >
> > coerce :: s -> t
> > coerce = subst s_eq_t
> >
> > {-
> > GHCi, version 7.7.20120830: http://www.haskell.org/ghc/ :? for help
> > *Main> coerce (4.0 :: Double) :: (Int,Int)
> > (Segmentation fault
> > -}
> >
> > -- Andrea Vezzosi
> >
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I'm going to defer to Conor on this one, as it is one of the examples from
his Kleisli Arrows of Outrageous fortune that I'm translating here. ;)
-Edward
On Fri, Aug 31, 2012 at 3:14 PM, Simon Peyton-Jones
wrote:
> Try translating into System FC! It’s not just a question of what the
> type checker will pass; we also have to produce a well-typed FC program.**
> **
>
> ** **
>
> Remember that (putting in all the kind abstractions and applications:
>
> Thrist :: forall i. ((i,i) -> *) -> (i,i) -> *
>
> (:*) :: forall i j k. forall (a: (i,j) -> *).
>
> a '(i,j) -> Thrist (j,k) a '(j,k) -> Thrist (i,k) a '(i,k)
>
> ** **
>
> So consider ‘irt’:
>
> ** **
>
> irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).
>
> a x -> Thrist i a x
>
> irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).
>
>(:*) ? ? ? ? ax (Nil ...)
>
> ** **
>
> So, what are the three kind args, and the type arg, to (:*)?
>
> ** **
>
> It doesn’t seem to make sense... in the body of irt, (:*) produces a
> result of type
>
> Thrist (i,k) a ‘(i,k)
>
> but irt’s signature claims to produce a result of type
>
> Thrist i a x
>
> So irt’s signature is more polymorphic than its body.
>
> ** **
>
> If we give irt a less polymorphic type signature, all is well
>
> ** **
>
> irt :: forall p,q. forall (a : ((p,q),(p,q)) -> *). forall (x :
> ((p,q),(p,q))).
>
> a x -> Thrist (p,q) a x
>
> ** **
>
> ** **
>
> Maybe you can explain what you want in System FC? Type inference and the
> surface language come after that. If it can’t be expressed in FC it’s out
> of court. Of course we can always beef up System FC.
>
> ** **
>
> I’m copying Stephanie and Conor who may have light to shed.
>
> ** **
>
> Simon
>
> ** **
>
> *From:* Edward Kmett [mailto:ekm...@gmail.com ]
> *Sent:* 31 August 2012 18:27
>
> *To:* Simon Peyton-Jones
> *Cc:* glasgow-haskell-users@haskell.org
> *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
> functional dependency?
>
> ** **
>
> It is both perfectly reasonable and unfortunately useless. :(
>
> ** **
>
> The problem is that the "more polymorphic" type isn't any more
> polymorphic, since (ideally) the product kind (a,b) is only inhabited by
> things of the form '(x,y).
>
> ** **
>
> The product kind has a single constructor. But there is no way to express
> this at present that is safe.
>
> ** **
>
> As it stands, I can fake this to an extent in one direction, by writing***
> *
>
> ** **
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, TypeFamilies,
>
> RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
>
> FlexibleInstances, UndecidableInstances #-}
>
> ** **
>
> module Kmett where
>
> ** **
>
> type family Fst (p :: (a,b)) :: a
>
> type instance Fst '(a,b) = a
>
> ** **
>
> type family Snd (p :: (a,b)) :: b
>
> type instance Snd '(a,b) = b
>
> ** **
>
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
>
> Nil :: Thrist a '(i,i)
>
> (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
>
> a ij -> Thrist a '(j,k) -> Thrist a ik
>
> ** **
>
> irt :: a x -> Thrist a x
>
> irt ax = ax :- Nil
>
> ** **
>
> and this compiles, but it just pushes the problem down the road, because
> with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
> ij, Snd ij) :: (x,y)
>
> ** **
>
> But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
> when you go to define an indexed bind, and type families are insufficient
> to the task. Right now to get this property I'm forced to fake it with
> unsafeCoerce.
>
> ** **
>
> -Edward
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Also, even after upgrading to HEAD, I'm getting a number of errors like:
[2 of 8] Compiling Indexed.Functor ( src/Indexed/Functor.hs,
dist/build/Indexed/Functor.o )
ghc: panic! (the 'impossible' happened)
(GHC version 7.7.20120830 for x86_64-apple-darwin):
tc_fd_tyvar
k{tv aZ8}
k{tv l} [sig]
ghc-prim:GHC.Prim.BOX{(w) tc 347}
I'll try to distill this down to a reasonable test case.
-Edward
On Fri, Aug 31, 2012 at 1:26 PM, Edward Kmett wrote:
> It is both perfectly reasonable and unfortunately useless. :(
>
> The problem is that the "more polymorphic" type isn't any more
> polymorphic, since (ideally) the product kind (a,b) is only inhabited by
> things of the form '(x,y).
>
> The product kind has a single constructor. But there is no way to express
> this at present that is safe.
>
> As it stands, I can fake this to an extent in one direction, by writing
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, TypeFamilies,
> RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
> FlexibleInstances, UndecidableInstances #-}
>
> module Kmett where
>
> type family Fst (p :: (a,b)) :: a
> type instance Fst '(a,b) = a
>
> type family Snd (p :: (a,b)) :: b
> type instance Snd '(a,b) = b
>
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
> Nil :: Thrist a '(i,i)
> (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
> a ij -> Thrist a '(j,k) -> Thrist a ik
>
> irt :: a x -> Thrist a x
> irt ax = ax :- Nil
>
> and this compiles, but it just pushes the problem down the road, because
> with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
> ij, Snd ij) :: (x,y)
>
> But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
> when you go to define an indexed bind, and type families are insufficient
> to the task. Right now to get this property I'm forced to fake it with
> unsafeCoerce.
>
> -Edward
>
> On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones > wrote:
>
>> Same question. Do you expect the code below to type-check? I have
>> stripped it down to essentials. Currently it’s rejected with
>>
>> ** **
>>
>> Couldn't match type `a' with '(,) k k1 b0 d0
>>
>> ** **
>>
>> And that seems reasonable, doesn’t it? After all, in the defn of
>> bidStar, (:*) returns a value of type
>>
>> Star x y ‘(a,c) ‘(b,d)
>>
>> which is manifestly incompatible with the claimed, more polymorphic
>> type. And this is precisely the same error as comes from your
>> class/instance example below, and for precisely the same reason.
>>
>> ** **
>>
>> I must be confused.
>>
>> ** **
>>
>> Simon
>>
>> ** **
>>
>>
>>
>>
>> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
>>
>> module Product where
>>
>> ** **
>>
>> data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where*
>> ***
>>
>> (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)
>>
>> ** **
>>
>> bidStar :: Star T T a a
>>
>> bidStar = bidT :* bidT
>>
>> ** **
>>
>> data T a b = MkT
>>
>> ** **
>>
>> bidT :: T a a
>>
>> bidT = MkT
>>
>> ** **
>>
>> ** **
>>
>> ** **
>>
>> *From:* Edward Kmett [mailto:ekm...@gmail.com]
>> *Sent:* 31 August 2012 13:45
>> *To:* Simon Peyton-Jones
>> *Cc:* glasgow-haskell-users@haskell.org
>> *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
>> functional dependency?
>>
>> ** **
>>
>> Hrmm. This seems to render product kinds rather useless, as there is no
>> way to refine the code to reflect the knowledge that they are inhabited by
>> a single constructor. =(
>>
>> ** **
>>
>> For instance, there doesn't even seem to be a way to make the following
>> code compile, either.
>>
>> ** **
>>
>> ** **
>>
>> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
>>
>> module Product where
>>
>> ** **
>>
>> import Prelude hiding (id,(.))
>>
>> ** **
>>
>> class Category k where
>>
>> id :: k a a
>>
>> (.) :: k b c -> k a b -> k a c
>>
>> ** **
>>
>> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where**
>> **
>>
>> (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)
>>
>> ** **
>>
>> instance (Category x, Category y) => Category (x * y) where
>>
>> id = id :* id
>>
>> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
>>
>> ** **
>>
>> This all works perfectly fine in Conor's SHE, (as does the thrist
>> example) so I'm wondering where the impedence mismatch comes in and how to
>> gain knowledge of this injectivity to make it work.
>>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
It is both perfectly reasonable and unfortunately useless. :(
The problem is that the "more polymorphic" type isn't any more polymorphic,
since (ideally) the product kind (a,b) is only inhabited by things of the
form '(x,y).
The product kind has a single constructor. But there is no way to express
this at present that is safe.
As it stands, I can fake this to an extent in one direction, by writing
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, TypeFamilies,
RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
FlexibleInstances, UndecidableInstances #-}
module Kmett where
type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a
type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Nil :: Thrist a '(i,i)
(:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
a ij -> Thrist a '(j,k) -> Thrist a ik
irt :: a x -> Thrist a x
irt ax = ax :- Nil
and this compiles, but it just pushes the problem down the road, because
with that I can show that given ij :: (x,y), I can build up a tuple '(Fst
ij, Snd ij) :: (x,y)
But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
when you go to define an indexed bind, and type families are insufficient
to the task. Right now to get this property I'm forced to fake it with
unsafeCoerce.
-Edward
On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones
wrote:
> Same question. Do you expect the code below to type-check? I have
> stripped it down to essentials. Currently it’s rejected with
>
> ** **
>
> Couldn't match type `a' with '(,) k k1 b0 d0
>
> ** **
>
> And that seems reasonable, doesn’t it? After all, in the defn of bidStar,
> (:*) returns a value of type
>
> Star x y ‘(a,c) ‘(b,d)
>
> which is manifestly incompatible with the claimed, more polymorphic type.
> And this is precisely the same error as comes from your class/instance
> example below, and for precisely the same reason.
>
> ** **
>
> I must be confused.
>
> ** **
>
> Simon
>
> ** **
>
>
>
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
>
> module Product where
>
> ** **
>
> data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where**
> **
>
> (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)
>
> ** **
>
> bidStar :: Star T T a a
>
> bidStar = bidT :* bidT
>
> ** **
>
> data T a b = MkT
>
> ** **
>
> bidT :: T a a
>
> bidT = MkT
>
> ** **
>
> ** **
>
> ** **
>
> *From:* Edward Kmett [mailto:ekm...@gmail.com]
> *Sent:* 31 August 2012 13:45
> *To:* Simon Peyton-Jones
> *Cc:* glasgow-haskell-users@haskell.org
> *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
> functional dependency?
>
> ** **
>
> Hrmm. This seems to render product kinds rather useless, as there is no
> way to refine the code to reflect the knowledge that they are inhabited by
> a single constructor. =(
>
> ** **
>
> For instance, there doesn't even seem to be a way to make the following
> code compile, either.
>
> ** **
>
> ** **
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
>
> module Product where
>
> ** **
>
> import Prelude hiding (id,(.))
>
> ** **
>
> class Category k where
>
> id :: k a a
>
> (.) :: k b c -> k a b -> k a c
>
> ** **
>
> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where***
> *
>
> (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)
>
> ** **
>
> instance (Category x, Category y) => Category (x * y) where
>
> id = id :* id
>
> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
>
> ** **
>
> This all works perfectly fine in Conor's SHE, (as does the thrist example)
> so I'm wondering where the impedence mismatch comes in and how to gain
> knowledge of this injectivity to make it work.
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg wrote: > I ran into this same issue in my own experimentation: if a type variable x > has a kind with only one constructor K, GHC does not supply the equality x > ~ K y for some fresh type variable y. Perhaps it should. I too had to use > similar workarounds to what you have come up with. > > One potential problem is the existence of the Any type, which inhabits > every kind. Say x gets unified with Any. Then, we would have Any ~ K y, > which is an inconsistent coercion (equating two types with distinct ground > head types). However, because the RHS is a promoted datatype, we know that > this coercion can never be applied to a term. Because equality is > homogeneous (i.e. ~ can relate only two types of the same kind), I'm not > convinced the existence of Any ~ K y is so bad. (Even with heterogeneous > equality, it might work out, given that there is more than one type > constructor that results in *...) > I think it may have to. Working the example further runs into a similar problem. When you go to implement indexed bind, there isn't a way to convince GHC that (Snd ij ~ i, Fst ij ~ j) entails (ij ~ '(i,j)) I'm working around it (for now) with unsafeCoerce. :-( But it with an explicitly introduced equality this code would just work, like it does in other platforms. https://github.com/ekmett/indexed/blob/master/src/Indexed/Thrist.hs#L21 > Regarding the m -> k fundep: my experiments suggest that this dependency > is implied when you have (m :: k), but I guess not when you have k appear > in the kind of m in a more complicated way. Currently, there are no > kind-level functions, so it appears that m -> k could be implied whenever k > appears anywhere in the kind of m. If (when!) there are kind-level > functions, we'll have to be more careful. > -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
This works, though it'll be all sorts of fun to try to scale up.
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances,
TypeFamilies #-}
module Indexed.Test where
class IMonad (m :: (k -> *) -> k -> *) | m -> k
where ireturn :: a x -> m a x
type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p
type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q
infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Nil :: Thrist a '(i,i)
(:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij ->
Thrist a jk -> Thrist a ik
instance IMonad Thrist where
ireturn a = a :- Nil
I know Agda has to jump through some hoops to make the refinement work on
pairs when they do eta expansion. I wonder if this could be made less
painful.
On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett wrote:
> Hrmm. This seems to work manually for getting product categories to work.
> Perhaps I can do the same thing for thrists.
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
> module Product where
>
> import Prelude hiding (id,(.))
>
> class Category k where
> id :: k a a
> (.) :: k b c -> k a b -> k a c
>
> type family Fst (a :: (p,q)) :: p
> type instance Fst '(p,q) = p
>
> type family Snd (a :: (p,q)) :: q
> type instance Snd '(p,q) = q
>
> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
> (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b
>
> instance (Category x, Category y) => Category (x * y) where
> id = id :* id
> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
>
>
>
> On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett wrote:
>
>> Hrmm. This seems to render product kinds rather useless, as there is no
>> way to refine the code to reflect the knowledge that they are inhabited by
>> a single constructor. =(
>>
>> For instance, there doesn't even seem to be a way to make the following
>> code compile, either.
>>
>>
>> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
>> module Product where
>>
>> import Prelude hiding (id,(.))
>>
>> class Category k where
>> id :: k a a
>> (.) :: k b c -> k a b -> k a c
>>
>> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
>> (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)
>>
>> instance (Category x, Category y) => Category (x * y) where
>> id = id :* id
>> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
>>
>> This all works perfectly fine in Conor's SHE, (as does the thrist
>> example) so I'm wondering where the impedence mismatch comes in and how to
>> gain knowledge of this injectivity to make it work.
>>
>> Also, does it ever make sense for the kind of a kind variable mentioned
>> in a type not to get a functional dependency on the type?
>>
>> e.g. should
>>
>> class Foo (m :: k -> *)
>>
>> always be
>>
>> class Foo (m :: k -> *) | m -> k
>>
>> ?
>>
>> Honest question. I can't come up with a scenario, but you might have one
>> I don't know.
>>
>> -Edward
>>
>> On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <
>> simo...@microsoft.com> wrote:
>>
>>> With the code below, I get this error message with HEAD. And that
>>> looks right to me, no?
>>>
>>> The current 7.6 branch gives the same message printed less prettily.
>>>
>>> ** **
>>>
>>> If I replace the defn of irt with
>>>
>>> irt :: a '(i,j) -> Thrist a '(i,j)
>>>
>>> irt ax = ax :- Nil
>>>
>>> ** **
>>>
>>> then it typechecks.
>>>
>>> ** **
>>>
>>> Simon
>>>
>>> ** **
>>>
>>> ** **
>>>
>>> Knett.hs:20:10:
>>>
>>> Couldn't match type `x' with '(i0, k0)
>>>
>>> `x' is a rigid type variable bound by
>>>
>>> the type signature for irt :: a x -> Thrist k a x at
>>> Knett.hs:19:8
>>>
>>> Expected type: Thrist k a x
>>>
>>> Actual type: Thrist k a '(i0, k0)
>>>
>>> In the expression:
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Hrmm. This seems to work manually for getting product categories to work.
Perhaps I can do the same thing for thrists.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c -> k a b -> k a c
type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p
type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q
data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
(:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b
instance (Category x, Category y) => Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett wrote:
> Hrmm. This seems to render product kinds rather useless, as there is no
> way to refine the code to reflect the knowledge that they are inhabited by
> a single constructor. =(
>
> For instance, there doesn't even seem to be a way to make the following
> code compile, either.
>
>
> {-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
> module Product where
>
> import Prelude hiding (id,(.))
>
> class Category k where
> id :: k a a
> (.) :: k b c -> k a b -> k a c
>
> data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
> (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)
>
> instance (Category x, Category y) => Category (x * y) where
> id = id :* id
> (xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
>
> This all works perfectly fine in Conor's SHE, (as does the thrist example)
> so I'm wondering where the impedence mismatch comes in and how to gain
> knowledge of this injectivity to make it work.
>
> Also, does it ever make sense for the kind of a kind variable mentioned in
> a type not to get a functional dependency on the type?
>
> e.g. should
>
> class Foo (m :: k -> *)
>
> always be
>
> class Foo (m :: k -> *) | m -> k
>
> ?
>
> Honest question. I can't come up with a scenario, but you might have one I
> don't know.
>
> -Edward
>
> On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones > wrote:
>
>> With the code below, I get this error message with HEAD. And that looks
>> right to me, no?
>>
>> The current 7.6 branch gives the same message printed less prettily.
>>
>> ** **
>>
>> If I replace the defn of irt with
>>
>> irt :: a '(i,j) -> Thrist a '(i,j)
>>
>> irt ax = ax :- Nil
>>
>> ** **
>>
>> then it typechecks.
>>
>> ** **
>>
>> Simon
>>
>> ** **
>>
>> ** **
>>
>> Knett.hs:20:10:
>>
>> Couldn't match type `x' with '(i0, k0)
>>
>> `x' is a rigid type variable bound by
>>
>> the type signature for irt :: a x -> Thrist k a x at
>> Knett.hs:19:8
>>
>> Expected type: Thrist k a x
>>
>> Actual type: Thrist k a '(i0, k0)
>>
>> In the expression: ax :- Nil
>>
>> In an equation for `irt': irt ax = ax :- Nil
>>
>> simonpj@cam-05-unx:~/tmp$
>>
>> ** **
>>
>> ** **
>>
>> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
>> MultiParamTypeClasses, PolyKinds,
>>
>> RankNTypes, TypeOperators, DefaultSignatures, DataKinds, ***
>> *
>>
>> FlexibleInstances, UndecidableInstances #-}
>>
>> ** **
>>
>> module Knett where
>>
>> ** **
>>
>> class IMonad (m :: (k -> *) -> k -> *) | m -> k where
>>
>> ireturn :: a x -> m a x
>>
>> ** **
>>
>> infixr 5 :-
>>
>> ** **
>>
>> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
>>
>> Nil :: Thrist a '(i,i)
>>
>> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
>>
>> ** **
>>
>> -- instance IMonad Thrist where
>>
>> -- ireturn a = a :- Nil
>>
>> ** **
>>
>> irt :: a x -> Thrist a x
>>
>> irt ax = ax :- Nil
>>
>> ** **
>>
>> ** **
>>
>> *From:* glasgow-haskell-users-boun...@haskell.org [mailto:
>> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett
>> *Sent:* 31 August 2012 03:38
>> *To:* glasgow-haskell-users@haskell.org
>
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
Hrmm. This seems to render product kinds rather useless, as there is no way
to refine the code to reflect the knowledge that they are inhabited by a
single constructor. =(
For instance, there doesn't even seem to be a way to make the following
code compile, either.
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where
import Prelude hiding (id,(.))
class Category k where
id :: k a a
(.) :: k b c -> k a b -> k a c
data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
(:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)
instance (Category x, Category y) => Category (x * y) where
id = id :* id
(xf :* yf) . (xg :* yg) = (xf . xg) :* (yf . yg)
This all works perfectly fine in Conor's SHE, (as does the thrist example)
so I'm wondering where the impedence mismatch comes in and how to gain
knowledge of this injectivity to make it work.
Also, does it ever make sense for the kind of a kind variable mentioned in
a type not to get a functional dependency on the type?
e.g. should
class Foo (m :: k -> *)
always be
class Foo (m :: k -> *) | m -> k
?
Honest question. I can't come up with a scenario, but you might have one I
don't know.
-Edward
On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones
wrote:
> With the code below, I get this error message with HEAD. And that looks
> right to me, no?
>
> The current 7.6 branch gives the same message printed less prettily.
>
> ** **
>
> If I replace the defn of irt with
>
> irt :: a '(i,j) -> Thrist a '(i,j)
>
> irt ax = ax :- Nil
>
> ** **
>
> then it typechecks.
>
> ** **
>
> Simon
>
> ** **
>
> ** **
>
> Knett.hs:20:10:
>
> Couldn't match type `x' with '(i0, k0)
>
> `x' is a rigid type variable bound by
>
> the type signature for irt :: a x -> Thrist k a x at
> Knett.hs:19:8
>
> Expected type: Thrist k a x
>
> Actual type: Thrist k a '(i0, k0)
>
> In the expression: ax :- Nil
>
> In an equation for `irt': irt ax = ax :- Nil
>
> simonpj@cam-05-unx:~/tmp$
>
> ** **
>
> ** **
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds,
>
> RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
>
> FlexibleInstances, UndecidableInstances #-}
>
> ** **
>
> module Knett where
>
> ** **
>
> class IMonad (m :: (k -> *) -> k -> *) | m -> k where
>
> ireturn :: a x -> m a x
>
> ** **
>
> infixr 5 :-
>
> ** **
>
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
>
> Nil :: Thrist a '(i,i)
>
> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
>
> ** **
>
> -- instance IMonad Thrist where
>
> -- ireturn a = a :- Nil
>
> ** **
>
> irt :: a x -> Thrist a x
>
> irt ax = ax :- Nil
>
> ** **
>
> ** **
>
> *From:* glasgow-haskell-users-boun...@haskell.org [mailto:
> glasgow-haskell-users-boun...@haskell.org] *On Behalf Of *Edward Kmett
> *Sent:* 31 August 2012 03:38
> *To:* glasgow-haskell-users@haskell.org
> *Subject:* PolyKind issue in GHC 7.6.1rc1: How to make a kind a
> functional dependency?
>
> ** **
>
> If I define the following
>
> ** **
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
> DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}*
> ***
>
> module Indexed.Test where
>
> ** **
>
> class IMonad (m :: (k -> *) -> k -> *) where
>
> ireturn :: a x -> m a x
>
> ** **
>
> infixr 5 :-
>
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
>
> Nil :: Thrist a '(i,i)
>
> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
>
> ** **
>
> instance IMonad Thrist where
>
> ireturn a = a :- Nil
>
> ** **
>
> Then 'ireturn' complains (correctly) that it can't match the k with the
> kind (i,i). The reason it can't is because when you look at the resulting
> signature for the MPTC it generates it looks like
>
> ** **
>
> class IMonad k m where
>
> ireturn :: a x -> m a x
>
> ** **
>
> However, there doesn't appear to be a way to say that the kind k should be
> determined by m.
>
> ** **
>
> I tried doing:
>
&g
Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
I tried this with the release candidate. I can go pull a more recent
version and try again.
On Thu, Aug 30, 2012 at 11:04 PM, Richard Eisenberg wrote:
> This looks related to bug #7128. In the response to that (fixed, closed)
> bug report, Simon PJ said that functional dependencies involving kinds are
> supported. Are you compiling with a version of 7.6 updated since that bug
> fix?
>
> Richard
>
> On Aug 30, 2012, at 10:38 PM, Edward Kmett wrote:
>
> If I define the following
>
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
> DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
> module Indexed.Test where
>
> class IMonad (m :: (k -> *) -> k -> *) where
> ireturn :: a x -> m a x
>
> infixr 5 :-
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
> Nil :: Thrist a '(i,i)
> (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
>
> instance IMonad Thrist where
> ireturn a = a :- Nil
>
> Then 'ireturn' complains (correctly) that it can't match the k with the
> kind (i,i). The reason it can't is because when you look at the resulting
> signature for the MPTC it generates it looks like
>
> class IMonad k m where
> ireturn :: a x -> m a x
>
> However, there doesn't appear to be a way to say that the kind k should be
> determined by m.
>
> I tried doing:
>
> class IMonad (m :: (k -> *) -> k -> *) | m -> k where
> ireturn :: a x -> m a x
>
> Surprisingly (to me) this compiles and generates the correct constraints
> for IMonad:
>
> ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
> -XDataKinds -XGADTs
> ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x
> -> m a x
> ghci> :info IMonad
> class IMonad k m | m -> k where
> ireturn :: a x -> m a x
>
> But when I add
>
> ghci> :{
> Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where
> Prelude| Nil :: Thrist a '(i,i)
> Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
> Prelude| :}
>
> and attempt to introduce the instance, I crash:
>
> ghci> instance IMonad Thrist where ireturn a = a :- Nil
> ghc: panic! (the 'impossible' happened)
> (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
> lookupVarEnv_NF: Nothing
>
> Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
> Moreover, attempting to compile them in separate modules leads to a
> different issue.
>
> Within the module, IMonad has a type that includes the kind k and the
> constraint on it from m. But from the other module, :info shows no such
> constraint, and the above code again fails to typecheck, but upon trying to
> recompile, when GHC goes to load the IMonad instance from the core file, it
> panicks again differently about references to a variable not present in the
> core.
>
> Is there any way to make such a constraint that determines a kind from a
> type parameter in GHC 7.6 at this time?
>
> I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be
> applicable to this situation.
>
> -Edward
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?
If I define the following
{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators,
DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
module Indexed.Test where
class IMonad (m :: (k -> *) -> k -> *) where
ireturn :: a x -> m a x
infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Nil :: Thrist a '(i,i)
(:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
instance IMonad Thrist where
ireturn a = a :- Nil
Then 'ireturn' complains (correctly) that it can't match the k with the
kind (i,i). The reason it can't is because when you look at the resulting
signature for the MPTC it generates it looks like
class IMonad k m where
ireturn :: a x -> m a x
However, there doesn't appear to be a way to say that the kind k should be
determined by m.
I tried doing:
class IMonad (m :: (k -> *) -> k -> *) | m -> k where
ireturn :: a x -> m a x
Surprisingly (to me) this compiles and generates the correct constraints
for IMonad:
ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies
-XDataKinds -XGADTs
ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x
-> m a x
ghci> :info IMonad
class IMonad k m | m -> k where
ireturn :: a x -> m a x
But when I add
ghci> :{
Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Prelude| Nil :: Thrist a '(i,i)
Prelude| (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
Prelude| :}
and attempt to introduce the instance, I crash:
ghci> instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
(GHC version 7.6.0.20120810 for x86_64-apple-darwin):
lookupVarEnv_NF: Nothing
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Moreover, attempting to compile them in separate modules leads to a
different issue.
Within the module, IMonad has a type that includes the kind k and the
constraint on it from m. But from the other module, :info shows no such
constraint, and the above code again fails to typecheck, but upon trying to
recompile, when GHC goes to load the IMonad instance from the core file, it
panicks again differently about references to a variable not present in the
core.
Is there any way to make such a constraint that determines a kind from a
type parameter in GHC 7.6 at this time?
I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be
applicable to this situation.
-Edward
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Why is Bag's Data instance "broken"?
I've been meaning to put in a proposal to replace the Data instances for
Map, etc. with one that pretends there is a fake 'fromList' constructor
that restores the invariants.
In my experience this works much better than just making everyone who
relies on Data randomly crash, and it preserves the invariants of the
opaque structure.
I use this approach on many of my own container types.
-Edward
On Wed, Aug 29, 2012 at 7:11 AM, José Pedro Magalhães wrote:
> Hi Philip,
>
> On Wed, Aug 29, 2012 at 12:01 PM, Philip Holzenspies <
> p...@st-andrews.ac.uk> wrote:
>
>> Dear GHCers,
>>
>> I'm performing traversals over GHC-API results (HsSyn et al). For this
>> purpose, I'm using SYB generics.
>>
>> I found that I couldn't use "ext1Q" for a function with type "Data x =>
>> Bag x -> String", i.e. that this function was never applied. The source of
>> Bag's instance of the Data class seems to explain why:
>>
>>
>> instance Data a => Data (Bag a) where
>> gfoldl k z b = z listToBag `k` bagToList b -- traverse abstract type
>> abstractly
>> toConstr _ = abstractConstr $ "Bag("++show (typeOf
>> (undefined::a))++")"
>> gunfold _ _ = error "gunfold"
>> dataTypeOf _ = mkNoRepType "Bag"
>>
>>
>> Is there a rationale to not allow gunfolds and to keep toConstr abstract?
>
>
> As far as I understand, this is to keep `Bag` itself abstract, preventing
> users from inspecting its internals.
>
>
>> More to the point for my needs, is there a reason to not allow dataCast1
>> casting of Bags?
>>
>
> That is a separate issue; I believe this instance is just missing a
> `dataCast1 = gcast1` line.
> All datatypes of kind `* -> *` should have such a definition.
>
> (Having a look at Data.Data, I guess the same applies to `Ptr a` and
> `ForeignPtr a`.
> And `Array a b` seems to be missing the `dataCast2` method. I propose
> fixing all of these.)
>
>
> Cheers,
> Pedro
>
>
>>
>> Regards,
>> Philip
>> ___
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users@haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>>
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Comparing StableNames of different type
On Tue, Aug 28, 2012 at 12:08 PM, Nicolas Frisby wrote: > On Tue, Aug 28, 2012 at 3:34 AM, Simon Marlow wrote: > On 24/08/2012 07:39, Emil Axelsson wrote: > > > > Are there any dangers in comparing two StableNames of different type? > > > >stEq :: StableName a -> StableName b -> Bool > >stEq a b = a == (unsafeCoerce b) > > > Ok, I've added it. It will be in GHC 7.8.1. > > > > Cheers, > > Simon > > Might we benefit from having a variant that returns Maybe (a :=: b)? > Is that safe? I have limited experience with StableNames, but that > intuitively seems safe. But polymorphism and references deserve more > thought than I've given this yet. > > I'm referring to "data (:=:) :: * -> * -> * where Refl :: (a :=: a)", > just to be clear. > > No. You can't safely determine that a ~ b given that two stablenames are equal. If you give Nothing a stableName, it'll have one stable name, regardless of if you use it as a Maybe Int or a Maybe Bool. Maybe Int and Maybe Bool are clearly not equal. This is admittedly an implementation detail. GHC would be perfectly within its rights (if somewhat silly) to construct a fresh Nothing every time, but it doesn't. The reasoning you applied only works for fully monomorphic types. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Comparing StableNames of different type
You can wind up with StableNames matching even when the types differ. Consider naming [] :: [Int] and [] :: [()]. This is harmless for most usecases. I've used unsafeCoerce to compare StableNames on different types for years without problems. Admittedly, I do find it a bit of an oddity that the type shows up in their signature at all. :) Sent from my iPhone On Aug 24, 2012, at 5:08 AM, Simon Marlow wrote: > On 24/08/2012 07:39, Emil Axelsson wrote: >> Hi! >> >> Are there any dangers in comparing two StableNames of different type? >> >> stEq :: StableName a -> StableName b -> Bool >> stEq a b = a == (unsafeCoerce b) >> >> I could guard the coercion by first comparing the type representations, >> but that would give me a `Typeable` constraint that would spread >> throughout the code. > > I think that's probably OK. It should be safe even if the types are > different, but I presume you expect the types to be the same, since otherwise > the comparison would be guaranteed to return False, right? > > Cheers, >Simon > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Request for comments on proposal for literate programming using markdown
Ultimately your best bet to actually get something integrated will be to find something that minimizes the amount of work on the part of GHC HQ. I don't think *anybody* there is interested in picking up a lot of fiddly formatting logic and carving it into stone. They might be slightly less inclined to shut the door in your face if the proposal only involved adding a few hooks in the AST for exposing alternative documentation formats, which would enable you to hook in via a custom unlit or do something like how haddock hooks in, but overall, if it involves folks at GHC HQ maintaining a full markdown parser I think they will (and should) just shrug and move on. The resulting system would be slightly less work for you, but would only see any improvements delayed a year between GHC releases, and then the community can't adopt the improvements in earnest for another year after that. This is *not* an encouraging development cycle, and doesn't strike me as a recipe for a successful project. As proposed, this would distract some pretty core resources from working on core functionality and I for one am heavily against it as I understand what has been proposed so far. Haddock works with some fairly simple extensions to GHC's syntax tree. If your proposal was modified so that it just requires a few hooks or worked with the existing haddock hooks in the syntax tree, then while I would hardly be a huge proponent due the fragmentation issues about how to deal with documentation, I would at least cease to be actively opposed. -Edward On Tue, Aug 21, 2012 at 7:45 AM, Philip Holzenspies wrote: > On 14 Aug 2012, at 07:48, Simon Hengel wrote: > > Personally, still do not see the big benefit for all that work, and I'm > > still somewhat worried that a mechanism that is not used by default (I'm > > talking about unliting with an external command) may start to bit rot. > > But as long as you are commit to keep `-pgmL` intact, I'm ok ;). > > A biggy that I had left out has just reoccurred to me. The very first > reason for me to look at how unlitting and preprocessing is done in GHC > was, because I was looking into what would be required for a refactoring > engine (like haRe) to be based on the GHC API. Of course, at the moment, > the API doesn't do anything with unlitting and preprocessing. > > > I think in the end it's best to go with the solution that works best for > > GHC-HQ. > > Still hoping to hear from them ;) > > Regards, > Philip > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADTs in the wild
On Tue, Aug 14, 2012 at 10:32 AM, Edward Kmett wrote: > data NonDetFork :: (*,*) -> * -> * where > NDL :: (a -> c) -> NonDetFork '(a, b) c > NDR :: (b -> c) -> NonDetFork '(a, b) c > NDB :: (a -> b) -> (b -> c) -> NonDetFork '(a, b) c > er.. NDB :: (a -> *c*) -> (b -> c) -> NonDetFork '(a, b) c ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: GADTs in the wild
We use a form of stream transducer here at Capital IQ that uses GADTs, kind polymorphism and data kinds: data SF k a b = Emit b (SF k a b) | Receive (k a (SF k a b)) data Fork :: (*,*) -> * -> * where L :: (a -> c) -> Fork '(a, b) c R :: (b -> c) -> Fork '(a, b) c type Pipe = SF (->) type Tee a b = SF Fork '(a, b) instance Category (SF (->)) where id = arr id Emit a as . sf = Emit a (as . sf) Receive f . Emit b bs = f b . bs sf . Receive g = Receive (\a -> sf . g a) arr :: (a -> b) -> Pipe a b arr f = z where loop a = Emit (f a) z z = Receive loop repeat :: b -> SF k a b repeat b = Emit b z where z = repeat b filter :: (a -> Bool) -> Pipe a a filter p = z where loop a | p a = Emit a z | otherwise = z z = Receive loop You can extend the model to support non-deterministic read from whichever input is available with data NonDetFork :: (*,*) -> * -> * where NDL :: (a -> c) -> NonDetFork '(a, b) c NDR :: (b -> c) -> NonDetFork '(a, b) c NDB :: (a -> b) -> (b -> c) -> NonDetFork '(a, b) c These could admittedly be implemented using a more traditional GADT without poly/data kinds, by just using (a,b) instead of '(a,b), though. -Edward Kmett On Tue, Aug 14, 2012 at 7:32 AM, Simon Peyton-Jones wrote: > Friends > > > I’m giving a series of five lectures at the Laser Summer > School<http://laser.inf.ethz.ch/2012/>(2-8 Sept), on “Adventures with types > in Haskell”. My plan is: > > > **1. **Type classes > > **2. **Type families [examples including Repa type tags] > > **3. **GADTs > > **4. **Kind polymorphism > > **5. **System FC and deferred type errors > > ** ** > > This message is to invite you to send me your favourite example of using a > GADT to get the job done. Ideally I’d like to use examples that are (a) > realistic, drawn from practice (b) compelling and (c) easy to present > without a lot of background. Most academic papers only have rather limited > examples, usually eval :: Term t -> t, but I know that GADTs are widely > used in practice. > > ** ** > > Any ideas from your experience, satisfying (a-c)? If so, and you can > spare the time, do send me a short write-up. Copy the list, so that we can > all benefit. > > ** ** > > Many thanks > > > Simon > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: PolyKinds, Control.Category and GHC 7.6.1
On Mon, Aug 13, 2012 at 9:55 AM, Dan Burton wrote: > Control.Category.Category is pretty much the only type in base that >> directly benefits from PolyKinds without any code changes, but without >> enabling the extension there nobody can define categories for kinds other >> than *, and most interesting categories actually have more exotic >> kinds. > > > What, precisely, is the benefit of turning on PolyKinds for that file > without changing the code? If we're cpp'ing it in, then are there further > benefits that we could also reap by cpp'ing some code changes? > The benefit is that the kind of Category changes to Category :: (x -> x -> *) -> Constraint This means I can do things like make data Dict p where Dict :: p => Dict p newtype a |- b = Sub (a => Dict b) and then (|-) :: Constraint -> Constraint -> * is a valid candidate to become a Category. Moreover, PolyKinds + DataKinds finally enable us to write product and sum categories, make categories for natural transformations, and generally finally put Category to work. These were all disallowed by the previous simpler kind. No code changes need be applied beyond permitting the type of Category to generalize and existing code continues to work. This change actually could have been applied in 7.4.1. -Edward Kmett ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
PolyKinds, Control.Category and GHC 7.6.1
Would it be possible to add something like
{-# LANGUAGE CPP #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704
{-# LANGUAGE PolyKinds #-}
#endif
to the top of Control.Category before the 7.6.1 final release?
Control.Category.Category is pretty much the only type in base that
directly benefits from PolyKinds without any code changes, but without
enabling the extension there nobody can define categories for kinds other
than *, and most interesting categories actually have more exotic kinds.
I only noticed that it wasn't there in the release candidate just now.
-Edward Kmett
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Call to arms: lambda-case is stuck and needs your help
Twan, The 0-ary version you proposed actually works even nicer with \of. foo'' = case () of () | quux -> ... | quaffle -> ... | otherwise -> ... Starting from the above legal haskell multi-way if, we can, switch to foo' = case of | quux -> ... | quaffle -> ... | otherwise -> ... using the 0-ary form of case as a multi-way if, but since the motivation was to allow the min \of, we get the very terse foo = \of | quux -> ... | quaffle -> ... | otherwise -> ... and you get wind up with layout starting on the |'s so they line up per-force. baz = \of Just x -> Just (x + 1) Nothing -> Nothing avoids an ugly temporary for baz' mx = case mx of Just x -> Just (x + 1) Nothing -> Nothing and in the multi-argument case, the resulting syntax is actually comparably noisy to the direct declaration syntax. One , as opposed to two pairs of parentheses in bar''' below. bar = \of Just x, Just y -> Just (x + y) _ , _ -> Nothing bar' mx my = case mx, my of Just x, Just y -> Just (x + y) _ , _ -> Nothing bar'' mx my = case (# mx, my #) of (# Just x, Just y #) -> Just (x + y) (# _ , _ #) -> Nothing bar''' (Just x) (Just y) = Just (x + y) bar''' _ _ = Nothing -Edward On Fri, Jul 6, 2012 at 3:12 AM, Edward Kmett wrote: > Oh, neat. I guess it does. :) I'll hack that into my grammar when I get > into work tomorrow. > > My main point with that observation is it cleanly allows for multiple > argument \of without breaking the intuition you get from how of already > works/looks or requiring you to refactor subsequent lines, to cram parens > or other odd bits of syntax in, but still lets the multi-argument crowd > have a way to make multi-argument lambdas with all of the expected > appropriate backtracking, if they want them. I definitely prefer \of to > \case given its almost shocking brevity and the fact that the fact that it > introduces a layout rule doesn't change any of the rules for when layout is > introduced. > > On Jul 5, 2012, at 5:33 PM, Twan van Laarhoven wrote: > > > On 2012-07-05 23:04, Edward Kmett wrote: > >> A similar generalization can be applied to the expression between case > and of > >> to permit a , separated list of expressions so this becomes applicable > to the > >> usual case construct. A naked unparenthesized , is illegal there > currently as > >> well. That would effectively be constructing then matching on an unboxed > >> tuple without the (#, #) noise, but that can be viewed as a separate > >> proposal' then the above is just the elision of the case component of: > > > > Should that also generalize to nullarry 'case of'? As in > > > >foo = case of > > | guard1 -> bar > > | guard2 -> baz > > > > instead of > > > >foo = case () of > >() | guard1 -> bar > > | guard2 -> baz > > > > > > > > I realize this is getting off-topic, and has become orthogonal to the > single argument λcase proposal. > > > > > > Twan > > > > ___ > > Glasgow-haskell-users mailing list > > Glasgow-haskell-users@haskell.org > > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Call to arms: lambda-case is stuck and needs your help
Oh, neat. I guess it does. :) I'll hack that into my grammar when I get into work tomorrow. My main point with that observation is it cleanly allows for multiple argument \of without breaking the intuition you get from how of already works/looks or requiring you to refactor subsequent lines, to cram parens or other odd bits of syntax in, but still lets the multi-argument crowd have a way to make multi-argument lambdas with all of the expected appropriate backtracking, if they want them. I definitely prefer \of to \case given its almost shocking brevity and the fact that the fact that it introduces a layout rule doesn't change any of the rules for when layout is introduced. On Jul 5, 2012, at 5:33 PM, Twan van Laarhoven wrote: > On 2012-07-05 23:04, Edward Kmett wrote: >> A similar generalization can be applied to the expression between case and of >> to permit a , separated list of expressions so this becomes applicable to the >> usual case construct. A naked unparenthesized , is illegal there currently as >> well. That would effectively be constructing then matching on an unboxed >> tuple without the (#, #) noise, but that can be viewed as a separate >> proposal' then the above is just the elision of the case component of: > > Should that also generalize to nullarry 'case of'? As in > >foo = case of > | guard1 -> bar > | guard2 -> baz > > instead of > >foo = case () of >() | guard1 -> bar > | guard2 -> baz > > > > I realize this is getting off-topic, and has become orthogonal to the single > argument λcase proposal. > > > Twan > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Call to arms: lambda-case is stuck and needs your help
I really like the \of proposal! It is a clean elision with \x -> case x of becoming \of I still don't like it directly for multiple arguments. One possible approach to multiple arguments is what we use for multi-argument case/alt here in our little haskell-like language, Ermine, here at S&P CapitalIQ, we allow for ',' separated patterns, but without surrounding parens to be treated as a multi argument case and alt pair. Internally we desugar our usual top level bindings directly to this representation. When mixed with the \of extension, this would give you: foo :: Num a => Maybe a -> Maybe a -> Maybe a foo = \of Just x, Just y -> Just (x*y) _, _ -> Nothing but it wouldn't incur parens for the usual constructor pattern matches and it sits cleanly in another syntactic hole. A similar generalization can be applied to the expression between case and of to permit a , separated list of expressions so this becomes applicable to the usual case construct. A naked unparenthesized , is illegal there currently as well. That would effectively be constructing then matching on an unboxed tuple without the (#, #) noise, but that can be viewed as a separate proposal' then the above is just the elision of the case component of: foo mx my = case mx, my of Just x, Just y -> Just (x*y) _, _ -> Nothing On Jul 5, 2012, at 2:49 PM, wagne...@seas.upenn.edu wrote: > Quoting wagne...@seas.upenn.edu: > >> Well, for what it's worth, my vote goes for a multi-argument \case. I > > Just saw a proposal for \of on the reddit post about this. That's even > better, since: > > 1. it doesn't change the list of block heralds > 2. it doesn't mention case, and therefore multi-arg \of is perhaps a bit less > objectionable to those who expect "case" to be single-argument > 3. 40% less typing! > > Can I change my vote? =) > ~d > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Kindness of strangers (or strangeness of Kinds)
On Mon, Jun 11, 2012 at 9:58 PM, AntC wrote: > Simon Peyton-Jones microsoft.com> writes: > > > > > There is a little, ill-documented, sub-kind hierarchy in GHC. I'm trying > hard to get rid of it as much as > > possible, and it is much less important than it used to be. It's always > been > there, and is nothing to do with polykinds. > > > > I've extended the commentary a bit: see "Types" and "Kinds" here > > http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler > > > > The ArgKind thing has gone away following Max's recent unboxed-tuples > patch, > so we now only have OpenKind > > (described on the above pages). > > Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!) > > It's not that I have a specific problem (requirement) I'm trying to solve. > It's more that I'm trying to understand how this ladder of > Sorts/Kinds/Types/values hangs together. > > With Phantom types, we've been familiar for many years with uninhabited > types, > so why are user-defined (promoted) Kinds/Types different? > > The Singletons stuff shows there are use cases for mapping from uninhabited > types to values -- but it seems to need a lot of machinery (all those > shadow > types and values). And indeed TypeRep maps from not-necessarily-inhabited > types to values. > > Is it that we really need to implement type application in the surface > language to get it all to come together? Then we won't need functions > applying > to dummy arguments whose only purpose is to carry a Type::Kind. > > To give a tight example: > >data MyNat = Z | S MyNat-- to be promoted > >data ProxyNat (a :: MyNat) = ProxyNat -- :k ProxyNat :: MyNat -> * > >proxyNat :: n -> ProxyNat n -- rejected: Kind mis-match >proxyNat _ = ProxyNat > > The parallel of that with phantom types (and a class constraint for MyNat) > seems unproblematic -- albeit with Kind *. > > Could we have :k (->) :: OpenKind -> * -> * -- why not? I don't quite understand why you would want arbitrary kinded arguments, but only in negative position. Internally its already more like (->) :: OpenKind -> OpenKind -> * at the moment. The changes simply permitted unboxed tuples in argument position, relaxing a previous restriction. OpenKind is just a superkind of * and #, not every kind. Kinds other than * and # just don't have a term level representation. (Well kind Constraint is inhabited by dictionaries for instances after a fashion, but you don't get to manipulate them directly.) I'm a lot happier with the new plumbing than I was with the crap I've been able to write by hand over the years for natural number types/singletons, and I'm actually pretty happy with the fact that it makes it clearer that there is a distinction between the type level and the term level, and I can't say that I buy the idea of just throwing things open like that. In particular, the "OpenKind" for all kinds that you seem to be proposing sounds more like letting (->) :: forall (a :: BOX?) (b :: BOX?). a -> b -> * (or (->) :: forall (a :: BOX?). a -> * -> *) than OpenKind, which exists to track where unboxed types can lurk until polymorphism forces it to *. With the 'more open' OpenKind you propose, it no longer collapses to * when used in a polymorphic fashion, but merely dumbs down to forall (a :: BOX). a, which strikes me as a particularly awkward transition. At the least, you'd need to actually break the 'BOX is the only superkind' rule to provide the quantification that can span over unboxed types and any boxed type, (scribbled as BOX? above). That seems to be a pretty big mess for something that can be solved readily with simpler tools. Mind you there is another case for breaking the BOX is the only superkind rule (that is the horrible syntax hack that requires monomorphization of the kinds of the results of type/data families can be cleaned up), but once you have more than one superkind, you start complicating type equality, needing other coercions, so it really shouldn't be done lightly. -Edward ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Kindness of strangers (or strangeness of Kinds)
ghci> :k Maybe Maybe :: * -> * On Sat, Jun 9, 2012 at 1:34 AM, Rustom Mody wrote: > On Thu, Jun 7, 2012 at 7:16 AM, AntC wrote: > >> I'm confused about something with promoted Kinds (using an example with >> Kind- >> promoted Nats). >> >> This is in GHC 7.4.1. (Apologies if this is a known bug/limitation/already >> explained somewhere >> > > Is there a way of seeing kinds in ghci? > [In gofer I could do :s +k -- yeah this was 20 years ago :-) ] > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
