diff --git a/src/convert.rs b/src/convert.rs index 17cdc5f..8c37c49 100644 --- a/src/convert.rs +++ b/src/convert.rs @@ -26,79 +26,22 @@ pub const fn infallible_to_never(infallible: Infallible) -> ! { infallible_elim(infallible) } -/// The bottom type ⊥ with no elements. Since it has no elements, having an element of `Bot` is an -/// inherent contradiction and it can therefore be converted to any other type. In MLTT, this -/// corresponds to a proof by contradiction. -/// -/// `Bot` serves the same purpose as `std::convert::Infallible` and the currently unstable "never" -/// type `!`, but provides more convenience methods than the former. -pub struct Bot(BotRepr); - -impl Bot { - #[inline] - #[must_use] - pub const fn elim(self) -> T { - self.0.elim() - } +pub trait Empty: Sized { + fn elim(self) -> T; #[inline] - #[must_use] - pub const fn elim_ref(&self) -> T { - self.0.elim() - } - - #[inline] - pub const fn never(self) -> ! { + fn never(self) -> ! { self.elim() } } -impl Clone for Bot { +impl Empty for Infallible { #[inline] - fn clone(&self) -> Self { - self.elim_ref() + fn elim(self) -> T { + infallible_elim(self) } } -impl Copy for Bot {} - -impl From for Bot { - #[inline] - fn from(infallible: Infallible) -> Self { - infallible_elim(infallible) - } -} - -impl From for Infallible { - #[inline] - fn from(bot: Bot) -> Self { - bot.elim() - } -} - -enum BotRepr {} - -impl BotRepr { - #[inline] - const fn elim(self) -> T { - match self {} - } - - #[inline] - const fn elim_ref(&self) -> T { - match *self {} - } -} - -impl Clone for BotRepr { - #[inline] - fn clone(&self) -> Self { - self.elim_ref() - } -} - -impl Copy for BotRepr {} - #[inline] #[must_use] pub fn clone(x: &T) -> T { diff --git a/src/either.rs b/src/either.rs index 6147957..b7137d8 100644 --- a/src/either.rs +++ b/src/either.rs @@ -1,7 +1,12 @@ -use std::{convert::identity, hint, ops::{Deref, DerefMut}}; +use std::{ + convert::identity, + hint, + ops::{Deref, DerefMut} +}; use Either::{Inl, Inr}; -use crate::convert::{clone, clone_mut, copy, copy_mut}; +use crate::convert::{clone, clone_mut, copy, copy_mut, Empty}; + pub enum Either { Inl(L), Inr(R), @@ -174,6 +179,24 @@ impl Either { self.fold(Inr, Inl) } + #[inline] + #[must_use] + pub fn elim_l(self) -> R + where + L: Empty, + { + self.fold_l(::elim) + } + + #[inline] + #[must_use] + pub fn elim_r(self) -> L + where + R: Empty, + { + self.fold_r(::elim) + } + #[inline] #[must_use] pub fn some_l(self) -> Option { @@ -489,19 +512,17 @@ impl Either { } } -impl Clone for Either -where - L: Clone, - R: Clone, -{ +impl Empty for Either { + fn elim(self) -> T { + self.fold(::elim, ::elim) + } +} + +impl Clone for Either { #[inline] fn clone(&self) -> Self { self.as_ref().map(::clone, ::clone) } } -impl Copy for Either -where - L: Copy, - R: Copy, -{} +impl Copy for Either {}