Numeric predicates don't support negative numbers

[adituv]

As the numeric predicates are parameterised on a Nat, they only support natural numbers. I've created a sketch of a possible way to support all integers in my fork: https://github.com/nikita-volkov/refined/compare/master...adituv:typeints

Non-negative refinement in this version is the same as before: From 3 Int.
Negative refinement uses a new empty datatype: To (Neg 3) Int.

I believe that by using PolyKinds I have defined them in a way that is fully compatible with existing code using refined, but I have not created a pull request because I feel like it would probably be better to depend on a library for type level integers rather than to bake them into refined, and wanted to get your feedback on this.

[chessai]

I've been thinking about doing something similar for a while. Let me look over this

[chessai]

Ah, I really wish we could use the Typeable machinery inside of GHC for Neg as well! Oh well.

I don't think KnownInt should be exported/defined as it is. My main issue is that KnownInt, like KnownNat, is essentially a class which is unsafe for an end user to define an instance of, but they still need to be able to write it as a constraint. 'intVal' should be exported, but not as a typeclass method of KnownInt, since we need people to be able to use it.

Note that the overlapping thing we have to do is an unfortunate consequence of not having access to internal typeable machinery.

[chessai]

I think the following is a better API:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Provides type-level signed integers using existing machinery for
--   type-level natural numbers
module Test (
  -- * Type-level Naturals
  Nat, KnownNat, natVal,

  -- * Type-level Integers
  KnownInt, Neg, intVal, intVal',

  -- * Comparison Operators
  type (<=?), type (<), type (<=), type (>), type (>=)
  ) where

import Data.Proxy(Proxy(..))
import Data.Typeable(Typeable)
import GHC.Prim(Proxy#)
import GHC.TypeLits(Nat, KnownNat, natVal)
import qualified GHC.TypeLits as G

-- | Analogue to 'KnownNat', gives the integer associated with a type-level
--   integer.
class KnownInt (n :: k) where
  intSing :: Neg n

intVal :: forall n proxy. KnownInt n => proxy n -> Integer
intVal _ = case intSing :: Neg n of
             Neg x -> x

intVal' :: forall n. KnownInt n => Proxy# n -> Integer
intVal' _ = case intSing :: Neg n of
              Neg x -> x

instance {-# OVERLAPPABLE #-} forall n. KnownNat n => KnownInt n where
  intSing = Neg (fromIntegral $ natVal (Proxy @n))

instance {-# OVERLAPPING #-} forall n. KnownNat n => KnownInt (Neg n) where
  intSing = Neg (negate $ fromIntegral (natVal (Proxy @n)))

type family (x :: k1) <=? (y :: k2) :: Bool where
    Neg x <=? Neg y = y <=? x
    Neg x <=? y     = 'True
    0     <=? Neg 0 = 'True
    x     <=? y     = (G.<=?) x y

type x <  y = (y <=? x) ~ 'False
type x <= y = (x <=? y) ~ 'True
type x >  y = (x <=? y) ~ 'False
type x >= y = (y <=? x) ~ 'True

newtype Neg (n :: k) = Neg Integer

[chessai]

Oh, also, I totally agree that this should be an external library on which refined depends. I would go ahead and create one, maybe call it 'type-ints' or something? Link me to the github repo when you make it, I'd love to take a look

[chessai]

Also I noticed some of the small changes you made that I can go ahead and incorporate into refined. I'll make sure to do that. Thank you!

[chessai]

Just realised I don't like the (<=?) conflict

[adituv]

Neg was meant to be a constructor for negative integers only, to maintain compatibility with any existing code using the predicates.

That is, I'd try something like this (away from computer right now, can't repl or typecheck it):

newtype TypeInt (n :: k) = TypeInt Integer
data Neg (n :: k)

class KnownInt (n :: k) where
  intSing :: TypeInt n

instance forall n. {-# OVERLAPPABLE #-} KnownNat n => KnownInt n where
  intSing = TypeInt (natVal (Proxy @n))

instance forall n. {-# OVERLAPPING #-} KnownNat n => KnownInt (Neg n) where
  intSing = TypeInt (negate $ natVal (Proxy @n))

Otherwise your feedback is great and I'll be taking that into account when later making the library, if one doesn't already exist. Thanks

[chessai]

It mostly typechecks, just that natVal returns Natural and not Integer. but otherwise that looks better. Specifies that TypeInt is Integer, and Neg should be negative

[adituv]

How does this look to you? https://github.com/adituv/typenums

I haven't exported (<=?) directly, instead leaving that as an export from the Data.TypeNums.Internal module; there is still a conflict with (<=) though, but that's unavoidable for the current design. I've aimed to make it so that for all type-level numeric things you can just import Data.TypeNums and not GHC.TypeLits, so conflicts should hopefully not matter, though!

[chessai]

I just skimmed over this; It looks good to me, and yeah, no way to get around those naming conflicts, but the fix (make it work for what GHC.TypeLits already did, in addition to what you provide) seems like a good fix. Just make sure that that is documented. I will look more in depth later. Thank you for doing this

[adituv]

Great. I've made a hackage account and emailed the admins to get upload privileges, and will upload it shortly :)

[chessai]

Before I use this inside of refined, i want to make sure there are no negative effects to usability for the end users of refined, e.g. behavioural changes of datatypes included. I'm not too concerned but I need to spend time on this, I'll make a fork where I do just that

[adituv]

Go for it! I've already done one using rationals for the predicates here, if you want to build off of this: https://github.com/adituv/refined/tree/typenums-port

[chessai]

Have not forgotten about this. Want it to be in 4.x

[adituv]

Build failures in typenums with GHC 8.6 are now fixed in version 0.1.2.1. It should be in stackage nightly shortly, and is already available on hackage.

[chessai]

Thanks @adituv !

[chessai]

moving milestone to 0.5

[chessai]

Sincerely sorry for the delay. I've been thinking about this on and off for a while, and now i think that this should be implemented on top of refined, rather than in it. IMO most predicates should exist separately from refined anyway - the ones i provide here are just ones i thought would be pretty commonly useful. But, i think supporting negative naturals is outside refined's scope as a library on top of which one implements refinements, and their addition would make the api more confusing - perhaps a refined-typenums library is in order? I'm going to close this for now. Let me know if you have any further ideas. Thank you