[PRL] multi-parameter type classes

Dave Herman dherman at ccs.neu.edu
Tue Jul 10 12:05:22 EDT 2007


For the Haskell gurus:

I've been working on a type class for nominal logics (cf. work by Pitts 
et al) which allows the user to define different universes of names. So 
I have a class representing name types:

     class Name a where ...

and then a class for nominal datatypes:

     class Name b => Nominal a b where ...
         swap :: (b,b) -> a -> a
         support :: a -> Set b

This was working fine until I tried to add an alpha-equivalence 
operation (~~):

         (~~) :: a -> a -> Bool

The problem is that the type signature doesn't refer to `b', i.e., the 
type of the names in the data structure. This leads to cryptic errors 
about deducing constraints when I try to define instances of Nominal 
that use ~~ on component sub-parts; I think the type inference engine is 
generating fresh type variables for `b' and then failing to prove the 
constraints, even though my intention was for the `b' to be the same on 
the sub-components.

I could add an argument of type `b' to (~~) and always disregard it, but 
this would be ugly and preclude using (~~) as an infix operator. I am 
not very familiar with phantom types and GADT's. Would it be possible to 
define a type class that requires its instances to be GADT's with a 
phantom type `b'? Or is there something like constructor classes that 
would solve the problem?

Thanks,
Dave



More information about the PRL mailing list