# Scala 3 Logic Programming

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.

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

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

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 `given`s 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

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

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

1 Like

That’s what I just did

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):