Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Decidable and Divisible instances for Size #118

Open
lambda-fairy opened this issue Sep 14, 2017 · 1 comment
Open

Decidable and Divisible instances for Size #118

lambda-fairy opened this issue Sep 14, 2017 · 1 comment

Comments

@lambda-fairy
Copy link

lambda-fairy commented Sep 14, 2017

The Size type can implement Divisible:

instance Divisible Size where
    divide f = combineSizeWith (fst . f) (snd . f)
    conquer = ConstSize 0

I think it can implement Decidable as well, though I'm not sure if my code is correct (or useful):

instance Decidable Size where
    choose f s t = VarSize (either (getSizeWith s) (getSizeWith t) . f)
    lose f = VarSize (absurd . f)
@mgsloan
Copy link
Owner

mgsloan commented Sep 15, 2017

Interesting! Seems potentially useful, feel free to open a PR. I think the Decidable instance could be useful, for computing the size of the encoding of a sum type.

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

No branches or pull requests

2 participants