Make operations on Index only unsafe by choice (#680).

[rowanG077]

Initial draft based on discussion in #680.

There are various issues with this implementation right now.

• Breaking backwards compatibility because new constraints (KnownSatMode and in some case 1 <= n) are added.
• No correct handling of overflow/underflow in various situations where fromInteger_INLINE and fromInteger# is used. I would like to centralize this overflow/underflow in some function.
• Introducing the SaturationMode type level parameter is confusing for users because Unsigned and Signed don't have them. Maybe a solution could be to remove the SaturatingNum instances and only use Num for numeric types. Or keep the SaturatingNum instances and use it as a kind of override if you explicitly want different behaviour (this is the route I took in the draft). Either way I think it's best to keep the API for the number types the same.

[martijnbastiaan]

I'm not super sold on the omnipresent KnownSatMode. My guess is that it complicates error message /usage too much. I haven't had the time to experiment with it, so I don't know whether it's a necessity or not. I think I'd rather see something like:

instance Num (Index 'SatSymmetric n) [..]
instance Num (Index 'SatZero n) [..]

where

satAdd SatZero (2 :: Index 'SatWrap 3) 1

would force a certain saturation mode, but where otherwise "normal" operations would act like the type indicates. That is, given

a :: Index 'SatWrap 3
a = ..

=>

a + 1 ~ satAdd SatWrap a 1

This would require the ability to write:

f :: Num (Index sat n) => ...

for some functions. I'm not sure if we can do that though. If we can though, we would eliminate the need for GADTs, which would make the API a bit more friendly to beginners.

I'll see if I can setup a proof of concept this week.

[martijnbastiaan]

Oh, and thanks for making yet another PR. You're on fire 😄 !

[martijnbastiaan]

Another way to avoid complexity for the user is to simply make multiple Index types:

• WrappingIndex
• ZeroIndex
• SaturatingIndex
• etc.

We could even use this to deprecate Index and in a later release remove it altogether.

[rowanG077]

Another way to avoid complexity for the user is to simply make multiple Index types:

• WrappingIndex
• ZeroIndex
• SaturatingIndex
• etc.

We could even use this to deprecate Index and in a later release remove it altogether.

This is something I would like to avoid. Specifically because I think it should be possible for users to write polymorphic functions over the index types. In general with small composable functions you don't care what kind of wrapping mode is chosen as long as the caller ensures the operation is correct for the given index type.

[martijnbastiaan]

Wouldn't you just ask for Num if you don't care about wrapping?

[martijnbastiaan]

Also, I'm not necessarily saying they should be completely different types. They could be aliases of some basic type.

[rowanG077]

Wouldn't you just ask for Num if you don't care about wrapping?

This implies your functions is intended to be used with all types that implement Num. Maybe your function is only meant to be used with Index types.

Also, I'm not necessarily saying they should be completely different types. They could be aliases of some basic type.

Is adding a SaturationMode really so hard for users? I mean they are already confronted with types that work in this way (Vec for instance). To me it would be more confusing to have two different types which really do the same thing (Index 'SatWrap n and WrappingIndex n).

[martijnbastiaan]

Wouldn't you just ask for Num if you don't care about wrapping?

To answer my own question, @leonschoorl offered an example function you might want to write:

elemAt :: Vec n a -> Index sat n -> a

Which offers multiple advantages over Num:

• The Index has a very clear intended use for the function
• It's (with the exception of Index 'Error) safe

Is adding a SaturationMode really so hard for users?

I don't know. It's an "add to the to pile" kind of thing. The Clash API is already quite intimidating for new users, especially users not having a Haskell background. Phantom type variables and GADTs don't make it easier. Maybe this is simply solvable by having good documentation. Maybe users don't care as long as there are many examples.

To me it would be more confusing to have two different types which really do the same thing (Index 'SatWrap n and WrappingIndex n).

I'd imagine the docs being laid out something like this (don't pin me down on the structure, it's just an example):

Index
 * Saturating
 * Wrapping
 * Zero

where the general case (housed in Base? Or Index?) would clearly state it's a generalization of the other ones.

To be clear, I'm not sold on this proposal either, as it has usability problems too: using type aliases makes GHC prone to "see through" the type in error messages, suddenly confronting users with the general Index type, even though they're using WrappingIndex. Not making it a type alias (but a newtype) makes it hard, as you noted, to use it in a polymorphic setting.

[martijnbastiaan]

The more I think about it, the more I'm inclined to think that my problems aren't actually with your implementation but with:

1. The awful way Haddock generates available instances. What looks like

really should look like

Instance	When
Bounded (BitVector n)	KnownNat n
Data (BitVector n)	KnownNat n
Enum (BitVector n)	KnownNat n
Eq (BitVector n)
Integral (BitVector n)	KnownNat n
Num (BitVector n)	KnownNat n
Ord (BitVector n)
Resize BitVector
[..]

(Look! It's even sorted!)

Making superclasses so much more annoying to deal with in documentation.

2. The (for good reasons) unhelpfully generic error messages GHC generates a user does something wrong. We might be able to fix this by using custom type errors if no instance for KnownSatMode can be found; offering an explanation on what it is, why we need it, and what a user can do to fix the error.

[rowanG077]

If I look at the haddock output then we can write something behind the instances. But it's really not as nice as having a nice When column which gives the constraint. I will investigate the possibility of a custom type error if the KnownSatMode constraint is violated.

[martijnbastiaan]

@rowanG077 There's a very nice blogpost about custom type errors: https://kodimensional.dev/type-errors

[rowanG077]

Something like this is possible for us since there are a finite number of SaturationModes.

class Bar a where
  bar :: a -> a

data Foo (n :: Nat) = Foo

instance {-# OVERLAPS #-} Bar (Foo 0) where
  bar = id

instance {-# OVERLAPS #-} Bar (Foo 1) where
  bar = id

instance {-# OVERLAPPABLE #-} (TypeError (Text "N is not known")) => Bar (Foo a) where
  bar = id

instance
  (Bar (Foo n))
  => Eq (Foo n) where (==) _ _ = True

r1 = (Foo :: Foo 0) == Foo
r2 = (Foo :: Foo 1) == Foo
r3 = (Foo :: Foo 2) == Foo

r1 and r2 are valid but r3 fails to type check with a custom error message.

[martijnbastiaan]

Yeah, exactly!

[rowanG077]

Using this I believe we can get rid of the KnownSatMode constraint entirely. We can create a helper type class that either converts a SaturationMode type parameter to it's value level value or else it creates a type error.

[rowanG077]

Ignore my last post we can't get rid of it. I'm typing up something right now so we look at it concretely.

[rowanG077]

I have updated the code to have a custom type error.

test1 :: Index SatWrap 10 -> Index SatWrap 10 -> Index SatWrap 10
test1 a b = a + b

test2 :: Index sat 10 -> Index sat 10 -> Index sat 10
test2 a b = a + b

test3 :: (KnownSatMode sat) => Index sat 10 -> Index sat 10 -> Index sat 10
test3 a b = a + b

test1 and test3 work. If a user doesn't write the KnownSatMode constraint(test2) the following is shown:

Testing.hs:474:13: error:
    • SaturationMode isn't known. Add the `KnownSatMode` constraint
    • In the expression: a + b
      In an equation for ‘test2’: test2 a b = a + b
    |
474 | test2 a b = a + b

We can work on creating a better message but this is a proof of concept.

[martijnbastiaan]

Looks great!

We can work on creating a better message but this is a proof of concept.

We will :)

---

I've had a quick discussion internally about this PR. We concluded that this is a change we want to make, and that your approach makes sense. We don't want to make it a breaking change for 1.0 however, as we think there's a viable upgrade path:

1. For 1.0, add SatIndex, like you proposed. Add a pragma to Index:

newtype Index n = [..]
{-# DEPRECATED Index "Use SatIndex instead. Clash 1.2 will change `Index` to be `SatIndex`." #-} 

(Note that 1.1 will never be released, similar to GHC 8.5)

2. For 1.2, we'd remove Index, and rename SatIndex to Index instead. Well add type alias for SatIndex, and add a deprecation message to it.

3. For 1.4, we'd remove SatIndex.

I'm sorry I'm making you changing it for a second time now 😓 .

[rowanG077]

It's fine. This is a draft. The entire point is to discuss the options so we can make a good implementation. How are we going to handle newtype Index n for the public API's? Is the Idea to refactor everything internally to use SatIndex and then wrap/unwrap it into the Index type at the boundaries? I can also come over a day so we can make a plan in person about this change. That's most likely faster then me doing everything over chat here.

[rowanG077]

This change should be close to finished now. I have done the following:

• Renamed the Index sat type to SatIndex sat.
• Introduced a type alias type Index = Satindex 'SatError to keep as much backwards compatibility as possible. The type alias has a deprecation warning.
• Changed usages of the Index type across the whole to SatIndex. Wherever a SatIndexis returned the 'SatError SaturationMode is chosen. Where possible functions still accept a generic SatIndex sat.
• Bits and FiniteBits instances are only implemented for SatIndex 'SatError.

[christiaanb]

@rowanG077 thanks for all the hard work. I should have said this way earlier in the process, but I don't want to change Index as it breaks the API, which we wouldn't do after the release of Clash 1.0.

The solution is straightforward, add SatIndex as completely separate type, and keep Index around at the same time. Similarly, add a new function called simap, as opposed to changing the type of imap.

Then in the documentation, we can steer people towards using SatIndex, instead of Index. This way people can upgrade to new versions of Clash without it breaking their code. People need to update to the latest versions to get the bug-fixes, as we lack the people power to maintain two separate branches.

[rowanG077]

@christiaanb I don't believe that this will change the API. The newtype wrapper around SatIndex 'SatError should be API compatible with the old Index type. At least I can't think of a case where the API would differ off the top of my head. Well some type signature would be superficially different (For instance KnownSatMode constraints) but that shouldn't have an impact if you use a SatIndex with a concrete SatMode.

Maybe an idea to ensure this is the case is to let me finish up this pull request as is and you guys can run this on some larger Clash code bases?

[martijnbastiaan]

So this PR has gone stale for a while - I think we should either accept it or reject it. In private channels I've heard people are worried it might make Clash code less clear (by default) as wrapping behavior now depends on the type. This would make it less clear in larger code blocks what operations like + and - actually do.

Given this, I think we should consider two things:

1. Adding this PR, but renamed to SatIndex as proposed earlier. This would leave the choice to the user whether the implicitness is a problem or not.

2. Change the default wrapping behavior of Index to SatWrap. This would make operations "safe by default".

I'm in favor of (1) and against (2). I think overflows should always result in an error unless the user makes an explicit choice (looking at you, Signed / Unsigned / Int).

Pinging @christiaanb .

[christiaanb]

There's a couple of things:

1. I'd like to rename SatIndex to BoundedNatural or some variation on that theme
2. I'd like to see a benchmarked performance difference between:

   newtype BoundedNatural overflow n = BN { unsafeFromBoundedNatural :: Natural }

   and

   data BoundedNatural overflow n = BN { overflowMode :: !SaturationMode; unsafeFromBounedNatural :: !Natural }

   as in: I want to know whether those inconvenient KnownSaturationMode constraints are really worth it. I wish DependentHaskell was already here so we could just use foreach (overflow :: SaturationMode) . For this to work we will need a overflowBehavior# :: BoundedNatural overflow n -> SaturationMode primitive which the compile-time evaluator will evaluate even when the argument is a variable (i.e. it needs to be made explicitly lazy like some other primitives (&&, lazyV, etc.)).
3. I don't want to deprecate Index

Ultimately: I don't want any users to have to make any changes to their type signatures when they upgrade to a version of Clash that includes this patch.

[martijnbastiaan]

Why the name? Index already is a bounded natural, adding another type with a name exactly describing what Index is would make the difference confusing / non-obvious. In other words, I like the name SatIndex, because you can explain it in terms of Index.

[christiaanb]

Well... I already dislike the mistake I made originally calling it SaturationMode instead of OverflowMode, so using the prefix Sat is already annoying me.

Also the name Index was a mistake, so I’m glad we’re getting the opportunity to pick a sensible name. Nothing in https://en.m.wikipedia.org/wiki/Index screams bounded natural to me.

[martijnbastiaan]

I can see that, on its own, the name BoundedNatural makes sense. Similarly, OverflowMode would probably have been better than SaturationMode. But.. it is what we have right now. Introducing another name to refer to the same concept but with a different API is a mistake IMO. At least be consistent in the same library. Picking a different name for this also doesn't really fix anything if you don't want to rename Index - we'd still be stuck with it. And lastly, I think in practice people will simply learn the name Index and no one will really care that it could have gotten a slightly better name - like almost all names in programming languages.

[christiaanb]

But I'm not suggesting we rename Index, but simply do what's already in the PR:

{-# LANGUAGE StandaloneKindSignatures #-}
type BoundedNatural :: SaturationMode -> Nat -> Type
type Index n = BoundedNatural 'SatError n

Question: is your issue with using the name BoundedNatural with:

In private channels I've heard people are worried it might make Clash code less clear (by default) as wrapping behavior now depends on the type.

And that calling it BoundedNatural instead of SatIndex would draw people to use BoundedNatural over Index?

[martijnbastiaan]

But I'm not suggesting we rename Index, but simply do what's already in the PR:

Right, I like the idea of sharing an implementation. My "complaint" is that there's now one concept (bounded naturals) exported under two different names (BoundedNatural and Index). Index is a specialized version of BoundedNatural, but:

• It's not clear why a BoundedNatural specialized on SatError is suddenly called an Index.
• If concepts are as closely related as these are, I'd expect to find them under a similar name.

Do these arguments make sense to you?

And that calling it BoundedNatural instead of SatIndex would draw people to use BoundedNatural over Index?

No, I wouldn't mind. I'm really on the fence on what's better:

• Current Index: Local explicitness through with satAdd and friends, but a "dangerous" default of +.
• Proposed SatIndex: Type level explicitness with KnownSaturationMode and friends, but local implicitness of +.

I'm very slightly leaning towards the first option because type signatures are already complex enough.

---

To recap, this is what my ideal path would look like:

• Either:
  • Introduce SatIndex as BoundedNatural. Rename Index to BoundedNaturalE. Perhaps even completing the family with BoundedNaturalW, BoundedNaturalS, ...
  • Rename Index to BoundedNatural. Introduce SatIndex as BoundedNaturalI (I just realized how awful that name is, but you get the idea :-)).

I don't mind which path is taken, as long as the names are related.

• Deprecation of the name Index. If it's a bad name, we should just clean it up - or we're going to be stuck with it to the end of times. I don't think it would have to impact users all that much, as this could be done veeeery slowly:
  • Clash 1.6: Rename, but keep exporting Index. Update documentation to clarify that Index is now known under a new name.
  • Clash 1.8: Do nothing.
  • Clash 1.10: Add a deprecation warning
  • Clash 1.12: Do nothing
  • Clash 1.14: Remove Index
  • (Insert more "do nothings" where needed. I think this gives users plenty of time to update.)

[alex-mckenna]

Only just looking at this PR now: I have some thoughts on it as a whole. Please don't treat this as me not appreciating your work so far @rowanG077, I'm just wondering if there's a way to implement it and get a more "beginner-friendly" API.

---

The intent of this PR seems to be "for some values you want a different Num instance with a particular behaviour". I think it might instead be worth doing something like:

newtype Saturating a where
  Saturating :: { getSaturating :: a } -> Saturating a

instance (SaturatingNum a) => Saturating a where
  (+) = coerce (satAdd SatBound)
  -- other functions similarly using `coerce`

for the different default behaviours that may be wanted. From looking at SaturationMode, I guess this would be something like (omitting Symmetric because I'm not sure if it should actually just be a Bool in the Saturating type)

type Wrapping, Saturating, Zeroing :: Type -> Type

There doesn't seem a sensible place to put such types right now, I guess they would live under a new Clash.Num namespace in clash-prelude 🤷‍♂️

The wrapped types would pretty much only have a Num instance, and any other trivial instances to add like Eq, Ord, Show, NFData, XException, BitPack etc. I don't think it's entirely unreasonable to tell people that using any arbitrary function from the underlying repr they want means leaving the safe bubble of "all my operations respect this overflow mode".

I'm a bit unsure what the default should be though. I see two convincing options:

• error by default on out of bounds. This has the benefit of helping identify unexpected overflow/underflow in code, but behaves differently to the Num instances for Haskell types like Int. It could be confusing having some types error and some silently wrap
• wrap by default on out of bounds. This has exactly the opposite pros/cons as the above. Error on out of bounds would be provided by some type (e.g. Checking) instead.

This seems a bit better than just adding a SatIndex type as it means you can override the behaviour of Num for any SaturatingNum type, which makes the API less weird IMO. I think it's clearer to users to see a type like Saturating (Index n) than SatIndex 'SatWrap n which has stranger names (and the -XDataKinds tick which could confuse beginners).

---

Unrelated: In terms of making Index a synonym, is there any reason we can't just have

type Index n = Unsigned (CLog 2 n)

If that works it would also mean the special paths for Index in clash-lib and clash-ghc can be removed instead of needing to be changed to work with some other type.

[martijnbastiaan]

@alex-mckenna I really like that idea. Perhaps we could express SaturatingNum in terms of the other classes then. Minor nitpick: I dislike the get* pattern. The name doesn't make sense when constructing. I'd rather have:

newtype Saturating a = Saturating a

toSaturating :: a -> Saturating a
toSaturating a = Saturating a

fromSaturating :: Saturating a -> a
fromSaturating (Saturating a) = a 

---

Unrelated: In terms of making Index a synonym, is there any reason we can't just have

Type synonyms wouldn't work because operations on Index are supposed to error on out-of-bounds operations. Or did you mean a newtype wrapper?

[martijnbastiaan]

Second thought: perhaps we could use the individual classes as a way to phase out SaturatingNum.

Probably not a good idea, nvm!

[rowanG077]

@alex-mckenna I like your approach with one caveat. One of the important things (for me) about this PR in the long run was that it would be possible to phase out the default behaviour of the unsafe Num instance on Index. The transition would have been something like:

• Index type as a deprecation warning
• Removal of Index type. Rename SatIndex to Index and keep SatIndex as a type synonym.
• Deprecation warning on SatIndex.
• Removal of SatIndex type synonym.

Maybe I'm missing something but creating a Saturating wrapper doesn't help much to make Index safe. It would just be a more convenient way to access the SaturatingNum instance functions as if they are the Num instance.

[alex-mckenna]

Maybe I'm missing something but creating a Saturating wrapper doesn't help much to make Index safe.

Just adding this type alone doesn't help so much, no. It makes it better in a way because you can switch any number with a SaturatingNum instance to handle overflow by a certain way by default (i.e. changing the behaviour of Num). My suggestion is more a replacement for the first part, replacing things like SatIndex mode and KnownSatMode with newtype wrappers for the different modes that work on multiple underlying types.

If Index is a newtype around Saturating, i.e. Index n = Saturating (Unsigned (CLog 2 n)) then the Num instance becomes safe so long as the SaturatingNum instance of the underlying repr is safe (which is true for Unsigned). This doesn't make all operations safe (quot on Unsigned can throw DivideByZero because it uses quotNatural), but these can be changed to be safer (the only offenders on a quick read seem to be quot and rem), which are both expressible as primitive recursive functions using the safe Num instance. As a bonus you can define these in an (Integral a) => Integral (Saturating a) instance so all Integral types which can be wrapped in Saturating become safe by default

[martijnbastiaan]

@rowanG077 Great to see you're still active :D.

To summarize/reiterate a bit:

1. This PR develops a type-level way of switching between different saturation modes. @alex-mckenna improved on this idea by making it more beginner friendly / more generic.
2. We might want to change the default wrap-around behavior on Index to SatWrap instead of SatError. (Also, we might want to add a SatError / SatChecked :-)).

This PR used (1) as a vehicle to smoothly introduce (2). Here's my thoughts:

• I think we can do @alex-mckenna's take on (1) independently of (2). I actually really dig the idea on its own, so I think we should introduce it!
• Changing the default behavior of Index to SatWrap makes operations on Index more expensive in hardware (by default, ofc).
• The fact that overflow does not yield an error on Unsigned / Signed is a sore point for me. I think users should always explicitly state what they want in face of ambiguity. As far as I can tell, the only reason for not throwing an error boils down to performance reasons. I don't think we should introduce more Nuclear Ganhi's.
• ..but, the fact that there's a difference between Index and Unsigned/Signed is also a bit weird.
• GitHub's linear comments are terrible for discussion 😣

I'm sorry if we're talking in circles a bit @rowanG077. I'm trying to get us to have a definitive answer on the questions you've posed.

[martijnbastiaan]

If Index is a newtype around Saturating, i.e. Index n = Saturating (Unsigned (CLog 2 n)) then the Num instance becomes safe so long as the SaturatingNum instance of the underlying repr is safe (which is true for Unsigned).

If n is not a power of two, superfluous states exist where the value of Unsigned would lie outside of the domain of Index n. We'll always need separate implementations for Index and Unsigned.

[alex-mckenna]

Hmm, not strictly true. But using Unsigned would mean double the bounds check for SaturatingNum functions (one for the limit on Index then another on the limit for the underlying Unsigned). So I agree, not a good idea in practice

[rowanG077]

Superseded by #1908