[Haskell-cafe] Type Family Relations

[Manuel M T Chakravarty]

Thomas DuBuisson:
> 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?

There are no type-level invariants, like your type axiom, at the  
moment, although there is active work in this area

   http://www.cs.kuleuven.be/~toms/Research/papers/plpv2009_draft.pdf
   -- Type Invariants for Haskell, T. Schrijvers, L.-J. Guillemette,  
S. Monnier. Accepted at PLPV 2009.

However, there is a simple solution to your problem.  To enforce a  
side condition on the type instances of two separate families, you  
need to bundle the families as associated types into a class.  Then,  
you can impose side conditions by way of super class constraints.  In  
your example, that *should* work as follows -- GHC currently doesn't  
accept this, due to superclass equalities not being fully implemented,  
but we'll solve this in a second step:

> class (HeaderOf a ~ h, AddressOf h ~ a) => Protocol h a where
>   type AddressOf h
>   type HeaderOf a
>
> -- Valid:
> instance Protocol IPv4Header IPv4 where
>   type AddressOf IPv4Header = IPv4
>   type HeaderOf IPv4 = IPv4Header
>
> -- Invalid
> instance Protocol AppHeader AppAddress where
>     type AddressOf AppHeader = AppAddress
>     type HeaderOf AppAddress = [AppHeader]

Superclass equalities are currently only partially implemented and GHC  
rejects them for this reason.  However, your application doesn't  
require the full power of superclass equalities and can be realised  
with normal type classes:

> class EQ a b
> instance EQ a a
>
> class (EQ (HeaderOf a) h, EQ (AddressOf h) a) => Protocol h a where
>   type AddressOf h
>   type HeaderOf a
>
> -- Valid:
> instance Protocol IPv4Header IPv4 where
>   type AddressOf IPv4Header = IPv4
>   type HeaderOf IPv4 = IPv4Header
>
> -- Invalid
> instance Protocol AppHeader AppAddress where
>     type AddressOf AppHeader = AppAddress
>     type HeaderOf AppAddress = [AppHeader]

With this definition, the invalid definition is rejected with the  
message

> /Users/chak/Code/haskell/main.hs:34:9:
>     No instance for (EQ [AppHeader] AppHeader)
>       arising from the superclasses of an instance declaration
>                    at /Users/chak/Code/haskell/main.hs:34:9-37
>     Possible fix:
>       add an instance declaration for (EQ [AppHeader] AppHeader)
>     In the instance declaration for `Protocol AppHeader AppAddress'

Manuel