Re: [Haskell-cafe] Safe Haskell and instance coherence
Hello David, On Wed, Oct 17, 2012 at 6:02 PM, David Mazieres expires 2013-01-15 PST mazieres-sebg4mvthwuzk9r27pqmr8j...@temporary-address.scs.stanford.edu wrote: Can you elaborate on how this can be used to break the data structure invariant? If in safe Haskell you import two modules that have overlapping instances, you will not be able to use the two instances. Modules that import only one instance will be able to use that instance. Please take a look at the code example I provided: https://gist.github.com/3854294 I don't use overlapping instances or any other extensions besides Safe Haskell. By defining two orphan Ord instances for U I'm able to construct a value of type Set U that contains two equal elements: test fromList [X,Y,X] This is what I meant by breaking the data structure invariant. This shouldn't normally be possible: the documentation for Data.Set.insert says: If the set already contains an element equal to the given value, it is replaced with the new value. Regarding your Monoid example, it will still be possible to make it work even if instance coherence is enforced by using a newtype wrapper (in fact, Data.Monoid already includes Sum and Product newtype wrappers that provide this functionality). -- () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
Hello David, On Thu, Oct 18, 2012 at 6:21 AM, David Mazieres expires 2013-01-15 PST mazieres-f97tx4hr7aw7n8sqs9kpcvu...@temporary-address.scs.stanford.edu wrote: What's interesting is that these examples doesn't violate the goals of Safe Haskell--i.e., they don't violate type safety, encapsulation, or semantic consistency as we defined it--but they are worrisome. I think that my example violates encapsulation in a similar way to how GND violates encapsulation in the MinList example from the Safe Haskell paper. IIUC, the problem is that all instances are assumed to be coherent (that's why it's an error to have two Monoid Int instances in the same module), but this assumption isn't actually enforced across module boundaries, even though it is reflected in the type system. GHC does print a warning after having encountered orphan instances, but that's all. This is essentially the same thing as my Monoid example. You've got two different dictionaries for the same type, and can pass either one around depending on what module you imported. Are dictionaries something that is a part of Haskell semantics or an artefact of the implementation? It's not hard to cook up a contrived example where some sort of security monitor hands over the keys to the kingdom if ever it encounters duplicate items in a set. Auditing the code, that might seem fine unless you understand the implementation of Set, which makes reasoning about security a lot harder. Agreed. What we really want is for the dictionary to be associated with the data structure at the time of creation, not passed in as an argument for each operation. But that's not even implementable without the existential types extension, and also would require re-writing all the containers, which is absolutely not what we want. This is what Scala does. Unfortunately, this can make some operations (e.g. set union) asymptotically less efficient (as it's now impossible to rely on the fact that both sets use the same associated dictionary). Failing that, I guess we could disallow overlapping instances even when they don't overlap in a single module. This is a whole-program check similar to what type families requires, so could possibly be implemented in a similar way. I'm really interested in the link-time check that is performed for type families. Is it described somewhere? However, as with type families, making it work with dynamic loading is going to be kind of hard. Essentially there would have to be some run-time inspectable information about all instances defined. I think that's why Rust chose to just disallow orphan instances :-) Even without dynamic loading, supporting all GHC extensions (e.g. FlexibleInstances) will probably be non-trivial. -- () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
On 08/10/2012 20:11, Mikhail Glushenkov wrote: Hello, It's a relatively well-known fact that GHC allows for multiple type class instances for the same type to coexist in a single program. This can be used, for example, to construct values of the type Data.Set.Set that violate the data structure invariant. I was mildly surprised to find out that this works even when Safe Haskell is turned on: https://gist.github.com/3854294 Note that the warnings tell us that both instances are [safe] which gives a false sense of security. I couldn't find anything on the interplay between orphan instances and Safe Haskell both in the Haskell'12 paper and online. Is this something that the authors of Safe Haskell are aware of/are intending to fix? A fine point. Arguably this violates the module abstraction guarantee, because you are able to discover something about the implementation of Set by violating its assumption that the Ord instance for a given type is always the same. I don't know what we should do about this. Disallowing orphan instances seems a bit heavy-handed. David, Simon, any thoughts? (can someone forward this to David Mazieres? all the email addresses I have for him seem to have expired :-) Cheers, Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
Hello Simon, On Thu, Oct 11, 2012 at 11:24 AM, Simon Marlow marlo...@gmail.com wrote: On 08/10/2012 20:11, Mikhail Glushenkov wrote: I couldn't find anything on the interplay between orphan instances and Safe Haskell both in the Haskell'12 paper and online. Is this something that the authors of Safe Haskell are aware of/are intending to fix? [...] I don't know what we should do about this. Disallowing orphan instances seems a bit heavy-handed. David, Simon, any thoughts? What about detecting duplicate instances at link time? We could put information about all instances defined in a given module into the .comment section of the corresponding .o file and then have a pre-link step script extract this information from all .o files in the program and check that there are no duplicate or conflicting instances. -- () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
On Oct 11, 2012, at 5:30 PM, Mikhail Glushenkov the.dead.shall.r...@gmail.com
wrote:
Hello Simon,
On Thu, Oct 11, 2012 at 11:24 AM, Simon Marlow marlo...@gmail.com wrote:
On 08/10/2012 20:11, Mikhail Glushenkov wrote:
I couldn't find anything on the interplay between orphan instances and
Safe Haskell both in the Haskell'12 paper and online. Is this
something that the authors of Safe Haskell are aware of/are intending
to fix?
[...]
I don't know what we should do about this. Disallowing orphan instances
seems a bit heavy-handed. David, Simon, any thoughts?
What about detecting duplicate instances at link time? We could put
information about all instances defined in a given module into the
.comment section of the corresponding .o file and then have a pre-link
step script extract this information from all .o files in the program
and check that there are no duplicate or conflicting instances.
You have a bigger problem coming. Some extensions make multiple instances OK,
even in Safe Haskell. For example:
{-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
module Over where
data Nil = Nil
newtype Cons a = Cons a
class Number n where value :: n - Integer
instance Number Nil where value Nil = 0
instance Number a = Number (Cons a) where value (Cons n) = value n + 1
instance Number (Cons (Cons Nil)) where value (Cons (Cons Nil)) = 2012
naturals = nats Nil where
nats :: Number n = n - [Integer]
nats n = value n : nats (Cons n)
Here we have two different instances Number (Con (Cons Nil)) at play, because
it gives you:
*Over value (Cons (Cons Nil))
2012
*Over take 5 naturals
[0,1,2,3,4]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
Hello,
On Thu, Oct 11, 2012 at 3:54 PM, MigMit miguelim...@yandex.ru wrote:
You have a bigger problem coming. Some extensions make multiple instances OK,
even in Safe Haskell. For example:
{-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
[...]
Safe Haskell already disallows OverlappingInstances. If we add a
requirement that it must be unambiguous which instance declaration a
given type class constraint resolves to (taking into account instances
defined in all modules), I think it will be necessary to also disallow
IncoherentInstances.
--
() ascii ribbon campaign - against html e-mail
/\ www.asciiribbon.org - against proprietary attachments
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
On Oct 11, 2012, at 6:23 PM, Mikhail Glushenkov the.dead.shall.r...@gmail.com
wrote:
Hello,
On Thu, Oct 11, 2012 at 3:54 PM, MigMit miguelim...@yandex.ru wrote:
You have a bigger problem coming. Some extensions make multiple instances
OK, even in Safe Haskell. For example:
{-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
[...]
Safe Haskell already disallows OverlappingInstances.
It doesn't. Overlapping instances are allowed in safe modules, provided that
they won't be used in other modules.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
Hello,
On Thu, Oct 11, 2012 at 4:33 PM, MigMit miguelim...@yandex.ru wrote:
On Oct 11, 2012, at 6:23 PM, Mikhail Glushenkov
the.dead.shall.r...@gmail.com wrote:
On Thu, Oct 11, 2012 at 3:54 PM, MigMit miguelim...@yandex.ru wrote:
You have a bigger problem coming. Some extensions make multiple instances
OK, even in Safe Haskell. For example:
{-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
[...]
Safe Haskell already disallows OverlappingInstances.
It doesn't. Overlapping instances are allowed in safe modules, provided that
they won't be used in other modules.
I stand corrected. Still, I think that something will have to be done
about IncoherentInstances if the aforementioned restriction will be
added.
--
() ascii ribbon campaign - against html e-mail
/\ www.asciiribbon.org - against proprietary attachments
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Safe Haskell and instance coherence
I hate to admit it, but it seems to me now that one would need dependent types
to guarantee Set's good behavior (so that the dictionary for the Ord instance
is contained within the Set type).
Отправлено с iPhone
Oct 11, 2012, в 18:42, Mikhail Glushenkov the.dead.shall.r...@gmail.com
написал(а):
Hello,
On Thu, Oct 11, 2012 at 4:33 PM, MigMit miguelim...@yandex.ru wrote:
On Oct 11, 2012, at 6:23 PM, Mikhail Glushenkov
the.dead.shall.r...@gmail.com wrote:
On Thu, Oct 11, 2012 at 3:54 PM, MigMit miguelim...@yandex.ru wrote:
You have a bigger problem coming. Some extensions make multiple instances
OK, even in Safe Haskell. For example:
{-# LANGUAGE FlexibleInstances, IncoherentInstances, Safe #-}
[...]
Safe Haskell already disallows OverlappingInstances.
It doesn't. Overlapping instances are allowed in safe modules, provided that
they won't be used in other modules.
I stand corrected. Still, I think that something will have to be done
about IncoherentInstances if the aforementioned restriction will be
added.
--
() ascii ribbon campaign - against html e-mail
/\ www.asciiribbon.org - against proprietary attachments
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Safe Haskell and instance coherence
Hello, It's a relatively well-known fact that GHC allows for multiple type class instances for the same type to coexist in a single program. This can be used, for example, to construct values of the type Data.Set.Set that violate the data structure invariant. I was mildly surprised to find out that this works even when Safe Haskell is turned on: https://gist.github.com/3854294 Note that the warnings tell us that both instances are [safe] which gives a false sense of security. I couldn't find anything on the interplay between orphan instances and Safe Haskell both in the Haskell'12 paper and online. Is this something that the authors of Safe Haskell are aware of/are intending to fix? -- () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
