Struggling with parameterizing type level scale

[symbiont-alexey-babkin]

Hi, I'm trying to use the lib to round up decimals at different places past the decimal point without reducing the scale.
I.e. to have roundHalfUp that would take a decimal and an Integer that would specify at what place past the decimal point the decimal should be rounded.
e.g. (pseudocode)roundHalfUp 2.415 2 would return 2.42 (round at 2 places after the decimal point)
Code is looking something like this:

roundDecimalBy ::
  D.Round r UnderlyingIntegral =>
  KnownNat k =>
  KnownNat n =>
  Proxy k ->
  D.Decimal r (n + k) UnderlyingIntegral ->
  D.Decimal r n UnderlyingIntegral
roundDecimalBy _ d = D.roundDecimal d 

roundHalfUp :: MyDecimal -> Integer -> Either SomeException MyDecimal
roundHalfUp (MyDecimal d) (someNatVal . naturalFromInteger -> (SomeNat n)) =
  map MyDecimal . D.scaleUpBounded $ roundDecimalBy n d

basically I'm trying to drive the scale change between scaleUpBounded and roundDecimal with an Integer value.
The hardship seems to be that scale is at the type level, so I need some dependently typed trickery to get this to work.
Would appreciate guidance on how to make this work.
Thank you

[symbiont-alexey-babkin]

ok I got it working as follows, but would really like to avoid the magic case statement and make it work for full range of Nat.

type Drs r s = D.Decimal r s UnderlyingIntegral

type Dr r = Drs r Scale

type Ds s = forall r. D.Round r UnderlyingIntegral => Dr r -> Drs r s

roundBy :: Integer -> (forall r. D.Round r UnderlyingIntegral => Dr r -> Either SomeException (Dr r))
roundBy = \case
  0 -> D.scaleUpBounded . (D.roundDecimal :: Ds 0)
  1 -> D.scaleUpBounded . (D.roundDecimal :: Ds 1)
  2 -> D.scaleUpBounded . (D.roundDecimal :: Ds 2)
  3 -> D.scaleUpBounded . (D.roundDecimal :: Ds 3)
  4 -> D.scaleUpBounded . (D.roundDecimal :: Ds 4)
  5 -> D.scaleUpBounded . (D.roundDecimal :: Ds 5)
  6 -> D.scaleUpBounded . (D.roundDecimal :: Ds 6)
  7 -> D.scaleUpBounded . (D.roundDecimal :: Ds 7)
  8 -> D.scaleUpBounded . (D.roundDecimal :: Ds 8)
  9 -> D.scaleUpBounded . (D.roundDecimal :: Ds 9)
  _ -> const $ throwM RoundingSpotOutOfBounds

roundHalfUp :: MyDecimal -> Integer -> Either SomeException MyDecimal
roundHalfUp (MyDecimal d) i = MyDecimal <$> roundBy i d

[lehins]

@symbiont-alexey-babkin You are exactly right, the way it is implemented now it does need some depend typing.

However it doesn't have to be that way. I'll make sure next version of safe-decimal will have rounding functions that don't change scaling of the decimal.

I wanted to experiment with this and see if I can get a solution for you by relying on the dependent types approach and I almost got it, but I hit a snag. Unfortunately, as far as GHC type checker is concerned, m ~ (n - k) is not the same as n ~ (m + k), so if we had this for roundDecimal's type signature:

roundDecimal' :: KnownNat k => Decimal r n p -> Decimal r (n - k) p

instead of this:

roundDecimal :: KnownNat k => Decimal r (n + k) p -> Decimal r n p

then I could use reflection package and its tricky reifyNat function to get what we want:

scaleUpProxy' :: forall k r n. KnownNat k => Proxy k -> Decimal r (n - k) Integer -> Decimal r n Integer
scaleUpProxy' px (Decimal d) = Decimal (d * (10 ^ natVal px))

roundDecimalProxy' :: (Round r p, KnownNat k) => Proxy k -> Decimal r n p -> Decimal r (n - k) p
roundDecimalProxy' _ = roundDecimal'

roundDecimalBy ::
     forall r n. (Round r Integer, KnownNat n)
  => Integer
  -> Decimal r n Integer
  -> Decimal r n Integer
roundDecimalBy k d = reifyNat (getScale d - k) $ \ px -> scaleUpProxy' px (roundDecimalProxy' px d)

and then we get:

λ> n <- arithM (1.2343567 :: Arith (Decimal RoundHalfUp 7 Integer))
λ> roundDecimalBy 5 n
1.2343600
λ> roundDecimalBy 4 n
1.2344000

But without the ghc's ability to infer the nat type variable's equality I can't figure it out. Maybe I'll just add

  roundDecimal' :: KnownNat k => Decimal r n p -> Decimal r (n - k) p

to the Round type class, just so others will not get into similar problem.