[Haskell-cafe] Help to write type-level function

[Aleksey Khudyakov]

On 27 February 2013 12:01, Raphael Gaschignard <dasuraga at gmail.com> 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