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.

Sign up for GitHub

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

Jump to bottom

Add Data.Constraints.Char for GHCs where it is available. #117

Closed
phadej opened this issue Aug 31, 2022 · 3 comments · Fixed by #122
Closed

Add Data.Constraints.Char for GHCs where it is available. #117

phadej opened this issue Aug 31, 2022 · 3 comments · Fixed by #122

Comments

@phadej
Copy link
Contributor

phadej commented Aug 31, 2022

No description provided.

@RyanGlScott
Copy link
Collaborator

RyanGlScott commented Aug 31, 2022 •
edited
Loading

Do you have suggestions for what operations such as module should provide? One of the main benefits of Data.Constraints.{Nat,Symbol} is that they provide useful operations that aren't expressible with the API in GHC.TypeLits. I'm not sure off the top of my head which operations would be most useful for Data.Constraints.Char to provide.

@phadej
Copy link
Contributor Author

phadej commented Aug 31, 2022 

unconsSymbol :: KnownSymbol sym :- KnownMaybe (KnownPair KnownChar KnownSymbol) (UnconsSymbol sym)
consSymbol :: ..

Though the problem is where to put KnownMaybe and KnownPair, and what they should look like.

But at least

charToNat :: KnownChar c :- KnownNat (CharToNat c)

is not problematic, and probably natToChar with additional constraint.

RyanGlScott added a commit that referenced this issue Aug 25, 2023
@RyanGlScott
Add Data.Constraint.Char
9e58eb7 
For now, this module only provides `charToNat` and `natToChar` operations, but
we may include more operations in the future.

Fixes #117.
RyanGlScott added a commit that referenced this issue Aug 25, 2023
@RyanGlScott
Add Data.Constraint.Char
d5937fc 
For now, this module only provides `charToNat` and `natToChar` operations, but
we may include more operations in the future.

Fixes #117.
@RyanGlScott RyanGlScott mentioned this issue Aug 25, 2023
Merged
@RyanGlScott
Copy link
Collaborator

I've implemented this in #122.

RyanGlScott added a commit that referenced this issue Aug 26, 2023
@RyanGlScott
Add Data.Constraint.Char
020ef78 
For now, this module only provides `charToNat` and `natToChar` operations, but
we may include more operations in the future.

Fixes #117.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Add Data.Constraint.Char ekmett/constraints
2 participants
@phadej @RyanGlScott