Type-level reasoning ability lost for TypeLits?

[Iavor Diatchki]

Hi Gabor,


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.

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140103/729f4ed3/attachment.html>