[Haskell-cafe] Type Family Relations

[Iavor Diatchki]

Hi,
I like collecting examples of different type system related issues,
and I am curious in what way is the solution that I posted limited. Do
you happen to have an example?
Thanks,
Iavor

On Sat, Jan 3, 2009 at 8:35 PM, Thomas DuBuisson
<thomas.dubuisson at gmail.com> wrote:
> Thank you all for the responses.  I find the solution that omits type
> families [Diatchki] to be too limiting while the solution 'class (Dual
> (Dual s) ~ s) =>' [Ingram] isn't globally enforced.  I've yet to
> closely study your first solution, Ryan, but it appears to be what I
> was looking for - I'll give it a try in the coming week.
>
> Tom
>
> On Sat, Jan 3, 2009 at 8:18 PM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
>> 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
>>>
>>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>