[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