Inferring types from functional dependencies

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Inferring types from functional dependencies

Jeff.Harper

The following message is in a Haskell module.  It will be easier to read in a fixed point font.

{-# OPTIONS -fglasgow-exts #-}

-- Hi,
--
-- I ran into an issue while working with functional dependencies.
-- Consider the following code.  I'm rewriting many of the prelude
-- operators using functional dependencies.  The type of he return value
-- is determined by the operators parameters.


-- Use "P." in front of functions to access the preludes version of these
-- functions.
import qualified Prelude as P

-- I override prelude operators with my own operators.
import Prelude hiding ( (*), recip )

import Ratio

-- recip returns the reciprocal of its parameter.  I've given the
-- Reciprocate class the ability to return a type that is different from
-- its argument.

class Reciprocate a b | a -> b where
     recip :: a -> b

-- Here are some example instances of Reciprocate.  In most cases,
-- recip will return the same type as it's argument.  However, taking
-- the reciprocal of an Integer returns a (Ratio Integer).

instance Reciprocate Double Double where
     recip = P.recip -- I call prelude's recip here.

instance Reciprocate (Ratio Integer) (Ratio Integer) where
     recip = P.recip -- I call prelude's recip here.

instance Reciprocate Integer (Ratio Integer) where
     recip x = (1::Integer) % x



-- (*) multiplies its parameters.  The resulting type is determined by
-- the type of the arguments

class Multiply a b c  | a b -> c where
    (*) :: a -> b -> c

-- Here are some example instances of Multiply.

instance Multiply Double Double Double where
    (*) = (P.*)

-- Multiplying Integer by Double returns a Double

instance Multiply Integer Double Double where
    (*) x y = (P.*) (fromIntegral x) y

instance Multiply Double Integer Double where
    (*) x y = (P.*) x (fromIntegral y)

instance Multiply Integer (Ratio Integer) (Ratio Integer) where
    (*) x y = (P.*) (x%1) y

-- Now, this is where I ran into some trouble I define a Divide class
-- as follows.  Here I define a default (/) operator that uses the
-- Reciprocate and Multiply class to perform division.  However, this code
-- produces error messages.  So, I commented it out.  Even if I don't want
-- to implement (/) with recip and (*), requiring this relationship --
--                                                                  |
--                     ----------------------------------------------
--                     |
--                     v                         is consistent with defining
--      _____________________________________    the divide operation in
--     |                                     |   terms of the multiplicative
--     |                                     |   inverse
{-
class (Reciprocate b recip, Multiply a recip c) => Divide a b c | a b -> c where
    (/) :: a -> b -> c
    (/) x y = x * (recip y)
-}

-- This definition of (/) works.  However, taking the reciprocal and then
-- multiplying may not always be the best way of dividing.  So, I'd like to
-- put this into a divide class, so (/) can be defined differently for
-- different types.
{-

(/) :: (Reciprocate b recip, Multiply a recip c) => a -> b -> c
(/) a b = a * (recip b)

-}

-- I finally discovered that the following definition of a Divide
-- class works
class (Reciprocate b recip_of_b, Multiply a recip_of_b c)
                 => Divide a b c recip_of_b | a b -> c recip_of_b where
    (/) :: a -> b -> c
    (/) a b = a * (recip b) -- Default definition can be overridden


-- The thing I don't like is that when defining a new Divide class, I have
-- to place the reciprocal of the "b" type into the class definition.

-- Here are some examples of Divide:
--
-- This type ----------------------------
-- must be the type that is             |
-- returned when this                   |
-- type ------------------              |
-- is passed to recip.   |              |
--                       |              |
--                       v              v
instance Divide Double Double Double Double where
   (/) x y = (P./) x y  -- For Doubles

-- Another example:
--
-- This type ------------------------------------------
-- must be the type that is                           |
-- returned when this                                 |
-- type -------------------                           |
-- is passed to recip.    |                           |
--                        |                           |
--                        v                           v
instance Divide Integer Integer (Ratio Integer) (Ratio Integer) where
   (/) x y = x % y

-- The reason I don't like it is there is enough information available to infer
-- the type of recip_of_b in the following class.  The Reciprocate class is
-- defined with functional dependencies, so that recip_of_b can be determined
-- by the type of b.--
--                   |
--             ______________________
--            |                      |
--
--     class (Reciprocate b recip_of_b, Multiply a recip_of_b c)
--                      => Divide a b c recip_of_b | a b -> c recip_of_b where
--         (/) :: a -> b -> c
--         (/) a b = a * (recip b)
--


-- Respecifying the recip_of_b when I declare an instance of Divide
-- seem redundant.  I'm wondering if there is a better way to
-- define this.  I also, wonder if it would be appropriate to include
-- in future versions of Haskell, the ability to infer functional
-- dependences in a new class definition, so that my first attempt
-- at a definition of class Divide works.








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

Re: Inferring types from functional dependencies

oleg-7

Jeff Harper defined typeclasses
> class Reciprocate a b | a -> b where
>      recip :: a -> b
> class Multiply a b c  | a b -> c where
>     (*) :: a -> b -> c

and encountered the problem with

> -- Here I define a default (/) operator that uses the
> -- Reciprocate and Multiply class to perform division.
> class (Reciprocate b recip, Multiply a recip c) => Divide a b c | a b -> c
> where
>     (/) :: a -> b -> c
>     (/) x y = x * (recip y)

which doesn't work, because the type variable 'recip' doesn't
appear in the class head. He wrote

> I also, wonder if it would be appropriate to include in future
> versions of Haskell, the ability to infer functional dependences in a
> new class definition, so that my first attempt at a definition of
> class Divide works.


I'm afraid there may be the problem with the example rather than with
Haskell. Let us suppose that the above definition of Divide
works. Jeff Harper writes elsewhere

> However, taking the reciprocal and then multiplying may not always be
> the best way of dividing.  So, I'd like to put this into a divide
> class, so (/) can be defined differently for different types.

The key phrase is that we wish (/) defined differently for different
types, because using reciprocals is not always the best way of
dividing. Then why do we insist that every instance of Divide must be
also an instance of Reciprocate (because that's what the definition of
Divide says)? Why is that that whenever we divide something by the
value of type 'b', it must be possible to reciprocate that value of
type b? Even if we don't use reciprocals in the division?

If we assume that we need Reciprocate only if we are going to use the
'default' method, the solution becomes obvious. It does involve
overlapping and undecidable instances, sorry. These extensions are
really useful in practice. Here's the solution:

> class Divide a b c | a b -> c where
>     (/) :: a -> b -> c


Here's the most general instance. It applies when nothing more
specific does.  It is in this case that we insist on being able to
take the reciprocal:

> instance (Reciprocate b recip, Multiply a recip c) =>
>     Divide a b c where
>     (/) x y = x * (recip y)

Now, a specific instance only for Integers, which involves no
reciprocals:

> instance Divide Integer Integer (Ratio Integer) where
>     (/) = (%)

Another specific instance. It too involves no
reciprocals. Incidentally, the posted code does not even define an
instance of Reciprocate for Ints!

> instance Divide Int Int (Ratio Integer) where
>     x / y = (fromIntegral x) % (fromIntegral y)

A few tests:

> test0 = (1::Int) / (2::Int)
> test1 = (1::Integer) / (2::Integer)
> test2 = (1::Double) /(2::Double)


P.S. A remark for Haskell': the most general instance above (repeated
below)

> instance (Reciprocate b recip, Multiply a recip c) =>
>     Divide a b c where
>     (/) x y = x * (recip y)

shows why we can never be satisfied with only decidable instances --
why we need the undecidable instances extension. The instance makes it
clear that we cannot decide if the instance selection process for
Divide terminates just by looking at this instance. There is no
information to decide on termination: we must examine instances of
Reciprocate and Multiply (in particular, we should check if those
instances refer back to Divide). Thus, no _local_ instance termination
criterion would ever be able to handle above instance. OTH, it seems
quite unreasonable to require a Haskell system to employ a global
instance selection termination criterion (short of recursion stack
limit or other such `dynamic' test).


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