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

Question

In the HLearn library that I'm working on, I have some 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 awkward to use because params and model are both uniquely determined from each other:

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

So it would be much more convenient if I didn't have to specify both of them when specifying the type. The compiler should be able to do it for me automatically.

My idea to solve this problem was to create a type alias that uses existential quantification:

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

But this doesn't work. If I make a Container' instance like normal, everything works fine:

data ContainerParams params = ContainerParams params

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

But when I use my Container type:

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

ghc explodes:

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

I have no idea what this error message means. Is it possible to fix my solution somehow to make a Container type where you don't have to specify the params?

Edit: I should note that moving the forall statement into the Container' declaration seems to require a bunch of unsafeCoerces, so that seems like a bad solution.

Also, I could change the type Container into data Container and get things to work, but this requires I redeclare all instances that Conatiner' is part of, and I don't want to do that. I have many different types that follow this pattern, and so it seems like there should be a generic way to solve this problem.

Philip JF Philip JF · Accepted Answer · 2013-01-22T03:50:54

I'm not sure if you want universal or existential quantification. Either way, best to wrap it in a fresh type.

Strong recommendation: don't use constraint heads on ordinary data types. They will make your life harder, not easier. They accomplish nothing useful.

Existential

{-# LANGUAGE GADTs #-}
data Container' params model = Container'
{ baseparams :: params
, basemodel  :: model
}
data Container p m 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 can not have a universal or qualified type in a type class instance. So

instance Model (ContainerParams params) (Container model)

is not permitted since the type synonym expands to

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

In my GADT solution, I treated both param and model as parameters. This is because of something important to know: functional dependencies are not confluent! And, the compiler does not assume them to be confluent for the purposes of type checking. Functional dependencies are only useful in guiding the constraint solver (in a way they resemble extra logical constructs like "cuts" in prolog). If you want confluence, use TypeFamilies.

class Model model where
  type Param model
  ...

Or the awesome way of doing it

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

which has the same bidirectionally as the fundep. And, which would then let you 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 combine two containers with the same model type, knowing that the existentially quantified params will match. 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 tuple (HasParam model, NewContainer model) is provably isomorphic to GADTContainer model which also explains the relationship between these types

Anyway, once you have that taken care of, you can define your instance just using the appropriate wrapped type.

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

1 Answers

Existential

Universal