0
# Type-level Natural Numbers
1

2
Type-level natural numbers in shapeless enable compile-time arithmetic and computations. They allow you to express constraints, perform calculations, and verify properties at the type level, providing additional safety and enabling advanced generic programming patterns.
3

4
## Core Types
5

6
### Base Natural Number Type
7

8
```scala { .api }
9
/**
10
 * Base trait for type-level natural numbers
11
 */
12
trait Nat
13
```
14

15
### Zero
16

17
```scala { .api }
18
/**
19
 * Type-level zero with implicit value
20
 */
21
class _0 extends Nat
22
implicit val _0: _0 = new _0
23
```
24

25
### Successor
26

27
```scala { .api }
28
/**
29
 * Successor type - represents N+1 for a natural number N
30
 */
31
case class Succ[P <: Nat]() extends Nat
32
```
33

34
### Generated Natural Numbers
35

36
Shapeless provides pre-defined type aliases for common natural numbers:
37

38
```scala { .api }
39
type _0 = shapeless._0
40
type _1 = Succ[_0]  
41
type _2 = Succ[_1]
42
type _3 = Succ[_2]
43
// ... continues up to _22
44
```
45

46
**Usage Examples:**
47

48
```scala
49
import shapeless._
50

51
// Using type-level numbers
52
val zero: _0 = _0
53
val one: _1 = Succ[_0]()  
54
val two: _2 = Succ[_1]()
55
val three: _3 = Succ[_2]()
56

57
// Type-level constraints
58
def takeN[L <: HList, N <: Nat](hlist: L, n: N)
59
  (implicit take: Take[L, N]): take.Out = hlist.take(n)
60

61
val hlist = 1 :: "hello" :: true :: 3.14 :: HNil
62
val first2 = takeN(hlist, _2)  // 1 :: "hello" :: HNil  
63
```
64

65
## Runtime Conversion
66

67
### ToInt Type Class
68

69
```scala { .api }
70
/**
71
 * Converts type-level Nat to runtime Int
72
 */
73
trait ToInt[N <: Nat] {
74
  def apply(): Int
75
}
76
```
77

78
### Utility Functions
79

80
```scala { .api }
81
/**
82
 * Convert type-level natural number to Int
83
 */
84
def toInt[N <: Nat](implicit toIntN: ToInt[N]): Int
85
def toInt[N <: Nat](n: N)(implicit toIntN: ToInt[N]): Int
86
```
87

88
**Usage Examples:**
89

90
```scala
91
import shapeless._
92

93
val five: _5 = Succ[Succ[Succ[Succ[Succ[_0]]]]]()
94

95
// Convert to runtime Int
96
val runtimeFive: Int = toInt[_5]        // 5
97
val alsoFive: Int = toInt(five)         // 5  
98

99
// Use in contexts requiring Int
100
def repeat[N <: Nat](s: String, n: N)(implicit toIntN: ToInt[N]): String = 
101
  s * toInt(n)
102

103
val repeated = repeat("hi", _3)  // "hihihi"
104
```
105

106
## Arithmetic Operations
107

108
### Addition
109

110
```scala { .api }
111
/**
112
 * Type-level addition A + B
113
 */
114
trait Sum[A <: Nat, B <: Nat] {
115
  type Out <: Nat
116
}
117
```
118

119
**Usage Examples:**
120

121
```scala
122
import shapeless._
123

124
// Type-level arithmetic in function signatures
125
def addLengths[L1 <: HList, L2 <: HList, N1 <: Nat, N2 <: Nat]
126
  (h1: L1, h2: L2)
127
  (implicit 
128
   len1: Length.Aux[L1, N1],
129
   len2: Length.Aux[L2, N2],  
130
   sum: Sum[N1, N2]): sum.Out = {
131
  // Implementation would use type class instances
132
  null.asInstanceOf[sum.Out]
133
}
134

135
val h1 = 1 :: 2 :: HNil           // Length = _2
136
val h2 = "a" :: "b" :: "c" :: HNil // Length = _3  
137
val totalLength = addLengths(h1, h2)  // Type: _5 (at type level)
138
```
139

