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

[Dmitry Kulagin]

Very clear solution, I will try to adopt it.

Thank you!


On Wed, Feb 27, 2013 at 12:17 PM, Aleksey Khudyakov <
alexey.skladnoy at gmail.com> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130227/d16cb8f7/attachment.htm>