On 1/3/14, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:

> Hi Gabor,

Hi Iavor, thanks for replying promptly!

>

>

> On Fri, Jan 3, 2014 at 9:33 AM, Gabor Greif <ggreif at gmail.com> 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 at Proxy) `addNumbers` (Number b at 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

>