Re: Linux deployment requirements for GHC-produced binaries
You may need to resort to strace to find out what's trying to pull in libgmp.so.whatever. I don't know how to do that. And anyway, I don't have access to the machine on which the customer is reporting this. I do believe the report - there is no compilation going on here, they are only running our GHC-compiled binary. They know nothing about GHC (not even that we are using it). I was hoping that there would be some general knowledge about this so I could just pass it on to our customers. But I see everyone else is as surprised as I am about a supposedly static GHC-compiled binary requiring a libgmp.so to run. Unless this program is like xmonad and requires ghc behind the scenes to build something, in which case you would indeed need everything that ghc requires (and, of course, ghc itself). No definitely not. Erik de Castro Lopo wrote: I suspect the OP's exectuable is already being compiled static. I compiled it static. Brandon Allbery wrote: Yes; which leaves the question of why it requires libgmp.so, and if it's static the only things I can think of are (a) it's using dlopen(), or (b) it's running something else that is not static and requires libgmp.so. Right. Could a dependent library be causing this? For example, this program depends on direct-sqlite, which in turn links to sqlite via FFI. It also depends on wai, which pulls in quite a few indirect dependencies. If so - how would I investigate this and get a complete list of the system libraries that customers are required to install as prerequisites? Jens Petersen wrote: You built ghc yourself? No. It is the generic Linux binary tarball from GHC HQ. And ran ldd on $bindir/ghc or $libdir/ghc-version ? No, in $bindir that's just a shell script. It's in $libdir. The executable is ghc; ghc-version is a directory containing object files compiled from libraries. Thanks, Yitz ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
I think it would be ok to expect the constructors to be visible, even
though it might need to a lot being needed.
BTW I think you might need S1 visible as well otherwise how would you
convert (S1 True :: S Bool Int) into (S1 True :: S Bool Age)?
If you don't derive the role from constructor visibility then I think it
should fail-safe and default to the nominal role - valid Haskell 2010
code shouldn't be exposed to an abstraction leak just because it's GHC
compiling it.
On 08/10/2013 14:23, Richard Eisenberg wrote:
Pedro is suggesting a way for a Haskell type-level program to gain
access to role information. This might indeed be useful, but it
doesn't seem terribly related to the problem of defaults /
abstraction. The problem has to do with definitions like these:
module A where
data S a b = S1 a | S2 b
data T a b = MkT (S a b)
module B where
import A ( {- what goes here? -} )
class C a where
mkT :: T Bool a
instance C Int where ...
newtype Age = MkAge Int deriving C
What constructors do we need in order to convert the (C Int) instance
to (C Age) by hand? To me, it looks like we need MkT and S2, but not
S1. Yet, this is not obvious and seems to be quite confusing.
I hope this helps understanding the issue!
Richard
On Oct 8, 2013, at 4:01 AM, José Pedro Magalhães drei...@gmail.com
mailto:drei...@gmail.com wrote:
Hi,
On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg e...@cis.upenn.edu
mailto:e...@cis.upenn.edu wrote:
We considered this for a while, but it led to a strange design --
to do it right, you would have to import all constructors for all
datatypes *recursively* out to the leaves, starting at the
datatypes mentioned in the class for which you wanted to use GND.
This would mean potentially a whole lot of imports for symbols
not actually used in the text of a program.
I'm not sure I understand why constructors are involved in this.
Wouldn't something like
the following potentially be useful?
data Role = Nominal | Representational | Phantom | Fun Role Role
type family HasRole (t :: k) :: Role
data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int
type instance HasRole MyData = Fun Representational Phantom
type instance HasRole MyGADT = Fun Representational Nominal
type instance HasRole Traversable = Nominal
HasRole instances would be automatically given by GHC.
Cheers,
Pedro
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
cabal upload -- error 404
Hi everybody, Does anybody know what this means and how to resolve it? I have updated my hackage account and can upload via the web interface, just not via cabal. cabal config file is new as well. cabal upload -c dist/PrimitiveArray-0.5.2.0.tar.gz Checking dist/PrimitiveArray-0.5.2.0.tar.gz... Error: dist/PrimitiveArray-0.5.2.0.tar.gz: 404 Not Found Sorry for this being the wrong mailing list ;-) Many thanks, Christian pgp1_9qBMCo5a.pgp Description: PGP signature ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: cabal upload -- error 404
If you really want to upload the package, then do cabal upload dist/PrimitiveArray-0.5.2.0.tar.gz (without -c). I'd guess that the new hackage server doesn't yet support the API required for -c. You can report this at https://github.com/haskell/cabal/issues although it will /probably/ end up at https://github.com/haskell/hackage-server/issues (Please also check that it isn't reported already.) Roman * Christian Hoener zu Siederdissen choe...@tbi.univie.ac.at [2013-10-09 16:32:17+0200] Hi everybody, Does anybody know what this means and how to resolve it? I have updated my hackage account and can upload via the web interface, just not via cabal. cabal config file is new as well. cabal upload -c dist/PrimitiveArray-0.5.2.0.tar.gz Checking dist/PrimitiveArray-0.5.2.0.tar.gz... Error: dist/PrimitiveArray-0.5.2.0.tar.gz: 404 Not Found Sorry for this being the wrong mailing list ;-) Many thanks, Christian ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users signature.asc Description: Digital signature ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
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 e...@cis.upenn.edu 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 = getSet
According to the way GND works, `good` and `bad` will have the same
runtime representation. But, using Set operations on `bad` would indeed be
bad -- because the Ord instance for Age is different than that for Int, Set
operations will fail unexpectedly on `bad`. The problem is that Set should
really be abstract, but we've been able to break this abstraction with GND.
Note that there is no type error in these operations, just wrong behavior.
So, if we default to *no* GND, then the deriving line above would have
an error and this problem wouldn't happen. If we default to *allowing* GND,
then the writer of Set would have to include
type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that
peculiar annotation? See the linked further reading, above.)
Although it doesn't figure in this example, a library writer who wishes to
allow GND in the default-no scenario would need a similar annotation
type role Foo representational
to allow it.
There are clearly reasons for and against either decision, but which is
better? Let the users decide!
Discussion time: 2 weeks.
Thanks!
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
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 iavor.diatc...@gmail.comwrote:
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 e...@cis.upenn.eduwrote:
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 = getSet
According to the way GND works, `good` and `bad` will have the same
runtime representation. But, using Set operations on `bad` would
Re: default roles
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 ekm...@gmail.com 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 restrictions on OverlappingInstances. -Edward On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki iavor.diatc...@gmail.com 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 e...@cis.upenn.edu 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
Re: Linux deployment requirements for GHC-produced binaries
I remember Tim Dysinger telling me some incantations needed to statically link Gmp into the static binary before deployment. I'll pester him to re remember what's needed, but the point is there's a way. On Wednesday, October 9, 2013, Yitzchak Gale wrote: You may need to resort to strace to find out what's trying to pull in libgmp.so.whatever. I don't know how to do that. And anyway, I don't have access to the machine on which the customer is reporting this. I do believe the report - there is no compilation going on here, they are only running our GHC-compiled binary. They know nothing about GHC (not even that we are using it). I was hoping that there would be some general knowledge about this so I could just pass it on to our customers. But I see everyone else is as surprised as I am about a supposedly static GHC-compiled binary requiring a libgmp.so to run. Unless this program is like xmonad and requires ghc behind the scenes to build something, in which case you would indeed need everything that ghc requires (and, of course, ghc itself). No definitely not. Erik de Castro Lopo wrote: I suspect the OP's exectuable is already being compiled static. I compiled it static. Brandon Allbery wrote: Yes; which leaves the question of why it requires libgmp.so, and if it's static the only things I can think of are (a) it's using dlopen(), or (b) it's running something else that is not static and requires libgmp.so. Right. Could a dependent library be causing this? For example, this program depends on direct-sqlite, which in turn links to sqlite via FFI. It also depends on wai, which pulls in quite a few indirect dependencies. If so - how would I investigate this and get a complete list of the system libraries that customers are required to install as prerequisites? Jens Petersen wrote: You built ghc yourself? No. It is the generic Linux binary tarball from GHC HQ. And ran ldd on $bindir/ghc or $libdir/ghc-version ? No, in $bindir that's just a shell script. It's in $libdir. The executable is ghc; ghc-version is a directory containing object files compiled from libraries. Thanks, Yitz ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org javascript:; 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: Linux deployment requirements for GHC-produced binaries
there seem to be two main approaches (which both require some testing) 1) build ghc with integer-simple 2) do some static linking tricks on your side, such as those described in http://stackoverflow.com/questions/809794/use-both-static-and-dynamically-linked-libraries-in-gcc, this might entail that you need to know the precise OS / Distro a client is using before you give them a binary, but might make the process much simpler overall (despite its relative hackiness) On Wed, Oct 9, 2013 at 2:22 PM, Carter Schonwald carter.schonw...@gmail.com wrote: I remember Tim Dysinger telling me some incantations needed to statically link Gmp into the static binary before deployment. I'll pester him to re remember what's needed, but the point is there's a way. On Wednesday, October 9, 2013, Yitzchak Gale wrote: You may need to resort to strace to find out what's trying to pull in libgmp.so.whatever. I don't know how to do that. And anyway, I don't have access to the machine on which the customer is reporting this. I do believe the report - there is no compilation going on here, they are only running our GHC-compiled binary. They know nothing about GHC (not even that we are using it). I was hoping that there would be some general knowledge about this so I could just pass it on to our customers. But I see everyone else is as surprised as I am about a supposedly static GHC-compiled binary requiring a libgmp.so to run. Unless this program is like xmonad and requires ghc behind the scenes to build something, in which case you would indeed need everything that ghc requires (and, of course, ghc itself). No definitely not. Erik de Castro Lopo wrote: I suspect the OP's exectuable is already being compiled static. I compiled it static. Brandon Allbery wrote: Yes; which leaves the question of why it requires libgmp.so, and if it's static the only things I can think of are (a) it's using dlopen(), or (b) it's running something else that is not static and requires libgmp.so. Right. Could a dependent library be causing this? For example, this program depends on direct-sqlite, which in turn links to sqlite via FFI. It also depends on wai, which pulls in quite a few indirect dependencies. If so - how would I investigate this and get a complete list of the system libraries that customers are required to install as prerequisites? Jens Petersen wrote: You built ghc yourself? No. It is the generic Linux binary tarball from GHC HQ. And ran ldd on $bindir/ghc or $libdir/ghc-version ? No, in $bindir that's just a shell script. It's in $libdir. The executable is ghc; ghc-version is a directory containing object files compiled from libraries. Thanks, Yitz ___ 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
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 e...@cis.upenn.edu 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 ekm...@gmail.com 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 restrictions on OverlappingInstances. -Edward On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki iavor.diatc...@gmail.comwrote: 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
Re: Linux deployment requirements for GHC-produced binaries
NB: I'm told that building ghc with integer-simple doesn't work on linux?! (though the person who told me this may not have filed a ticket about this on trac, so i'm not sure if its still an issue with ghc head or not ) On Wed, Oct 9, 2013 at 2:47 PM, Carter Schonwald carter.schonw...@gmail.com wrote: there seem to be two main approaches (which both require some testing) 1) build ghc with integer-simple 2) do some static linking tricks on your side, such as those described in http://stackoverflow.com/questions/809794/use-both-static-and-dynamically-linked-libraries-in-gcc, this might entail that you need to know the precise OS / Distro a client is using before you give them a binary, but might make the process much simpler overall (despite its relative hackiness) On Wed, Oct 9, 2013 at 2:22 PM, Carter Schonwald carter.schonw...@gmail.com wrote: I remember Tim Dysinger telling me some incantations needed to statically link Gmp into the static binary before deployment. I'll pester him to re remember what's needed, but the point is there's a way. On Wednesday, October 9, 2013, Yitzchak Gale wrote: You may need to resort to strace to find out what's trying to pull in libgmp.so.whatever. I don't know how to do that. And anyway, I don't have access to the machine on which the customer is reporting this. I do believe the report - there is no compilation going on here, they are only running our GHC-compiled binary. They know nothing about GHC (not even that we are using it). I was hoping that there would be some general knowledge about this so I could just pass it on to our customers. But I see everyone else is as surprised as I am about a supposedly static GHC-compiled binary requiring a libgmp.so to run. Unless this program is like xmonad and requires ghc behind the scenes to build something, in which case you would indeed need everything that ghc requires (and, of course, ghc itself). No definitely not. Erik de Castro Lopo wrote: I suspect the OP's exectuable is already being compiled static. I compiled it static. Brandon Allbery wrote: Yes; which leaves the question of why it requires libgmp.so, and if it's static the only things I can think of are (a) it's using dlopen(), or (b) it's running something else that is not static and requires libgmp.so. Right. Could a dependent library be causing this? For example, this program depends on direct-sqlite, which in turn links to sqlite via FFI. It also depends on wai, which pulls in quite a few indirect dependencies. If so - how would I investigate this and get a complete list of the system libraries that customers are required to install as prerequisites? Jens Petersen wrote: You built ghc yourself? No. It is the generic Linux binary tarball from GHC HQ. And ran ldd on $bindir/ghc or $libdir/ghc-version ? No, in $bindir that's just a shell script. It's in $libdir. The executable is ghc; ghc-version is a directory containing object files compiled from libraries. Thanks, Yitz ___ 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
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 ekm...@gmail.com 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. 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 e...@cis.upenn.edu 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
Re: default roles
Hi, Am Mittwoch, den 09.10.2013, 15:21 -0400 schrieb Richard Eisenberg: 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. what do you need the extra bit for? During GHD, can’t you just create the new dictionary (using method = coerce original_method) and then see if it typechecks, i.e. if the method types can be coerced. (If not, the error messages might need massaging, though.) Greetings, Joachim -- 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 signature.asc Description: This is a digitally signed message part ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg e...@cis.upenn.edu 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
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 e...@cis.upenn.edu 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 ekm...@gmail.com 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. 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 e...@cis.upenn.eduwrote: I don't quite agree with your analysis, Edward. Eq can be auto-derived, so it makes for
Re: default roles
On Oct 9, 2013, at 3:41 PM, Joachim Breitner m...@joachim-breitner.de wrote: what do you need the extra bit for? During GHD, can’t you just create the new dictionary (using method = coerce original_method) and then see if it typechecks, i.e. if the method types can be coerced. Efficiency. You're absolutely right -- you could just run the check at a use site of GND. I just thought it was cleaner to talk about storing it. On Oct 9, 2013, at 3:41 PM, Edward Kmett ekm...@gmail.com wrote: This strikes me as a remarkably straightforward solution. Does it strike you as something implementable in time for 7.8 though? Yes. I imagine updating the documentation will be harder than updating the implementation, especially if we go with Joachim's checking lazily idea -- that is, at the use site of GND instead of pre-calculating whether GND would work. The error messages would be easy to get right, and might actually be more informative than they currently are. Come to think of it, calculating this at the use site of GND is probably preferable as it will improve error messages -- users will see exactly which feature of a class makes it unsuitable for GND. This is a big improvement over the error message now. And, just a slightly-cleverer-than-the-dumbest-possible test here would allow, say, GND to work with (IArray UArray), a need which came up within GHC and with one of the failing packages on Hackage. 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. Yes, of course. That's why it must be the way it is. On Oct 9, 2013, at 3:44 PM, Edward Kmett ekm...@gmail.com wrote: 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. ;) Perhaps if IncoherentInstances is on, classes get representational roles. This actually makes sense -- IncoherentInstances says not to care about coherence, and the nominal roles on classes are to enforce coherence. The Coercible class is very incoherent (as in, *any* instance of the right type will work; we don't care which one), and so it should have representational roles, according to this logic. This default could be overridden by a type annotation, but I'm inclined *not* to let users override a class's default nominal role with an annotation. Richard ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
Hi, not sure if this is not old news to you all, but I think that for this discussion, it helps to consider these two aspects of a class instance separately: (1) An instance is a record of functions (2) An instance is a function of sorts¹ from types to (1) and clearly, type parameters of (1) can be representational, but the function in (2) should have its parameters nominal. Therefore it is fine to coerce the dictionary of a function (and would we want to implement GND this ways, that would be fine), but not a type involving a constraint. Inside GHC, as far as I can tell, (2) exists in the form of the instance metadata, and disappears after desugaring, while (1) is the actual dictionary that exists in core as a regular data type. So the conclusion is indeed: Let type class constraints have a nominal role, and all is fine. Greetings, Joachim ¹ well, a kind of function. But not that type of kind, but the other type. Sort of, at least. -- 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 signature.asc Description: This is a digitally signed message part ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: default roles
On Oct 9, 2013, at 6:24 PM, Joachim Breitner m...@joachim-breitner.de wrote: So the conclusion is indeed: Let type class constraints have a nominal role, and all is fine. But, then it would seem that any class with a superclass wouldn't be compatible with GND. Do you see that detail as a consequence of this design? I think this approach might work, but I'm not yet convinced. Richard ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
