[RFC] Type-level Integers

Change Proposals
#1

I’ve recently started working on adding support for Type-level Integers and would like to open an RFC regarding the following features. As a short introduction, this PR essentially adds syntax for type-level integers (kinded with the Int type), as well as type classes for operations such Add, Mul, Compare, and IsReflectable. I’d like to ask about the following concerns that we’ve encountered in the PR, in no particular order.

  1. IsReflectable's name was chosen as to parallel the existing convention with IsSymbol, whose purpose it also overrides. As discussed in the PR, other names for IsReflectable can be Reflectable, Reifies, Reflect, or Reify. Breaking precedence with these alternative options seems optimal if we eventually want to remove IsSymbol in the future, as well as to make Symbols kinded with String instead.
class IsReflectable t v | v -> t where
  reflectType :: forall proxy. proxy v -> t
  1. With regards to a type-level DivMod operation, what are some possible “practical” use-cases for it? Existing packages which depend on typelevel-peano only seem to make use of addition/multiplication. At the moment, DivMod is constrained as to only allow for denominators that are > 0, and there’s also the question whether or not negative denominators are significant enough to relax this constraint.
class (Compare 0 denominator LT) <= DivMod (numerator :: Int) (denominator :: Int) (quotient :: Int) (remainder :: Int) | numerator denominator -> quotient remainder
  1. The Compare type class for type-level integers involves a solving algorithm which can infer relationships like so. Should Compare this be backported for Symbols as well?
7 Likes
#2

Regarding 2:

I think this could be very useful for vectors:

  • splitting up a Vect of n elements into Vectors of m elements, typically called grouped. e.g. grouped [1,2,3,4,5] == { groups: [[1,2], [3,4]], remaining: [5] }
  • sliding window on Vectors: slidingSizeStep 3 2 [0,1,2,3,4,5,6,7,8,9,10] = [[0,1,2],[2,3,4],[4,5,6],[6,7,8],[8,9,10],[10]]
  • scanLeft probably also

Regarding 3:

I personally wouldn’t need it for symbols.

Would be very interested in seeing some performance benchmarks. How does it perform on large numbers?

1 Like
#3

Practically native performance. The integers are backed by Haskell’s Integer type, and the type classes are solved by the compiler.

Agreed, I’d imagine that grouped would look like the following:

grouped 
  :: DivMod n d q r
  => Proxy d 
  -> Vec n a 
  -> { groups :: Vec q (Vec q a)
     , remaining :: Vec r a 
     }
#4

yep, but you probably meant

If you get practically native performance that would be really awesome! Have to try it in my vector lib :slight_smile:

#5

For some additional motivation: with row types, I think you could make a really wonderful lightweight system for units-of-measure types with this.

4 Likes