Type-level reasoning ability lost for TypeLits?

[Gabor Greif]

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
>