[Haskell-cafe] Type Family Relations
Ryan Ingram
ryani.spam at gmail.com
Sat Jan 3 16:58:11 EST 2009
I've been fighting this same problem for a while. The solution I've
come up with is to encode the axioms into a typeclass which gives you
a proof of the axioms.
Here's an excerpt from some code I've been playing around with; HaskTy
and Lift are type families.
-- Theorem: for all t instance of Lift, (forall env. HaskTy (Lift t) env == t)
data HaskTy_Lift_Id t env = (t ~ HaskTy (Lift t) env) => HaskTy_Lift_Id
class Thm_HaskTy_Lift_Id t where
thm_haskty_lift_id :: forall env. HaskTy_Lift_Id t env
instance Thm_HaskTy_Lift_Id Int where
thm_haskty_lift_id = HaskTy_Lift_Id
instance Thm_HaskTy_Lift_Id Bool where
thm_haskty_lift_id = HaskTy_Lift_Id
lemma_haskty_lift_id_app :: HaskTy_Lift_Id a env -> HaskTy_Lift_Id b
env -> HaskTy_Lift_Id (a -> b) env
lemma_haskty_lift_id_app HaskTy_Lift_Id HaskTy_Lift_Id = HaskTy_Lift_Id
instance (Thm_HaskTy_Lift_Id a, Thm_HaskTy_Lift_Id b)
=> Thm_HaskTy_Lift_Id (a -> b) where
thm_haskty_lift_id = lemma_haskty_lift_id_app thm_haskty_lift_id
thm_haskty_lift_id
As you can see, I encode a witness of the type equality into a
concrete data type. You then direct the typechecker as to how to
prove the type equality using the typeclass mechanism; the class
instances closely mirror the type family instances.
You then add this typeclass as a context on functions that require the equality.
Control.Coroutine[1] uses a similar restriction:
class Connect s where
connect :: (s ~ Dual c, c ~ Dual s) => InSession s a -> InSession
c b -> (a,b)
A cleaner solution, that sadly doesn't work in GHC6.10 [2], would be
something like:
class (s ~ Dual (Dual s)) => Connect s where
connect :: InSession s a -> InSession (Dual s) b -> (a,b)
The difference is mainly one of efficiency; even though there is only
one constructor for Thm_HaskTy_Lift_Id t env, at runtime the code
still has to prove that evaluation terminates (to avoid _|_ giving an
unsound proof of type equality). This means that deeply nested
instances of the (a -> b) instance require calling dictionary
constructors to match the tree, until eventually we see that each leaf
is a valid constructor. If the type equality could be brought into
scope by just bringing the typeclass into scope, the dictionaries
themselves could remain unevaluated at runtime.
-- ryan
[1] http://hackage.haskell.org/cgi-bin/hackage-scripts/package/Coroutine
[2] http://hackage.haskell.org/trac/ghc/ticket/2102
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