CODEWITHSUNDEEP
haskellghcfunctional-dependencies
mb14
mb14

Reputation: 22596

Recursive functional dependency not working

I'm trying to multiply array of units (from dimensional) in a phantom type and I'm having trouble with functional dependencies. A simplified version of the problem is the following :

I have the following type

data F (a:: [*]) = F String

Where the string represent an expression in a foreign language and a phantom type representing a list of types.

I can do things like 

x = F "x" :: F '[Double]
y = F "(1,3)" :: F '[Int, Int]

I managed to implements arithmetics operators like this by creating a Nums class which is a list of Num.

class Nums (a::[*])
instance Nums '[]
instance (Num a, Nums as) => Num (a ': as)

Then I can do instanciate Num F 

instance Nums as => F as where
   (F a) * (F b) = F (a ++ "*" ++ b)
   ... etc ...

Now, I'm trying to do the same using physical units. I can do it with a list of one type this way

import qualified Numeric.Units.Dimensional as Dim

data F (a::[*]) = F String
(!*!) :: (Num n, Dim.Mul a b c) => F '[Dim.Dimensional v a n]
                                -> F '[Dim.Dimensional v b n]
                                -> F '[Dim.Dimensional v c n]

(F a) !*! (F b) = F (a ++ "*" ++ b)

That's seem to work, I can "multiply" 2 'F's of different units, and the result is in the corret unit. Obviously, I want to generalize this to any list and use the same tricks as Nums which I call Muls.

class Muls a b c | a b -> c
instance '[] '[] '[]
instance (Num n, Mul a b c, Muls as bs cs) 
   => Muls (Dim.Dimensional v a n ': as)
           (Dim.Dimensional v b n ': bs)
           (Dim.Dimensional v c n ': cs)

!*! :: (Muls as bs cs) => F as -> F bs -> F cs
(F a) !*! (F b) = F (a ++ "*" ++ b)

I got an Illegal Instance declaration error :

Illegal instance declaration for
 ‘Muls
    (Dim.Dimensional v a n : as)
    (Dim.Dimensional v b n : bs)
    (Dim.Dimensional v c n : cs)’
 The coverage condition fails in class ‘Muls’
   for functional dependency: ‘a b -> c’
 Reason: lhs types ‘Dim.Dimensional v a n : as’, ‘Dim.Dimensional
                                                    v b n
                                                    : bs’
   do not jointly determine rhs type ‘Dim.Dimensional v c n : cs’
 Using UndecidableInstances might help
In the instance declaration for
 ‘Muls (Dim.Dimensional v a n : as) (Dim.Dimensional v b n
                                    : bs) (Dim.Dimensional v c n : cs)’

If I use the UndecidableInstances extension, it seems to work indeed. My question, is why do I need this extension and is there a way I could avoid it ?

Alternatively, I probably could get this working using the type family version of dimensional. Unfortunatly, I need custom units and it's not clear if dimensional-tf supports user defined units.

Upvotes: 4

Views: 185

Answers (1)

user2407038
user2407038

Reputation: 14578

By default Haskell requires that instance selection be decidable, ie, that an attempt to decide if an type satisfy a constraint cannot cause an infinite loop in the compiler. Consider the following code:

class A (a :: *)
class B (a :: *) 
instance A a => B a

This obviously instance could cause an infinite loop (it won't do so necessarily!). Even if every other instance by itself can't cause an infinite loop, the addition of this instance can. There is probably a rigorous proof of this somewhere but I don't know it.

The only thing UndecidableInstances does is say "I promise I will never call my functions with types which cause infinite loops, so even though my instances can produce infinite loops, I accept responsibility for making sure that doesn't happen."

On the other hand, instances of the form:

instance (C1 a1, C2 a2 ... Cn an) => C (T a1 a2 .. an)

Will never produce an infinite loop, since Haskell doesn't allow infinite types, and this instance unpacks a single constructor, so even if Ci refers back to C you will eventually get to a type constructor which has 0 type parameters.

If you write an instance which is not decidable, you should get 

test.hs:26:10:
    Constraint is no smaller than the instance head
      in the constraint: A a
    (Use UndecidableInstances to permit this)
    In the instance declaration for `B a'

I think this is the error you should see in your case and that displaying the error you actually see should be considered a bug.

Upvotes: 2

Related Questions