On 1/3/14, Iavor Diatchki <[email protected]> wrote: > Hi Gabor,
Hi Iavor, thanks for replying promptly! > > > 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. Edwardkmettian dictionary-coercion tricks might help, but: > instance (KnownNat a, KnownNat b) => KnownNat (a + b) testTypeNats.lhs:1:40: Illegal type synonym family application in instance: a + b In the instance declaration for 'KnownNat (a + b)' So we have more fundamental problems here. Why is this illegal? > > 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. Okay, I'll ponder a bit how such a thing would look like. > > > 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 I souped this up thus: > {-# LANGUAGE TypeSynonymInstances, TypeOperators, GADTs #-} > import GHC.TypeLits > import Data.Proxy > import Control.Monad > data Number nat = KnownNat nat => Number !(Proxy nat) > addNumbers :: Number a -> Number b -> Maybe (Number (a + b)) > (Number a@Proxy) `addNumbers` (Number b@Proxy) > = case addNumber (\_ _-> True) a b of Just p -> Just $ Number p > addNumber :: (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 And I get an error where I wrap the Number constructor around the resulting proxy: testTypeNats.lhs:11:60: Could not deduce (KnownNat (a + b)) arising from a use of 'Number' from the context (KnownNat a) bound by a pattern with constructor Number :: forall (nat :: Nat). KnownNat nat => Proxy nat -> Number nat, in an equation for 'addNumbers' at testTypeNats.lhs:10:4-17 or from (KnownNat b) bound by a pattern with constructor Number :: forall (nat :: Nat). KnownNat nat => Proxy nat -> Number nat, in an equation for 'addNumbers' at testTypeNats.lhs:10:34-47 In the second argument of '($)', namely 'Number p' In the expression: Just $ Number p In a case alternative: Just p -> Just $ Number p Getting the sum proxy is not the problem. > > > > >> >> 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. Yeah, this would be helpful! It does not matter whether the TestEquality interface is there, as I can define that for my Number data type. But I don't want to sprinkle my code with unsafeCoerce! (Btw, these functions should be named: sameNat, sameSymbol.) Thanks again, Gabor > > -Iavor > _______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
