Hi Gabor,
On Fri, Jan 3, 2014 at 9:33 AM, Gabor Greif <[email protected]> wrote: > 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
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
