[Haskell-cafe] Records and associated types

[Ryan Ingram]

I don't think you can get a type equality comparison test into type
families without additional compiler support.  If you are willing to
restrict your labels to type-level naturals or some other closed
universe, and allow undecidable instances, you can do something like
this:

data Z   = Z
data S a = S a

type family Select label record
type instance Select lbl (rlbl, ty, rest) = IfEq lbl rlbl ty (Select lbl rest)

type family IfEq n0 n1 t f
type instance IfEq Z Z t f = t
type instance IfEq Z (S n) t f = f
type instance IfEq (S n) Z t f = f
type instance IfEq (S n0) (S n1) t f = IfEq n0 n1 t f

Better support for closed type families that allowed overlap would be
quite useful.

   -- ryan

2008/12/11 Taru Karttunen <taruti at taruti.net>:
> Hello
>
> What is the correct way to transform code that uses record selection
> with TypeEq (like HList) to associated types? I keep running into
> problems with overlapping type families which is not allowed unless
> they match.
>
> The fundep code:
>
> class Select rec label val | rec label -> val
> instance TypeEq label label True => Select (Label label val :+: rest) label val
> instance (Select tail field val) => Select (any :+: tail) field val
>
> And a conversion attempt:
>
> class SelectT rec label where
>    type S rec label
> instance TypeEq label label True => SelectT (Label label val :+: rest) label where
>    type S (Label label val :+: rest) label = val
> instance (SelectT tail field) => SelectT (any :+: tail) field where
>    type S (any :+: tail) field = S tail field
>
> which fails with:
>
>    Conflicting family instance declarations:
>      type instance S (Label label val :+: rest) label
>        -- Defined at t.hs:19:9
>      type instance S (any :+: tail) field -- Defined at t.hs:23:9
>
>
> How is it possible to get the TypeEq constraint into the type family?
>
>
> Attached is a complete example that illustrates the problem.
>
>
> - Taru Karttunen
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>