id: 61d6aa79b16e4c1e80bb30fc0f942742
parent_id: 8665e8be71204bc98f2f75665d09e145
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1696252040915
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"??)\\\n  - \"],[1,\"Polymorphic lightweight guards (g?)\\\n  - Polymorphic featherweight guards (g??)\\\n  - Polymorphic cover tags (t@)\\\n  - Polymorphic cover guards (g@)\\\n \\\nThe cover encodings allow us to omit some type arguments (i.e. cons(b, X, Xs) becomes cons(X, Xs)) in exchange for more protectors (i.e. cons(A, X, Xs) becomes cons(t(A, X), Xs)) in other places.\\\n \\\n As for the results: occasionally, the lightweight/featherweight tags and guards come out on top, and they are certainly much better than t and g, but it surprises me how competitive e (full type erasure) and a (type annotation) are for monomorphic and polymorphic problems, respectively.\\\n \\\n Like, E is able to prove 361 polymorphic problems with a, and only 347/344 with t?? and g??. `a` comes out on top in 3 out of 5 provers in the polymorphic case... In the monomorphic case, `e` never wins, but it is surprisingly competitive; Z3: 354 vs 355, E: 393 vs 401, Vampire: 393 vs 403... \"],[0,\"\\\n\\\n## Arc\"]],\"start1\":11866,\"start2\":11866,\"length1\":16,\"length2\":947}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-02T13:07:23.414Z
created_time: 2023-10-02T13:07:23.414Z
type_: 13