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.dubuis...@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.diatc...@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.dubuis...@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@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.schrijv...@cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
