"publicly opaque" concept would be useful when working with laws

[samuelchassot]

when working with laws in trait, for example:

sealed trait Serialiser[T]:
  def serialise(x: T): List[Char]
  def deserialise(l: List[Char]): Option[T]
  @law def serialiseDeserialise(x: T): Boolean = deserialise(serialise(x)) == x
end Serialiser

I would like to be able to make the serialise and deserialise functions opaque from the outside of a class implementing this trait, so that the proof does rely only on the laws. However, I'd like the functions to not be opaque inside the class definition itself.

Here for example, a class implementing the trait Serialiser should be able to see its own implementation of serialise and deserialise to prove that the laws hold. However, other classes having access to an instance of such class shouldn't be able to access the implementation details, but only the laws.

Ex:

case class CharSerialiser extends Serialiser[Char]:
  def serialise(x: T): List[Char]
  def deserialise(l: List[Char]): Option[T]
  override def serialiseDeserialise(x: T): Boolean = 
    // Here the definitions are visible
    deserialise(serialise(x)) == x

case class ConcatSerialiser[T, U](
    ts: FixedSizeSerialiser[T],
    us: FixedSizeSerialiser[U]
) extends FixedSizeSerialiser[(T, U)]:
   def serialise(t: (T, U) ): List[Char] = ...
   def deserialise(l: List[Char]): Option[(T, U) ] = ...
     override def serialiseDeserialise(x: (T, U) ): Boolean = 
    // Here the implementations of ts and us should be opaque, and the proof should rely on the laws
    deserialise(serialise(x)) == x

[samuelchassot]

So in summary, it would be interesting to have a notion of "private" vs "public" implementations: so

• alwaysopaque
• opaque from the outside of the class
• not opaque

[samuelchassot]

can use the unfold operator where the opaque function body should be visible. Maybe we could add it automatically?