Skip to content

Instantly share code, notes, and snippets.

@johnynek

johnynek/NatMatch.scala

Created January 10, 2023 18:40
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save johnynek/fd74bef5e4aab13bea0c07dcd553a8e5 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save johnynek/fd74bef5e4aab13bea0c07dcd553a8e5 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. johnynek created this gist Jan 10, 2023.
    43 changes: 43 additions & 0 deletions NatMatch.scala
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,43 @@
    package dev.posco.nui

    import scala.compiletime.{erasedValue, error, ops, requireConst}

    object NatExample {
    sealed trait Nat
    object Nat {
    case object Zero extends Nat
    case class Succ[N <: Nat](prev: N) extends Nat

    given zero: Zero.type = Zero
    given buildSucc[N <: Nat](using n: N): Succ[N] =
    Succ(n)

    def value[N <: Nat](using n: N): N = n

    type FromInt[I <: Int] <: Nat = I match {
    case 0 => Zero.type
    case _ =>
    // commented out trying to get fromInt to work
    // ops.int.<[I, 0] match {
    // case true => Nothing
    // case false =>
    Succ[FromInt[ops.int.-[I, 1]]]
    // }
    }

    inline def fromInt[I <: Int](inline i: I): FromInt[I] = {
    requireConst(i)
    inline i match {
    case _: 0 => Zero
    case _ =>
    inline if i < 0 then error("cannot convert negative to Nat")
    else {
    // obviously the cast is bad
    val prev: ops.int.-[I, 1] = (i - 1).asInstanceOf[ops.int.-[I, 1]]
    // this fails because prev is not a const even though this all should be inlined.
    Succ(fromInt[ops.int.-[I, 1]](prev))
    }
    }
    }
    }
    }