affine-logic-in-constraints.hs

{- 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