[Haskell-cafe] Type Family Relations

[Ryan Ingram]

I've been fighting this same problem for a while.  The solution I've
come up with is to encode the axioms into a typeclass which gives you
a proof of the axioms.

Here's an excerpt from some code I've been playing around with; HaskTy
and Lift are type families.

-- Theorem: for all t instance of Lift, (forall env. HaskTy (Lift t) env == t)
data HaskTy_Lift_Id t env = (t ~ HaskTy (Lift t) env) => HaskTy_Lift_Id

class Thm_HaskTy_Lift_Id t where
    thm_haskty_lift_id :: forall env. HaskTy_Lift_Id t env

instance Thm_HaskTy_Lift_Id Int where
    thm_haskty_lift_id = HaskTy_Lift_Id
instance Thm_HaskTy_Lift_Id Bool where
    thm_haskty_lift_id = HaskTy_Lift_Id

lemma_haskty_lift_id_app :: HaskTy_Lift_Id a env -> HaskTy_Lift_Id b
env -> HaskTy_Lift_Id (a -> b) env
lemma_haskty_lift_id_app HaskTy_Lift_Id HaskTy_Lift_Id = HaskTy_Lift_Id

instance (Thm_HaskTy_Lift_Id a, Thm_HaskTy_Lift_Id b)
        => Thm_HaskTy_Lift_Id (a -> b) where
    thm_haskty_lift_id = lemma_haskty_lift_id_app thm_haskty_lift_id
thm_haskty_lift_id

As you can see, I encode a witness of the type equality into a
concrete data type.  You then direct the typechecker as to how to
prove the type equality using the typeclass mechanism; the class
instances closely mirror the type family instances.

You then add this typeclass as a context on functions that require the equality.

Control.Coroutine[1] uses a similar restriction:

class Connect s where
    connect :: (s ~ Dual c, c ~ Dual s) => InSession s a -> InSession
c b -> (a,b)

A cleaner solution, that sadly doesn't work in GHC6.10 [2], would be
something like:

class (s ~ Dual (Dual s)) => Connect s where
    connect :: InSession s a -> InSession (Dual s) b -> (a,b)

The difference is mainly one of efficiency; even though there is only
one constructor for Thm_HaskTy_Lift_Id t env, at runtime the code
still has to prove that evaluation terminates (to avoid _|_ giving an
unsound proof of type equality).   This means that deeply nested
instances of the (a -> b) instance require calling dictionary
constructors to match the tree, until eventually we see that each leaf
is a valid constructor.  If the type equality could be brought into
scope by just bringing the typeclass into scope, the dictionaries
themselves could remain unevaluated at runtime.

  -- ryan

[1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/Coroutine
[2] http://hackage.haskell.org/trac/ghc/ticket/2102

On Sat, Jan 3, 2009 at 7:22 AM, Thomas DuBuisson
<thomas.dubuisson at gmail.com> wrote:
> Cafe,
> I am wondering if there is a way to enforce compile time checking of
> an axiom relating two separate type families.
>
> Mandatory contrived example:
>
>> type family AddressOf h
>> type family HeaderOf a
>>
>> -- I'm looking for something to the effect of:
>> type axiom HeaderOf (AddressOf x) ~ x
>>
>> -- Valid:
>> type instance AddressOf IPv4Header = IPv4
>> type instance HeaderOf IPv4 = IPv4Header
>>
>> -- Invalid
>> type instance AddressOf AppHeader = AppAddress
>> type instance HeaderOf AppAddress = [AppHeader]
>
> So this is  a universally enforced type equivalence.  The stipulation
> could be arbitrarily complex, checked at compile time, and must hold
> for all instances of either type family.
>
> Am I making this too hard?  Is there already a solution I'm missing?
>
> Cheers,
> Tom
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>