How to use functional dependencies and existential quantification to remove an unnecessary parameter in my type

Question

In the HLearn library I'm working on, I have a container data type that looks like this:

data (Model params model) => Container' params model = Container' { baseparams :: params , basemodel :: model } 

The problem is that this type is embarrassing to use, because params and model uniquely defined from each other:

 class Model params model | params -> model, model -> params 

So it would be much more convenient if I did not have to specify both of them when indicating the type. The compiler should be able to do this for me automatically.

My idea to solve this problem was to create an alias of the type that uses existential quantification:

 type Container model = forall params . (Model params model) => Container' params model 

But that does not work. If I make an instance of Container' as normal, everything works fine:

 data ContainerParams params = ContainerParams params instance (Model params model) => Model (ContainerParams params) (Container' params model) 

But when I use my type Container :

 instance (Model params model) => Model (ContainerParams params) (Container model) 

ghc explodes:

Illegal polymorphic or qualified type: container model In the instance declaration for the parameter Model (ContainerParams params) (container model) '

I have no idea what this error message means. Is there any way I can fix my solution to create a Container type where you do not need to specify parameters?

---

Edit: I have to note that moving the forall statement to the Container' declaration seems to require a bunch of unsafeCoerce s, so this seems like a bad solution.

In addition, I could change type Container to data Container and make it work, but this requires that I update all instances of which Conatiner' is part, and I do not want to do this. I have many different types that follow this pattern, and therefore it seems that there should be a general way to solve this problem.

Answer 1

I'm not sure if you need a universal or existential quantification. In any case, it is best to wrap it with a new type.

Strong recommendation: do not use bounding boxes for common data types. They will make your life harder, not easier. They do not bring anything.

Existential

 {-# LANGUAGE GADTs #-} data Container' params model = Container' { baseparams :: params , basemodel :: model } data Container pm where Container :: Model params model => Container' params model -> Container params model 

Universal

 {-# LANGUAGE Rank2Types #-} data Container' params model = Container' { baseparams :: params , basemodel :: model } newtype Container model = Container (forall params . Model params model => Container' params model) 

You cannot have a generic or qualified type in an instance of a type class. So

 instance Model (ContainerParams params) (Container model) 

not allowed because type synonym expands to

 instance Model (ContainerParams params) (forall ...) 

In my GADT solution, I considered both param and model as parameters. This is because of something important: functional dependencies do not merge! And, the compiler does not assume that they will be confluent for type checking purposes. Functional dependencies are only useful for guiding the constraint resolver (thus, they resemble additional logical constructs, such as “cuts” in the prologue). If you want a merge, use TypeFamilies .

 class Model model where type Param model ... 

Or an awesome way to do it

 class (model ~ (TheModel param),param ~ (TheParam model)) => Model model param where type TheModel param type TheParam model 

which has the same bidirectional as fundep. And, which then allows you to write your existential instance as

 data Container model where Container :: Model model param => Container' model param -> Container model 

and then you can do things like combining two containers with the same model type, knowing that the numerical value of params will match with existential precision. Using this, you can define

 data HasParam model where HasParam :: Model model param => HasParam model data GADTContainer model where GADTContainer :: Model model param => Container' model param -> GADTContainer model newtype NewContainer model = NewContainer (forall param. Model model param => Container' model param) 

and then the set (HasParam model, NewContainer model) provably isomorphic to the GADTContainer model , which also explains the relationship between these types

In any case, after you have taken care of this, you can only define your instance using the corresponding wrapped type.