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.

I think that you would need overlap to write this. Here's the GHC page on it. With type families you can do overlap, but in that case, the result of unification must be the same. So basically :

T a a === T a b (with b set to a)

whereas the "intuitive" way of doing Find requires a way of differentiating between these two cases.

On Wed, Feb 27, 2013 at 4:33 PM, Dmitry Kulagin <dmitry.kulagin@gmail.com> wrote:

Hi,

I try to implement typed C-like structures in my little dsl.
I was able to express structures using type-level naturals (type Ty is promoted):

> data Ty = TInt | TBool | TStruct Symbol [Ty]

That allowed to implement all needed functions, including type-level function:

> type family Get (n :: Nat) (xs :: [Ty]) :: Ty

But it is not very convenient to identify struct's fields using naturals, and I wanted to change Ty definition to:

> data Ty = TInt | TBool | TStruct Symbol [(Symbol, Ty)]

It is much closer to how C-struct looks, but I was unable to implement required type function:

> type family Find (s :: Symbol) (xs :: [(Symbol,Ty)]) :: Ty

Which just finds a type in a associative list.

Could someone give me a hint, how to do it?
Or perhaps, is it just impossible thing to do?

Thanks!

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe