Skip to content

Instantly share code, notes, and snippets.

@johnynek

johnynek/NatInc.scala

Created June 23, 2021 00:38
Show Gist options

  • Select an option

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

Select an option

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

Revisions

  1. johnynek created this gist Jun 23, 2021.
    20 changes: 20 additions & 0 deletions NatInc.scala
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,20 @@
    package example

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

    type Inc[N <: Nat] <: Nat =
    N match {
    case Zero.type => Succ[Zero.type]
    case Succ[n] => Succ[Inc[n]]
    }

    object Nat {
    def inc[N <: Nat](n: N): Inc[N] =
    // it's important to match on the type below, or it won't unify (for some reason)
    n match {
    case _: Zero.type => Succ(Zero)
    case s: Succ[a] => Succ(inc(s.n))
    }
    }