Type Family Relations

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

Type Family Relations

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?

Cheers,
Tom
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Austin Seipp
Excerpts from Thomas M. DuBuisson's message of Sat Jan 03 09:22:47 -0600 2009:

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

The problem is that type classes are open - anybody can
extend this family i.e.

> type instance AddressOf IPv4Header = IPv4
> type instance HeaderOf IPv4 = IPv4Header
> type instance AddressOf IPv6Header = IPv4
>
> ipv4func :: (AddressOf x ~ IPv4) => x -> ...

And it will perfectly accept arguments with a type of IPv6Header.

There is a proposal for extending GHC to support type invariants of
this nature, but it is not implemented:

      http://tomschrijvers.blogspot.com/2008/11/type-invariants-for-haskell.html

Austin
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Ryan Ingram
In reply to this post by Thomas DuBuisson
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
<[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Iavor Diatchki
In reply to this post by Thomas DuBuisson
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
<[hidden email]> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Thomas DuBuisson
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 <[hidden email]> 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
> <[hidden email]> 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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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
<[hidden email]> 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 <[hidden email]> 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
>> <[hidden email]> 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
>>> [hidden email]
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Tom Schrijvers-2
> 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
> <[hidden email]> 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 <[hidden email]> 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
>>> <[hidden email]> 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
>>>> [hidden email]
>>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>>
>>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> 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: [hidden email]
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Mark P. Jones
In reply to this post by Thomas DuBuisson
Hi Thomas,

The specific problem you describe has a simple solution using
multiple parameter classes with syntactic sugar for functional
notation instead of type families [1]:

 > class AddressOf h a | h -> a, a -> h  -- bijections
 > class HeaderOf a h  | a -> h, h -> a
 > instance HeaderOf (AddressOf h) h     -- "your axiom"

By the way, without the syntactic sugar, the instance
declaration shown here is just:

 > instance AddressOf h a => HeaderOf a h  -- also "your axiom"

Individual (address,header) pairs are documented with a
single instance, as in:

 > instance AddressOf IPv4Header IPv4

And now the type system can derive "HeaderOf IPv4 IPv4Header"
automatically using "your axiom".  But you won't be able to add
the invalid AppHeader example because it will conflict (either
with overlapping instances or with covering, depending on how
you approach it).  I like this approach because we only have to
give a single instance instead of writing a pair of declarations
that have to be checked for mutual consistency.

I conclude that perhaps your example doesn't illustrate the kind
of "arbitrarily complex" constraints you had in mind.  Maybe you
could elaborate?

All the best,
Mark

[1] http://web.cecs.pdx.edu/~mpj/pubs/fundeps-design.html

Thomas DuBuisson 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Matt Morrow
In reply to this post by Thomas DuBuisson
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Matt Morrow
Generalizing the previous post, with:

-----------------------------------------------------------------------------
{-# LANGUAGE GADTs #-}

module Equ where

data a:==:b where
  Equ :: (a ~ b) => a:==:b

symm :: (a:==:a)
symm = Equ

refl :: (a:==:b) -> (b:==:a)
refl Equ = Equ

trans :: (a:==:b) -> (b:==:c) -> (a:==:c)
trans Equ Equ = Equ

cast :: (a:==:b) -> (a -> b)
cast Equ = id
-----------------------------------------------------------------------------

We can do (e.g.):

> data IPv4Header = C1
> data IPv4       = C2
> type instance HeaderOf IPv4 = IPv4Header
> type instance AddressOf IPv4Header = IPv4

t0 :: IPv4 :==: AddressOf IPv4Header
t0 = Equ

t1 :: IPv4Header :==: HeaderOf IPv4
t1 = Equ

t2 :: IPv4 :==: AddressOf (HeaderOf IPv4)
t2 = Equ

t3 :: IPv4Header :==: HeaderOf (AddressOf IPv4Header)
t3 = Equ

-- And interestingly `t6' shows that the type family option
-- in the previous case is slightly stronger that the funcdeps
-- option, ie the type fams one corresponds to the funcdeps
-- addr -> hdr, hdr -> addr (instead of the weaker addr -> hdr).
-- If this isn't desired I'd bet there's a way to modify the type
-- instances to get the desired behavior.

t5 :: AddrHdrPair a b
    -> a :==: AddressOf (HeaderOf a)
t5 AddrHdrPair = Equ

t6 :: AddrHdrPair a b
    -> b :==: HeaderOf (AddressOf b)
t6 AddrHdrPair = Equ

Matt
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Type Family Relations

Manuel M T Chakravarty
In reply to this post by Thomas DuBuisson
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe