Haskell Typeclass Function with Polymorphic Output-CodePudding

I would like to define a function in a typeclass that outputs a result of an arbitrary Num type in Haskell. To illustrate this, I will use the below example:

class Exclass c where
    exFunc :: (Num a) => c -> a

For a simple newtype shown below:

newtype Extype a = Extype a

I would like to write an instance of it under Exclass when the encapsulated value is of typeclass Num:

instance (Num b) => Exclass (Extype b) where
    exFunc (Extype x) = x

However, the compiler compains that:

• Couldn't match expected type ‘a’ with actual type ‘b’
  ‘a’ is a rigid type variable bound by
    the type signature for:
      exFunc :: forall a. Num a => Extype b -> a
    at C:\Users\ha942\OneDrive\Documents\Haskell\Qaskell\src\Example.hs:9:5-10
  ‘b’ is a rigid type variable bound by
    the instance declaration
    at C:\Users\ha942\OneDrive\Documents\Haskell\Qaskell\src\Example.hs:8:10-38
• In the expression: x
  In an equation for ‘exFunc’: exFunc (Extype x) = x
  In the instance declaration for ‘Exclass (Extype b)’

Why can type a and b not equal to each other in this case? In foldr, the accumulation function signature is (a->b->b), but it would also take f::a->a->a. Why is it that in this case, the compiler complains? Is there a way to resolve this without declaring a higher-kinded typeclass? Any information is appreciated.

CodePudding user response：

The explanation why it doesn't work this way.

We can simulate the instance (Num b) => Exclass (Extype b) with this simplified illustration:

num2num :: (Num a, Num b) => a -> b 
num2num a = a  -- ignoring the wrapper Extype

The above will similarly to the instance above.

Now notice that in pseudo haskell we could write the type of num2num as (Num a => a) -> (Num b => b). I use this contrived notation to give emphasis to the fact we don't know if Num a and Num b are actually the same instance. For example, a could be CBool and b Int8.

On the other hand we can add bit more constraints to our signature we make it work:

num2num' :: (Integral a, Num b) => a -> b 
num2num' a = fromIntegral a
> :t num2num' 10
num2num' 10 :: Num b => b

fromIntegral :: (Integral a, Num b) => a -> b does the conversion from one numeric type to the other.

instance (Num b) => Exclass (Extype b) where
    exFunc (Extype x) = x

Num b doesn't have enough functionality to perform the conversion.

Researching your problem I came up with a few simple examples that work and a bit of hacking to "force" it to work:

{-# LANGUAGE InstanceSigs #-}

class Exclass c where         
    exFunc :: Num a => c -> a

--- The simplest

instance Exclass Integer where 
    exFunc a = fromInteger a

instance Exclass Int where
    exFunc a = fromIntegral a

-- Notice Integer and Int already pull the instances for the fromInteger and fromIntegral, so they don't need more constraints.

-- Your use case
-- ^^^^^^^^^^^^^

newtype Extype a = Extype a

instance (Integral b) => Exclass (Extype b) where
    exFunc :: Num a => (Extype b) -> a
    exFunc             (Extype x) = fromIntegral x

-- A hacking "forcing" it, but I'd say it completely defeats the purpose

class Exclass2 c where         
    exFunc2 :: (a ~ c, Num a) => c -> a -- (a ~ c) gives proof that a and c are in indeed the same....

instance Exclass2 Integer where
    exFunc2 = id   -- .. therefore `id` simply works.

I left the hacking as a demonstration that the problem lies in fact that Num a and Num b can't be know by GHC to be the same and making the being the same works around that.

As a final note, numeric types are rich and some would say complicated. I don't know what use cases you have for the Exclass. But I advise you to fill the Xs carefully in instance (X b) => Exclass (Extype b) and consider only the use cases you really have.

You may also consider not using type classes simply implement ad hoc functions.

CodePudding user response：

Suppose for a moment that the compiler accepted your instance. Here is what would go wrong:

> :t Extype (0 :: Rational)
Extype (0 :: Rational) :: Extype Rational
> :t exFunc (Extype (0 :: Rational))
exFunc (Extype (0 :: Rational)) :: Num a => a
> :t exFunc (Extype (0 :: Rational)) :: Complex Double
exFunc (Extype (0 :: Rational)) :: Complex Double :: Complex Double

Uh-oh... the fact that this last term type-checks is a problem. Because now if we try to evaluate it...

exFunc (Extype (0 :: Rational)) :: Complex Double
= { definition of exFunc for Extype a }
(0 :: Rational) :: Complex Double

...we have broken type-safety! We are now treating a Rational as if it were a Complex Double, which is a completely different type that interprets its bits a completely different way!

CodePudding user response：

You define

instance (Num b) => Exclass (Extype b) where
    exFunc (Extype x) = x

This exFunc has type (Num b) => (Extype b) -> b (1) but you promised

class Exclass c where
    exFunc :: (Num a) => c -> a

that it will have the type (Num a) => c -> a (2) with a completely independent from c.

Sure, if the function (2) existed for your type (which is what it means to define an instance -- it means to define that function, for that type), a particular use of that function, a particular call you'd make in your code could be at some related types, just like a generally typed a -> b -> b function can be used at a ~ b, as you correctly point out.

But when you're defining that instance, you're not using that function, you're defining it. And you've promised it to have more general type than the one your definition could possibly have.

So when a particular use of the function (1) would correspond to its narrow type, all would seem to be good and well. But another call might actually take it at its word (2) and use it at two independent types. And then what would happen? Kaboom would happen (see the answer by Daniel Wagner for an example).

So this is rejected, and rightfully so.