Skip to content

Conversation

@katrinafyi
Copy link
Member

@katrinafyi katrinafyi commented Aug 27, 2025

cc @b-paul for LatticeCollections :)

This does a major refactor of the lattices to use Lattice[T] as /the/ representation for lattice operations. The Lattice[T] trait itself is largely unchanged, but it is instantiated in more places as an type class instance and it fully takes over the role of InternalLattice.

The InternalLattice abstraction had two major problems, stemming from the fact that it implements the lattice functions as instance methods within the lattice element class.

  • It forces the user to pass around an arbitrary value to access conceptually "global" functions like top and bottom.
  • Flexibility is severely limited, because the type constraint T <: InternalLattice[T] forces the trait to be implemented on the class type itself. This makes it impossible to have multiple lattices on the same type, and it makes it very difficult to do certain compositions of lattices to derive other lattices.

In making this change, we gain notable benefits:

  • No need to have implicit vals for every lattice instance to access the top/bottom functions. (Though givens are similar, it is conceptually nicer because it's an implicit Lattice[T] value which precisely scopes its purpose. This is rather than an implicit T lattice element which happens to be a subtype of InternalLattice[T])
  • LatticeMap methods are simplified to avoid the need for implicit parameters and an implicit subtyping proof. I don't actually know why the <:< proof was needed, but I guess it was because of certain subtypings of InternalLattice.

Along the way, I have made some incidental changes:

  • all methods of Lattice[T] are now abstract, with no default implementations. previously, top and glb defaulted to ???. i think it's better to be explicit here.
  • In Lattice[T], I've added extension methods to define meet and join. This means that if you have a Lattice[T] in scope, you can call .join on values of type T to access the lattice functions. That is, x.join(y) simply invokes lattice.lub(x, y). This matches the previous API of InternalLattice and makes it similarly convenient to use.
  • However, there are still some places (mostly in Lattice.scala) where lattice elements are passed explicitly and classes have too many type parameters. These are no longer necessary because the given system should be able to summon a Lattice when needed. I tried to change this too, but I gave up because it's a whole house of cards. These classes are used and subclassed everywhere.

All of the tests pass just the same, so I'm reasonably confident I haven't broken anything.

I am also very happy to take feedback on the design. Type classes are another Scala feature to learn, but I think it is much more familiar than implicit vals and leads to a more regular interface.

The relevant scala documentation pages are:

Note that we have to use the "previous" given syntax since we're on Scala 3.3 LTS. Also, note that these docs are actually good - this is because it's a new feature in Scala 3.

@katrinafyi
Copy link
Member Author

I think this PR does make the code nicer, but my main worry is about the learning curve for new basillers and the discoverability of typeclass instances. What're your thoughts?

Since typeclasses separate the typeclass methods away from the type they operate on, there is no link in the docs to go from, for example, enum LatticeSet[T] to the given [T]: Lattice[LatticeSet[T]] instance. And basillers will only know to look for the given instance if they already know about typeclasses.

Haskell solves this by adding an "Instances" list to each datatype (showing all its implemented typeclasses) and each typeclass (showing all types which implement that typeclass). This bidirectional cross-referencing would help a lot.

I can imagine some ways to help with this problem:

  • manually add links in the scaladoc comments to point to the implemented given instances, or
  • implement the typeclasses on the companion object (though this only works for non-generic lattice types, e.g. not LatticeSet[T]), or
  • make a new scala PR to add a "Known instances" list, like Haskell and like scaladoc's "Known subtypes" list.

@agle
Copy link
Contributor

agle commented Aug 28, 2025

I think its probably OK to teach new basilers about type-classes through documentation of a specific example e.g. a tutorial or documentation links in a representative lattice (or even just this tutorial https://web.archive.org/web/20250317112721/https://continuation.passing.style/blog/writing-abstract-interpreter-in-scala.html). The custom error messages probably help too? When I looked at this problem I decided it was more straightforward to explicitly pass around AbstractDomain[T] classes that hold the methods for the lattice with elements of type T, but typeclasses hopefully make it less clunky to define and compose these.

make a new scala PR to add a "Known instances" list, like Haskell and like scaladoc's "Known subtypes" list.

I imagine you will end up doing this regardless of what I say :)

@katrinafyi
Copy link
Member Author

katrinafyi commented Sep 8, 2025

@j-tobler I would be grateful for your review of this change request. In particular, does the motivation to you and do the changes make sense? I think you have worked with the Lattice trait before, but maybe not InternalLattice. Bother me immediately if there are any questions.

todo:

  • remove extension methods for Lattice[T]

agle and others added 8 commits September 16, 2025 12:24
Some initial progress towards cleaning up RunUtils.

Created classes Transform, StaticAnalysis and AnalysisManager.
Refactored doCleanup, prepareForTranslation,
generateRelyGuaranteeConditions, and generateFunctionSummaries to use
the Transform class.
ci: `mill -i` to disable daemon
Conflicts:
src/main/scala/ir/IRLoading.scala
src/main/scala/util/RunUtils.scala
@github-actions
Copy link
Contributor

github-actions bot commented Sep 16, 2025

automated scalafmt applied successfully.

last updated at 17b6e38 (logs).

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

Successfully merging this pull request may close these issues.

4 participants