[Haskell-cafe] topEq for types

[Nicolas Frisby]

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