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

2013-02-27 Thread 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.

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

2013-02-27 Thread Aleksey Khudyakov
On 27 February 2013 12:01, Raphael Gaschignard dasur...@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

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

2013-02-27 Thread oleg
Dmitry Kulagin wrote: I try to implement typed C-like structures in my little dsl. HList essentially had those http://code.haskell.org/HList/ I was unable to implement required type function: type family Find (s :: Symbol) (xs :: [(Symbol,Ty)]) :: Ty Which just finds a type in a

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

2013-02-27 Thread Dmitry Kulagin
That seems to be very relevant to my problem (especially HList.Record). Am I right that UndecidableInstances is required mostly because of eq on types, like in this instances: class HRLabelSet (ps :: [*]) instance HRLabelSet '[] instance HRLabelSet '[x] instance ( HEq l1 l2 leq ,

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

2013-02-27 Thread 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.sklad...@gmail.com wrote: On 27 February 2013 12:01, Raphael Gaschignard dasur...@gmail.com wrote: I think it might be impossible with type families. I don't think it's

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

2013-02-27 Thread Dmitry Kulagin
Hi Aleksey, Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced the problem to: -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq instance TypeEq a a True -- instance TypeEq a b False instance eq ~ False = TypeEq a b eq

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

2013-02-27 Thread Aleksey Khudyakov
On 27.02.2013 17:35, Dmitry Kulagin wrote: Hi Aleksey, Unfortunately, your solution does not work for me (ghc 7.6.2). I reduced the problem to: -- | Type class for type equality. class TypeEq (a :: α) (b :: α) (eq :: Bool) | a b - eq instance TypeEq a a True -- instance TypeEq a

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

2013-02-27 Thread Dmitry Kulagin
Oh, that is my fault - I was sure that I specified the extension and it didn't help. It really works with OverlappingUndecidable. Thank you! On Wed, Feb 27, 2013 at 10:36 PM, Aleksey Khudyakov alexey.sklad...@gmail.com wrote: On 27.02.2013 17:35, Dmitry Kulagin wrote: Hi Aleksey,

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

2013-02-26 Thread Dmitry Kulagin
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 ::