[Haskell-cafe] Type Family Relations

[Mark P. Jones]

Hi Thomas,

The specific problem you describe has a simple solution using
multiple parameter classes with syntactic sugar for functional
notation instead of type families [1]:

 > class AddressOf h a | h -> a, a -> h  -- bijections
 > class HeaderOf a h  | a -> h, h -> a
 > instance HeaderOf (AddressOf h) h     -- "your axiom"

By the way, without the syntactic sugar, the instance
declaration shown here is just:

 > instance AddressOf h a => HeaderOf a h  -- also "your axiom"

Individual (address,header) pairs are documented with a
single instance, as in:

 > instance AddressOf IPv4Header IPv4

And now the type system can derive "HeaderOf IPv4 IPv4Header"
automatically using "your axiom".  But you won't be able to add
the invalid AppHeader example because it will conflict (either
with overlapping instances or with covering, depending on how
you approach it).  I like this approach because we only have to
give a single instance instead of writing a pair of declarations
that have to be checked for mutual consistency.

I conclude that perhaps your example doesn't illustrate the kind
of "arbitrarily complex" constraints you had in mind.  Maybe you
could elaborate?

All the best,
Mark

[1] http://web.cecs.pdx.edu/~mpj/pubs/fundeps-design.html

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