140
### Subtraction
141

142
```scala { .api }
143
/**
144
 * Type-level subtraction A - B  
145
 */
146
trait Diff[A <: Nat, B <: Nat] {
147
  type Out <: Nat
148
}
149
```
150

151
**Usage Examples:**
152

153
```scala
154
import shapeless._
155

156
// Use in take/drop operations
157
def takeAndCount[L <: HList, N <: Nat, M <: Nat]
158
  (hlist: L, take: N, total: M)
159
  (implicit 
160
   takeOp: Take.Aux[L, N, _],
161
   diff: Diff[M, N]): diff.Out = {
162
  // Would return remaining count after taking N elements
163
  null.asInstanceOf[diff.Out]
164
}
165
```
166

167
### Multiplication
168

169
```scala { .api }
170
/**
171
 * Type-level multiplication A * B
172
 */
173
trait Prod[A <: Nat, B <: Nat] {
174
  type Out <: Nat
175
}
176
```
177

178
### Division and Modulo
179

180
```scala { .api }
181
/**
182
 * Type-level division A / B
183
 */
184
trait Div[A <: Nat, B <: Nat] {
185
  type Out <: Nat
186
}
187

188
/**
189
 * Type-level modulo A % B  
190
 */
191
trait Mod[A <: Nat, B <: Nat] {
192
  type Out <: Nat
193
}
194
```
195

196
## Comparison Operations
197

198
### Less Than
199

200
```scala { .api }
201
/**
202
 * Witnesses that A < B
203
 */
204
trait LT[A <: Nat, B <: Nat]
205

206
/**
207
 * Convenient type alias for LT
208
 */
209
type <[A <: Nat, B <: Nat] = LT[A, B]
210
```
211

212
**Usage Examples:**
213

214
```scala
215
import shapeless._
216

217
// Safe head operation that requires non-empty evidence
218
def safeHead[L <: HList, N <: Nat]
219
  (hlist: L)
220
  (implicit 
221
   len: Length.Aux[L, N],
222
   nonEmpty: _0 < N): hlist.H = hlist.head
223

224
val hlist = 1 :: "hello" :: HNil
225
val head = safeHead(hlist)  // Works: length is _2, and _0 < _2
226

227
// This would fail at compile time:
228
// val emptyHead = safeHead(HNil)  // Error: can't prove _0 < _0
229
```
230

231
### Less Than or Equal
232

233
```scala { .api }
234
/**
235
 * Witnesses that A <= B  
236
 */
237
trait LTEq[A <: Nat, B <: Nat]
238

239
/**
240
 * Convenient type alias for LTEq
241
 */
242
type <=[A <: Nat, B <: Nat] = LTEq[A, B]
243
```
244

245
### Predecessor
246

247
```scala { .api }
248
/**
249
 * Predecessor operation - computes N-1
250
 */
251
trait Pred[N <: Nat] {
252
  type Out <: Nat
253
}
254
```
255

256
**Usage Examples:**
257

258
```scala
259
import shapeless._
260

261
// Safe tail that maintains length relationship
262
def safeTail[L <: HList, N <: Nat]
263
  (hlist: L)
264
  (implicit 
265
   len: Length.Aux[L, N],
266
   pred: Pred[N],
267
   nonEmpty: _0 < N): Sized[HList, pred.Out] = {
268
  // Would return tail with length N-1
269
  ???
270
}
271
```
272

273
## Integration with HList Operations
274

275
Type-level natural numbers integrate deeply with HList operations:
276

277
### Indexed Access
278

