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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
