Re: A question about run-time errors when class members are undefined
Hi. > Thanks Carlos. I wish I could say thank you for clarifying, but I'm > afraid this is as muddled as all the comments on the two proposals. > > I don't want to go over it again. I just want to say that my > suggestion earlier in the thread is fundamentally different. > >>Global instance scope is not ok either: instances should be modular. > I just plain disagree. Fundamentally. Global instance scope is not required for principal typing: a principal type is (just) a type of an expression in a given typing context that has all other types of this expression in that typing context as instances. (Also: instance modularity is not the central issue.) >>> Wadler & Blott's 1988 paper last paragraph had already explained: "But >>> there is no principal type! " >> There is always a principal type, for every expression. >> Of course the type depends on the context where the expression occurs. > Then it's not a _principal_ type for the expression, it's just a local type. > http://foldoc.org/principal A type system has the principal type property if, given a term and a typing context, there exists a type for this term in this typing context such that all other types for this term in this typing context are an instance of this type. > We arrive at the principal type by unifying the principal types of > the sub-expressions, down to the principal types of each atom. W > are pointing out that without global scope for instances, typing > cannot assign a principal type to each method. (They left that as an > open problem at the end of the paper. Haskell has resolved that > problem by making all instances global. Changing Haskell to modular > instances would be a breakage. Fundamentally.) > > Under my suggestion, we can assign a (global) principal type to each > method -- indeed you must, by giving a signature very similar to a > class declaration; and that distinguishes overloaded functions from > parametric polymorphic functions. A principal type theorem has been proved: see, for example, Theorem 1 in [1]. Kind regards, Carlos [1] Ambiguity and Constrained Polymorphism, Carlos Camarão, Lucília Figueiredo, Rodrigo Ribeiro, Science of Computer Programming 124(1), 1--19, August 2016. On Mon, 8 Oct 2018 at 20:03, Anthony Clayden wrote: > On Tue, 9 Oct 2018 at 7:30 AM, wrote: > > Thanks Carlos. I wish I could say thank you for clarifying, but I'm afraid > this is as muddled as all the comments on the two proposals. > > I don't want to go over it again. I just want to say that my suggestion > earlier in the thread is fundamentally different. > > Em 2018-10-08 06:21, Anthony Clayden escreveu: >> > On Mon, 8 Oct 2018 at 8:41 PM, Simon Peyton Jones wrote: >> > > > > Strange: Simon's message has not appeared on the forum (he did send to > it). I've quoted it in full in my reply, but did break it into separate > pieces. > > >> >> Global instance scope is not ok either: instances should be modular. > > > I just plain disagree. Fundamentally. > > >> > >> > Wadler & Blott's 1988 paper last paragraph had already explained: "But >> > there is no principal type! " >> >> There is always a principal type, for every expression. >> Of course the type depends on the context where the expression occurs. > > > Then it's not a _principal_ type for the expression, it's just a local > type. > http://foldoc.org/principal > > We arrive at the principal type by unifying the principal types of the > sub-expressions, down to the principal types of each atom. W are pointing > out that without global scope for instances, typing cannot assign a > principal type to each method. (They left that as an open problem at the > end of the paper. Haskell has resolved that problem by making all instances > global. Changing Haskell to modular instances would be a > breakage. Fundamentally.) > > Under my suggestion, we can assign a (global) principal type to each > method -- indeed you must, by giving a signature very similar to a class > declaration; and that distinguishes overloaded functions from parametric > polymorphic functions. > > > AntC > ___ > Haskell-prime mailing list > Haskell-prime@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime > ___ Haskell-prime mailing list Haskell-prime@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-prime
Reachable variables exercise
Hi. Consider for example an expression e0 like: fst (True,e) where e is any expression. e0 should have type Bool IMHO irrespectively of the type of e. In Haskell this is the case if e's type is monomorphic, or polymorphic, or constrained and there is a default in the current module that removes the constraints. However, e0 is not type-correct if e has a constrained type and the constraints are not subject to defaulting. For example: class O a where o::a main = print $ fst(True,o) generates a type error; in GHC: Ambiguous type variable `a' in the constraint: `O a' arising from a use of `o' at ... Probable fix: add a type signature that fixes these type variable(s) A solution (that avoids type signatures) can be given as follows. The type of f e, for f of type, say, K=t'-t and e of type K'= t' should be: K +_t K' = t (not K U K' = t) where K +_t K' denotes the constraint-set obtained by adding from K' only constraints with type variables reachable from t. (A type variable is reachable if it appears in the same constraint as either a type variable free in the type, or another reachable type variable.) Comments? Does that need and deserve a proposal? Cheers, Carlos ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Fwd: [Haskell-cafe] Reachable variables exercise
-- Forwarded message --
From: Carlos Camarao carlos.cama...@gmail.com
Date: Fri, Sep 17, 2010 at 12:01 AM
Subject: Re: [Haskell-cafe] Reachable variables exercise
To: Luke Palmer lrpal...@gmail.com
boolify o has type Boolable a = Bool under the proposal, then
we have ambiguity, type error, right?
In general, consider 'e' as (g:: K=a - t) (o:: O a=a); then the
type of 'e' has constraint (O a) iff 'a' occurs in t.
Let's think about how could 'a' not occur in t. That happens if 'o' is
not needed for computing the result; well, or, as in your example, 'g'
is overloaded and requires the argument to resolve the overloading
('a' occurs in K and does not occur in t), in which case K=t is
ambiguous.
Cheers,
Carlos
On Thu, Sep 16, 2010 at 6:56 PM, Luke Palmer lrpal...@gmail.com wrote:
I am not totally sure if I understand your proposal correctly, but if
I do, then it has a flaw. Consider:
class Boolable a where
boolify :: a - Bool
class O a where
o :: a
main = print $ boolify o
It seems like under your proposal this should not be a type error.
But if that is so, then what is its output?
Luke
On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao
carlos.cama...@gmail.com wrote:
Hi. Consider for example an expression e0 like:
fst (True,e)
where e is any expression.
e0 should have type Bool IMHO irrespectively of the type of e. In Haskell
this is the case if e's type is monomorphic, or polymorphic, or
constrained and there is a default in the current module that removes
the constraints. However, e0 is not type-correct if e has a
constrained type and the constraints are not subject to
defaulting. For example:
class O a where o::a
main = print $ fst(True,o)
generates a type error; in GHC:
Ambiguous type variable `a' in the constraint:
`O a' arising from a use of `o' at ...
Probable fix: add a type signature that fixes these type variable(s)
A solution (that avoids type signatures) can be given as follows.
The type of f e, for f of type, say, K=t'-t and e of type K'= t'
should be:
K +_t K' = t (not K U K' = t)
where K +_t K' denotes the constraint-set obtained by adding from K'
only constraints with type variables reachable from t.
(A type variable is reachable if it appears in the same constraint as
either a type variable free in the type, or another reachable type
variable.)
Comments? Does that need and deserve a proposal?
Cheers,
Carlos
___
Haskell-Cafe mailing list
haskell-c...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: [Haskell-cafe] Reachable variables exercise
Ah... now I understand your concern; I should have written something like: where K +_t K' denotes the set of constraints from K plus those from K' that have type variables reachable from t. instead of: where K +_t K' denotes the constraint-set obtained by adding from K' only constraints with type variables reachable from t. Cheers, Carlos On Thu, Sep 16, 2010 at 6:56 PM, Luke Palmer lrpal...@gmail.com wrote: I am not totally sure if I understand your proposal correctly, but if I do, then it has a flaw. Consider: class Boolable a where boolify :: a - Bool class O a where o :: a main = print $ boolify o It seems like under your proposal this should not be a type error. But if that is so, then what is its output? Luke On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao carlos.cama...@gmail.com wrote: Hi. Consider for example an expression e0 like: fst (True,e) where e is any expression. e0 should have type Bool IMHO irrespectively of the type of e. In Haskell this is the case if e's type is monomorphic, or polymorphic, or constrained and there is a default in the current module that removes the constraints. However, e0 is not type-correct if e has a constrained type and the constraints are not subject to defaulting. For example: class O a where o::a main = print $ fst(True,o) generates a type error; in GHC: Ambiguous type variable `a' in the constraint: `O a' arising from a use of `o' at ... Probable fix: add a type signature that fixes these type variable(s) A solution (that avoids type signatures) can be given as follows. The type of f e, for f of type, say, K=t'-t and e of type K'= t' should be: K +_t K' = t (not K U K' = t) where K +_t K' denotes the constraint-set obtained by adding from K' only constraints with type variables reachable from t. (A type variable is reachable if it appears in the same constraint as either a type variable free in the type, or another reachable type variable.) Comments? Does that need and deserve a proposal? Cheers, Carlos ___ Haskell-Cafe mailing list haskell-c...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
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-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
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-c...@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-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Proposal to solve Haskell's MPTC dilemma
On Thu, May 27, 2010 at 5:43 PM, David Menendez d...@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 Menendez d...@zednenem.com
http://www.eyrie.org/~zednenem/ 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.
Thanks for the clarification. I thought the point was about coherence.
Cheers,
Carlos
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
