Skip to content

Comments

Implement ElemOf as an integer tag#428

Merged
isovector merged 2 commits intomasterfrom
unsafe-proof
Nov 16, 2021
Merged

Implement ElemOf as an integer tag#428
isovector merged 2 commits intomasterfrom
unsafe-proof

Conversation

@isovector
Copy link
Member

This PR implements ElemOf as an (unsafe) newtype around Int, and then does some pattern-synonym trickery to re-expose the safe Here/There constructors.

In the real world, this is a significant improvement in polysemy's code generation. When building Galley.API.Public from wireapp/wire-server#1917, this change is:

- terms: 16,086
+ terms: 13,280
- types: 7,910,353
+ types: 6,465,139
- coercions: 13,919,222
+ coercions: 13,522,063
- ppr core size: 951956810
+ ppr core size: 949201550

Fixes #427

@isovector isovector merged commit ac431a1 into master Nov 16, 2021
@isovector isovector deleted the unsafe-proof branch November 16, 2021 22:49
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.

ElemOf proofs are huge

1 participant