Unification benchmark using 'map' and 'stream' #798
+196
−4
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This comment was marked as resolved.
This comment was marked as resolved.
|
Here's a slightly minified version: /// Robinson-style Unification Algorithm
module examples/benchmarks/unify
import map
import result
import bytearray
type Type {
Var(name: String)
Con(name: String, args: List[Type])
}
type Substitution = Map[String, Type]
type UnificationError {
OccursCheckFailure(variable: String, tpe: Type)
UnificationFailure(tpe1: Type, tpe2: Type)
UnificationManyFailure(tps1: List[Type], tps2: List[Type])
}
def showType(ty: Type): String = ty match {
case Var(name) => name
case Con(name, Nil()) => name
case Con(name, args) =>
name ++ "(" ++ args.map { t => showType(t) }.join(", ") ++ ")"
}
def show(err: UnificationError): String = err match {
case OccursCheckFailure(variable, ty) =>
"Occurs check failed: " ++ variable ++ " occurs in " ++ showType(ty)
case UnificationFailure(ty1, ty2) =>
"Cannot unify " ++ showType(ty1) ++ " with " ++ showType(ty2)
case UnificationManyFailure(tps1, tps2) =>
"Cannot unify " ++ tps2.map { t => showType(t) }.join(", ") ++ " with " ++ tps1.map { t => showType(t) }.join(", ")
}
def reporting { body : => Substitution / Exception[UnificationError] }: Unit = {
val res = result[Substitution, UnificationError] {
body()
}
res match {
case Success(subst) => {
println("Unification successful!")
println("Substitution:")
subst.foreach { (k, v) =>
println(" " ++ k ++ " -> " ++ showType(v))
}
}
case Error(err, msg) =>
println("Unification failed: " ++ show(err))
if (msg.length > 0) {
println(msg)
}
}
}
def main() = reporting {
val intType = Con("Int", [])
val listType = Con("List", [intType])
val typeVar = Var("a")
do raise(UnificationManyFailure([intType], [listType, typeVar]), "")
}seems to crash the normaliser! When I do |
jiribenes
commented
Jan 23, 2025
jiribenes
commented
Jan 23, 2025
Co-authored-by: Jonathan Brachthäuser <[email protected]>
jiribenes
commented
Jan 23, 2025
effekt/shared/src/main/scala/effekt/core/optimizer/Normalizer.scala
Outdated
Show resolved
Hide resolved
jiribenes
changed the title
jiribenes
commented
Jan 23, 2025
jiribenes
commented
Jan 23, 2025
Comment on lines
+159
to
+160
| // the actual test | ||
| val N = 12 |
There was a problem hiding this comment.
N = 12 means unification of two trees of depth 12, i.e. tree of tuples with 2^12 = 4096 variables in the leaves.
We can tweak this number or even use the benchmarks/runner...
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Resolves #796
It's an OK (not great, not terrible) benchmark:
(...((XLLL, XLLR), (XLRL, XLRR)), ...forX = { A, B },ALLL -> BLLL.Configurable with a given
Nif some tweaking is needed.Perf:
My machine
On my computer with
N = 12:On my computer with
N = 16(16x more work thanN = 12)CI
With
N = 12in CI (measured imprecisely in two CI rounds):With
N = 16in CI (measured imprecisely in two CI rounds):