indirectly recursive dictionaries

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

indirectly recursive dictionaries

Ralf Laemmel
{-

Recursive instance heads as in ...
 instance C0 (x,Bool) => C0 x
... are Ok if we allow for typechecking scheme as described in "SYB with class".
The main idea is to assume C0 x in proving the preconditions of the
body of the clause.
This is also works for mutual recursion among type classes and
instances to the extent exercised in ditto paper.

What about the below example though?
Here recursion detours through an extra class in a way that leads to
nonterminating typechecking with GHC 6.10.1.
Does anyone agree that a constraint resolution scheme like the one
mentioned could be reasonably expected to cover this case?

Regards,
Ralf

-}

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-- Direct recursion terminates (typechecking-wise)

class C0 x
 where
 m0 :: x -> ()
 m0 = const undefined

instance (C0 x, C0 y) => C0 (x,y)
instance C0 Bool
instance C0 (x,Bool) => C0 x

foo :: ()
foo = m0 (1::Int)


-- Indirect recursion does not terminate (typechecking-wise)

class C1 x
 where
 m1 :: x -> ()
 m1 = const undefined

instance (C1 x, C1 y) => C1 (x,y)
instance C1 Bool
instance (C2 x y, C1 (y,Bool)) => C1 x

class C2 x y | x -> y
instance C2 Int Int

-- It is this declaration that causes nontermination of typechecking.
bar :: ()
bar = m1 (1::Int)
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: indirectly recursive dictionaries

Tom Schrijvers-2
> {-

>
> Recursive instance heads as in ...
>  instance C0 (x,Bool) => C0 x
> ... are Ok if we allow for typechecking scheme as described in "SYB with class".
> The main idea is to assume C0 x in proving the preconditions of the
> body of the clause.
> This is also works for mutual recursion among type classes and
> instances to the extent exercised in ditto paper.
>
> What about the below example though?
> Here recursion detours through an extra class in a way that leads to
> nonterminating typechecking with GHC 6.10.1.
> Does anyone agree that a constraint resolution scheme like the one
> mentioned could be reasonably expected to cover this case?
>
> Regards,
> Ralf
>
> -}
>
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> -- Direct recursion terminates (typechecking-wise)
>
> class C0 x
>  where
>  m0 :: x -> ()
>  m0 = const undefined
>
> instance (C0 x, C0 y) => C0 (x,y)
> instance C0 Bool
> instance C0 (x,Bool) => C0 x
>
> foo :: ()
> foo = m0 (1::Int)
>
>
> -- Indirect recursion does not terminate (typechecking-wise)
>
> class C1 x
>  where
>  m1 :: x -> ()
>  m1 = const undefined
>
> instance (C1 x, C1 y) => C1 (x,y)
> instance C1 Bool
> instance (C2 x y, C1 (y,Bool)) => C1 x
>
> class C2 x y | x -> y
> instance C2 Int Int
The cyclic dictionaries approach is a bit fragile. The problem appears to
be here that GHC alternates exhaustive phases of constraint reduction and
functional dependency improvement. The problem is that in your example you
need both for detecting a cycle.

This can happen:

  C1 Int
  ==> 3rd C1 inst
  C2 Int y, C1 (y,Bool)
  ==> 1st C1 inst
  C2 Int y, C1 y, C1 Bool
  ==> 2nd C1 inst
  C2 Int y, C1 y
  ==> 3rd C1 inst
  C2 Int y, C2 y z, C1 (z,Bool)
  ==>
  ...

where all the constraint are different because fresh variables are
introduced.

What you want to happen is:

  C1 Int
  ==> 3rd C1 inst
  C2 Int y, C1 (y,Bool)
  ==> 1st C1 inst
  C2 Int y, C1 y, C1 Bool
  ==> 2nd C1 inst
  C2 Int y, C1 y
  ==> C2 FD improvement {Int/y}  <<<<
  C2 Int Int, C1 Int
  ==> C1 Int cycle detected
  C2 Int Int
  ==> C2 1st instance
  {}

It seems that you want improvement to happen at a higher priority than GHC
does now.

Tom

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: indirectly recursive dictionaries

oleg-30
In reply to this post by Ralf Laemmel

Ralf wrote:
> class C1 x
>  where
>  m1 :: x -> ()
>  m1 = const undefined

> instance (C1 x, C1 y) => C1 (x,y)
> instance C1 Bool
> instance (C2 x y, C1 (y,Bool)) => C1 x

> class C2 x y | x -> y
> instance C2 Int Int

> bar :: ()
> bar = m1 (1::Int)

I believe it works very well (meaning bar typechecks and even runs)
if we either add an instance
        instance C1 Int
or change the instance of C2 to
        instance C2 Int Bool
