implicit params in instance contexts
Hi,
It seems that from GHC 7.4, the prohibition on implicit parameter
constraints in instance declarations has been relaxed. The program below
gives the error Illegal constraint ?fooRev::Bool in GHC 7.2.1 but
loads fine in GHC 7.4.2 and GHC 7.6.2.
I can't spot anything about this in the release notes, and the
documentation
(http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-extensions.html#idp49069584)
still says You can't have an implicit parameter in the context of a
class or instance declaration.
So I wonder if this happened by accident, perhaps as part of the
ConstraintKinds work or similar?
I've wanted this feature a few times so if it's going to stay I might
start using it. However it is a bit dangerous, so if it was added by
accident it might warrant some discussion before deciding to keep it.
For example as the value set2 below shows, it can be used to violate
datatype invariants.
Cheers,
Ganesh
{-# LANGUAGE ImplicitParams #-}
module Ord where
import Data.Set ( Set )
import qualified Data.Set as Set
newtype Foo = Foo Int
deriving (Eq, Show)
instance (?fooRev :: Bool) = Ord Foo where
Foo a `compare` Foo b =
if ?fooRev then b `compare` a else a `compare` b
set1 = let ?fooRev = False in Set.fromList [Foo 1, Foo 3]
set2 = let ?fooRev = True in Set.insert (Foo 2) set1
-- Ord set2
-- fromList [Foo 2,Foo 1,Foo 3]
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: implicit params in instance contexts
| It seems that from GHC 7.4, the prohibition on implicit parameter
| constraints in instance declarations has been relaxed. The program below
| gives the error Illegal constraint ?fooRev::Bool in GHC 7.2.1 but
| loads fine in GHC 7.4.2 and GHC 7.6.2.
I don't I changed this intentionally, but the type system has been refactored
so massively over the years (it's way better than before!) that it's entirely
possible it happened as an unintentional consequence.
There is actually a good reason. For a function
f :: (?x::Int) = blah
it's clear where 'f' occurs, and hence which ?x you get:
g y = let ?x=4 in (let ?x=5 in ...f...) ...f...
The first call to 'f' sees ?x=5, and the second sees ?x=4. IP bindings are
like local instance declarations.
But suppose we had
class D a where { op :: a - a }
instance (?x::Int) = D Int where ...
g y = let ?x=4 in (let ?x=5 in ...op (y::Int)...) ..
The call to op gives rise to a constraint (D Int). Where does that constraint
get solved? Right at the call to 'op'? Then it'll see ?x=5? or further out?
then it'll see ?x=4. Or at top level? Then it won't see a binding for ?x at
all.
This is bad. Currently the site at which instance declarations are used isn't
important, but now it would become important, and the semantics of the program
would depend on it.
I think I should disable it again!
Simon
| -Original Message-
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Ganesh Sittampalam
| Sent: 16 July 2013 07:21
| To: glasgow-haskell-users@haskell.org
| Subject: implicit params in instance contexts
|
| Hi,
|
| It seems that from GHC 7.4, the prohibition on implicit parameter
| constraints in instance declarations has been relaxed. The program below
| gives the error Illegal constraint ?fooRev::Bool in GHC 7.2.1 but
| loads fine in GHC 7.4.2 and GHC 7.6.2.
|
| I can't spot anything about this in the release notes, and the
| documentation
| (http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-
| extensions.html#idp49069584)
| still says You can't have an implicit parameter in the context of a
| class or instance declaration.
|
| So I wonder if this happened by accident, perhaps as part of the
| ConstraintKinds work or similar?
|
| I've wanted this feature a few times so if it's going to stay I might
| start using it. However it is a bit dangerous, so if it was added by
| accident it might warrant some discussion before deciding to keep it.
| For example as the value set2 below shows, it can be used to violate
| datatype invariants.
|
| Cheers,
|
| Ganesh
|
|
| {-# LANGUAGE ImplicitParams #-}
| module Ord where
|
| import Data.Set ( Set )
| import qualified Data.Set as Set
|
| newtype Foo = Foo Int
| deriving (Eq, Show)
|
| instance (?fooRev :: Bool) = Ord Foo where
| Foo a `compare` Foo b =
| if ?fooRev then b `compare` a else a `compare` b
|
| set1 = let ?fooRev = False in Set.fromList [Foo 1, Foo 3]
|
| set2 = let ?fooRev = True in Set.insert (Foo 2) set1
| -- Ord set2
| -- fromList [Foo 2,Foo 1,Foo 3]
|
| ___
| 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: implicit params in instance contexts
On Mon, Jul 15, 2013 at 11:21 PM, Ganesh Sittampalam gan...@earth.li wrote: Hi, It seems that from GHC 7.4, the prohibition on implicit parameter constraints in instance declarations has been relaxed. The program below gives the error Illegal constraint ?fooRev::Bool in GHC 7.2.1 but loads fine in GHC 7.4.2 and GHC 7.6.2. I can't spot anything about this in the release notes, and the documentation (http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-extensions.html#idp49069584) still says You can't have an implicit parameter in the context of a class or instance declaration. So I wonder if this happened by accident, perhaps as part of the ConstraintKinds work or similar? I've wanted this feature a few times so if it's going to stay I might start using it. However it is a bit dangerous, so if it was added by accident it might warrant some discussion before deciding to keep it. For example as the value set2 below shows, it can be used to violate datatype invariants. There was a post about this previously: http://joyoftypes.blogspot.com/2013/01/using-compiler-bugs-for-fun-and-profit.html And a GHC ticket: http://ghc.haskell.org/trac/ghc/ticket/7624 See also the discussion at http://www.reddit.com/r/haskell/comments/178w9u/using_compiler_bugs_for_fun_and_profit/ Shachaf ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: implicit params in instance contexts
GHC ticket:
http://ghc.haskell.org/trac/ghc/ticket/7624
2013/7/16 Ganesh Sittampalam gan...@earth.li
Hi,
It seems that from GHC 7.4, the prohibition on implicit parameter
constraints in instance declarations has been relaxed. The program below
gives the error Illegal constraint ?fooRev::Bool in GHC 7.2.1 but
loads fine in GHC 7.4.2 and GHC 7.6.2.
I can't spot anything about this in the release notes, and the
documentation
(
http://www.haskell.org/ghc/docs/7.6.3/html/users_guide/other-type-extensions.html#idp49069584
)
still says You can't have an implicit parameter in the context of a
class or instance declaration.
So I wonder if this happened by accident, perhaps as part of the
ConstraintKinds work or similar?
I've wanted this feature a few times so if it's going to stay I might
start using it. However it is a bit dangerous, so if it was added by
accident it might warrant some discussion before deciding to keep it.
For example as the value set2 below shows, it can be used to violate
datatype invariants.
Cheers,
Ganesh
{-# LANGUAGE ImplicitParams #-}
module Ord where
import Data.Set ( Set )
import qualified Data.Set as Set
newtype Foo = Foo Int
deriving (Eq, Show)
instance (?fooRev :: Bool) = Ord Foo where
Foo a `compare` Foo b =
if ?fooRev then b `compare` a else a `compare` b
set1 = let ?fooRev = False in Set.fromList [Foo 1, Foo 3]
set2 = let ?fooRev = True in Set.insert (Foo 2) set1
-- Ord set2
-- fromList [Foo 2,Foo 1,Foo 3]
___
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: [GHC] #7279: warning for unused type variables in instance contexts; -fwarn-unreachable-type-variables?
#7279: warning for unused type variables in instance contexts;
-fwarn-unreachable-
type-variables?
--+-
Reporter: nfrisby | Owner:
Type: feature request | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type checker) |Version: 7.6.1
Resolution: fixed| Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: typecheck/should_fail/T7279 | Blockedby:
Blocking: |Related:
--+-
Changes (by simonpj):
* status: new = closed
* difficulty: = Unknown
* resolution: = fixed
* testcase: = typecheck/should_fail/T7279
Comment:
This fix to ambiguity checking solves the problem
{{{
commit 97db0edc4e637dd61ec635d1f9b6b6dd25ad890c
Author: Simon Peyton Jones simo...@microsoft.com
Date: Tue Jan 8 08:26:40 2013 +
Re-engineer the ambiguity test for user type signatures
Two main changes. First, re-engineer the ambiguity test. Previously
TcMType.checkAmbiguity used a rather syntactic test to detect some
types that are certainly ambiguous. But a much easier test is
available,
and it is used for inferred types in TcBinds. Namely
type is ambiguous
iff
type `TcUnify.isSubType` type
fails to hold, where isSubType means is provably more polymorphic
than.
Example:
C a = Int
is ambiguous, because isSubType instantiates the (C a = Int)
to (C alpha = Int) and then tries to deduce (C alpha) from (C a).
This is
Martin Sulzmann's definition of ambiguity. (Defn 10 of Understanding
functional dependencies via constraint handling rules, JFP.)
This change is neat, reduces code, and correctly rejects more
programs.
However is *is* just possible to have a useful program that would be
rejected. For example
class C a b
f :: C Int b = Int - Int
Here 'f' would be rejected as having an ambiguous type. But it is
just possible that, at a *call* site there might be an instance
declaration instance C Int b, which does not constrain 'b' at all.
This is pretty strange -- why is 'b' overloaded at all? -- but it's
possible, so I also added a flag -XAllowAmbiguousTypes that simply
removes the ambiguity check. Let's see if anyone cares. Meanwhile
the earlier error report will be useful for everyone else.
A handful of regression tests had to be adjusted as a result, because
they used ambiguous types, somewhat accidentally.
Second, split TcMType (already too large) into two
* TcMType: a low-level module dealing with monadic operations like
zonking, creating new evidence variables, etc
* TcValidity: a brand-new higher-level module dealing with
validity checking for types: checkValidType, checkValidInstance,
checkFamInstPats etc
Apart from the fact that TcMType was too big, this allows TcValidity
to import TcUnify(tcSubType) without causing a loop.
compiler/ghc.cabal.in |1 +
compiler/main/DynFlags.hs |2 +
compiler/typecheck/TcBinds.lhs | 28 +-
compiler/typecheck/TcDeriv.lhs | 132 +
compiler/typecheck/TcErrors.lhs | 143 ++---
compiler/typecheck/TcEvidence.lhs |4 +-
compiler/typecheck/TcHsType.lhs |1 +
compiler/typecheck/TcInstDcls.lhs |1 +
compiler/typecheck/TcMType.lhs | 1063
+--
compiler/typecheck/TcPat.lhs|1 +
compiler/typecheck/TcRnTypes.lhs|8 +-
compiler/typecheck/TcSMonad.lhs |9 +-
compiler/typecheck/TcSimplify.lhs | 152 +-
compiler/typecheck/TcTyClsDecls.lhs |1 +
14 files changed, 248 insertions(+), 1298 deletions(-)
}}}
Now the instance declaration will (rightly) be rejected as ambiguous. So
either you get
{{{
T7279.hs:5:10:
Variable `b' occurs more often than in the instance head
in the constraint: Show b
(Use -XUndecidableInstances to permit this)
In the instance declaration for `Eq (T a)'
}}}
or, if you add `-XUndecidableInstances` you get the ambiguity error
instead:
{{{
T7279.hs:6:10:
Could not deduce (Show b0)
arising from the ambiguity check for an instance declaration
from the context (Eq a, Show b)
bound by an instance declaration: (Eq a, Show b) = Eq (T a)
at T7279.hs:6:10-35
The type variable `b0' is ambiguous
In the ambiguity check for: forall a b. (Eq
[GHC] #7279: warning for unused type variables in instance contexts; -fwarn-unreachable-type-variables?
#7279: warning for unused type variables in instance contexts;
-fwarn-unreachable-
type-variables?
--+-
Reporter: nfrisby | Owner:
Type: feature request | Status: new
Priority: normal| Component: Compiler (Type checker)
Version: 7.6.1 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby:| Blocking:
Related:|
--+-
I just spend 90 minutes tracking down what ended up being a typo
introduced via find-and-replace.
I accidentally introduced a spurious constraint on an instance context:
{{{
instance (Monoid m, Context t) = Class t where …
}}}
I would like to be warned about constraints on variables that certainly
have no connection to variables in the instance head. {{{-fwarn-
unreachable-type-variables}}}?
This might also help catch those signatures where all occurrences of type
variable are as index arguments to a type family, rendering the functional
unusable because of ambiguous type variable errors at every call site.
--
Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/7279
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler
___
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
[Haskell-cafe] Difference between class and instance contexts
Below are examples of using the sub-class context at class level and at instance level. In this simple case they seem to give the same resultsIn general, are there certain situations in which one or the other is preferred? Patmodule CLASS where-- class and sub-classclass Class a where foo :: a - a foo a = aclass Class a = SubClass a where moo :: a - a moo a = foo ainstance Class Integer whereinstance SubClass Integer where*CLASS :t foo 2foo 2 :: forall t. (Class t, Num t) = t*CLASS :t moo 2moo 2 :: forall t. (SubClass t, Num t) = tmodule INSTANCE where-- Using context at instance level-- Is class Class a where foo :: a - a foo a = aclass SubClass a where moo :: a - ainstance Class Integer whereinstance Class Integer = SubClass Integer where moo a = foo aINSTANCE :t foo 2foo 2 :: forall t. (Class t, Num t) = tINSTANCE :t moo 2moo 2 :: forall t. (SubClass t, Num t) = t ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Difference between class and instance contexts
On Aug 3, 2011 1:33 PM, Patrick Browne patrick.bro...@dit.ie wrote: instance Class Integer = SubClass Integer where moo a = foo a Since you've just written the Class instance for Integer, the superclass context is actually irrelevant there. You may as well just write instance SubClass Integer where moo a = foo a And that goes to the point of what the difference is. In the first case, you were declaring that all SubClass instances are Class instances, and that mo defaults to foo for ALL types. In the latter case, you're defining this just for Integer. The difference is whether that default exists for other tyoes, or if its specific to Integer. -- Chris Smith ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Difference between class and instance contexts
Try :t (foo 2, moo 2) On 3 Aug 2011, at 23:31, Patrick Browne wrote: Below are examples of using the sub-class context at class level and at instance level. In this simple case they seem to give the same results In general, are there certain situations in which one or the other is preferred? Pat module CLASS where -- class and sub-class class Class a where foo :: a - a foo a = a class Class a = SubClass a where moo :: a - a moo a = foo a instance Class Integer where instance SubClass Integer where *CLASS :t foo 2 foo 2 :: forall t. (Class t, Num t) = t *CLASS :t moo 2 moo 2 :: forall t. (SubClass t, Num t) = t module INSTANCE where -- Using context at instance level -- Is class Class a where foo :: a - a foo a = a class SubClass a where moo :: a - a instance Class Integer where instance Class Integer = SubClass Integer where moo a = foo a INSTANCE :t foo 2 foo 2 :: forall t. (Class t, Num t) = t INSTANCE :t moo 2 moo 2 :: forall t. (SubClass t, Num t) = t ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Instance contexts constraining only type variables?
Wolfgang Lux wrote: Wolfgang Jeltsch wrote Hello, say I have a type T defined the follwing way: newtype T a b = T (a b) Now I want to make every T a b with a b beeing an instance of Eq also an instance of Eq where (==) just test for equality of the encapsulated values. I try this instance Eq (a b) = Eq (T a b) where (T x) == (T x') = x == x' but it seems that this is not Haskell 98 conformant. You probably meant a and b being an instance of Eq, No! Look at the definition of T. Right to the equals sign there is T (a b) which implies that a b has kind * and therefore kind (a) = kind (b) - * if for any type t kind (t) is the kind of t. So a can never be an instance of Eq because it doesn't have kind *. Every value of type T encapsulates exactly one value which is of type a b. I want to test for equality of these values wherefore a b has to be an instance of Eq. By the way, why is (* - *) - * - * the infered kind of T and not for instance ((* - *) - *) - (* - *) - *? so you should write it down the same way :-) instance (Eq a,Eq b) = Eq (T a b) where ... Wolfgang -- Wolfgang Lux Phone: +49-251-83-38263 Institut fuer Wirtschaftinformatik FAX: +49-251-83-38259 Universitaet Muenster Email: [EMAIL PROTECTED] Wolfgang ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Non-variable instance contexts.
I hate this error. Whilst arguably this is an "untested" extension
to Standard Haskell, it seemed pretty sound in practice. Can't
we at least have it back as a GlaExt? (MSExt?) I'm starting to
feel more than a little Quaint having to use ghc-3.01, just to get
my programs to compile... (If anyone has a good systematic workaround
to suggest, I'm all ears.)
ghc-4.00 -c Intervals.hs -H30m -K2M -recomp -fglasgow-exts -cpp -syslib
misc -Rgc-stats -dshow-passes -fmax-simplifier-iterations4
-funfolding-use-threshold-0 -fvia-C
Intervals.hs:460:
Illegal constaint `Ord (s e)' in instance context
(Instance contexts must constrain only type variables)
[etc, etc]
Slainte,
Alex.
Re: Instance contexts.
| I'd like to support Alex here: it is absolutely necessary to relax | condition 10 of SPJ's list. | | http://www.dcs.gla.ac.uk/~simonpj/multi-param.html | | Idioms like the one above (`Ord (s a)' or | `Show (s a)') arise too often and are completely natural. | | One of the great merits of imposing restrictions is that | you hear about when they are irritating :-). (The reverse does | not hold.) Examples like this are jolly useful. | | Ralf: can you supply other examples? Here is another one. It seems that condition 10 hinders the use of abstraction. Consider the following innocent looking definitions data Tree a = Empty | Node (Tree a) a (Tree a) deriving (Show) data Cons a = Cons a (Tree a) deriving (Show) and suppose that we want to abstract away `Cons's dependency on `Tree'. data Cons tree a = Cons a (tree a) deriving (Show) Now, we have a context of the form instance (Show (tree a), Show a) = Show (Cons tree a) which violates condition 10. And note that this might happen as soon as you use higher-order polymorphism (types of kind * - *). Cheers, Ralf
the monomorphism restriction (was: instance contexts)
On 15-Jul-1998, Alex Ferguson [EMAIL PROTECTED] wrote: Fergus Henderson writes of: the monomorphism restriction (which exists for a similar reason, to ensure termination of type inference). Is this true? The rationale normally given for it by its advocates (boo, hiss) seems invariably the "no re-evaluation of CAFs" mantra. Thanks to some discussion with Mark Jones, I realized that what I was calling "the monomorphism restriction" is actually a completely different restriction to the one everyone else here was discussing. The one I was talking about is perhaps better called the "monomorphic recursion" restriction: Haskell only allows polymorphic recursion if you give an explicit type declaration. This is described in section 4.4.1 of the Haskell report | However, to ensure that type inference | is still possible, the defining occurrence, and all uses of f | within its declaration group must have the same monomorphic type That is the restriction which Mercury does not have, which can lead to non-termination. This is of course a completely different thing to "The monomorphism restriction" discussed in section 4.5.5. Sorry for my misuse of terminology, and apologies for any confusion that resulted! -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Instance contexts.
On 15-Jul-1998, Mark P Jones [EMAIL PROTECTED] wrote: We've seen several examples now, from Ralf, Alex, and others, where it is useful to relax the proposed restriction: The types in an instance-declaration context must all be type variables. ... Without the restriction, it is easy to come up with examples that could lead to non-termination. Is non-termination really a problem in practice? A simple work-around is for the type checker to perform only up to a certain number of iterations, and if that fails, to report an error message, with the error message specifying the compiler option that can be used to increase the iteration limit. The Mercury compiler uses this work-around to avoid the need to enforce the monomorphism restriction (which exists for a similar reason, to ensure termination of type inference). In practice, this seems to work fine; people very rarely write type-correct programs that require more that a few iterations to type check, so by setting the iteration limit to a reasonably large number, the only programs it catches are the occaisional type-incorrect program. The only real drawback is that for a very few really complex programs, the first compilation will fail, and users will need to recompile with the iteration limit set higher. But this is not a major drawback. Many existing systems have similar schemes, where you need to recompile with a different option if you exceed some limit. For example, on many OSs, when building very large shared libraries, you need to use `-fPIC' instead of `-fpic'. Similarly, on the AMD29000, gcc requires that source files which compile to more than 256k bytes be compiled with `-mlarge'. And on RS/6000 and PowerPC, large programs (those with more than 16384 different global variables or floating point constants) need to be compiled with `-mminimal-toc'. On the MIPS, if the program is bigger than 512M, it may need to be compiled with `-mlong-calls'. On HPPA, very large shared libraries sometimes need to be compiled with `-mmillicode-long-calls'. And so on. (I could go on, but I think those examples are enough to make my point ;-) -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
Re: Instance contexts.
On 15-Jul-1998, Alex Ferguson [EMAIL PROTECTED] wrote: Mark Jones: Looking at the `size' of types is, of course, a generalization of Simon's suggestion that contexts might be allowed to constrain only proper sub- expressions of types in the context. (Proper sub-expressions are, by definition, smaller in size.) However, it is still too strict to allow useful things like: instance Monad m = Functor m where ..., so there is still some work to be done ... I haven't looked at this in great detail, so forgive me if I'm talking through my hat, as seems quite likely: is it workable to require only that contexts be non-increasing in size, and that there be no manifest circularity where the sizes are non-decreasing? That is, rule out having both instance Monad m = Functor m and instance Functor m = Monad m. Or is that not sufficient to ensure termination of CR? There will still be problems with things like instance Foo [m] = Foo m Fergus Henderson writes of: the monomorphism restriction (which exists for a similar reason, to ensure termination of type inference). Is this true? Well, I had assumed that was the reason. I could be wrong. The rationale normally given for it by its advocates (boo, hiss) seems invariably the "no re-evaluation of CAFs" mantra. Could you elaborate about how the "no re-evaluation of CAFs" mantra justifies the monomorphism restriction? -- Fergus Henderson [EMAIL PROTECTED] | "I have always known that the pursuit WWW: http://www.cs.mu.oz.au/~fjh | of excellence is a lethal habit" PGP: finger [EMAIL PROTECTED]| -- the last words of T. S. Garp.
RE: Instance contexts.
We've seen several examples now, from Ralf, Alex, and others, where it is useful to relax the proposed restriction: The types in an instance-declaration context must all be type variables. (Item 10 in Simon's list: http://www.dcs.gla.ac.uk/~simonpj/multi-param.html) Hugs and GHC are currently taking different positions on this. The latest version of the Hugs type checker (in Hugs 1.3c) does not restrict the types appearing in instance contexts or heads (other than ensuring that they are valid and appropriately kinded). GHC imposes restrictions that limit its expressiveness but also guarantee decidability (i.e., that type checking will terminate). Without the restriction, it is easy to come up with examples that could lead to non-termination. For example, try to establish Foo Maybe Int using the following: instance Foo f (f a) = Foo f a where ... Or, if you want an example with at least one non-tyvar in the instance head, then try to establish Bar Maybe [Int] using: instance Bar f [f a] = Bar f [a] where ... My hope is that, over a period of time, the two systems will converge on some happy compromise between the current extremes that offers the advantages of both. From my perspective, it is a definite policy to leave this part of the design space open for further exploration. There is good reason to believe that a suitable compromise can be reached. For example, in both of the instance decls above, the types on the left of the = arrow are strictly larger than those on the right (an extra type application and variable in each case). On the other hand, in Alex's example: instance (Set s n, Num (s n), POrd (s n)) = Num [s n] where ... the types in the three context constraints contain strictly smaller types than those in the head. Likewise, in Ralf's example: instance (PriorityQueue q a, PriorityQueue p a, Show (p a)) = PriorityQueue (ControlBy q p) a where ... the only compound type in the context is (p a), which is strictly smaller than (Control q p) in the head. Looking at the `size' of types is, of course, a generalization of Simon's suggestion that contexts might be allowed to constrain only proper sub- expressions of types in the context. (Proper sub-expressions are, by definition, smaller in size.) However, it is still too strict to allow useful things like: instance Monad m = Functor m where ..., so there is still some work to be done ... I hope this helps, at least to explain the current background! Mark
RE: Instance contexts.
Mark Jones: Looking at the `size' of types is, of course, a generalization of Simon's suggestion that contexts might be allowed to constrain only proper sub- expressions of types in the context. (Proper sub-expressions are, by definition, smaller in size.) However, it is still too strict to allow useful things like: instance Monad m = Functor m where ..., so there is still some work to be done ... I haven't looked at this in great detail, so forgive me if I'm talking through my hat, as seems quite likely: is it workable to require only that contexts be non-increasing in size, and that there be no manifest circularity where the sizes are non-decreasing? That is, rule out having both instance Monad m = Functor m and instance Functor m = Monad m. Or is that not sufficient to ensure termination of CR? Fergus Henderson writes of: the monomorphism restriction (which exists for a similar reason, to ensure termination of type inference). Is this true? The rationale normally given for it by its advocates (boo, hiss) seems invariably the "no re-evaluation of CAFs" mantra. Slainte, Alex.
RE: Instance contexts.
Hi Fergus, | Without the restriction, it is easy to come up with examples that could | lead to non-termination. | | Is non-termination really a problem in practice? I don't think so, which is why I've been happy not to enforce restrictions in Hugs. For example, Gofer programs can potentially cause the type checker to go into an infinite loop for much the same reasons that we see here, but it seems that very few users ever noticed, or even realized that this was possible. Those that did were usually trying to probe the limits of what was decidable, coding up all kinds of interesting logic programs using instance decls as horn clauses. If anything, the problems would have been even easier to spot with Gofer than Hugs because Gofer is more strict in building dictionaries; it insists on building all of the dictionaries that might be needed before the program is executed. Hugs, by contrast, will build dictionaries more lazily as it goes. So practical experience suggests that people just don't tend to write programs that cause non-terminating type checking unless that is specifically what they were trying to do! | A simple work-around is for the type checker to perform only | up to a certain number of iterations, and if that fails, to | report an error message, with the error message specifying | the compiler option that can be used to increase the iteration | limit. Gofer had a similar mechanism, but Hugs doesn't bother ... the type checker isn't really likely to go into an infinite loop ... instead, it will just run out of stack or heap space, and so just fail to terminate `properly'. All the best, Mark
Re: Instance contexts.
Fergus Henderson, replaying to me: I haven't looked at this in great detail, so forgive me if I'm talking through my hat, as seems quite likely: is it workable to require only that contexts be non-increasing in size, and that there be no manifest circularity where the sizes are non-decreasing? That is, rule out having both instance Monad m = Functor m and instance Functor m = Monad m. Or is that not sufficient to ensure termination of CR? There will still be problems with things like instance Foo [m] = Foo m This would be ruled out as the size of the context is greater than the size of the instance head. The rationale normally given for it by its advocates (boo, hiss) seems invariably the "no re-evaluation of CAFs" mantra. Could you elaborate about how the "no re-evaluation of CAFs" mantra justifies the monomorphism restriction? It doesn't. ;-) The Official Haskell Committee line on this, which I don't find at all convincing, is on John Hughes's web site. See for example: http://www.cs.chalmers.se/~rjmh/Haskell/Messages/Display.cgi?id=130 Slainte, Alex.
RE: Instance contexts.
| Fergus Henderson writes of: | the monomorphism restriction (which exists for a similar reason, | to ensure termination of type inference). | | Is this true? The rationale normally given for it by its advocates | (boo, hiss) seems invariably the "no re-evaluation of CAFs" mantra. Yes, I think the second explanation is the right one. The monomorphism restriction doesn't have any effect on termination. Mark
