Type-level Natural Numbers

/**
 * Base trait for type-level natural numbers
 */
trait Nat

/**
 * Type-level zero with implicit value
 */
class _0 extends Nat
implicit val _0: _0 = new _0

/**
 * Successor type - represents N+1 for a natural number N
 */
case class Succ[P <: Nat]() extends Nat

type _0 = shapeless._0
type _1 = Succ[_0]  
type _2 = Succ[_1]
type _3 = Succ[_2]
// ... continues up to _22

import shapeless._

// Using type-level numbers
val zero: _0 = _0
val one: _1 = Succ[_0]()  
val two: _2 = Succ[_1]()
val three: _3 = Succ[_2]()

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

val hlist = 1 :: "hello" :: true :: 3.14 :: HNil
val first2 = takeN(hlist, _2)  // 1 :: "hello" :: HNil

/**
 * Converts type-level Nat to runtime Int
 */
trait ToInt[N <: Nat] {
  def apply(): Int
}

/**
 * Convert type-level natural number to Int
 */
def toInt[N <: Nat](implicit toIntN: ToInt[N]): Int
def toInt[N <: Nat](n: N)(implicit toIntN: ToInt[N]): Int

import shapeless._

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

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

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

val repeated = repeat("hi", _3)  // "hihihi"

/**
 * Type-level addition A + B
 */
trait Sum[A <: Nat, B <: Nat] {
  type Out <: Nat
}

import shapeless._

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

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

/**
 * Type-level subtraction A - B  
 */
trait Diff[A <: Nat, B <: Nat] {
  type Out <: Nat
}

import shapeless._

// Use in take/drop operations
def takeAndCount[L <: HList, N <: Nat, M <: Nat]
  (hlist: L, take: N, total: M)
  (implicit 
   takeOp: Take.Aux[L, N, _],
   diff: Diff[M, N]): diff.Out = {
  // Would return remaining count after taking N elements
  null.asInstanceOf[diff.Out]
}

/**
 * Type-level multiplication A * B
 */
trait Prod[A <: Nat, B <: Nat] {
  type Out <: Nat
}

/**
 * Type-level division A / B
 */
trait Div[A <: Nat, B <: Nat] {
  type Out <: Nat
}

/**
 * Type-level modulo A % B  
 */
trait Mod[A <: Nat, B <: Nat] {
  type Out <: Nat
}

/**
 * Witnesses that A < B
 */
trait LT[A <: Nat, B <: Nat]

/**
 * Convenient type alias for LT
 */
type <[A <: Nat, B <: Nat] = LT[A, B]

import shapeless._

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

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

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

/**
 * Witnesses that A <= B  
 */
trait LTEq[A <: Nat, B <: Nat]

/**
 * Convenient type alias for LTEq
 */
type <=[A <: Nat, B <: Nat] = LTEq[A, B]

/**
 * Predecessor operation - computes N-1
 */
trait Pred[N <: Nat] {
  type Out <: Nat
}

import shapeless._

// Safe tail that maintains length relationship
def safeTail[L <: HList, N <: Nat]
  (hlist: L)
  (implicit 
   len: Length.Aux[L, N],
   pred: Pred[N],
   nonEmpty: _0 < N): Sized[HList, pred.Out] = {
  // Would return tail with length N-1
  ???
}

import shapeless._

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

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

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

import shapeless._

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

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

// Split maintains type-level relationship
val (prefix, suffix) = hlist.split(_2)  
// prefix: 1 :: 2 :: HNil
// suffix: 3 :: 4 :: 5 :: HNil

import shapeless._

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

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

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

import shapeless._
import syntax.sized._

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

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

import shapeless._

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

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

val shortList = 1 :: 2 :: HNil
// processAtLeast3(shortList)  // Error: can't prove _3 <= _2

import shapeless._

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

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

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

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

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