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

Removed _|_ as a built in declaration and renamed it to Void #1619

Merged
merged 2 commits into from
Oct 14, 2014
Merged

Removed _|_ as a built in declaration and renamed it to Void #1619

merged 2 commits into from
Oct 14, 2014

Conversation

ahmadsalim
Copy link

FalseElim now void to match up.
This is in line with (and concludes) the #1516 renaming effort.

@ahmadsalim
Copy link
Author

The choice of renaming FalseElim to void was suggested by @Melvar (thanks!).
I believe it lines up well with the list and either functions that do the same for the (in order) List and Either datatypes.
Perhaps, boolElim should rather be just bool.

@ahmadsalim ahmadsalim changed the title Removed '_|_' as a built in declaration and renamed it to 'Void' Removed _|_ as a built in declaration and renamed it to Void Oct 11, 2014
@david-christiansen
Copy link
Contributor

Out of curiosity, why not do something like

class Uninhabited a where
  uninhabited : a -> Void
  absurd : a -> b
  absurd x = (elim_for Builtins.Void) (uninhabited x)

instance Uninhabited Void where
  uninhabited = id

This completely avoids needing to name the eliminator, and it shepherds users towards absurd, which IMHO makes easier-to-read programs.

@edwinb
Copy link
Contributor

edwinb commented Oct 12, 2014

Is this also updated in the tutorials? I'll merge if so. Once this is done, I'll get a new release together.

@ahmadsalim
Copy link
Author

@david-christiansen I actually thought of that, but I was unsure if I should have taken a big semantics altering decision like that, especially since errors are reported differently when type class resolution is performed. So I chose to do a conservative change with only renaming, although I definitely think that absurd is the way to go for most cases.

@edwinb No, not yet. I will get on it soon.

@david-christiansen
Copy link
Contributor

That makes sense. Thanks for doing all this!

@ahmadsalim
Copy link
Author

OK, the tutorials are updated now.

edwinb added a commit that referenced this pull request Oct 14, 2014
Removed `_|_` as a built in declaration and renamed it to `Void`
@edwinb edwinb merged commit e890280 into idris-lang:master Oct 14, 2014
@ahmadsalim ahmadsalim deleted the feature/renamevoid branch October 14, 2014 10:25
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.

3 participants