Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Automatically deriving show instances for GADTs

Assume I have a complex GADT which with many hidden type parameters as constructors:

data T where
  A :: Num n => n -> T
  B :: (Num n, Integral m) => n -> m -> T
  C :: Floating a => [a] -> T
  -- and so on
  Z :: Num n => n -> n -> T

I want to make this datatype showable without having to manually write the instance. Problem is, that since Show isn't a superclass of Num anymore, adding a simple deriving instance Show T isn't enough for the compiler to infer that it has to add Show constraints to all the internal hidden type parameters.

For each hidden type parameter, it outputs something like

Could not deduce (Show n) arising from a use of 'showsPrec'
from the context Num n
  bound by a pattern with constructor
             A :: forall n. Num n => n -> T
...
Possible fix:
  add (Show n) to the context of the data constructor 'A'

Adding a Show constraint to the datatype isn't an option either, since it limits the possible inhabitants of T. It seems like deriving instanec Show T should introduce the constraint Show on the hidden data types, although I am not sure.

How can I go about this?

like image 361
ThreeFx Avatar asked Nov 26 '25 03:11

ThreeFx


1 Answers

I had an interesting thought, not sure how practical it is. But if you want T to be showable when the parameters are showable, but also usable with not showable parameters, you could parameterize T over a constraint, using ConstraintKinds.

{-# LANGUAGE GADTs, ConstraintKinds #-}

import Data.Kind

data T :: (* -> Constraint) -> * where
    A :: (Num n, c n) => n -> T c
    B :: (Num n, c n, Integral m, c m) => n -> m -> T c
    ...

Then T Show will be showable... maybe

deriving instance Show (T Show)

(with StandaloneDeriving extension) will work, but at the very least, T is showable in principle and you could write the instance manually.

Though my practical advice is to reify the existentials. An existential type is equivalent to the collection of its observations. For example, if you had a class like

class Foo a where
   getBool :: a -> Bool
   getInt  :: a -> Int

then the existential

data AFoo where
   AFoo :: Foo a => a

is exactly equivalent to (Bool,Int), because the only thing you can do with a Foo whose type you don't know is call getBool on it or getInt on it. You use Num in your datatype, and Num has no observations, since if you have an unknown a with Num a, the only thing you can do by calling methods of Num is get more as out, and nothing ever concrete. So your A constructor

A :: (Num n) => n -> T

gives you nothing and you might as well just say

A :: T

Integral, on the other hand, has toInteger as an observation. So you could probably replace

B :: (Num n, Integral m) => n -> m -> T

with

B :: Integer -> T

(we lost the n argument and replaced m with Integer). I don't think this is technically equivalent since we could have implemented its operations differently than Integral does, but we're getting pretty technical at this point and I doubt you have need for it (I'd be interested in how if you do).

like image 136
luqui Avatar answered Nov 28 '25 21:11

luqui



Donate For Us

If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!