CODEWITHSUNDEEP
haskellexistential-type
Impredicative
Impredicative

Reputation: 5069

Existential typing ambiguity

Apologies for the somewhat contrived example. I've tried to simplify this to the extent that I can without losing the justification:

Suppose I have a multi-parameter typeclass Relation:

class Relation r a b where ....

And a function which is existentially quantified over such a type:

neighbours :: forall r a b. Relation r a b => a -> r -> Graph -> [b]

Now I introduce a couple of instances of Relation:

data Person = Person String
data Pet = Pet String
data Owns = Owns
data Desires = Desires
instance Relation Owns Person Pet
instance Relation Desires Person Pet

Now I would like to write a method which fetches all the pets associated with a given person through some means, without exposing the complexity of implementation:

data PetAttachment = AttachOwns | AttachDesires

personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att g = 
    neighbours person r g
  where
    r = case PetAttachment of
      AttachOwns -> Owns
      AttachDesires -> Desires

My question is: how do I appropriately type r. With no hints, it will try to type as Owns and hence fail. I can alternatively hint that it should be existentially typed:

r :: forall r. Relation r Person Pet => r

But the compiler does not seem able to deduce that Relation r0 Person Pet, saying that r0 is ambiguous:

relation.hs:26:5: No instance for (Relation r0 Person Pet) arising from a use of ‘neighbours’

The type variable ‘r0’ is ambiguous

Can I persuade r to type in such a way as to let this compile?

Full compilable example:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}

data Graph = Graph

class Relation r a b where
  relation :: (r,a,b) -> Int

neighbours :: forall r a b. Relation r a b => a -> r -> Graph -> [b]
neighbours = undefined

data Person = Person String
data Pet = Pet String
data Owns = Owns
data Desires = Desires
instance Relation Owns Person Pet where
  relation _ = 1
instance Relation Desires Person Pet where
  relation _ = 2

data PetAttachment = AttachOwns | AttachDesires

personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att =
    neighbours person r
  where
    r :: forall r. Relation r Person Pet => r
    r = case att of
      AttachOwns -> Owns
      AttachDesires -> Desires

main :: IO ()
main = undefined

Upvotes: 4

Views: 132

Answers (2)

Cactus
Cactus

Reputation: 27636

A low-tech solution:

personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att = case att of
    AttachOwns -> neighbours person Owns
    AttachDesires -> neighbours person Desires

Upvotes: 2

Cirdec
Cirdec

Reputation: 24166

Here are two approaches to writing this, one using a GADT and one using a Rank 2 Type.

GADT

A GADT can capture the constraint on r that there must exist an instance for Relation r Person Pet. To use a GADT you'll need to add 

{-# LANGUAGE GADTs #-}

RelationOf a b will capture the Relation r a b instance in the constructor RelationOf due to the Relation r a b => constraint on the constructor.

data RelationOf a b where
    RelationOf :: Relation r a b => r -> RelationOf a b

personPets can then be written much as you desire as

personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att =
  case r of (RelationOf r') -> neighbours person r'
  where
    r :: RelationOf Person Pet
    r = case att of
      AttachOwns -> RelationOf Owns
      AttachDesires -> RelationOf Desires

The case on what was the neighbors person r line is required to get the captured Relation r Person Pet instance from the RelationOf constructor. The instances captured by existentially qualified GADTs can only be recovered by pattern matching against them.

Rank 2 Type

To use a Rank 2 Type, you will need to add one of the following

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RankNTypes #-}

With a Rank 2 Type, we can split personPets into two parts. The first will figure out what r is, either Owns or Desires, and pass that to a universally quantified function in continuation passing style.

withAttachment :: PetAttachment -> (forall r. Relation r Person Pet => r -> c) -> c
withAttachment AttachOwns    f = f Owns
withAttachment AttachDesires f = f Desires

personPets will call withAttachment, passing it a partially applied neighbours as the continuation.

personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att = withAttachment att (neighbours person)

Upvotes: 4

Related Questions