279
```scala
280
import shapeless._
281

282
val hlist = "a" :: "b" :: "c" :: "d" :: HNil
283

284
// Type-safe indexed access
285
val first: String = hlist(0)   // "a" (using _0)  
286
val second: String = hlist(1)  // "b" (using _1)
287
val third: String = hlist(2)   // "c" (using _2)
288

289
// This would fail at compile time:
290
// val outOfBounds = hlist(5)  // Error: can't prove 5 < length
291
```
292

293
### Take and Drop Operations
294

295
```scala
296
import shapeless._
297

298
val hlist = 1 :: 2 :: 3 :: 4 :: 5 :: HNil
299

300
// Type-safe slicing with compile-time verification
301
val first3 = hlist.take(_3)    // 1 :: 2 :: 3 :: HNil (type: Take[..., _3])
302
val last2 = hlist.drop(_3)     // 4 :: 5 :: HNil (type: Drop[..., _3])
303

304
// Split maintains type-level relationship
305
val (prefix, suffix) = hlist.split(_2)  
306
// prefix: 1 :: 2 :: HNil
307
// suffix: 3 :: 4 :: 5 :: HNil
308
```
309

310
### Length Verification
311

312
```scala
313
import shapeless._
314

315
// Function that only accepts HLists of specific length
316
def processPair[T](pair: T :: T :: HNil): String = 
317
  s"Processing pair: ${pair.head} and ${pair.tail.head}"
318

319
val validPair = 1 :: 2 :: HNil
320
val result = processPair(validPair)  // Works
321

322
// This would fail at compile time:
323
// val invalidPair = 1 :: 2 :: 3 :: HNil  
324
// processPair(invalidPair)  // Error: doesn't match T :: T :: HNil
325
```
326

327
## Advanced Usage Patterns
328

329
### Sized Collection Integration
330

331
```scala
332
import shapeless._
333
import syntax.sized._
334

335
// Create sized collections with type-level length
336
val sizedList = List(1, 2, 3, 4, 5).sized(_5)  // Option[Sized[List[Int], _5]]
337

338
sizedList.map { sized =>
339
  val head = sized.head     // Safe: _0 < _5 is provable
340
  val tail = sized.tail     // Type: Sized[List[Int], _4]
341
  val first3 = sized.take(_3)  // Type: Sized[List[Int], _3]
342
}
343
```
344

345
### Type-level Constraints
346

347
```scala
348
import shapeless._
349

350
// Function that requires minimum length
351
def processAtLeast3[L <: HList, N <: Nat]
352
  (hlist: L)
353
  (implicit 
354
   len: Length.Aux[L, N],
355
   minLength: _3 <= N): String = s"Processing ${toInt[N]} elements"
356

357
val longList = 1 :: 2 :: 3 :: 4 :: HNil  
358
val result = processAtLeast3(longList)  // Works: _4 >= _3
359

360
val shortList = 1 :: 2 :: HNil
361
// processAtLeast3(shortList)  // Error: can't prove _3 <= _2
362
```
363

364
### Compile-time Arithmetic
365

366
```scala
367
import shapeless._
368

369
// Type-level function that doubles a number
370
trait Double[N <: Nat] {
371
  type Out <: Nat  
372
}
373

374
implicit val doubleZero: Double[_0] { type Out = _0 } = 
375
  new Double[_0] { type Out = _0 }
376

377
implicit def doubleSucc[N <: Nat, D <: Nat]
378
  (implicit double: Double.Aux[N, D], sum: Sum[D, _2]): Double[Succ[N]] { type Out = sum.Out } =
379
  new Double[Succ[N]] { type Out = sum.Out }
380

381
// Usage in type constraints
382
def repeatDouble[N <: Nat](s: String)
383
  (implicit double: Double[N], toInt: ToInt[double.Out]): String = 
384
  s * toInt[double.Out]
385

386
val doubled = repeatDouble[_3]("hi")  // Would repeat "hi" 6 times
387
```
388

389
Type-level natural numbers provide the foundation for compile-time verification and enable shapeless to catch errors at compile time rather than runtime, making generic programming both safer and more expressive.