Sized Collections

/**
 * Wrapper witnessing statically known collection size
 * Repr - underlying collection type, L - size as type-level natural number  
 */
abstract class Sized[+Repr, L <: Nat](r: Repr) {
  type A  // Element type
  def unsized = r  // Extract underlying collection
}

object Sized {
  /**
   * Create sized collection factory for given collection type
   */
  def apply[CC[_]] = new SizedBuilder[CC]
  
  /**
   * Create empty sized collection
   */
  def apply[CC[_]]()(implicit cbf: CanBuildFrom[Nothing, Nothing, CC[Nothing]]): Sized[CC[Nothing], _0]
  
  /**
   * Wrap existing collection with size witness
   */
  def wrap[A0, Repr, L <: Nat](r: Repr): Sized[Repr, L]
}

import shapeless._
import syntax.sized._

// Create sized collections with known size
val sizedList: Sized[List[Int], _3] = Sized[List](1, 2, 3)
val sizedVector: Sized[Vector[String], _2] = Sized[Vector]("hello", "world")

// Verify size at runtime, get sized collection
val maybeList: Option[Sized[List[Int], _4]] = List(1, 2, 3, 4).sized(_4)
val maybeTooShort: Option[Sized[List[Int], _5]] = List(1, 2, 3).sized(_5)  // None

maybeList match {
  case Some(sized) => println(s"Got sized list of ${sized.unsized}")
  case None => println("Size mismatch")
}

/**
 * Provides sizing operations for collections
 */
class SizedConv[A, Repr <% GenTraversableLike[A, Repr]](r: Repr) {
  /**
   * Try to create sized collection of specified length (safe)
   */
  def sized[L <: Nat](implicit toInt: ToInt[L]): Option[Sized[Repr, L]]
  
  /**
   * Create sized collection of specified length (unsafe - throws on mismatch)
   */
  def ensureSized[L <: Nat](implicit toInt: ToInt[L]): Sized[Repr, L]  
}

import shapeless._
import syntax.sized._

val numbers = List(1, 2, 3, 4, 5)

// Safe sizing - returns Option
val sized5: Option[Sized[List[Int], _5]] = numbers.sized(_5)       // Some(...)
val sized3: Option[Sized[List[Int], _3]] = numbers.sized(_3)       // None (wrong size)

// Unsafe sizing - throws exception on mismatch
val ensured: Sized[List[Int], _5] = numbers.ensureSized(_5)        // Works
// val failed = numbers.ensureSized(_3)                            // Throws exception

// Use with different collection types  
val stringVec = Vector("a", "b", "c")
val sizedVec: Option[Sized[Vector[String], _3]] = stringVec.sized(_3)  // Some(...)

/**
 * Enhanced operations for sized collections
 */
class SizedOps[A, Repr, L <: Nat] {
  // Safe access (requires evidence that size > 0)
  def head(implicit ev: _0 < L): A
  def tail(implicit pred: Pred[L]): Sized[Repr, pred.Out]
  
  // Size-preserving slicing  
  def take[M <: Nat](implicit diff: Diff[L, M], ev: ToInt[M]): Sized[Repr, M]
  def drop[M <: Nat](implicit diff: Diff[L, M], ev: ToInt[M]): Sized[Repr, diff.Out]
  def splitAt[M <: Nat](implicit diff: Diff[L, M], ev: ToInt[M]): (Sized[Repr, M], Sized[Repr, diff.Out])
  
  // Size-changing operations
  def +:(elem: A)(implicit cbf: CanBuildFrom[Repr, A, Repr]): Sized[Repr, Succ[L]]
  def :+(elem: A)(implicit cbf: CanBuildFrom[Repr, A, Repr]): Sized[Repr, Succ[L]]
  def ++[B >: A, That, M <: Nat](that: Sized[That, M]): Sized[That, sum.Out] // where sum.Out = L + M
  
  // Size-preserving transformations
  def map[B, That](f: A => B)(implicit cbf: CanBuildFrom[Repr, B, That]): Sized[That, L]
}

import shapeless._
import syntax.sized._

val sizedList = List(1, 2, 3, 4, 5).ensureSized(_5)

// Safe head - compiles because _0 < _5
val head: Int = sizedList.head           // 1

// Safe tail - type shows decremented size
val tail: Sized[List[Int], _4] = sizedList.tail  // List(2, 3, 4, 5) with size _4

// Empty list would fail to compile:
val empty = List.empty[Int].ensureSized(_0) 
// empty.head  // Compile error: can't prove _0 < _0

import shapeless._
import syntax.sized._

val sizedList = List("a", "b", "c", "d", "e").ensureSized(_5)

// Take operations with compile-time size checking
val first3: Sized[List[String], _3] = sizedList.take(_3)       // List("a", "b", "c")
val last2: Sized[List[String], _2] = sizedList.drop(_3)        // List("d", "e")

