Re: Hiding module *exports*
-BEGIN PGP SIGNED MESSAGE- Hash: SHA256 I like symmetry. +1 from me. - -- Alexander alexan...@plaimi.net https://secure.plaimi.net/~alexander -BEGIN PGP SIGNATURE- Version: GnuPG v2 Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/ iF4EAREIAAYFAlRN/y8ACgkQRtClrXBQc7WR4AD/f6AXDZyAMk/oyn2SaVDigPr7 Xi/psgHQ+aoNKENSJLEA/13bfUPgW9sAaDNy+PwQ5QQb4PPcDE8NK/sVe3DVRXFJ =nXtH -END PGP SIGNATURE- ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
On 2014-10-26 at 20:28:41 +0100, Tom Murphy wrote: [...] > I propose that instead, we're able to simply say what we mean: > > module Foo hiding (Lockbox(MkLockbox), internalFunction) where > > I think its semantics are immediately clear to the reader. > > There's a little bit of bikeshedding that needs to happen (e.g. is "hiding > (Foo(..))" sufficient to hide the type Foo and not just its constructors), > but are people +1 on this? I've frequently wanted this behavior. I'm generally +1 on this, and I even suggested that one myself some time ago: http://www.haskell.org/pipermail/haskell-prime/2014-January/003910.html Cheers, hvr ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
+1 from me I was looking for the feature a few times. On 26 October 2014 19:28, Tom Murphy wrote: > (Not to be confused with the "hiding import behavior" discussion also > going on) > > -- > > Currently, I'm able to write "module Foo where" to export everything > defined in Foo. > > If, though, I add to the module some definitions which I don't want to > export... > > data Lockbox = MkLockbox Int > > internalFunction = ... > > ...I then have to explicitly enumerate everything that I *do* want the > module to export, and add to that list each time I add to the module. > > I propose that instead, we're able to simply say what we mean: > > module Foo hiding (Lockbox(MkLockbox), internalFunction) where > > I think its semantics are immediately clear to the reader. > > There's a little bit of bikeshedding that needs to happen (e.g. is "hiding > (Foo(..))" sufficient to hide the type Foo and not just its constructors), > but are people +1 on this? I've frequently wanted this behavior. > > Tom > > > ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > -- *Λ\ois* http://twitter.com/aloiscochard http://github.com/aloiscochard ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
On 2014-10-26 at 20:28:41 +0100, Tom Murphy wrote: [...] > module Foo hiding (Lockbox(MkLockbox), internalFunction) where > > I think its semantics are immediately clear to the reader. > > There's a little bit of bikeshedding that needs to happen (e.g. is "hiding > (Foo(..))" sufficient to hide the type Foo and not just its constructors), > but are people +1 on this? I've frequently wanted this behavior. PS: As for semantics, I'd suggest to have module Foo hiding (Lockbox(MkLockbox), internalFunction) where the same effect moving the definitions of `Foo` into an hidden/internal module `_Foo` and having `Foo` re-export it in the following way: module Foo (module _Foo) where import _Foo hiding (Lockbox(MkLockbox), internalFunction) that should result the least surprise IMHO Cheers, hvr ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
Hi Tom, +1 > There's a little bit of bikeshedding that needs to happen (e.g. is "hiding > (Foo > (..))" sufficient to hide the type Foo and not just its constructors), but are > people +1 on this? I've frequently wanted this behavior. I would be surprised if 'Foo(..)' would mean in this case something different, so yes, the type Foo should be hidden too. Greetings, Daniel ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
On Mon, Oct 27, 2014 at 2:41 PM, Daniel Trstenjak wrote: >> There's a little bit of bikeshedding that needs to happen (e.g. is "hiding >> (Foo >> (..))" sufficient to hide the type Foo and not just its constructors), but >> are >> people +1 on this? I've frequently wanted this behavior. > > I would be surprised if 'Foo(..)' would mean in this case something > different, so yes, the type Foo should be hidden too. One related question: how would you export only the type if you have newtype Foo = Foo ... which is a pretty common pattern? Since "hiding (Foo(Foo))" would also hide the type, I don't see many options, which is unfortunate. In general, I'm +1 on the proposal. Erik ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
El Oct 27, 2014, a las 7:42, Herbert Valerio Riedel escribió: > On 2014-10-26 at 20:28:41 +0100, Tom Murphy wrote: > > [...] > >>module Foo hiding (Lockbox(MkLockbox), internalFunction) where >> >> I think its semantics are immediately clear to the reader. >> >> There's a little bit of bikeshedding that needs to happen (e.g. is "hiding >> (Foo(..))" sufficient to hide the type Foo and not just its constructors), >> but are people +1 on this? I've frequently wanted this behavior. > > PS: As for semantics, I'd suggest to have > > module Foo hiding (Lockbox(MkLockbox), internalFunction) where > > the same effect moving the definitions of `Foo` into an hidden/internal > module `_Foo` and having `Foo` re-export it in the following way: > > module Foo (module _Foo) where > import _Foo hiding (Lockbox(MkLockbox), internalFunction) > > that should result the least surprise IMHO > Right -- hiding a type necessarily hides its constructors (and importing a constructor necessarily imports its type), which actually implies an obvious semantics. So there's less to bikeshed than I had thought. Tom ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
No, there's not another way to do this with built-in Nats, and there probably won't ever be. There are two advantages to the built-in Nats over hand-rolled ones: 1) Better syntax / error messages. 2) Built-in Nats are much more efficient than hand-rolled ones, because the hand-rolled ones are unary and take up space linear in the value of the number. If you re-hash your proposal for a Successor constructor down to the term level, it looks juts like (n+k)-patterns, which were discarded as a bad idea. The reason that the type-level numbers are natural numbers and not integers is because natural numbers have a simpler theory to solve for. I'm personally hoping for proper type-level integers at some point, and the type-checker plugins approach may make that a reality sooner than later. I hope this helps! Richard On Oct 25, 2014, at 9:53 AM, Barney Hilken wrote: > If you define your own type level naturals by promoting > > data Nat = Z | S Nat > > you can define data families recursively, for example > > data family Power :: Nat -> * -> * > data instance Power Z a = PowerZ > data instance Power (S n) a = PowerS a (Power n a) > > But if you use the built-in type level Nat, I can find no way to do the same > thing. You can define a closed type family > > type family Power (n :: Nat) a where > Power 0 a = () > Power n a = (a, Power (n-1) a) > > but this isn't the same thing (and requires UndecidableInstances). > > Have I missed something? The user guide page is pretty sparse, and not up to > date anyway. > > If not, are there plans to add a "Successor" constructor to Nat? I would have > thought this was the main point of using Nat rather than Int. > > Barney. > > ___ > 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: Hiding module *exports*
El Oct 27, 2014, a las 9:57, Erik Hesselink escribió: > On Mon, Oct 27, 2014 at 2:41 PM, Daniel Trstenjak > wrote: >>> There's a little bit of bikeshedding that needs to happen (e.g. is "hiding >>> (Foo >>> (..))" sufficient to hide the type Foo and not just its constructors), but >>> are >>> people +1 on this? I've frequently wanted this behavior. >> >> I would be surprised if 'Foo(..)' would mean in this case something >> different, so yes, the type Foo should be hidden too. > > One related question: how would you export only the type if you have > >newtype Foo = Foo ... > > which is a pretty common pattern? Since "hiding (Foo(Foo))" would also > hide the type, I don't see many options, which is unfortunate. > > In general, I'm +1 on the proposal. > I'd say "hiding (Foo)" hides the type and constructor; "hiding (Foo(Foo))" hides only the constructor. Tom > 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: Recursion on TypeNats
> No, there's not another way to do this with built-in Nats, and there probably > won't ever be. I do hope you're wrong. > There are two advantages to the built-in Nats over hand-rolled ones: 1) > Better syntax / error messages. 2) Built-in Nats are much more efficient than > hand-rolled ones, because the hand-rolled ones are unary and take up space > linear in the value of the number. If you re-hash your proposal for a > Successor constructor down to the term level, it looks juts like > (n+k)-patterns, which were discarded as a bad idea. (n+k) patterns are clearly a bad idea on integers, because the integers don't have the inductive structure, but they're a good idea on natural numbers, which is why they were in the language originally. > The reason that the type-level numbers are natural numbers and not integers > is because natural numbers have a simpler theory to solve for. I'm personally > hoping for proper type-level integers at some point, and the type-checker > plugins approach may make that a reality sooner than later. Type-level integers could well be useful, but they shouldn't replace type-level naturals, because they have completely different uses. At the value level, you can fudge the differences, because you can always return bottom, but at the type level you have to take correctness much more seriously if your type system is to be any use at all. The fact that Carter (and I) are forced to define hand-rolled nats on top of the built in ones demonstrates a clear need for this feature. It seems to me a valuable extension, whether the syntax uses Successor or (n+k). Why can't we combine the advantages of built-in Nats and hand-rolled ones? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
Your argument here is compelling. I have wanted type-level integers from the beginning and saw Nats as just a step toward integers. But, of course, this is silly -- you're right that Nats deserve their own place. Perhaps make a feature request for this. It may be related to type-level pattern synonyms, as proposed in #8828, comment:2. Richard On Oct 27, 2014, at 10:39 AM, Barney Hilken wrote: >> No, there's not another way to do this with built-in Nats, and there >> probably won't ever be. > > I do hope you're wrong. > >> There are two advantages to the built-in Nats over hand-rolled ones: 1) >> Better syntax / error messages. 2) Built-in Nats are much more efficient >> than hand-rolled ones, because the hand-rolled ones are unary and take up >> space linear in the value of the number. If you re-hash your proposal for a >> Successor constructor down to the term level, it looks juts like >> (n+k)-patterns, which were discarded as a bad idea. > > (n+k) patterns are clearly a bad idea on integers, because the integers don't > have the inductive structure, but they're a good idea on natural numbers, > which is why they were in the language originally. > >> The reason that the type-level numbers are natural numbers and not integers >> is because natural numbers have a simpler theory to solve for. I'm >> personally hoping for proper type-level integers at some point, and the >> type-checker plugins approach may make that a reality sooner than later. > > Type-level integers could well be useful, but they shouldn't replace > type-level naturals, because they have completely different uses. At the > value level, you can fudge the differences, because you can always return > bottom, but at the type level you have to take correctness much more > seriously if your type system is to be any use at all. > > The fact that Carter (and I) are forced to define hand-rolled nats on top of > the built in ones demonstrates a clear need for this feature. It seems to me > a valuable extension, whether the syntax uses Successor or (n+k). Why can't > we combine the advantages of built-in Nats and hand-rolled ones? > > Barney. > > > > ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Hiding module *exports*
+1. On Sun, Oct 26, 2014 at 3:28 PM, Tom Murphy wrote: > (Not to be confused with the "hiding import behavior" discussion also > going on) > > -- > > Currently, I'm able to write "module Foo where" to export everything > defined in Foo. > > If, though, I add to the module some definitions which I don't want to > export... > > data Lockbox = MkLockbox Int > > internalFunction = ... > > ...I then have to explicitly enumerate everything that I *do* want the > module to export, and add to that list each time I add to the module. > > I propose that instead, we're able to simply say what we mean: > > module Foo hiding (Lockbox(MkLockbox), internalFunction) where > > I think its semantics are immediately clear to the reader. > > There's a little bit of bikeshedding that needs to happen (e.g. is "hiding > (Foo(..))" sufficient to hide the type Foo and not just its constructors), > but are people +1 on this? I've frequently wanted this behavior. > > Tom > > > ___ > 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: Recursion on TypeNats
Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 Unfortunately I don't know enough about ghc internals to try implementing it. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
