On 27 February 2013 12:01, Raphael Gaschignard wrote:

I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a.

It's indeed impossible to write such type function using type families. It will be possible with new closed type familes (they are in GHC head already). But for now it's possible to use overlapping instances and fundeps. Implementation of type level equality is simple and it's only instances which need ovelap. -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq instance TypeEq a a True instance eq ~ False => TypeEq a b eq Implementation of lookup by key is relatively straightforward. Note that it doesn't check that key is unique. data k :> v infix 6 :> -- | Lookup type for given key class TyLookup (map :: [*]) (k :: *) (v :: *) | map k -> v where class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k eq -> v where instance ( TypeEq k k' eq , TyLookupCase (k :> v ': xs) k' v' eq ) => TyLookup (k :> v ': xs) k' v' where instance TyLookupCase (k :> v ': xs) k v True where instance TyLookup xs k v => TyLookupCase (k' :> v' ': xs) k v False where

Hi Aleksey, Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced the problem to: -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq instance TypeEq a a True -- instance TypeEq a b False instance eq ~ False => TypeEq a b eq f :: TypeEq Int Int True => Int f = 1 When I try to invoke f, I get overlapping instances error: Overlapping instances for TypeEq * Int Int 'True arising from a use of `f' Matching instances: instance TypeEq k a a 'True -- Defined at Test.hs:14:24 instance eq ~ 'False => TypeEq k a b eq -- Defined at Test.hs:16:10 Thanks. On Wed, Feb 27, 2013 at 12:17 PM, Aleksey Khudyakov < alexey.skladnoy@gmail.com> wrote:

On 27 February 2013 12:01, Raphael Gaschignard wrote:

...

I think it might be impossible with type families. I don't think it's possible to differentiate with type families something like T a a, and T a b, with b different from a.

It's indeed impossible to write such type function using type families. It will be possible with new closed type familes (they are in GHC head already).

But for now it's possible to use overlapping instances and fundeps. Implementation of type level equality is simple and it's only instances which need ovelap.

-- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq instance TypeEq a a True instance eq ~ False => TypeEq a b eq

Implementation of lookup by key is relatively straightforward. Note that it doesn't check that key is unique.

data k :> v infix 6 :>

-- | Lookup type for given key class TyLookup (map :: [*]) (k :: *) (v :: *) | map k -> v where

class TyLookupCase (map :: [*]) (k :: *) (v :: *) (eq :: Bool) | map k eq -> v where

instance ( TypeEq k k' eq , TyLookupCase (k :> v ': xs) k' v' eq ) => TyLookup (k :> v ': xs) k' v' where

instance TyLookupCase (k :> v ': xs) k v True where instance TyLookup xs k v => TyLookupCase (k' :> v' ': xs) k v False where

Oh, that is my fault - I was sure that I specified the extension and it didn't help. It really works with Overlapping&Undecidable. Thank you! On Wed, Feb 27, 2013 at 10:36 PM, Aleksey Khudyakov < alexey.skladnoy@gmail.com> wrote:

On 27.02.2013 17:35, Dmitry Kulagin wrote:

...

Hi Aleksey,

Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced the problem to:

-- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b -> eq instance TypeEq a a True -- instance TypeEq a b False instance eq ~ False => TypeEq a b eq

You need to add pragma {-# LANGUAGE OverlappingInstances #-} to the file where instances defined. Without it GHC will complain about overlap and unlike other extensions won't recommend pragma