Scala 3 Logic Programming

Question
#1

I don’t understand why the following code won’t compile.

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT

type _1 = Succ[Zero]
type _2 = Succ[_1]

type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
  case Zero => X
  case Succ[y] => NatSum[Succ[X], y]

sealed trait NatDivides[X <: Succ[NatT], Y <: NatT]
object NatDivides:
  given baseCase[X <: Succ[NatT]]: NatDivides[X, Zero]()
  given inductiveCase[X <: Succ[NatT], Y <: NatT](using proof: NatDivides[X, Y]): NatDivides[X, NatSum[Y, X]]()

@main def main(): Unit =
  summon[NatDivides[_1, _2]]
  summon[NatDivides[_2, _2]]

I find it particularly odd since it does compile if I comment out the last line. I do not know how the compiler searches for a proof/instance of a type, but it seems to me that proving the last line should be easier than the line before it.

#2

I have the feeling that your clever trick, creating givens by induction is not understood by the compiler. If you write it out by hand, there is no problem, for example:

object NatDivides:
  given baseCase[X <: Succ[NatT]]: NatDivides[X, Zero]()
  given inductiveCase[X <: Succ[NatT], Y <: NatT](using proof: NatDivides[X, Y]): NatDivides[X, NatSum[Y, X]]()
  given p22: NatDivides[_2, _3] = new NatDivides[_2, _3]{}
  given p23: NatDivides[_3, _3] = new NatDivides[_3, _3]{}

@main def main(): Unit =
  summon[NatDivides[_1, _3]]
  summon[NatDivides[_2, _3]]
  summon[NatDivides[_3, _3]]
3 Likes
#3

I find it quite surprising that the _1 case worked at all.

I did managed to get something working using match types to represent whether or not something is a divisor Scastie - An interactive playground for Scala.

This seems to work, but there could be some edge cases which break

1 Like
#4

I don’t fully understand your example. You seem to be hard-coding that 2 divides 3 and that 3 divides 3 with p22 and p23. If I remove these, then NatDivides[_3, _3] doesn’t work anymore.

Inductive givens should work. However, in my code, the compiler would have to run NatSum backwards; that is probably the issue in general. Maybe that’s what you meant by “clever trick”?

1 Like
#5

That’s a nice way to do it. More straightforward. Thanks!

#6

I’ve just realised that a slight tweak to that NatDiv would make a modulus by returning X rather than Nothing

1 Like
#7

That’s what I just did :slight_smile:

#8

Hello @Bersier,

While I look forward to learning a bit of type level programming through your post (I have not done any yet), I am posting this on the off chance that you find it useful or interesting (examples in Haskell and Scala 2):

image
image1920×1071 200 KB

From Folding Unfolded - Polyglot FP for Fun and Profit - Haskell and Scala.