GADT typechecking requires unification analogue (via ConstraintHandling) #4176
Comments
|
See also test in #4069: object i3666 {
sealed trait Exp[T]
case class Num(n: Int) extends Exp[Int]
case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
case class Var[T](name: String) extends Exp[T]
case class Lambda[T, U](x: Var[T], e: Exp[U]) extends Exp[T => U]
case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]
abstract class Env { outer =>
def apply[T](x: Var[T]): T
def + [T](xe: (Var[T], T)) = new Env {
def apply[T](x: Var[T]): T =
if (x == xe._1) xe._2.asInstanceOf[T]
else outer(x)
}
}
object Env {
val empty = new Env {
def apply[T](x: Var[T]): T = ???
}
}
object Test {
val exp = App(Lambda(Var[Int]("x"), Plus(Var[Int]("x"), Num(1))), Var[Int]("2"))
def eval[T](e: Exp[T])(env: Env): T = e match {
case Num(n) => n
case Plus(e1, e2) => eval(e1)(env) + eval(e2)(env)
case v: Var[_] =>
env(v)
case Lambda(x: Var[s], e) => ((y: s) => eval(e)(env + (x -> y)))
case App(f, e) => eval(f)(env)(eval(e)(env))
}
eval(exp)(Env.empty)
}
}
// A HOAS well-typed interpreter
object i3666Hoas {
sealed trait Exp[T]
case class IntLit(n: Int) extends Exp[Int]
case class BooleanLit(b: Boolean) extends Exp[Boolean]
case class GenLit[T](t: T) extends Exp[T]
case class Plus(e1: Exp[Int], e2: Exp[Int]) extends Exp[Int]
case class Fun[S, T](f: Exp[S] => Exp[T]) extends Exp[S => T]
case class App[T, U](f: Exp[T => U], e: Exp[T]) extends Exp[U]
def eval[T](e: Exp[T]): T = e match {
case IntLit(n) => n
case BooleanLit(b) => b
case GenLit(t) => t
case Plus(e1, e2) => eval(e1) + eval(e2)
case f: Fun[s, t] =>
(v: s) => eval(f.f(GenLit(v)))
case App(f, e) => eval(f)(eval(e))
}
val exp = App(Fun[S = Int](x => Plus(x, IntLit(1))), IntLit(2))
eval(exp)
} |
|
While reviewing the literature and unification one should also consider #4471. |
This was referenced Sep 6, 2018
|
Here's a version of the original file which compiles even on master: object i4176 {
sealed trait TNat
case class TZero() extends TNat
case class TSucc[N <: TNat] extends TNat
object TNatSum {
sealed trait TSum[M, N, R]
case class TSumZero[N]() extends TSum[TZero, N, N]
case class TSumM[M <: TNat, N, R <: TNat](sum: TSum[M, N, R]) extends TSum[TSucc[M], N, TSucc[R]]
}
import TNatSum._
implicit def tSumZero[N]: TSum[TZero, N, N] =
TSumZero()
implicit def tSumM[M <: TNat, N, R <: TNat](implicit sum: TSum[M, N, R]): TSum[TSucc[M], N, TSucc[R]] =
TSumM(sum)
sealed trait Vec[T, N <: TNat]
case object VNil extends Vec[Nothing, TZero] // fails but in refchecks
case class VCons[T, N <: TNat](x: T, xs: Vec[T, N]) extends Vec[T, TSucc[N]]
def append0[T, M <: TNat, N <: TNat, R <: TNat]($this: Vec[T, M], that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] =
($this, tsum) match {
case (VNil, TSumZero()) => that
case (VCons(x, xs), TSumM(sum)) => VCons(x, append0(xs, that)(sum))
}
def append[T, M <: TNat, N <: TNat, R <: TNat]($this: Vec[T, M], that: Vec[T, N])(implicit tsum: TSum[M, N, R]): Vec[T, R] =
tsum match {
case TSumZero() =>
$this match { case VNil => that }
case TSumM(sum) =>
$this match { case VCons(x, xs) => VCons(x, append(xs, that)(sum)) }
}
}Original code wasn't compiling because class parameters aren't considered for GADT narrowing, which is already tracked in #5068. The code does compile with multiple spurious warnings of this sort: We may want to open a separate issue to track that. |
Merged
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In #4069 @smarter suggests GADT constraints might require unification:
So here's an unification-based use of GADTs: length-indexed vectors, which indeed doesn't typecheck. I also initially hoped to use
erasedforTNatSum(which would maybe work in Agda), but that'd be a request for enhancement in fact (and not sure it's one we should grant).I think this is still a relatively simple testcase, and I'm not sure it requires ConstraintHandling in the way @smarter meant, but I hope it is helpful. Before fixing this, I'd suggest a review the literature to find a comprehensive design (and I volunteer to take a look).
"Principal Type Inference for GADTs", from 2016, is a relatively recent reference (and pretty original) with a decent review of related work; I think "Complete and Decidable Type Inference for GADTs" and "OutsideIn(x) modular type inference with local assumptions" describe GHC's basic approach, while "GADTs Meet Their Match: Pattern-matching Warnings That Account for GADTs, Guards, and Laziness" describe GHC extensions for warnings.
The text was updated successfully, but these errors were encountered: