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

[Raphael Gaschignard]

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<http://www.haskell.org/ghc/docs/7.4.2/html/users_guide/type-families.html#data-family-overlap>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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130227/aa9a7bab/attachment-0001.htm>