Re: [Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
The situation is as if we [had] a FD: Well, that is indeed equivalent here in the second argument of class F, but I constructed the example to show an issue in the class's *first* argument. The example should be equivalent in all respects (at least that was my motivation when I wrote it). Notice you needed to add type-signatures, on the functions you named g -- in particular their first arguments -- to make the example work with only FDs? I wrote g, with type signatures, just to avoid writing the type signatures (f:: Bool-Bool and f::Int-Bool) inside (f o). I wanted to use, textually, the same expression. These are two different expressions that are being printed, because :: Bool - Bool is different from :: Int - Bool. In my example of using your proposal, one cannot inline in the same way, I wrote the example just to show that one can obtain the same effect with FDs: one not inline, i.e. use g o, in the same way. If your proposal was able to require those -- and only those -- bits of type signatures that were essential to resolve the above ambiguity; for example, the ( :: Int) below, module Q where import C instance F Int Bool where f = even instance O Int where o = 0 k = f (o :: Int) , then I would be fine with your proposal (but then I suspect it would have to be equivalent to FDs -- or in other words, that it's not really practical to change your proposal to have that effect). I stand by my assertion that the same expression means different things in two different modules is undesirable, (and that I suspect but am unsure that this undesirability is named incoherent instances). k::Bool; k=f o in Q has exactly the same effect as k=f(o::Int), under our proposal. (f o)::Bool in P and in Q are not the same expression, they are distinct expressions, because they occur in distinct contexts which make f and o in (f o)::Bool denote distinct values, just as (g o)::Bool are distinct expressions in P and Q in the example with a FD (because g and o in (g o)::Bool denote distinct values in P and in Q). Cheers, Carlos ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
On Fri, May 28, 2010 at 2:36 AM, Isaac Dupree
m...@isaac.cedarswampstudios.org wrote:
On 05/27/10 17:42, Carlos Camarao wrote:
On Thu, May 27, 2010 at 5:43 PM, David Menendezd...@zednenem.com
wrote:
On Thu, May 27, 2010 at 10:39 AM, Carlos Camarao
carlos.cama...@gmail.com wrote:
Isaac Dupree:
Your proposal appears to allow /incoherent/ instance selection.
This means that an expression can be well-typed in one module, and
well-typed in another module, but have different semantics in the
two modules. For example (drawing from above discussion) :
module C where
class F a b where f :: a - b
class O a where o :: a
module P where
import C
instance F Bool Bool where f = not
instance O Bool where o = True
k :: Bool
k = f o
module Q where
import C
instance F Int Bool where f = even
instance O Int where o = 0
k :: Bool
k = f o
module Main where
import P
import Q
-- (here, all four instances are in scope)
main = do { print P.k ; print Q.k }
-- should result, according to your proposal, in
-- False
-- True
-- , am I correct?
If qualified importation of k from both P and from Q was specified, we
would have two *distinct* terms, P.k and Q.k.
I think Isaac's point is that P.k and Q.k have the same definition (f
o). If they don't produce the same value, then referential
transparency is lost.
--
Dave Menendezd...@zednenem.com
http://www.eyrie.org/~zednenem/ http://www.eyrie.org/%7Ezednenem/
http://www.eyrie.org/%7Ezednenem/
The definitions of P.k and Q.k are textually the same but the contexts are
different. f and o denote distinct values in P and Q. Thus, P.k and
Q.k
don't have the same definition.
Oh, I guess you are correct: it is like defaulting: it is a similar effect
where the same expression means different things in two different modules as
if you had default (Int) in one, and default (Bool) in the other. Except:
Defaulting according to the standard only works in combination with the 8
(or however many it is) standard classes; and defaulting in Haskell is
already a bit poorly designed / frowned upon / annoying that it's specified
per-module when nothing else in the language is*.(that's a rather
surmountable argument)
It may be worth reading the GHC user's guide which attempts to explain the
difference between incoherent and non-incoherent instance selection,
http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/type-class-extensions.html#instance-overlap
I didn't read both it and your paper closely enough that I'm sure anymore
whether GHC devs would think your extension would require or imply
-XIncoherentInstances ... my intuition was that IncoherentInstances would be
implied...
*(it's nice when you can substitute any use of a variable, such as P.k,
with the expression that it is defined as -- i.e. the expression written so
that it refer to the same identifiers, not a purely textual substitution --
but in main above, you can't write [assuming you imported C] print (f o)
because it will be rejected for ambiguity. (Now, there is already an
instance-related situation like this where Main imports two different
modules that define instances that overlap in an incompatible way, such as
two different instances for Functor (Either e) -- not everyone is happy
about how GHC handles this, but at least those overlaps are totally useless
and could perhaps legitimately result in a compile error if they're even
imported into the same module.))
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
I have no idea why you think IncoherentInstances would be implied. The
proposal says: do not issue ambiguity error if, using whatever means
permitted and specified (OverlappingInstances, IncoherentInstances,
whatever), you can select a single instance.
The situation is as if we a FD:
module C where
class F a b | a-b where f :: a - b
class O a where o :: a
module P where
import C; instance F Bool Bool where f = not
instance O Bool where o = True
g:: Bool - Bool
g = f
k::Bool
k = g o
module Q where
import C
instance F Int Bool where f = even
instance O Int where o = 0
g::Int-Bool
g = f
k :: Bool
k = g o
module Main where
import P
import Q
main = do { print P.k ; print Q.k }
Cheers,
Carlos
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Proposal to solve Haskell's MPTC dilemma
On 05/29/10 21:24, Carlos Camarao wrote:
The situation is as if we a FD:
Well, that is indeed equivalent here in the second argument of class F,
but I constructed the example to show an issue in the class's *first*
argument.
Notice you needed to add type-signatures, on the functions you named g
-- in particular their first arguments -- to make the example work with
only FDs?
module C where
class F a b | a-b where f :: a - b
class O a where o :: a
module P where
import C; instance F Bool Bool where f = not
instance O Bool where o = True
g:: Bool - Bool
g = f
k::Bool
k = g o
module Q where
import C
instance F Int Bool where f = even
instance O Int where o = 0
g::Int-Bool
g = f
k :: Bool
k = g o
you can inline these k-definitions into module Main and it will work
(modulo importing C).
module Main where
import C
import P
import Q
main = do { print (((f :: Bool - Bool) o) :: Bool);
print (((f :: Int - Bool) o) :: Bool) }
These are two different expressions that are being printed, because
:: Bool - Bool is different from :: Int - Bool. In my example
of using your proposal, one cannot inline in the same way, if I
understand correctly (the inlining would cause ambiguity errors --
unless of course the above distinct type-signatures are added).
If your proposal was able to require those -- and only those -- bits of
type signatures that were essential to resolve the above ambiguity; for
example, the ( :: Int) below,
module Q where
import C
instance F Int Bool where f = even
instance O Int where o = 0
k = f (o :: Int)
, then I would be fine with your proposal (but then I suspect it would
have to be equivalent to FDs -- or in other words, that it's not really
practical to change your proposal to have that effect).
I stand by my assertion that the same expression means different things
in two different modules is undesirable, (and that I suspect but am
unsure that this undesirability is named incoherent instances).
I'm trying to work out whether it's possible to violate the invariants
of a Map by using your extension (having it select a different instance
in two different places, given the same type).. I think, no it is not
possible for Ord or any single-parameter typeclass, though there might
be some kind of issues with multi-parameter typeclasses, if the library
relies on a FD-style relationship between two class type-parameters and
then two someones each add an instance that together violate that
implied FD-relationship (which is allowed under your scheme, unlike if
there was an actual FD). Er, odd, I need to play with some actual FD
code to think about this, but I'm too sleepy / busy packing for a trip.
Did any of the above make sense to you? It's fine if some didn't, type
systems are complicated... and please point out if something I said was
outright wrong.
-Isaac
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
