-
Notifications
You must be signed in to change notification settings - Fork 483
[Evaluation] Autocompute 'NumberOfStepCounters' #6798
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
[Evaluation] Autocompute 'NumberOfStepCounters' #6798
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks OK to me. It should certainly avoid the problem that we had before.
-- So that we don't need to update 'NumberOfStepCounters' manually, which would be extremely | ||
-- error-prone and has caused a bug in the past. | ||
type CountConstructorsEnum :: (GHC.Type -> GHC.Type) -> Nat | ||
type family CountConstructorsEnum rep where |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was going to suggest that we should put this somewhere else since it's not very Cek-specific, but I don't know where would be a sensible place for it. Maybe StepCounter.hs
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd like to keep it in there in case the structure of StepKind
somehow changes. Like, what if it becomes parameterized for whatever reason? Currently it's written specifically with the structure of the existing StepKind
in mind.
CountConstructorsEnum V1 = TypeError ('Text "Cannot be empty") | ||
CountConstructorsEnum (K1 _ _) = TypeError ('Text "Cannot be a non-enumeration type") | ||
CountConstructorsEnum (f :*: g) = TypeError ('Text "Cannot be a non-enumeration type") | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't understand generics or (especially) type families very well, but if I add a case for Par1
here the whole thing compiles without error. I can also remove the cases involving TypeError
and it still all works OK, presumably because they don't come into play for StepKind
. I'm not sure exactly what I'm trying to say, but I guess I'm wondering if something could change that would make this stop working (although I suppose the test should detect that kind of thing).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
OK, I've added
CountConstructorsEnum (Rec1 _ _) = TypeError ('Text "Cannot be a non-enumeration type")
CountConstructorsEnum (Par1 _ _) =
TypeError ('Text "If you really want a parameterized type, handle this clause")
It doesn't really matter, if one of those isn't handled, at worst you'll get a less readable type checking error and that's it, we don't even need the test for that.
@@ -0,0 +1 @@ | |||
9 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We can also compute this number dynamically by looking at the enumeration of StepKind
. Would it be sensible to do that, or is this safer?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great idea, I've added that test alongside the other one. Thanks!
2afae20
to
40dbaec
Compare
This makes it so that we no longer need to update
NumberOfStepCounters
, it'll be updated increased automatically when a new constructor is added toStepKind
.