// Split preserves size relationships
val (prefix, suffix) = sizedList.splitAt(_2)
// prefix: Sized[List[String], _2] = List("a", "b")  
// suffix: Sized[List[String], _3] = List("c", "d", "e")

// This would fail at compile time:
// val tooMany = sizedList.take(_6)  // Error: can't prove _6 <= _5

import shapeless._
import syntax.sized._

val sized3 = List(1, 2, 3).ensureSized(_3)

// Prepend and append increment size
val sized4: Sized[List[Int], _4] = 0 +: sized3        // List(0, 1, 2, 3)  
val sized4b: Sized[List[Int], _4] = sized3 :+ 4       // List(1, 2, 3, 4)

// Concatenation adds sizes
val other2 = List(10, 20).ensureSized(_2)
val sized5: Sized[List[Int], _5] = sized3 ++ other2   // List(1, 2, 3, 10, 20)

import shapeless._
import syntax.sized._

val numbers = List(1, 2, 3, 4).ensureSized(_4)

// Map preserves size
val doubled: Sized[List[Int], _4] = numbers.map(_ * 2)        // List(2, 4, 6, 8)
val strings: Sized[List[String], _4] = numbers.map(_.toString) // List("1", "2", "3", "4")

// Size is preserved even with different collection types
val sizedVec: Sized[Vector[Int], _4] = numbers.map(identity)(Vector.canBuildFrom)

import shapeless._
import syntax.sized._

// Function requiring minimum size
def processAtLeast3[A, Repr, N <: Nat]
  (sized: Sized[Repr, N])
  (implicit ev: _3 <= N, toInt: ToInt[N]): String = 
  s"Processing ${toInt()} elements (at least 3)"

val validList = List(1, 2, 3, 4).ensureSized(_4)
val result = processAtLeast3(validList)  // "Processing 4 elements (at least 3)"

val tooSmall = List(1, 2).ensureSized(_2)
// processAtLeast3(tooSmall)  // Compile error: can't prove _3 <= _2

// Function requiring exact size
def processPair[A, Repr](pair: Sized[Repr, _2]): String = "Processing pair"

val exactPair = List("a", "b").ensureSized(_2)
val pairResult = processPair(exactPair)  // Works

val notPair = List("a", "b", "c").ensureSized(_3)  
// processPair(notPair)  // Compile error: type mismatch

import shapeless._
import syntax.sized._

// Combine sized collections with known total size
def combineAndVerifySize[A, N <: Nat, M <: Nat]
  (left: Sized[List[A], N], right: Sized[List[A], M])
  (implicit sum: Sum[N, M]): Sized[List[A], sum.Out] = left ++ right

val list3 = List(1, 2, 3).ensureSized(_3)
val list2 = List(4, 5).ensureSized(_2)  
val list5: Sized[List[Int], _5] = combineAndVerifySize(list3, list2)  // List(1, 2, 3, 4, 5)

import shapeless._
import syntax.sized._

// Create sized collection from user input
def createUserList[N <: Nat](elements: List[String])
  (implicit toInt: ToInt[N]): Either[String, Sized[List[String], N]] = {
  
  elements.sized[N] match {
    case Some(sized) => Right(sized)
    case None => Left(s"Expected ${toInt[N]} elements, got ${elements.length}")  
  }
}

val userInput = List("apple", "banana", "cherry")
val result: Either[String, Sized[List[String], _3]] = createUserList[_3](userInput)
// Right(Sized(...))

val wrongSize: Either[String, Sized[List[String], _5]] = createUserList[_5](userInput)  
// Left("Expected 5 elements, got 3")

import shapeless._
import syntax.sized._

// Convert between sized collections and HLists
def sizedToHList[A, N <: Nat](sized: Sized[List[A], N]): HList = {
  // This would require complex type machinery in practice
  // Shown conceptually - real implementation needs more infrastructure
  ???
}

// Type-safe indexing matching HList capabilities
val sized = List("a", "b", "c").ensureSized(_3)
val first = sized.head        // "a" - safe because size >= 1
val second = sized.tail.head  // "b" - safe because size >= 2  
val third = sized.tail.tail.head  // "c" - safe because size >= 3

import shapeless._
import syntax.sized._

// Sized collections don't add runtime overhead
val normalList = List(1, 2, 3, 4, 5)
val sizedList = normalList.ensureSized(_5)

// Operations compile to same bytecode as normal collections
val doubled = sizedList.map(_ * 2)  // No extra runtime cost
val underlying = doubled.unsized    // Extract original collection type

// Size checking happens only at creation time
val validated = normalList.sized(_5)  // O(n) to check size
// All subsequent operations are O(1) for size tracking