Home > Software engineering >  can't use pattern matching with datatypes defined using GADT in haskell
can't use pattern matching with datatypes defined using GADT in haskell

Time:04-24

I'm trying to define a Complex datatype, and I want the constructors to be able to take any number as instance, so I would like to use a generic type as long as it does implement a Num instance

I'm usind GADTs in order to do so since to my understanding the DataTypeContexts language extension was a "misfeature" even if I think that would have been useful in this case...

In any case this is my code:

data Complex where
    Real            :: ( Num num, Show num ) => num -> Complex
    Imaginary       :: ( Num num, Show num ) => num -> Complex
    Complex         :: ( Num num, Show num ) => num -> num -> Complex


real :: ( Num num, Show num ) => Complex -> num
real (Real r)        = r
real (Imaginary _i ) = 0
real (Complex r _i ) = r

here the real implementation gives the following error:

Couldn't match expected type ‘num’ with actual type ‘num1’
  ‘num1’ is a rigid type variable bound by
    a pattern with constructor:
      Real :: forall num. (Num num, Show num) => num -> Complex,
    in an equation for ‘real’
    at <...>/Complex.hs:29:7-12
  ‘num’ is a rigid type variable bound by
    the type signature for:
      real :: forall num. (Num num, Show num) => Complex -> num
    at <...>/Complex.hs:28:1-47
• In the expression: r
  In an equation for ‘real’: real (Real r) = r
• Relevant bindings include
    r :: num1
      (bound at <...>/Complex.hs:29:12)
    real :: Complex -> num
      (bound at <...>/Complex.hs:29:1)

which to my understanding is due to the return type do be interpreted as different... so I tried removing the type definition and letting ghc do his magic with the type but turns out the type signature was the same...

can anyone please explain to me what is wrong here?

CodePudding user response:

Problem is, these definitions allow you to choose different types when (1) constructing a Complex value and when (2) applying the real function. These two situations are not connected to each other in any way, so there is nothing to force the type to be the same between them. For example:

c :: Complex
c = Real (42 :: Int)

d :: Double
d = real c

The definition of d requires the real function to return a Double, but there is no Double wrapped inside of c, there is only Int.


As for solutions, there are two possible ones: (1) establish a connection between these two points, forcing the type to be the same, and (2) allow the type inside to be converted to any other numeric type.

To establish a type-level connection between two points, we need to use a type that is present at both points. What type would that be? Quite obviously, that's the type of c. So we need to make the type of c somehow convey what's wrapped inside it:

data Complex num = Real num | Imaginary num | Complex num num

real :: Complex num -> num
real = ...

-- Usage:
c :: Complex Int
c = Real 42

d :: Int
d = real c

Note that I don't actually need GADTs for this.


To allow type conversion, you'll need to require another type class for the num type. The class Num has a way to convert from any integral type, but there is no way to convert to any such type, because it doesn't make sense: 3.1415 can't be meaningfully converted to an integral type.

So you'll have to come up with your own way to convert, and implement it for all allowed types too:

class Convert a where
  toNum :: Num n => a -> n

data Complex where
    Real            :: ( Num num, Show num, Convert num ) => num -> Complex
    ...

real :: Num num => Complex -> num
real (Real r) = toNum r
...

Just to be clear, I consider the second option quite insane. I only provided it for illustration. Don't do it. Go with option 1.

  • Related