[Haskell-cafe] Type Family Relations

[Matt Morrow]

Hi,

> I think that
> >>> class HeaderOf addr hdr | addr -> hdr
> does not enforce that there must be a corresponding instance
> AddressOf hdr addr. Hence, the type checker cannot use that information
> either. Do you have a way to remedy that?

I've often wanted something similar, and experimenting with this
the following two options seem to be equivalent and work as desired:

-----------------------------------------------------------------------------

-- both options share this code:

-- | The crucial assertion
ipv4 :: AddrHdrPair IPv4 IPv4Header
ipv4 = AddrHdrPair

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

-----------------------------------------------------------------------------

-- OPTION(1):
-- type families + GADT with equality constraints

type family HeaderOf addr
type family AddressOf hdr
data AddrHdrPair hdr addr
  where AddrHdrPair :: (hdr ~ HeaderOf addr
                       ,addr ~ AddressOf hdr) => AddrHdrPair addr hdr

type instance HeaderOf IPv4 = IPv4Header
type instance AddressOf IPv4Header = IPv4

-----------------------------------------------------------------------------

-- OPTION(2):
-- classes + GADT with instance constraints

class HeaderOf addr hdr | addr -> hdr
class AddressOf hdr addr | addr -> hdr
data AddrHdrPair hdr addr
  where AddrHdrPair :: (HeaderOf addr hdr
                       ,AddressOf hdr addr) => AddrHdrPair addr hdr

instance AddressOf IPv4Header IPv4
instance HeaderOf IPv4 IPv4Header

-----------------------------------------------------------------------------

-- And commenting out the above instances in turn
-- to verify that everything indeed works, and to
-- compare error message content:

{-
-- type instance HeaderOf IPv4 = IPv4Header
Cafe0.hs:9:0:
    Couldn't match expected type `HeaderOf IPv4'
           against inferred type `IPv4Header'
    When generalising the type(s) for `ipv4'
Failed, modules loaded: none.

-- type instance AddressOf IPv4Header = IPv4
Cafe0.hs:9:0:
    Couldn't match expected type `AddressOf IPv4Header'
           against inferred type `IPv4'
    When generalising the type(s) for `ipv4'
Failed, modules loaded: none.
-}

{-
-- instance AddressOf IPv4Header IPv4
Cafe0.hs:9:7:
    No instance for (AddressOf IPv4Header IPv4)
      arising from a use of `AddrHdrPair' at Cafe0.hs:9:7-17
    Possible fix:
      add an instance declaration for (AddressOf IPv4Header IPv4)
    In the expression: AddrHdrPair
    In the definition of `ipv4': ipv4 = AddrHdrPair
Failed, modules loaded: none.

-- instance HeaderOf IPv4 IPv4Header
Cafe0.hs:9:7:
    No instance for (HeaderOf IPv4 IPv4Header)
      arising from a use of `AddrHdrPair' at Cafe0.hs:9:7-17
    Possible fix:
      add an instance declaration for (HeaderOf IPv4 IPv4Header)
    In the expression: AddrHdrPair
    In the definition of `ipv4': ipv4 = AddrHdrPair
Failed, modules loaded: none.
-}

-- endcode
-----------------------------------------------------------------------------

I'm not sure if there are any circumstances under
which these two don't behave equivalently.

All the best,
Matt