Otherwise, the problem really has no solution, and looping is an
indication. I used GHC 6.8.3....
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: indirectly recursive dictionaries

Ralf Laemmel
In reply to this post by Ralf Laemmel
Re: Tom: Thanks. This was an excellent analysis.

Re: Oleg: Obviously, I don't want to add instance C1 int. Rather C1
Int should be implied by the existing scheme for recursive dictionary
construction and bar should typecheck fine. (foo already relies on
this scheme.) However, as Tom pointed out, we would need FD
improvement to happen more intermittently.

... and that's the Gretchen-Frage I guess whether there is a
reasonable (enough) scheme of doing so? The *intention* sounds
reasonable. In fact, to me it sounds less reasonable to defer FD
improvement and go on with an unnecessarily general goal C1 (y, Bool),
i.e., without taking advantage of the fact that y is functionally
determined by a constant type Int.

That's a slippery slope - I know.

Ralf

PS:
Is this a topic that should relocate to haskell-cafe, if there is
further interest?
I don't know ...


On Tue, Mar 17, 2009 at 2:52 AM, Ralf Laemmel <[hidden email]> wrote:

> {-
>
> Recursive instance heads as in ...
>  instance C0 (x,Bool) => C0 x
> ... are Ok if we allow for typechecking scheme as described in "SYB with class".
> The main idea is to assume C0 x in proving the preconditions of the
> body of the clause.
> This is also works for mutual recursion among type classes and
> instances to the extent exercised in ditto paper.
>
> What about the below example though?
> Here recursion detours through an extra class in a way that leads to
> nonterminating typechecking with GHC 6.10.1.
> Does anyone agree that a constraint resolution scheme like the one
> mentioned could be reasonably expected to cover this case?
>
> Regards,
> Ralf
>
> -}
>
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-overlapping-instances #-}
> {-# OPTIONS -fallow-undecidable-instances #-}
>
> -- Direct recursion terminates (typechecking-wise)
>
> class C0 x
>  where
>  m0 :: x -> ()
>  m0 = const undefined
>
> instance (C0 x, C0 y) => C0 (x,y)
> instance C0 Bool
> instance C0 (x,Bool) => C0 x
>
> foo :: ()
> foo = m0 (1::Int)
>
>
> -- Indirect recursion does not terminate (typechecking-wise)
>
> class C1 x
>  where
>  m1 :: x -> ()
>  m1 = const undefined
>
> instance (C1 x, C1 y) => C1 (x,y)
> instance C1 Bool
> instance (C2 x y, C1 (y,Bool)) => C1 x
>
> class C2 x y | x -> y
> instance C2 Int Int
>
> -- It is this declaration that causes nontermination of typechecking.
> bar :: ()
> bar = m1 (1::Int)
>
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell
Reply | Threaded
Open this post in threaded view
|

Re: indirectly recursive dictionaries

oleg-30
In reply to this post by Ralf Laemmel

Tom Schrijvers wrote:
> The cyclic dictionaries approach is a bit fragile. The problem appears to
> be here that GHC alternates exhaustive phases of constraint reduction and
> functional dependency improvement. The problem is that in your example you
> need both for detecting a cycle.

It seems we can convince GHC to do constraint reduction and
improvement in the order we desire. The key is to use the
continuation-passing style -- which forces things to happen in the
right order, both at the run-time and at the compile time. I took the
liberty to flesh out the example a bit more, to verify that recursive
dictionaries are indeed constructed and used. The trace statement
shows it.

{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-undecidable-instances #-}

import Debug.Trace

class C1 x where
 m1 :: x -> Int

instance (C1 x, C1 y) => C1 (x,y) where
    m1 (x,y) = m1 x + m1 y
instance C1 Bool where
    m1 = fromEnum
-- Was: instance (C2 x y, C1 (y,Bool)) => C1 x
instance C2CPS x (C1K Bool) => C1 x where
    m1 x = trace "recursive C1" $ c2invoke (C1K True) x

newtype C1K a = C1K a

-- The class C2CPS below is a CPS version of the class C2 below
-- class C2 x y | x -> y where c2 :: x -> y
-- instance C2 Int Int where c2 = id
-- The functional dependency becomes implicit

class C2CPS x k where
    c2invoke :: k -> x -> Int
instance Apply k Int Int => C2CPS Int k where
    c2invoke k x = apply k x

class Apply f x y | f x -> y where
    apply:: f -> x -> y
instance C1 (b,a) => Apply (C1K a) b Int where
    apply (C1K a) x = m1 (x,a)

-- It is this declaration that was causing nontermination of typechecking.
-- Not any more
bar :: Int
bar = m1 (1::Int)

_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell