Thank you Adam.
One example is https://github.com/haskell/vector/issues/34
Yes, this looks like an example where injectivity will work. One question here:
how does one build
vector with GHC HEAD? I tried but failed because of dependencies.
I see lots of potential uses in HList. For example
On Tue, Feb 10, 2015 at 6:38 AM, Jan Stolarek jan.stola...@p.lodz.pl wrote:
I don't know how realistic this is but a constraint (HLength x ~
HLength y) would ideally have the same result as SameLength x y.
I'm not sure if I understand that part. HLength is not injective. How would
injectivity
Haskellers,
I am finishing work on adding injective type families to GHC. I know that in
the past many people
have asked for this feature. If you have use cases for injective type families
I would appreciate
if you could show them to me. My implementation has some restrictions and I
want
]
current :: HLength y ~ 'HSucc ('HSucc 'HZero) = Proxy y
Regards,
Adam
On Mon, Feb 9, 2015 at 10:58 AM, Jan Stolarek jan.stola...@p.lodz.pl wrote:
Haskellers,
I am finishing work on adding injective type families to GHC. I know that in
the past many people
have asked for this feature. If you have
