GADT in polymorphic function

Question

I have a problem with a function which I want to make very polymorphic. I would like to integrate functions, either analytically or numerically. When integrating analytically I provide the result. In the numeric case I would like to use various methods, for now, the tanhsinh routine from tanhsinh. I also want to learn more about gadts, so I tried to find a solution using them.

So far I have the following:

import qualified Data.VectorSpace as DV
import Numeric.Integration.TanhSinh

data IntegrationType a b  where
      MkAnalytic :: (DV.AdditiveGroup b) =>  (c -> b) -> c -> c -> IntegrationType Analytic b
      MkNumeric ::  NumericType  -> IntegrationType  Numeric [Result]

data Analytic = Analytic
data Numeric = Numeric
data Method = Trapez | Simpson
data IntBounds = Closed | NegInfPosInf | ZeroInf

data NumericType = MkSingleCoreTanhSinh  IntBounds Method  (Double -> Double)  Double Double
              | MkParallelTanhSinhExplicit IntBounds (Strategy [Double])  Method  (Double -> Double)  Double  Double
              | MkParallelTanhSinh IntBounds  Method  (Double -> Double)  Double  Double 

integrate :: IntegrationType a b -> b
integrate (MkAnalytic f l h) = f h DV.^-^ f l
integrate (MkNumeric (MkSingleCoreTanhSinh Closed Trapez f l h )) =  trap f l h
integrate (MkNumeric (MkSingleCoreTanhSinh Closed Simpson f l h )) =  simpson f l h

This code compiles , because I expicitly state in the constructor MkNumeric that the type variable b is

[Result]

Why do I have to do this? Can I not leave the type variable b as in

data IntegrationType a b  where
     MkNumeric ::  NumericType  -> IntegrationType  Numeric b

When I do this I get an error:

Could not deduce (b ~ [Result])
from the context (a ~ Numeric)
  bound by a pattern with constructor
             MkNumeric :: forall b. NumericType -> IntegrationType Numeric b,
           in an equation for `integrate'
  at test-classes-new-programm.hs:139:12-64
  `b' is a rigid type variable bound by
      the type signature for integrate :: IntegrationType a b -> b
      at test-classes-new-programm.hs:137:14
Relevant bindings include
  integrate :: IntegrationType a b -> b
    (bound at test-classes-new-programm.hs:138:1)
In the expression: trap f l h
In an equation for `integrate':
    integrate (MkNumeric (MkSingleCoreTanhSinh Closed Trapez f l h))
      = trap f l h

dfeuer dfeuer · Accepted Answer · 2015-10-04T16:15:44

The type

integrate :: IntegrationType a b -> b

says that, for any a and b of my choice, if I call integrate with a value of type IntegrationType a b, I will get back a value of type b. When you define

MkNumeric ::  NumericType -> IntegrationType Numeric b

you let whoever applies the constructor decide what b is. So I could use MkNumeric to manufacture a value of, say, type IntegrationType Numeric Int. But your integrate knows how to produce [Result], not Int.

In the working code, as soon as integrate "opens up the evidence box" by matching MkNumeric, it learns that b ~ [Result] and therefore it can return something of that type.

GADT in polymorphic function

1 Answers