Skip to content

Instantly share code, notes, and snippets.

@ekmett
Created April 3, 2021 01:48
Show Gist options
  • Save ekmett/db43c1489294876f226f61458ce27de4 to your computer and use it in GitHub Desktop.
Save ekmett/db43c1489294876f226f61458ce27de4 to your computer and use it in GitHub Desktop.
{- cabal:
build-depends: base, constraints
-}
{-# language TypeFamilies, TypeFamilyDependencies, ConstraintKinds, ScopedTypeVariables, NoStarIsType, TypeOperators, TypeApplications, GADTs, AllowAmbiguousTypes, FunctionalDependencies, UndecidableSuperClasses, UndecidableInstances, FlexibleInstances, QuantifiedConstraints, BlockArguments, RankNTypes, FlexibleContexts, StandaloneKindSignatures, DefaultSignatures #-}
-- ⊷, ≕, =∘, =◯ These choices all look like something out of Star Trek, so let's boldly go...
import Data.Constraint hiding (top, bottom, Bottom)
import Data.Kind
import Data.Some
import Data.Void
import Unsafe.Coerce
class (Not p ~ Never p) => Never p where
never :: p => Dict r
class (Prop (Not p), Not (Not p) ~ p) => Prop (p :: Constraint) where
type Not p :: Constraint
type Not p = Never p
contradiction :: (p, Not p) => Dict r
default contradiction :: (Not p ~ Never p, p, Not p) => Dict r
contradiction = never @p
instance (Prop p, Not p ~ Never p) => Prop (Never p) where
type Not (Never p) = p
contradiction = never @p
instance Prop (Bounded a)
instance Prop (Num a)
instance Never (Bounded Void) where never = absurd minBound
instance Never (Num Void) where never = absurd (fromInteger 0)
class (p, q) => p * q
instance (p, q) => p * q
class (Not p => q, Not q => p) => p ⅋ q
instance (Not p => q, Not q => p) => p ⅋ q
instance (Prop p, Prop q) => Prop (p ⅋ q) where
type Not (p ⅋ q) = Not p * Not q
contradiction = contradiction @p
instance (Prop p, Prop q) => Prop (p * q) where
type Not (p * q) = Not p ⅋ Not q
contradiction = contradiction @p
infixr 0 ⊸
type (⊸) p = (⅋) (Not p)
fun :: (Prop p, Prop q, p) => (p ⊸ q) :- q
fun = Sub Dict
contra :: (Prop p, Prop q, Not q) => (p ⊸ q) :- Not p
contra = Sub Dict
class (p, q) => p & q
instance (p, q) => p & q
class p + q where
runEither :: (p => Dict r) -> (q => Dict r) -> Dict r
data G p q k = G ((forall r. (p => Dict r) -> (q => Dict r) -> Dict r))
-- (Eq a + Ord [a]) :- Eq [a]
inl :: forall p q. p :- (p + q)
inl = Sub let
go :: (p => Dict r) -> (q => Dict r) -> Dict r
go pr _ = pr
in unsafeCoerce (G go)
inr :: forall q p. q :- (p + q)
inr = Sub let
go :: (p => Dict r) -> (q => Dict r) -> Dict r
go _ qr = qr
in unsafeCoerce (G go)
instance (Prop p, Prop q) => Prop (p & q) where
type Not (p & q) = Not p + Not q
contradiction = runEither @(Not p) @(Not q) (contradiction @p) (contradiction @q)
instance (Prop p, Prop q) => Prop (p + q) where
type Not (p + q) = Not p & Not q
contradiction = runEither @p @q (contradiction @(Not p)) (contradiction @(Not q))
withL' :: (p & q) :- p
withL' = Sub Dict
withR' :: (p & q) :- q
withR' = Sub Dict
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment