Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
samuelchassot opened this issue Mar 1, 2024 · 2 comments
Open

Comments

@samuelchassot
Copy link
Collaborator

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
Copy link
Collaborator Author

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
Copy link
Collaborator Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant