I'm sharing what I think is a novel extension of TypeEq. Please 1) cope with my introduction of the motivating problem 2) inform me if something similar has already been presented 3) criticize the solution This presentation is quite a simplification of my actual problem/code, but I'm trying to just show the essence of the technique. Feel free to request the real story or for me to actually code this up. Disclaimer: the following is an untested presentation of correctly functioning code. Thanks for your time. Motivation: In the HList paper, a subtle example involved polymorphism and the singleton list. Because the list was a singleton, TypeCast can be used to resolve the polymorphism. Otherwise, the polymorphism (i.e. free type variables) would prevent crucial typeclass instances from firing. This has inspired a solution to a recent problem of mine. I essentially had an HList of functor values that share the same carrier type. Envision the type of such a list as [F0 Char, F1 Char, ..., Fn Char] where Fi is a functor. I occasionally wanted to "update" one of these values: fn :: F0 Char -> F0 Char fn (F0_CtorOfInterest c) = ...new value... fn f0_c = f0_c newList = specialHMap fn oldList This works fine; the specialHMap method/class is pretty easy to write using TypeEq. The problem arises when I introduce more interesting functors; consider [F Char, G Char, (BF Int) Char] where BF is a bifunctor. Targeting such an functor with an update operation will fail if the update does not specify t. fn2 :: (BF t) Char -> (BF t) Char fn2 (C0 _) = C1 'c' fn2 x = x When the typeclass instances traverse the HList and check each element for a type match, the polymorphism of t in fn2 precludes a successful match of any TypeEq instance. This was frustrating, because it prohibited me from writing modular code! Solution: My solution to the problem was to indicate to the typechecker that certain functors were unique in my HList. So if BF showed up in the HList with a first argument of t', then it would be safe to unify the free t from fn2 with t' (via TypeCast), because no other BF will show up in my list. This quickly generalized to types of various kind with various parameters free. The key to the solution is this class:
class TypeTopEq' () teq x y bn => TypeTopEq teq x y bn | teq x y -> bn class TypeTopEq' q teq x y bn | q teq x y -> bn class TypeTopEq'' q teq x y bn | q teq x y -> bn
instance TypeTopEq' () teq x y bn => TypeTopEq teq x y bn
instance TypeCast bn HTrue => TypeTopEq' () TEQ_ hd hd bn
instance TypeCast bn HTrue => TypeTopEq' () TEQ_0 (hd a) (hd z) bn instance TypeCast bn HTrue => TypeTopEq' () TEQ_1 (hd a) (hd a) bn
instance TypeCast bn HTrue => TypeTopEq' () TEQ_00 (hd a b) (hd z y) bn instance TypeCast bn HTrue => TypeTopEq' () TEQ_01 (hd a b) (hd z b) bn instance TypeCast bn HTrue => TypeTopEq' () TEQ_10 (hd a b) (hd a y) bn instance TypeCast bn HTrue => TypeTopEq' () TEQ_11 (hd a b) (hd a b) bn
-- more instances and TEQ_* for higher kinds of hd
TEQ stands for "top equality qualifier". Each 0 specifies that the corresponding argument to the functor is "soft" and not required to match while each 1 specifies that the type is "hard" and is required to match. For example, these instances result in TypeTopEq TEQ_ Int Char HFalse TypeTopEq TEQ_ Int Int HTrue TypeTopEq TEQ_0 (F Int) (F Int) HTrue TypeTopEq TEQ_0 (F Int) (F Char) HTrue TypeTopEq TEQ_0 (F Int) (F Char) HTrue TypeTopEq TEQ_1 (F Int) (F Char) HFalse TypeTopEq TEQ_0 (F Int) (G Int) HFalse TypeTopEq TEQ_1 (F Int) (G Int) HFalse TypeTopEq TEQ_00 (F2 Int Int) (F2 Char Char) HTrue TypeTopEq TEQ_01 (F2 Int Int) (F2 Char Char) HFalse TypeTopEq TEQ_10 (F2 Int Int) (F2 Char Char) HFalse TypeTopEq TEQ_11 (F2 Int Int) (F2 Char Char) HFalse TypeTopEq TEQ_01 (BF t x) (BF Int x) HTrue --- solves the problem above TypeTopEq TEQ_00 (F2 Int Char) (F2 Char Char) HTrue TypeTopEq TEQ_01 (F2 Int Char) (F2 Char Char) HTrue TypeTopEq TEQ_10 (F2 Int Char) (F2 Char Char) HFalse TypeTopEq TEQ_11 (F2 Int Char) (F2 Char Char) HFalse And so on. This class enables typecases based on the "top equality" of two type variables instead of requiring total equality. For example
class SpecialHMap a b l l' | a b l -> l' where specialHMap :: (a -> b) -> l -> l' -- HNil case elided instance ( TypeTopEq teq a head bn, HMap_Case bn a b (HCons teq head tail) l' ) => SpecialHMap a b (HCons teq head tail) l' where specialHMap = hmap_case (undefined :: bn)
class HMap_Case a b l l' | a b l -> l' where hmap_case :: bn -> (a -> b) -> l -> l' instance ( SpecialHMap a b tail tail' , TypeCast head a ) => HMap_Case HTrue a b (HCons teq head tail) (HCons teq b tail) where hmap_case _ fn (HCons hd tl) = HCons (fn . typeCast $ hd) (specialHMap fn tail)
-- HFalse/recursive instance elided
Note that the HTrue instance uses TypeCast instead of multiple occurences of the same variable in the instance parameters. Unfortunately TypeTopEq wanders into the territory of varying kinds and gets a bit out of hand. It has, however, solved my problem. I used a variant of HCons that also has, as a phantom argument, the TEQ to be used for that element. When the typeclass instances traverse the HList, they use the TEQ for each element to decide how to check for a type match with the domain of the update function. Alternatively, I could try to write an overloaded uHCons function that will calculate the proper TEQ value for an element as it adds it to a list; but that was overkill at the moment. I hope that was interesting! I think this could be quickly expanded to other sorts of type-level pattern matching. Please share any thoughts. Thanks again, Nick