module Data.Type.Combinator.Singletons (
TC(..)
, singLength
, singSome, someSing
, singWit1, wit1Sing
, Sing(SZ, SS), SN, ZSym0, SSym0, SSym1
) where
import Data.Kind
import Data.Singletons
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Type.Boolean
import Data.Type.Conjunction
import Data.Type.Disjunction
import Data.Type.Length
import Data.Type.Option
import Data.Type.Product
import Type.Class.Higher
import Type.Class.Known
import Data.Type.Nat
import Type.Class.Witness
import Type.Family.Constraint
import Type.Family.Nat
instance SingI a => Known Sing a where
type KnownC Sing a = SingI a
known = sing
instance Witness ØC (SingI a) (Sing a) where
x \\ s = withSingI s x
instance SEq k => Eq1 (Sing :: k -> Type) where
eq1 x y = fromSing $ x %:== y
neq1 x y = fromSing $ x %:/= y
instance SOrd k => Ord1 (Sing :: k -> Type) where
compare1 x y = fromSing $ sCompare x y
x <# y = fromSing $ x %:< y
x ># y = fromSing $ x %:> y
x <=# y = fromSing $ x %:<= y
x >=# y = fromSing $ x %:>= y
genSingletons [''N]
class TC f where
fromTC :: f a -> Sing a
toTC :: Sing a -> f a
instance TC (Prod Sing) where
toTC = \case
SNil -> Ø
x `SCons` xs -> x :< toTC xs
fromTC = \case
Ø -> SNil
x :< xs -> x `SCons` fromTC xs
instance TC Boolean where
fromTC = \case
False_ -> SFalse
True_ -> STrue
toTC = \case
SFalse -> False_
STrue -> True_
instance TC Nat where
fromTC = \case
Z_ -> SZ
S_ n -> SS (fromTC n)
toTC = \case
SZ -> Z_
SS n -> S_ (toTC n)
instance TC (Sing :*: Sing) where
fromTC (x :*: y) = STuple2 x y
toTC (STuple2 x y) = x :*: y
instance TC (Sing :+: Sing) where
fromTC = \case
L' x -> SLeft x
R' x -> SRight x
toTC = \case
SLeft x -> L' x
SRight x -> R' x
instance TC (Option Sing) where
fromTC = \case
Nothing_ -> SNothing
Just_ x -> SJust x
toTC = \case
SNothing -> Nothing_
SJust x -> Just_ x
singLength :: Sing as -> Length as
singLength = \case
SNil -> LZ
_ `SCons` xs -> LS (singLength xs)
singSome :: SomeSing k -> Some (Sing :: k -> Type)
singSome (SomeSing s) = Some s
someSing :: Some (Sing :: k -> Type) -> SomeSing k
someSing ss = some ss SomeSing
singWit1 :: SingInstance a -> Wit1 SingI a
singWit1 SingInstance = Wit1
wit1Sing :: Wit1 SingI a -> SingInstance a
wit1Sing Wit1 = SingInstance