Christopher Lane Hinson wrote:
On Fri, 16 Jul 2010, Paul L wrote:
Does anybody know why the type families only supports equality test
like a ~ b, but not its negation?
I would suggest that type equality is actually used for type inference,
whereas proof of type inequality would have no
On 07/17/2010 03:50 AM, Gábor Lehel wrote:
Does TypeEq a c HFalse imply proof of inequality, or unprovability
of equality?
Shouldn't these two be equivalent for types?
On Sat, Jul 17, 2010 at 2:32 AM, Steffen Schuldenzucker
sschuldenzuc...@uni-bonn.de wrote:
On 07/17/2010 01:08 AM, Paul L
Does anybody know why the type families only supports equality test
like a ~ b, but not its negation?
--
Regards,
Paul Liu
Yale Haskell Group
http://www.haskell.org/yale
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
I was wondering this. I was recently able to write some code for
negation of type equality, using the encoding Not p == p - forall
a. a
But it doesn't generalize; you need to create a witness of inequality
for every pair of types you care about.
{-# LANGUAGE RankNTypes, TypeFamillies,
Paul L nine...@gmail.com writes:
Does anybody know why the type families only supports equality test
like a ~ b, but not its negation?
At a guess, solely because no-one has implemented such functionality.
--
Ivan Lazar Miljenovic
ivan.miljeno...@gmail.com
IvanMiljenovic.wordpress.com
On 07/17/2010 01:08 AM, Paul L wrote:
Does anybody know why the type families only supports equality test
like a ~ b, but not its negation?
This has annoyed me, too. However, HList provides something quite similar,
namely the TypeEq[1] fundep-ed class which will answer type-equality with a
HList certainly provides an alternative. But given the use of
UndecidableInstances and OverlappingInstances, I was hoping that type
families could come a little cleaner. Or does it not matter?
On Fri, Jul 16, 2010 at 8:32 PM, Steffen Schuldenzucker
sschuldenzuc...@uni-bonn.de wrote:
On
Does TypeEq a c HFalse imply proof of inequality, or unprovability
of equality?
On Sat, Jul 17, 2010 at 2:32 AM, Steffen Schuldenzucker
sschuldenzuc...@uni-bonn.de wrote:
On 07/17/2010 01:08 AM, Paul L wrote:
Does anybody know why the type families only supports equality test
like a ~ b, but
On Fri, 16 Jul 2010, Paul L wrote:
Does anybody know why the type families only supports equality test
like a ~ b, but not its negation?
I would suggest that type equality is actually used for type inference,
whereas proof of type inequality would have no consequence (that I can think of)
