Why do I need UndecidableInstances?

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

Why do I need UndecidableInstances?

Alejandro Serrano Mena
Dear café,
I'm trying to compile a set of simple examples using Functional Dependencies. One of the first ones is the case of natural numbers, which I've defined along with some operations as:

data Zero
data Succ a

class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)

class Max x y z | x y -> z
instance Max Zero     y    y
instance Max (Succ x) Zero (Succ x)
instance Max x y z => Max (Succ x) (Succ y) (Succ z)

I thought the compiler would accept this only with the extensions EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies and FlexibleInstances. But, to my surprise, GHC is also asking me for UndecidableInstances. Why is this the case?

Thanks in advance :)

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Why do I need UndecidableInstances?

Stijn van Drongelen
On Thu, Oct 24, 2013 at 12:37 PM, Alejandro Serrano Mena <[hidden email]> wrote:
Dear café,
I'm trying to compile a set of simple examples using Functional Dependencies. One of the first ones is the case of natural numbers, which I've defined along with some operations as:

data Zero
data Succ a

class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)

class Max x y z | x y -> z
instance Max Zero     y    y
instance Max (Succ x) Zero (Succ x)
instance Max x y z => Max (Succ x) (Succ y) (Succ z)

I thought the compiler would accept this only with the extensions EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies and FlexibleInstances. But, to my surprise, GHC is also asking me for UndecidableInstances. Why is this the case?

Thanks in advance :)

Hi Alejandro,

The error messages mention that the 'Coverage Condition' fails for the last instance of both classes. This condition is defined in the manual of GHC (http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/type-class-extensions.html#instance-rules):

> For each functional dependency, tvs_left -> tvs_right, of the class, every type variable in S(tvs_right) must appear in S(tvs_left), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.

Let's look at the Plus instance: every type variable in S(z) must appear in S(x) or S(y). This is false for both the context and the instance type: the variable 'z' in "Plus x y z" occurs in neither 'x' or 'y', and the variable 'z' in "Plus (Succ x) y (Succ z)" occurs in neither 'Succ x' or 'y'.

I'm not familiar enough (yet) with the reasons behind this rule to explain why it's there (if anyone can explain this in detail, please do!), but this should be a direct answer to your question: it's against the rules.

Kind regards,

Stijn van Drongelen

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Why do I need UndecidableInstances?

Adam Vogt
On Thu, Oct 24, 2013 at 9:08 AM, Stijn van Drongelen <[hidden email]> wrote:
> I'm not familiar enough (yet) with the reasons behind this rule to explain
> why it's there (if anyone can explain this in detail, please do!), but this
> should be a direct answer to your question: it's against the rules.

Hello,

Perhaps those rules are unnecessarily restrictive? Maybe the check
could be changed to something like "at least one of the types is
shrinking if all the other are not growing", rather than the current
rule that seems to be "all types must be smaller in the recursive
call". The equivalent code using type families doesn't need
undecidable instances in my ghc-7.6.2.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
data Nat = Zero | Succ Nat

type family Plus (a :: Nat) (b :: Nat) :: Nat

type instance Plus Zero x = x
type instance Plus (Succ x) y = Succ (Plus x y)

type family Max (x :: Nat) (y :: Nat) :: Nat
type instance Max Zero y = y
type instance Max (Succ x) Zero = Succ x
type instance Max (Succ a) (Succ b) = Succ (Max a b)

Also using normal data types instead of the datakinds doesn't make a difference.

Regards,
Adam
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Why do I need UndecidableInstances?

Adam Vogt
On Thu, Oct 24, 2013 at 11:23 AM, Stijn van Drongelen <[hidden email]> wrote:

> Hi,
>
> As far as I know, you're referring to the Paterson Conditions. Condition 'b'
> kind of corresponds to "at least one of the types is shrinking", while
> condition 'a' corresponds to "all the other are not growing", so the rules
> are already formulated in the way you suggest. The Paterson Conditions are
> also not the issue here; the Coverage Condition is.
>
>> The equivalent code using type families doesn't need
>> undecidable instances in my ghc-7.6.2.
>
>
> This is because (I think) type family instances are not subject to the
> Coverage Condition. In principle, type families are to type classes as
> functions are to relations. Functional dependencies may be used to make type
> classes more 'function-like'. I guess(!) the Coverage Condition is trying to
> capture this notion.
>
> I don't know why it's formulated in this way, because in Alejandro's
> example, the classes really look 'function-like'.
>
> Kind regards,
>
> Stijn van Drongelen

Hi Stijn,

Thanks for clarifying the issue.

There is an example of why the coverage condition is needed on line
512 of (github doesn't handle line numbers in lhs correctly
unfortunately):

https://github.com/ghc/ghc/blob/9a04e1c7257f93f0c1cadc56a5e2a177574f6871/compiler/types/FunDeps.lhs#L512

It doesn't seem possible to write a type for that function with just a
type family; you need a class Mul to get into an infinite loop while
looking for instances. So it seems appropriate that the coverage
condition does not apply to type families.

Regards,
Adam
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe