Skip to content
This repository was archived by the owner on Feb 8, 2022. It is now read-only.

Law testing guidelinesΒ #209

@denisrosset

Description

@denisrosset

(This comment is not about the simpler encoding discussed in #206.)

I remarked that the laws structure does not follow the typeclass structure exactly. For example, we have tests for Lattice[A] with BoundedJoinSemilattice[A], which simply collect laws of Lattice and BoundedJoinSemilattice, however the corresponding combined typeclass does not exist.

Combinations with DistributiveLattice[A] do not exist: thus we have the quite obtuse fragment

  def generalizedBool(implicit A: GenBool[A]) = new LogicProperties(
    name = "generalized bool",
    parents = Seq(),
    ll = new LatticeProperties(
      name = "lowerBoundedDistributiveLattice",
      parents = Seq(boundedJoinSemilattice, distributiveLattice),
      join = Some(boundedSemilattice(A.joinSemilattice)),
      meet = Some(semilattice(A.meetSemilattice))
    ),

in the definition of generalizedBool.

Laws should serve as executable documentation, and this goes against the spirit.

I don't know what is the good solution there

Solution 1: the law hierarchy follows the typeclass hierarchy. Extra laws that occur when multiple types interact are proposed separately (i.e. lattices with partial orders). For this to work, we need a way to merge RuleSets.

Solution 2: close the hierachy by adding all combinations. That would double the size of the lattice laws, as every instance would have a distributive copy alongside.

I'll try to come up with something better with my reformulation of laws; in case it does not go through, I'll let this issue remind us of the problem.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions