Closed remi-delmas-3000 closed 4 years ago
As of #6398, the runtime check warnings are no longer emitted. The only remaining problem is the exhaustivity warning:
scala> /** Natural transformation. */
| trait ~>[F[_], G[_]] {
| def apply[A](fa: F[A]): G[A]
| }
|
| /** Higher-kinded pattern functor typeclass. */
| trait HFunctor[H[f[_], i]] {
| def hmap[A[_], B[_]](nt: A ~> B): ([x] =>> H[A,x]) ~> ([x] =>> H[B,x])
| }
|
| /** Some HK pattern functor. */
| enum ExprF[R[_],I] {
| case Const[R[_]](i: Int) extends ExprF[R,Int]
| case Neg[R[_]](l: R[Int]) extends ExprF[R,Int]
| case Eq[R[_]](l: R[Int], r: R[Int]) extends ExprF[R,Boolean]
| }
|
| /** Companion. */
| object ExprF {
| implied hfunctor for HFunctor[ExprF] {
| def hmap[A[_], B[_]](nt: A ~> B): ([x] =>> ExprF[A,x]) ~> ([x] =>> ExprF[B,x]) = {
| new ~>[[x] =>> ExprF[A,x], [x] =>> ExprF[B,x]] {
| def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
| case Const(i) => Const(i)
| case Neg(l) => Neg(nt(l))
| case Eq(l, r) => Eq(nt(l), nt(r))
| }
| }
| }
| }
| }
23 | def apply[I](fa: ExprF[A,I]): ExprF[B,I] = fa match {
| ^^
|match may not be exhaustive.
|
|It would fail on pattern case: ExprF.Const(_), ExprF.Neg(_), ExprF.Eq(_, _)
// defined trait ~>
// defined trait HFunctor
// defined class ExprF
// defined object ExprF
Experimenting with higher-kinded recursion schemes and dotty, I got exhaustivity and unchecked type warnings with the attached code, and I can't make up my mind they are right or spurious
The enum is sealed and all cases are matched so the exhaustivity warning seems spurious.
If the exhaustivity warning is due to the fact that
ExprF[_[_], _]
is a higher-kinded GADT, well it seems that incorrect uses of a natural transformationA ~> B
lifted to[x] => ExprF[A, x] ~> [x] => ExprF[B, x]
usingExprF.hfunctor
will be caught anyway as demonstrated below:So it seems to me that the pattern match is exhaustive and that unchecked warnings are kind of noisy as I see no way of providing wrong input to
nt
that would get uncaught by the type system beforehand.Any how, dotty seems super nice for generic programming !
Attached is a fully working example of higher-kinded catamorphism, only issue are these warnings.
Best regards.
HK.scala.gz