Is it possible to emulate a limited form of intesection types in Haskell with ConstraintKinds?

Question

Recently, I came up with the idea that one could potentially emulate "intersection types" in Haskell. Specifically, I mean intersection of "interfaces", as they are usually conceived in OOP languages. For instance, to use some pseudo-code for a language with interfaces and intersection types to see what I mean:

interface HasName {
    val name: String
}

interface HasAge {
    val age: Int
}

-- An object of type HasName & HasAge can call the methods of both
type HasNameAndAge = HasName & HasAge

-- For example:
val myObject: HasNameAndAge = ...
val example = "My name is: ${myObject.name}. My age is ${myObject.age}"

I am looking to do something similar with Haskell typeclasses. My approach was to replace interfaces with elements of kind * -> Constraint in Haskell (so, for instance, single parameter type classes):

class HasName a where
  name :: a -> String

class HasAge a where
  age :: a -> Int

Now, given such type classes, the idea is that elements of types of the form exists a. C a => a (where c :: * -> Constraint) correspond to implementations of the "interface" C. Given such an identification, we can easily construct non-anonymous intersection types by appending constraints, for instance:

{-# LANGUAGE ExistentialQuantification, RankNTypes #-}

-- The intersection of HasName and HasAge:
data HasNameAndAge = forall a. HasNameAndAge ((HasName a, HasAge a) => a)

-- Example:
data Person = Person {
    personName :: String,
    personAge  :: Int
}

instance HasName Person where
    name = personName
instance HasAge Person where
    age = personAge

myObject :: HasNameAndAge
myObject = HasNameAndAge (Person "Nathan" 27)

The issue is, trying to generalize this and make this generic in a list [* -> Constraint] of interfaces that an "object" implements, I am having trouble getting GHC to deduce what it needs to get this to work properly. This is my latest attempt:

{-# LANGUAGE
   ConstraintKinds, 
   KindSignatures, 
   ExistentialQuantification,
   DataKinds,
   TypeFamilies,
   TypeOperators,
   RankNTypes,
   AllowAmbiguousTypes,
   TypeSynonymInstances,
   FlexibleInstances,
   MultiParamTypeClasses,
   FlexibleContexts,
   UndecidableInstances
#-}

import Data.Kind

class Elem (x :: * -> Constraint) (xs :: [* -> Constraint]) where
instance Elem x (x ': xs) where
instance Elem x xs => Elem x (y ': xs) where

type family All (cs :: [* -> Constraint]) a :: Constraint where
  All '[] x = ()
  All (c ': cs) x = (c x, All cs x)

-- The type of "objects" implementing all interfaces cs.
data AbstractType (cs :: [* -> Constraint]) 
    = forall a. All cs a => AbstractType a

-- An example object of type HasName & HasAge.
myObject :: AbstractType '[HasName, HasAge]
myObject = AbstractType $ Person "Nathan" 27

-- Instances needed for every "interface" to get this to work.
instance Elem HasName cs => HasString (AbstractType cs) where
  name (AbstractType x) = name x
instance Elem HasAge cs => HasAge (AbstractType cs) where
  age (AbstractType x) = age x

-- Example:
myObject :: AbstractType '[HasName, HasAge]
myObject = AbstractType $ Person "Nathan" 27

example = do
  print $ age myObject
  putStrLn $ name myObject

It seems that I need to do a little more prodding to make GHC accept the instances I want at the end here. When I try compiling the above, I get errors like:

* Could not deduce (HasName a) arising from a use of `name'
      from the context: Elem HasName cs

Intuitively, HasName should hold for AbstractType cs whenever HasName is in cs, since AbstractType cs is an existential type with the constraint All cs a. For instance, All '[HasName, HasAge] a = (HasName a, HasAge a), however, I am unsure of how to convince the GHC typechecker of this fact.

I am also getting errors like:

* No instance for (Elem HasName '[HasName, HasAge])
    arising from a use of `name'

So it appears that either my implementation of a type-level elem is incorrect, or GHC just can't test equality between terms of kind * -> Constraint, so I am not sure if what I am trying to do is even possible with current versions of GHC.

Answer 1

Just having a class with instances for when c is an element of cs is not enough. GHC actually needs access to the dictionaries associated with these constraints in order to do any computation with them, but the class you wrote doesn't provide that. What you need to do is extend the class with a function that captures this context. Something like this:

{-# LANGUAGE TypeApplications #-}

class Elem (c :: * -> Constraint) (cs :: [* -> Constraint]) where
  withC :: All cs a => (c a => a -> x) -> a -> x

instance {-# OVERLAPS #-} Elem x (x ': xs) where
  withC f a = f a

instance Elem x xs => Elem x (y ': xs) where
  withC = withC @x @xs

(EDIT NOTE: Weirdly, GHC doesn't require that we put in the OVERLAPS pragma here, but if we don't include it, then we can never actually use this type class. Thanks to @dfeuer in the comments for figuring this out!)

This withC function says that if we know that all of the constraints in cs are satisfied by some a, then surely this particular c is satisfied. Therefore, if we have a function from a -> x that requires the constraint c a, then we can convert an a into an x.

With this, we can then write the HasName and HasAge instances you want:

instance Elem HasName cs => HasName (AbstractType cs) where
  name (AbstractType x) = withC @HasName @cs name x

instance Elem HasAge cs => HasAge (AbstractType cs) where
  age (AbstractType x) = withC @HasAge @cs age x

This all type checks (although it is a little annoying that we have to do some explicit type annotations).

---

As @dfeuer points out in the comments, we can make the Elem class even more general by changing the type of withC as follows:

{-# LANGUAGE AllowAmbiguousTypes #-}

class Elem (c :: * -> Constraint) (cs :: [* -> Constraint]) where
  withC :: forall a r. All cs a => (c a => r) -> r

instance {-# OVERLAPS #-} Elem x (x ': xs) where
  withC r = r

instance Elem x xs => Elem x (y ': xs) where
  withC = withC @x @xs

Note that for this to type check, we need to enable AllowAmbiguousTypes because the a type in withC is otherwise impossible for GHC to deduce at this point.

This seems great and is definitely more general (we can recover the old behavior by simply considering the specification that r is a function type a -> x), but having to specify the type of a is a little cumbersome. Consider our new instances for AbstractType:

instance Elem HasName cs => HasName (AbstractType cs) where
  name (AbstractType (x :: a)) = withC @HasName @cs @a name x

instance Elem HasAge cs => HasAge (AbstractType cs) where
  age (AbstractType (x :: a)) = withC @HasAge @cs @a age x

We now need to capture the type of x in the pattern so that we can provide it to withC.

Answer 2

Depends on what you want to do with that list, but one solution is to just flatten it away, and instead of using Elem to look up the constraint as a tag, use evidence that the desired constraint is implied by the intersection.

To do that, you’d make All take a [Type -> Constraint] and return a Type -> Constraint, so that you can partially apply it:

type family All cs where
  All (c ': cs) = c :/\ All cs
  All '[]       = T

-- Top: trivial constraint.
class    T a
instance T a

-- Meet: conjunction of constraints.
class    (c1 a, c2 a) => (c1 :/\ c2) a
instance (c1 a, c2 a) => (c1 :/\ c2) a

Then store the dict for that conjunction of constraints in your existential type:

data Some c where
  Some :: c a => a -> Some c

type Abstract cs = Some (All cs)

And finally, define instances for Some using a quantified constraint, namely, “Some c is in the class of types that { have a name, have an age, … } if c a implies that a is also in that class, for all types a”. In other words, c must be a subset of HasName.

instance
  (forall a. c a => HasName a)
  => HasName (Some c) where
  name (Some x) = name x

instance
  (forall a. c a => HasAge a)
  => HasAge (Some c) where
  age (Some x) = age x

Then your example works directly:

myObject :: Abstract '[HasName, HasAge]
myObject = Some (Person "Nathan" 27)

example = do
  print $ age myObject
  putStrLn $ name myObject

If you need to do more complex manipulations of the instances, and keep information about each constraint separately, then you can use the constraints package to explicitly store a dictionary value Dict (c a), or multiple {Dict (c1 a), …, Dict (cn a)}, instead of just the constraint c a => …. An implication constraint can then be reified as a value c a :- HasName a, which you can obtain from an instance of Class (for superclass constraints) or :=> (for instance constraints) depending on what you need it for.