[Haskell-cafe] Type Family Relations

[Tom Schrijvers]

> 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?

Hi Iavor,

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?

Cheers,

Tom

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

--
Tom Schrijvers

Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium

tel: +32 16 327544
e-mail: tom.schrijvers at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/