Promoting and Demoting All Sorts of Stuff

Lies.hs

{-# Language RankNTypes #-}
{-# Language PolyKinds #-}
{-# Language DataKinds #-}
{-# Language PatternSynonyms #-}
{-# Language DerivingStrategies #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language ViewPatterns #-}
{-# Language RoleAnnotations #-}
{-# Language StandaloneKindSignatures #-}
{-# Language ConstraintKinds #-}
{-# Language QuantifiedConstraints #-}
{-# Language LambdaCase #-}
{-# Language EmptyCase #-}
{-# Language NPlusKPatterns #-}
{-# Language TypeFamilies #-}
{-# Language UndecidableInstances #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language FlexibleInstances #-}
{-# Language FlexibleContexts #-}
{-# Language TypeApplications #-}
{-# Language AllowAmbiguousTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language TemplateHaskell #-}

module Lies where

import Control.Exception
import Data.Function
import Data.Kind
import Data.Proxy
import Data.Type.Equality
import Data.Void
import GHC.Exts
import GHC.TypeNats as TN
import GHC.TypeLits as TL
import Numeric.Natural
import Text.Read hiding (Symbol)
import Text.Show.Deriving
import Type.Reflection
import Unsafe.Coerce

type Z = 0
type S n = 1+n

--------------------------------------------------------------------------------
-- * Singletons
--------------------------------------------------------------------------------

class SingKind k where
  type Sing :: k -> Type
  fromSing :: Sing (a :: k) -> k

class SingI (a :: k) where
  sing :: Sing a

type GSingKind :: forall i. (i -> Type) -> Constraint
type GSingKind k = forall x. SingKind (k x)

type SingKind1 :: (Type -> Type) -> Constraint
type SingKind1 k = forall x. SingKind x => SingKind (k x)

type SingKind2 :: (Type -> Type -> Type) -> Constraint
type SingKind2 k = forall x y. (SingKind x, SingKind y) => SingKind (k x y)

--------------------------------------------------------------------------------
-- * Lifting Types
--------------------------------------------------------------------------------
--
instance SingKind Type where
  type Sing = TypeRep
  fromSing _ = error "lowered type"

instance Typeable a => SingI (a :: Type) where
  sing = typeRep

--------------------------------------------------------------------------------
-- * Lowering Nats
--
-- (let's make up a value rep for Nat til we get Nat=Natural in base)
--------------------------------------------------------------------------------

instance SingKind Nat where
  type Sing = SNat
  fromSing = unsafeCoerce

instance KnownNat a => SingI a where
  sing = UnsafeSNat $ TN.natVal (Proxy @a)

newtype SNat (n :: Nat) = UnsafeSNat { snatVal :: Natural }
  deriving newtype (Eq, Show)

instance TestEquality SNat where
  testEquality i j
    | snatVal i == snatVal j = Just (unsafeCoerce Refl)
    | otherwise = Nothing

instance Show Nat where
  showsPrec d = showsPrec d . fromNat

instance Eq Nat where
  (==) = (==) `on` fromNat

instance Ord Nat where
  compare = compare `on` fromNat

instance Read Nat where
  readPrec = Nat <$> readPrec

toNat :: Natural -> Nat
toNat = unsafeCoerce

fromNat :: Nat -> Natural
fromNat = unsafeCoerce

liftN2 :: (Natural -> Natural -> Natural) -> Nat -> Nat -> Nat
liftN2 f x y = toNat $ f (fromNat x) (fromNat y)

liftN :: (Natural -> Natural) -> Nat -> Nat
liftN f = toNat . f . fromNat

instance Num Nat where
  (+) = liftN2 (+)
  (-) = liftN2 (-)
  (*) = liftN2 (*)
  abs = liftN abs
  signum = liftN signum
  negate = liftN negate
  fromInteger = toNat . fromInteger

instance Enum Nat where
  succ = liftN succ
  pred = liftN pred
  toEnum = Nat . toEnum
  fromEnum = fromEnum . fromNat
  enumFrom = fmap Nat . enumFrom . fromNat
  enumFromTo (Nat n) (Nat m) = Nat <$> enumFromTo n m
  enumFromThen (Nat n) (Nat m) = Nat <$> enumFromThen n m
  enumFromThenTo (Nat n) (Nat m) (Nat o) = Nat <$> enumFromThenTo n m o

instance Real Nat where
  toRational = toRational . fromNat

instance Integral Nat where
  quot = liftN2 quot
  rem = liftN2 rem
  div = liftN2 rem
  mod = liftN2 rem
  quotRem (Nat n) (Nat m) = case quotRem n m of
    (q,r) -> (Nat q, Nat r)
  divMod (Nat n) (Nat m) = case divMod n m of
    (q,r) -> (Nat q, Nat r)
  toInteger = toInteger . fromNat

pattern Nat :: Natural -> Nat
pattern Nat n <- (fromNat -> n) where
  Nat n = toNat n

{-# complete Nat #-}

pattern Z :: Nat
pattern Z = Nat 0

safePred :: Natural -> Maybe Natural
safePred 0 = Nothing
safePred n = Just (n-1)

pattern S :: Nat -> Nat
pattern S n <- (safePred . fromNat -> Just (toNat -> n)) where
  S n = toNat (fromNat n + 1)

{-# complete Z, S #-}

--------------------------------------------------------------------------------
-- * Units
--------------------------------------------------------------------------------

type SUnit :: () -> Type
type role SUnit nominal
data SUnit a where
  SUnit :: SUnit '()

deriveShow ''SUnit

instance SingKind () where
  type Sing = SUnit
  fromSing SUnit = ()

instance SingI '() where
  sing = SUnit

instance TestEquality SUnit where
  testEquality SUnit SUnit = Just Refl

--------------------------------------------------------------------------------
-- * Void
--------------------------------------------------------------------------------

type SVoid :: Void -> Type
type role SVoid nominal
data SVoid a

deriveShow ''SVoid

instance SingKind Void where
  type Sing = SVoid
  fromSing = \case

instance TestEquality SVoid where
  testEquality = \case

--------------------------------------------------------------------------------
-- * Lifting Ints
--------------------------------------------------------------------------------

data family FromNat :: Nat -> k

type MkInt :: Nat -> Int
type MkInt = FromNat

type SInt :: Int -> Type
type role SInt nominal
newtype SInt n = UnsafeSInt { fromSInt :: Int }
  deriving newtype Show

instance SingKind Int where
  type Sing = SInt
  fromSing = fromSInt

instance KnownNat n => SingI (MkInt n) where
  sing
    | n > fromIntegral (maxBound @Word) = throw Overflow
    | otherwise = UnsafeSInt $ fromIntegral n
    where n = TL.natVal $ Proxy @n

instance TestEquality SInt where
  testEquality i j
    | fromSInt i == fromSInt j = Just (unsafeCoerce Refl)
    | otherwise = Nothing

data SInt' (n :: Int) where
  SZ' :: SInt' (MkInt Z)
  SS' :: SInt (MkInt i) -> SInt' (MkInt (S i))

upSInt :: SInt n -> SInt' n
upSInt (UnsafeSInt 0) = unsafeCoerce SZ'
upSInt (UnsafeSInt n) = unsafeCoerce $ SS' (UnsafeSInt (n-1))

pattern SZ :: () => (n ~ MkInt Z) => SInt n
pattern SZ <- (upSInt -> SZ') where
  SZ = UnsafeSInt 0

pattern SS :: () => (i ~ MkInt i', j ~ MkInt (S i')) => SInt i -> SInt j
pattern SS n <- (upSInt -> SS' n) where
  SS n = UnsafeSInt $ succ $ fromSInt n

{-# complete SS, SZ #-}

--------------------------------------------------------------------------------
-- * Lifting Char
--------------------------------------------------------------------------------

data family FromSymbol :: Symbol -> k

type MkChar :: Symbol -> Char
type MkChar = FromSymbol

type SChar :: Char -> Type
type role SChar nominal
newtype SChar n = UnsafeSChar { fromSChar :: Char }
  deriving newtype Show

instance SingKind Char where
  type Sing = SChar
  fromSing = fromSChar

instance KnownSymbol s => SingI (MkChar s) where
  sing = case symbolVal $ Proxy @s of
    [c] -> UnsafeSChar c
    _ -> error "SChar.sing: bad argument"

instance TestEquality SChar where
  testEquality i j
    | fromSChar i == fromSChar j = Just (unsafeCoerce Refl)
    | otherwise = Nothing

--------------------------------------------------------------------------------
-- * Lowering Symbol
--------------------------------------------------------------------------------

instance SingKind Symbol where
  type Sing = SSymbol
  fromSing = unsafeCoerce

toSymbol :: String -> Symbol
toSymbol = unsafeCoerce

fromSymbol :: Symbol -> String
fromSymbol = unsafeCoerce

pattern Symbol :: String -> Symbol
pattern Symbol s <- (fromSymbol -> s) where
  Symbol s = toSymbol s

{-# Complete Symbol #-}

instance Eq Symbol where
  (==) = (==) `on` fromSymbol

instance Ord Symbol where
  compare = compare `on` fromSymbol

instance Show Symbol where
  showsPrec d = showsPrec d . fromSymbol

instance Read Symbol where
  readPrec = Symbol <$> readPrec

instance IsList Symbol where
  type Item Symbol = Char
  fromList = Symbol . fromList 
  fromListN n xs = Symbol (fromListN n xs)
  toList = toList . fromSymbol

instance IsString Symbol where
  fromString = toSymbol

type SSymbol :: Symbol -> Type
type role SSymbol nominal
newtype SSymbol n = UnsafeSSymbol { fromSSymbol :: String }
  deriving newtype Show

instance TestEquality SSymbol where
  testEquality i j
    | fromSSymbol i == fromSSymbol j = Just (unsafeCoerce Refl)
    | otherwise = Nothing

instance KnownSymbol s => SingI s where
  sing = UnsafeSSymbol $ symbolVal $ Proxy @s

--------------------------------------------------------------------------------
-- * Lifting Lists
--------------------------------------------------------------------------------

type SList :: forall a. [a] -> Type
type role SList nominal
data SList a where
  SNil  :: SList '[]
  SCons :: Sing a -> Sing as -> SList (a ': as)

instance SingKind a => SingKind [a] where
  type Sing = SList
  fromSing SNil = []
  fromSing (SCons a as) = fromSing a : fromSing as

instance SingI '[] where
  sing = SNil

instance (SingI a, SingI as) => SingI (a ': as) where
  sing = SCons sing sing

instance Show (SList '[]) where
  showsPrec _ SNil = showString "SNil"

instance (Show (Sing a), Show (SList as)) => Show (SList (a ': as)) where
  showsPrec d (SCons a as) = showParen (d > 10) $
    showString "SCons " . showsPrec 11 a . showChar ' ' . showsPrec 11 as

--------------------------------------------------------------------------------
-- * Lifting Maybe
--------------------------------------------------------------------------------

type SMaybe :: forall a. Maybe a -> Type
type role SMaybe nominal
data SMaybe a where
  SNothing :: SMaybe 'Nothing
  SJust    :: Sing a -> SMaybe ('Just a)

instance SingKind i => SingKind (Maybe i) where
  type Sing = SMaybe
  fromSing SNothing = Nothing
  fromSing (SJust a) = Just (fromSing a)

instance SingI 'Nothing where
  sing = SNothing

instance SingI a => SingI ('Just a) where
  sing = SJust sing

instance Show (SMaybe 'Nothing) where
  showsPrec _ SNothing = showString "SNothing"

instance Show a => Show (SMaybe ('Just a)) where
  showsPrec d (SJust a) = showParen (d > 10 ) $
    showString "SJust " . showsPrec 11 a

--------------------------------------------------------------------------------
-- * Lifting Products
--------------------------------------------------------------------------------

type SPair :: forall a b. (a,b) -> Type
type role SPair nominal
data SPair t where
  SPair :: Sing a -> Sing b -> SPair '(a, b)

instance (SingKind i, SingKind j) => SingKind (i, j) where
  type Sing = SPair
  fromSing (SPair a b) = (fromSing a, fromSing b)

instance (SingI a, SingI b) => SingI '(a, b) where
  sing = SPair sing sing

instance (Show a, Show b) => Show (SPair '(a,b)) where
  showsPrec d (SPair a b) = showParen (d > 10) $
    showString "SPair " . showsPrec 11 a . showChar ' ' . showsPrec 11 b

--------------------------------------------------------------------------------
-- * Lifting Booleans
--------------------------------------------------------------------------------

type SBool :: Bool -> Type
type role SBool nominal
data SBool t where
  SFalse :: SBool 'False
  STrue :: SBool 'True

deriveShow ''SBool

instance SingKind Bool where
  type Sing = SBool
  fromSing SFalse = False
  fromSing STrue = True

instance SingI 'True where
  sing = STrue

instance SingI 'False where
  sing = SFalse

instance TestEquality SBool where
  testEquality SFalse SFalse = Just Refl
  testEquality STrue STrue = Just Refl
  testEquality _ _ = Nothing

--------------------------------------------------------------------------------
-- * Lifting Ordering
--------------------------------------------------------------------------------

type SOrdering :: Ordering -> Type
type role SOrdering nominal
data SOrdering t where
  SLT :: SOrdering 'LT
  SEQ :: SOrdering 'EQ
  SGT :: SOrdering 'GT

deriveShow ''SOrdering

instance SingKind Ordering where
  type Sing = SOrdering
  fromSing SLT = LT
  fromSing SEQ = EQ
  fromSing SGT = GT

instance TestEquality SOrdering where
  testEquality SLT SLT = Just Refl
  testEquality SEQ SEQ = Just Refl
  testEquality SGT SGT = Just Refl
  testEquality _ _ = Nothing

instance SingI 'LT where sing = SLT
instance SingI 'EQ where sing = SEQ
instance SingI 'GT where sing = SGT

--------------------------------------------------------------------------------
-- * Lifting Either
--------------------------------------------------------------------------------

type SEither :: forall a b. Either a b -> Type
type role SEither nominal
data SEither t where
  SLeft :: Sing a -> SEither ('Left a)
  SRight :: Sing b -> SEither ('Right b)

instance Show (Sing a) => Show (SEither ('Left a)) where
  showsPrec d (SLeft a) = showParen (d > 10) $
    showString "SLeft " . showsPrec 11 a

instance Show (Sing b) => Show (SEither ('Right b)) where
  showsPrec d (SRight b) = showParen (d > 10) $
    showString "SRight " . showsPrec 11 b

instance (SingKind i, SingKind j) => SingKind (Either i j) where
  type Sing = SEither
  fromSing (SLeft a)  = Left (fromSing a)
  fromSing (SRight a) = Right (fromSing a)

instance SingI a => SingI ('Left a) where
  sing = SLeft sing

instance SingI b => SingI ('Right b) where
  sing = SRight sing