[Haskell-cafe] Type Family Relations

Iavor Diatchki iavor.diatchki at gmail.com
Sat Jan 3 20:18:59 EST 2009


Hello,
Usually, you can program such things by using super-classes.  Here is
how you could encode your example:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
FlexibleInstances #-}

class HeaderOf addr hdr | addr -> hdr
class HeaderOf addr hdr => AddressOf hdr addr | addr -> hdr

data IPv4Header = C1
data IPv4       = C2
data AppAddress = C3
data AppHeader  = C4

instance AddressOf IPv4Header IPv4
instance HeaderOf IPv4 IPv4Header

{- results in error:
instance AddressOf AppHeader AppAddress
instance HeaderOf AppAddress [AppHeader]
-}

Hope that this helps,
Iavor



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
>


More information about the Haskell-Cafe mailing list