konn/type-natural

Type-level well-kinded natural numbers.

type-natural

Type-level well-kinded peano natural numbers and singletons with proofs of their properties.

type-natural's Issues

cmpZero does not terminate

Expected

> cmpZero sOne
Refl
> cmpZero Zero
Refl

but got

> cmpZero sOne
*** Exception: stack overflow
> cmpZero Zero

The 0 case never seems to reach a stack overflow, it just loops forever with constant memory usage. Nonetheless, the function is currently unusable.

Functions in the Data.Type.Natural.Lemma.Order module that don't depend on cmpZero seem to work fine.

In case it's version-specific:

• GHC 8.10.7
• type-natural 1.1.0.0
• constraints 0.13
• equational-reasoning 0.7
• ghc-typelits-knownnat 0.7.6
• ghc-typelits-natnormalise 0.7.6
• ghc-typelits-presburger 0.6.0.0
• integer-logarithms 1.0.3.1

ghc-typelits-natnormalise-0.6

Version 0.6 of the ghc-typelits-natnormalise plugin emits a b <= a constraints when it finds a solution for a constraint that contain a subtraction a - b. Without this b <= a constraint, the found solution for the equation involving a subtraction might otherwise potentially lead to unsound behaviour.

As a result this change, your package will no longer type-check if you build it with version 0.6 of the plugin. As a work-around you can add the

{-# OPTIONS_GHC -fplugin-opt GHC.TypeLits.Normalise:allow-negated-numbers #-}

pragma to the Data.Type.Natural.Builtin module. However, I advice you to check: https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.6/docs/GHC-TypeLits-Normalise.html and see if you can fix your code by adding b <= a constraints instead of that above pragma.

Please release a new version supporting singletons 2.5

HEAD does not compile with singletons-2.5.1.

Support for singletons 1.1?

Hi, would it be possible to get a new release of this library that accepts the current version of singletons as a build input?

Update for Singletons-2.0

Singletons released version 2.0 (and 2.0.0.1) in mid-September. It'd be great to get a new type-naturals!

Compilation error on 7.8.3

Hi,

When trying to compile under GHC 7.8.3, I get this error:

[2 of 2] Compiling Data.Type.Ordinal ( Data/Type/Ordinal.hs, dist/build/Data/Type/Ordinal.o )

Data/Type/Ordinal.hs:88:17:
    Couldn't match type ‘n0’ with ‘a’
      because type variable ‘a’ would escape its scope
    This (rigid, skolem) type variable is bound by
      a pattern with constructor
        Monomorphic :: forall (k :: BOX) (k1 :: k -> *) (a :: k).
                       k1 a -> Monomorphic k1,
      in a case alternative
      at Data/Type/Ordinal.hs:87:7-20
    Expected type: SNat n0
      Actual type: Sing a
    Relevant bindings include
      sn :: Sing a (bound at Data/Type/Ordinal.hs:87:19)
    In the first argument of ‘sS’, namely ‘sn’
    In the first argument of ‘(%:<<=)’, namely ‘sS sn’

Data/Type/Ordinal.hs:89:20:
    Could not deduce (('S a :<<= n) ~ 'True)
    from the context (SingI n)
      bound by the type signature for
                 unsafeFromInt :: SingI n => Int -> Ordinal n
      at Data/Type/Ordinal.hs:84:18-54
    or from (('S n0 :<<= n) ~ 'True)
      bound by a pattern with constructor
                 STrue :: forall (z0 :: Bool). z0 ~ 'True => Sing z0,
               in a case alternative
      at Data/Type/Ordinal.hs:89:11-15
    Relevant bindings include
      sn :: Sing a (bound at Data/Type/Ordinal.hs:87:19)
      unsafeFromInt :: Int -> Ordinal n
        (bound at Data/Type/Ordinal.hs:85:1)
    In the expression: sNatToOrd' (sing :: SNat n) sn
    In a case alternative: STrue -> sNatToOrd' (sing :: SNat n) sn
    In the expression:
      case sS sn %:<<= (sing :: SNat n) of {
        STrue -> sNatToOrd' (sing :: SNat n) sn
        SFalse -> error "Bound over!" }
cabal: Error: some packages failed to install:
type-natural-0.2.1.1 failed during the building phase. The exception was:
ExitFailure 1

The error is the same whether I use a cabal sandbox or not.

Allow constraints-0.9

type-natural-0.7.1.3 compiles with constraints-0.9. Please update the dependency on Hackage.

wrong constraint on %-

I think the constraint should be (m :<<= n) ~ True, not n :<<= m, since we're subtracting m from n.

Allow singletons-1.0

Would it be possible to update the package for compatibility with the (recently released) singletons-1.0? It may be as easy as updating the dependencies in the cabal file.

Create Typeable Instance

In this ticket, GHC.TypeLits were made to be typeable. Can this idea be used to make a Typeable instance for Z, S Z, etc?

lneqSucc n does not terminate for n > 0

Actual:

> case lneqSucc (SS SZ) of Witness -> "Hello sailor!"
"

Expected:

> case lneqSucc (SS SZ) of Witness -> "Hello sailor!"
"Hello sailor!"

Tested on type-natural 0.7.1.2 and GHCi 8.0.1.