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.
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
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
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
,
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
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
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
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,
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 ::