{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Data.Type.Sing where import Data.Bifunctor import Data.Kind import Data.Singletons import Data.Singletons.Prelude.List hiding (Length, Reverse, sReverse, Head, (%:++), Replicate) import Data.Type.Index import Data.Type.Length import Data.Type.Nat import Data.Type.Product import Data.Type.Uniform import Type.Class.Known import Type.Class.Witness import Type.Family.Constraint import Type.Family.List import Type.Family.List.Util import Type.Family.Nat instance Witness ØC (SingI a) (Sing a) where q \\ s = withSingI s q singLength :: Sing ns -> Length ns singLength = \case SNil -> LZ _ `SCons` s -> LS (singLength s) singProd :: Sing as -> Prod Sing as singProd = \case SNil -> Ø s `SCons` ss -> s :< singProd ss prodSing :: Prod Sing as -> Sing as prodSing = \case Ø -> SNil s :< ss -> s `SCons` prodSing ss splitSing :: Length ns -> Sing (ns ++ ms) -> (Sing ns, Sing ms) splitSing = \case LZ -> \ss -> (SNil, ss) LS l -> \case s `SCons` ss -> first (s `SCons`) (splitSing l ss) takeSing :: Length ns -> Length ms -> Sing (ns ++ ms) -> Sing ns takeSing = \case LZ -> \_ _ -> SNil LS l -> \lM -> \case s `SCons` ss -> s `SCons` takeSing l lM ss singProdNat :: forall (as :: [N]). () => Sing as -> Prod Nat as singProdNat = \case SNil -> Ø (SN n) `SCons` ns -> n :< singProdNat ns data instance Sing (n :: N) where SN :: { getNat :: !(Nat n) } -> Sing n instance Known Nat a => SingI (a :: N) where sing = SN known entailNat :: forall n. (SingI n :- Known Nat n) entailNat = Sub $ case (sing :: Sing n) of SN n -> Wit \\ n singSings :: forall ns. () => SingI ns :- ListC (SingI <$> ns) singSings = Sub (witSings (sing :: Sing ns)) witSings :: forall ns. () => Sing ns -> Wit (ListC (SingI <$> ns)) witSings = \case SNil -> Wit s `SCons` ss -> case witSings ss of Wit -> withSingI s Wit entailEvery :: forall (as :: [k]) (f :: k -> Constraint). () => (forall (a :: k). SingI a :- f a) -> (SingI as :- Every f as) entailEvery e = Sub (go (sing :: Sing as)) where go :: forall bs. () => Sing bs -> Wit (Every f bs) go = \case SNil -> Wit s `SCons` ss -> case go ss of Wit -> withSingI s (Wit \\ (e :: SingI (Head bs) :- f (Head bs))) singUniform :: Uniform a (b ': bs) -> (SingI b :- SingI a) singUniform = \case US _ -> Sub Wit entailSing :: forall a b. () => (Sing a -> Sing b) -> (SingI a :- SingI b) entailSing f = Sub $ withSingI (f (sing :: Sing a)) Wit entailSing2 :: forall a b c. () => (Sing a -> Sing b -> Sing c) -> ((SingI a, SingI b) :- SingI c) entailSing2 f = Sub $ withSingI (f (sing :: Sing a) (sing :: Sing b)) Wit singWit :: forall a p q t. (p, Witness p q t) => (Sing a -> t) -> (SingI a :- q) singWit f = Sub $ Wit \\ f (sing :: Sing a) infixr 5 %:++ (%:++) :: Sing as -> Sing bs -> Sing (as ++ bs) (%:++) = \case SNil -> id x `SCons` xs -> \ys -> x `SCons` (xs %:++ ys) sReverse :: Sing as -> Sing (Reverse as) sReverse = \case SNil -> SNil x `SCons` xs -> sReverse xs `sSnoc` x sSnoc :: Sing as -> Sing a -> Sing (as >: a) sSnoc = \case SNil -> (`SCons` SNil) x `SCons` xs -> (x `SCons`) . (xs `sSnoc`) sOnly :: Sing a -> Sing '[a] sOnly = (`SCons` SNil) replicateSing :: Sing a -> Nat n -> Sing (Replicate n a) replicateSing s = \case Z_ -> SNil S_ n -> s `SCons` replicateSing s n