GADT type refinement without GADTs

Question
1

Co/Contra-variance in Dependent Types

Hi all. The following piece of code will not compile and any help at all would be much appreciated.
What I am trying to do is provide a verified less-than checker on Peano natural numbers.
However, upon compiling I get the errors

  1. LTEZero(x) in case (Z,x) => Some(LTEZero(x)) has type LTEZero[B] and not LTENat[A,B], as expected.

  2. Similarly, LTESucc(pf) has type LTESucc[Nat, Nat] and not LTENat[A,B], as expected.

I suspect (please correct me if I’m wrong) that the issue lies in some co and contra variance relationships.
If so, could someone suggest a better definition of LTENat? Any and all related pages you could suggest would be helpful! Thanks!

// singleton Nats. E.g., One is S(Z): S[Z]
sealed trait Nat
trait Z extends Nat
case object Z extends Z
case class S[N <: Nat](n: N) extends Nat

// LTE is less-than-or-equal-to
abstract class LTENat[A <: Nat, B <: Nat]
case class LTEZero[A <: Nat](x: A) extends LTENat[Z, A]
case class LTESucc[A <: Nat, B <: Nat](x: LTENat [A, B])
    extends LTENat[S[A], S[B]]

object Proofs  extends App {

  def queryLT[A <: Nat, B <: Nat](n:A, m: B): Option[LTENat[A,B]] = {
    (n,m) match {
      case (Z, x) => Some(LTEZero(x))
      case (_, Z) => None
      case (S(x), S(y)) => None
        queryLT(x,y) match {
          case Some(pf) => Some(LTESucc(pf))
          case None => None
        }
    }
  }
}
1 Like
2

Reminds me of typelevel fizzbuzz https://gist.github.com/stew/4074742

3

Uh, have seen that, and marked it as wontfix: GADTs and top-level type variables · Issue #127 · scala/bug · GitHub — it’s not really a bug. See below for a fixed variant.

Variance doesn’t enter the picture. Scalac does not learn that type variable A maps to Z in that branch, because your Nat is not a GADT, while LTENat is.

More precisely: if A is a type variable and you match an instance of Foo[A] against a value, Scalac can refine A by usual GADT rules.
Instead, if you match an instance of A against a value, Scalac can’t refine A — it would be unsound in general, because A could be a Scala singleton type (say v.type, with v = S(Z)). In the example in GADTs and top-level type variables · Issue #127 · scala/bug · GitHub that’s clearly bad, but even above LETNat[v.type, B] is an empty type for all B.

These rules are no more restrictive than the ones you have in Haskell — there, if a: A and A is a type variable, you just cannot match on a.

BTW, other than this your code makes a lot of sense. Below’s the fixed version—the body of queryLT is the same! The entire code (including the redundancy between type-level and value-level naturals) is the same as in other non-dependently-typed languages like Haskell.

object PeanoLessThan {
  // Type-level numbers. All these types are empty.
  sealed trait TNat
  sealed trait TZ extends TNat
  sealed trait TS[TN <: TNat] extends TNat
  
  // Value-level numbers. For each `TN` there's only one value of `Nat[TN]`, up to structural equality.
  sealed trait Nat[TN <: TNat]
  case object Z extends Nat[TZ]
  case class S[TN <: TNat](s: Nat[TN]) extends Nat[TS[TN]]

  // LTE is less-than-or-equal-to
  abstract class LTENat[A <: TNat, B <: TNat]
  case class LTEZero[A <: TNat](x: Nat[A]) extends LTENat[TZ, A]
  case class LTESucc[A <: TNat, B <: TNat](x: LTENat[A, B])
    extends LTENat[TS[A], TS[B]]

  def queryLT[A <: TNat, B <: TNat](n: Nat[A], m: Nat[B]): Option[LTENat[A, B]] = {
    (n, m) match {
      case (Z, x) => Some(LTEZero(x))
      case (_, Z) => None
      case (S(x), S(y)) => None
        queryLT(x,y) match {
          case Some(pf) => Some(LTESucc(pf))
          case None => None
        }
    }
  }
}

Last: this is not an use of dependent types—Scala only has path-dependent types (which you are not using), and this is just a standard encoding of dependent types using GADTs and non-dependent types (the same possible in Haskell).
EDIT1: so I took the liberty of editing the title to be more accurate.
EDIT2: I forgot to say “congrats” for making the code so correct (apart from this issue, which is confusing). :slight_smile: