On 1/3/14, Iavor Diatchki wrote:

Hi Gabor,

Hi Iavor, thanks for replying promptly!

On Fri, Jan 3, 2014 at 9:33 AM, Gabor Greif 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