Hi Gabor,
On Fri, Jan 3, 2014 at 9:33 AM, Gabor Greif
Hi devs,
with recent iterations of GHC.TypeLits (HEAD) I am struggling to get something simple working. I have
data Number nat = KnownNat nat => Number !(Proxy nat)
and want to write
addNumbers :: Number a -> Number b -> Maybe (Number (a + b))
Unfortunately I cannot find a way to create the necessary KnownNat (a + b) constraint.
Indeed, there is no way to construct `KnownNumber (a + b)` from `(Known a, Known b)`. This is not something that we lost, it was just never implemented. We could make something like it work, I think, but it'd make things a bit more complex: the representation of `KnownNumber` dictionaries would have to be expressions, rather than a simple constant. I'd be inclined to leave this as is for now---let's see what we can do with the current system, before we add more functionality. Declaring the function thus
addNumbers :: KnownNat (a + b) => Number a -> Number b -> Maybe (Number (a + b))
only dodges the problem around.
Dodging problems is good! :-) I don't fully understand from the type what the function is supposed to do, but I'd write something like this: addNumbers :: (KnownNat a, KnownNat b) => (Integer -> Integer -> Bool) -- ^ Some constraint? Proxy a -> Proxy b -> Maybe (Proxy (a + b)) addNumber p x y = do guard (p (natVal x) (natVal y)) return Proxy
Also I am wondering where the ability to perform a type equality check went. I.e. I cannot find the relevant functionality to obtain
sameNumber :: Number a -> Number b -> Maybe (a :~: b)
I guess there should be some TestEquality instance (for Proxy Nat?, is this possible at all), but I cannot find it. Same applies for Symbols.
Ah yes, I thought that this was supposed to be added to some other library, but I guess that never happened. It was implemented like this, if you need it right now. sameNumber :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) sameNumber x y | natVal x == natVal y = Just (unsafeCoerce Refl) | otherwise = Nothing This doesn't fit the pattern for the `TestEquality` class (due to the constraints on the parameters), so perhaps I'll add it back to GHC.TypeLits. -Iavor