Re: relaxed instance rules spec (was: the MPTC Dilemma (please solve))

2006-03-07 Thread Ben Rudiak-Gould

John Meacham wrote:

On Thu, Mar 02, 2006 at 03:53:45AM -, Claus Reinke wrote:

the problem is that we have somehow conjured up an infinite
type for Mul to recurse on without end! Normally, such infinite
types are ruled out by occurs-checks (unless you are working
with Prolog III;-), so someone forgot to do that here. why?
where? how?


Polymorphic recursion allows the construction of infinite types if I
understand what you mean.


No, that's different. An infinite type can't be written in (legal) Haskell. 
It's something like


type T = [T]

-- Ben

___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime


RE: relaxed instance rules spec (was: the MPTC Dilemma (please solve))

2006-03-01 Thread Simon Peyton-Jones
Claus,

I urge you to read our paper Understanding functional dependencies via
Constraint Handling Rules, which you can find here
http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/.

It will tell you more than you want to know about why relaxing
apparently-conservative rules is entirely non-trivial.   It's one of
those areas in which it is easy to suggest a plausible-sounding
alternative, but much harder to either prove or disprove whether the
alternative a sound one.

The paper describes rules we are reasonably sure of.   It would be great
to relax those rules.  But you do need to have a proof that the
relaxation preserves the properties we want.  Go right ahead!  The paper
provides a good framework for such work, I think.

Simon

| -Original Message-
| From: Claus Reinke [mailto:[EMAIL PROTECTED]
| Sent: 28 February 2006 19:54
| To: Simon Peyton-Jones; haskell-prime@haskell.org
| Subject: relaxed instance rules spec (was: the MPTC Dilemma (please
solve))
| 
| The specification is here:
|
http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extension
s.html#instance-decls
| 
| two questions/suggestions about this:
| 
| 1. there are other termination criteria one migh think of, though
| many will be out because they are not easy to specify. but here
| is an annoyingly simple example that doesn't fit the current rules
| even though it is clearly terminating (it's not even recursive):
| 
| class Fail all -- no instances!
| 
| class TypeNotEq a b
| instance Fail a = TypeNotEq a a
| instance TypeNotEq a b
| 
| class Test a b where test :: a - b - Bool
| instance TypeNotEq a b = Test a b where test _ _ = False
| instance Test a a where test _ _ = True
| 
| main = print $ (test True 'c', test True False)
| 
| never mind the overlap, the point here is that we redirect from
| Test a b to TypeNotEq a b, and ghc informs us that the
| Constraint is no smaller than the instance head.
| 
| it is true that the parameters don't get smaller (same number,
| same number of constructors, etc.), but they are passed to a
| smaller predicate (in terms of call-graph reachability: there
| are fewer predicates reachable from TypeNotEq than from
| Test - in particular, Test is not reachable from TypeNotEq).
| 
| this is a non-local criterion, but a fairly simple one. and it
seems
| very strange to invoke undecidable instances for this example
| (or is there anything undecidable about it?).
| 
| 2. the coverage condition only refers to the instance head. this
| excludes programs such as good old record selection (which
| should terminate because it recurses over finite types, and is
| confluent -in fact deterministic- because of best-fit overlap
| resolution):
| 
| -- | field selection
| infixl #?
| 
| class Select label val rec | label rec - val where
|   (#?) :: rec - label - val
| 
| instance Select label val ((label,val),r) where
|   ((_,val),_) #? label = val
| 
| instance Select label val r = Select label val (l,r) where
|   (_,r)   #? label = r #? label
| 
| now, it is true that in the second instance declaration, val is
| not covered in {label,(l,r)}. however, it is covered in the
recursive
| call, subject to the very same FD, if that recursive call complies
| with the (recursive) coverage criterion. in fact, for this
particular
| task, that is the only place where it could be covered.
| 
| would it be terribly difficult to take such indirect coverage (via
| the instance constraints) into account? there'd be no search
| involved (the usual argument against looking at the constraints),
| and it seems strange to exclude such straightforward consume
| a type recursions, doesn't it?
| 
| cheers,
| claus

___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime


Re: relaxed instance rules spec (was: the MPTC Dilemma (please solve))

2006-03-01 Thread John Meacham
On Thu, Mar 02, 2006 at 03:53:45AM -, Claus Reinke wrote:
 - Mul recurses down a type in its second parameter
 - types in Haskell are finite
 - there is a non-terminating Mul inference
 
 the problem is that we have somehow conjured up an infinite
 type for Mul to recurse on without end! Normally, such infinite
 types are ruled out by occurs-checks (unless you are working
 with Prolog III;-), so someone forgot to do that here. why?
 where? how?

Polymorphic recursion allows the construction of infinite types if I
understand what you mean. if you are clever (or unlucky) you can get
jhcs middle end to go into an infinite loop by using them.

 -- an infinite binary tree
 data Bin a = Bin a (Bin (a,a))


John
-- 
John Meacham - ⑆repetae.net⑆john⑈
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime