{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MagicHash #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Singletons -- Copyright : (C) 2013 Richard Eisenberg -- License : BSD-style (see LICENSE) -- Maintainer : Ryan Scott -- Stability : experimental -- Portability : non-portable -- -- This module exports the basic definitions to use singletons. For routine -- use, consider importing 'Data.Singletons.Prelude', which exports constructors -- for singletons based on types in the @Prelude@. -- -- You may also want to read -- the original papers presenting this library, available at -- -- and . -- ---------------------------------------------------------------------------- module Data.Singletons ( -- * Main singleton definitions Sing, SLambda(..), (@@), SingI(..), SingKind(..), -- * Working with singletons KindOf, SameKind, SingInstance(..), SomeSing(..), singInstance, pattern Sing, withSingI, withSomeSing, pattern FromSing, singByProxy, demote, singByProxy#, withSing, singThat, -- ** @WrappedSing@ WrappedSing(..), SWrappedSing(..), UnwrapSing, -- $SingletonsOfSingletons -- ** Defunctionalization TyFun, type (~>), TyCon1, TyCon2, TyCon3, TyCon4, TyCon5, TyCon6, TyCon7, TyCon8, TyCon, Apply, type (@@), -- ** Defunctionalized singletons -- | When calling a higher-order singleton function, you need to use a -- @singFun...@ function to wrap it. See 'singFun1'. singFun1, singFun2, singFun3, singFun4, singFun5, singFun6, singFun7, singFun8, unSingFun1, unSingFun2, unSingFun3, unSingFun4, unSingFun5, unSingFun6, unSingFun7, unSingFun8, -- $SLambdaPatternSynonyms pattern SLambda2, pattern SLambda3, pattern SLambda4, pattern SLambda5, pattern SLambda6, pattern SLambda7, pattern SLambda8, -- | These type synonyms are exported only to improve error messages; users -- should not have to mention them. SingFunction1, SingFunction2, SingFunction3, SingFunction4, SingFunction5, SingFunction6, SingFunction7, SingFunction8, -- * Auxiliary functions Proxy(..), -- * Defunctionalization symbols DemoteSym0, DemoteSym1, SameKindSym0, SameKindSym1, SameKindSym2, KindOfSym0, KindOfSym1, type (~>@#@$), type (~>@#@$$), type (~>@#@$$$), ApplySym0, ApplySym1, ApplySym2, type (@@@#@$), type (@@@#@$$), type (@@@#@$$$) ) where import Data.Singletons.Internal import Data.Singletons.Prelude.Enum import Data.Singletons.Prelude.Eq import Data.Singletons.Prelude.Instances import Data.Singletons.Prelude.IsString import Data.Singletons.Prelude.Monoid import Data.Singletons.Prelude.Num import Data.Singletons.Prelude.Ord import Data.Singletons.Prelude.Semigroup import Data.Singletons.Promote import Data.Singletons.ShowSing import Data.Singletons.Single (singITyConInstances) import Data.String import qualified Data.Text as T (pack) ---------------------------------------------------------------------- ---- SingI TyCon{N} instances ---------------------------------------- ---------------------------------------------------------------------- {- Generates SingI instances for TyCon1 through TyCon8: instance (forall a. SingI a => SingI (f a), ...) => SingI (TyCon1 f) instance (forall a b. (SingI a, SingI b) => SingI (f a b), ...) => SingI (TyCon2 f) ... -} $(singITyConInstances [1..8]) ---------------------------------------------------------------------- ---- SomeSing instances ---------------------------------------------- ---------------------------------------------------------------------- instance SEq k => Eq (SomeSing k) where SomeSing a == SomeSing b = fromSing (a %== b) SomeSing a /= SomeSing b = fromSing (a %/= b) instance SOrd k => Ord (SomeSing k) where SomeSing a `compare` SomeSing b = fromSing (a `sCompare` b) SomeSing a < SomeSing b = fromSing (a %< b) SomeSing a <= SomeSing b = fromSing (a %<= b) SomeSing a > SomeSing b = fromSing (a %> b) SomeSing a >= SomeSing b = fromSing (a %>= b) instance SBounded k => Bounded (SomeSing k) where minBound = SomeSing sMinBound maxBound = SomeSing sMaxBound instance SEnum k => Enum (SomeSing k) where succ (SomeSing a) = SomeSing (sSucc a) pred (SomeSing a) = SomeSing (sPred a) toEnum n = withSomeSing (fromIntegral n) (SomeSing . sToEnum) fromEnum (SomeSing a) = fromIntegral (fromSing (sFromEnum a)) enumFromTo (SomeSing from) (SomeSing to) = listFromSingShallow (sEnumFromTo from to) enumFromThenTo (SomeSing from) (SomeSing then_) (SomeSing to) = listFromSingShallow (sEnumFromThenTo from then_ to) -- Like the 'fromSing' implementation for lists, but bottoms out at -- 'SomeSing' instead of recursively invoking 'fromSing'. listFromSingShallow :: SList (x :: [a]) -> [SomeSing a] listFromSingShallow SNil = [] listFromSingShallow (SCons x xs) = SomeSing x : listFromSingShallow xs instance SNum k => Num (SomeSing k) where SomeSing a + SomeSing b = SomeSing (a %+ b) SomeSing a - SomeSing b = SomeSing (a %- b) SomeSing a * SomeSing b = SomeSing (a %* b) negate (SomeSing a) = SomeSing (sNegate a) abs (SomeSing a) = SomeSing (sAbs a) signum (SomeSing a) = SomeSing (sSignum a) fromInteger n = withSomeSing (fromIntegral n) (SomeSing . sFromInteger) instance ShowSing k => Show (SomeSing k) where showsPrec p (SomeSing (s :: Sing a)) = showParen (p > 10) $ showString "SomeSing " . showsPrec 11 s :: ShowSing' a => ShowS instance SSemigroup k => Semigroup (SomeSing k) where SomeSing a <> SomeSing b = SomeSing (a %<> b) instance SMonoid k => Monoid (SomeSing k) where mempty = SomeSing sMempty instance SIsString k => IsString (SomeSing k) where fromString s = withSomeSing (T.pack s) (SomeSing . sFromString) ---------------------------------------------------------------------- ---- Defunctionalization symbols ------------------------------------- ---------------------------------------------------------------------- $(genDefunSymbols [''Demote, ''SameKind, ''KindOf, ''(~>), ''Apply, ''(@@)]) -- WrapSing, UnwrapSing, and SingFunction1 et al. are not defunctionalizable -- at the moment due to Trac #9269 {- $SingletonsOfSingletons Aside from being a data type to hang instances off of, 'WrappedSing' has another purpose as a general-purpose mechanism for allowing one to write code that uses singletons of other singletons. For instance, suppose you had the following data type: @ data T :: Type -> Type where MkT :: forall a (x :: a). 'Sing' x -> F a -> T a @ A naïve attempt at defining a singleton for @T@ would look something like this: @ data ST :: forall a. T a -> Type where SMkT :: forall a (x :: a) (sx :: 'Sing' x) (f :: F a). 'Sing' sx -> 'Sing' f -> ST (MkT sx f) @ But there is a problem here: what exactly /is/ @'Sing' sx@? If @x@ were 'True', for instance, then @sx@ would be 'STrue', but it's not clear what @'Sing' 'STrue'@ should be. One could define @SSBool@ to be the singleton of 'SBool's, but in order to be thorough, one would have to generate a singleton for /every/ singleton type out there. Plus, it's not clear when to stop. Should we also generate @SSSBool@, @SSSSBool@, etc.? Instead, 'WrappedSing' and its singleton 'SWrappedSing' provide a way to talk about singletons of other arbitrary singletons without the need to generate a bazillion instances. For reference, here is the definition of 'SWrappedSing': @ newtype 'SWrappedSing' :: forall k (a :: k). 'WrappedSing' a -> Type where 'SWrapSing' :: forall k (a :: k) (ws :: 'WrappedSing' a). { 'sUnwrapSing' :: 'Sing' a } -> 'SWrappedSing' ws type instance 'Sing' \@('WrappedSing' a) = 'SWrappedSing' @ 'SWrappedSing' is a bit of an unusual singleton in that its field is a singleton for @'Sing' \@k@, not @'WrappedSing' \@k@. But that's exactly the point—a singleton of a singleton contains as much type information as the underlying singleton itself, so we can get away with just @'Sing' \@k@. As an example of this in action, here is how you would define the singleton for the earlier @T@ type: @ data ST :: forall a. T a -> Type where SMkT :: forall a (x :: a) (sx :: 'Sing' x) (f :: F a). 'Sing' ('WrapSing' sx) -> 'Sing' f -> ST (MkT sx f) @ With this technique, we won't need anything like @SSBool@ in order to instantiate @x@ with 'True'. Instead, the field of type @'Sing' ('WrapSing' sx)@ will simply be a newtype around 'SBool'. In general, you'll need /n/ layers of 'WrapSing' if you wish to single a singleton /n/ times. Note that this is not the only possible way to define a singleton for @T@. An alternative approach that does not make use of singletons-of-singletons is discussed at some length . Due to the technical limitations of this approach, however, we do not use it in @singletons@ at the moment, instead favoring the slightly-clunkier-but-more-reliable 'WrappedSing' approach. -} {- $SLambdaPatternSynonyms @SLambda{2...8}@ are explicitly bidirectional pattern synonyms for defunctionalized singletons (@'Sing' (f :: k '~>' k' '~>' k'')@). As __constructors__: Same as @singFun{2..8}@. For example, one can turn a binary function on singletons @sTake :: 'SingFunction2' TakeSym0@ into a defunctionalized singleton @'Sing' (TakeSym :: Nat '~>' [a] '~>' [a])@: @ >>> import Data.Singletons.Prelude.List >>> :set -XTypeApplications >>> >>> :t 'SLambda2' 'SLambda2' :: 'SingFunction2' f -> 'Sing' f >>> :t 'SLambda2' \@TakeSym0 'SLambda2' :: 'SingFunction2' TakeSym0 -> 'Sing' TakeSym0 >>> :t 'SLambda2' \@TakeSym0 sTake 'SLambda2' :: 'Sing' TakeSym0 @ This is useful for functions on singletons that expect a defunctionalized singleton as an argument, such as @sZipWith :: 'SingFunction3' ZipWithSym0@: @ sZipWith :: Sing (f :: a '~>' b '~>' c) -> Sing (xs :: [a]) -> Sing (ys :: [b]) -> Sing (ZipWith f xs ys :: [c]) sZipWith ('SLambda2' \@TakeSym0 sTake) :: Sing (xs :: [Nat]) -> Sing (ys :: [[a]]) -> Sing (ZipWith TakeSym0 xs ys :: [[a]]) @ As __patterns__: Same as @unSingFun{2..8}@. Gets a binary term-level Haskell function on singletons @'Sing' (x :: k) -> 'Sing' (y :: k') -> 'Sing' (f \@\@ x \@\@ y)@ from a defunctionalised @'Sing' f@. Alternatively, as a record field accessor: @ applySing2 :: 'Sing' (f :: k '~>' k' '~>' k'') -> 'SingFunction2' f @ -}