singletons 0.8.6 → 0.9.0
raw patch · 24 files changed
+2377/−1170 lines, 24 filesdep +th-desugardep ~base
Dependencies added: th-desugar
Dependency ranges changed: base
Files
- CHANGES +0/−57
- CHANGES.md +96/−0
- Data/Singletons.hs +107/−103
- Data/Singletons/Bool.hs +111/−0
- Data/Singletons/Core.hs +144/−0
- Data/Singletons/CustomStar.hs +112/−25
- Data/Singletons/Decide.hs +30/−0
- Data/Singletons/Either.hs +107/−0
- Data/Singletons/Eq.hs +61/−0
- Data/Singletons/Exports.hs +0/−65
- Data/Singletons/List.hs +70/−0
- Data/Singletons/Maybe.hs +120/−0
- Data/Singletons/Prelude.hs +102/−0
- Data/Singletons/Promote.hs +129/−109
- Data/Singletons/Singletons.hs +339/−270
- Data/Singletons/TH.hs +89/−0
- Data/Singletons/Tuple.hs +61/−0
- Data/Singletons/TypeRepStar.hs +85/−18
- Data/Singletons/Types.hs +55/−0
- Data/Singletons/Util.hs +132/−67
- Data/Singletons/Void.hs +78/−0
- README +0/−441
- README.md +302/−0
- singletons.cabal +47/−15
− CHANGES
@@ -1,57 +0,0 @@-Changelog for singletons project-================================--0.8.6--------Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.--0.8.5--------Bug fix to make singletons compatible with GHC 7.6.1.--Added git info to cabal file.--0.8.4--------Update to work with latest version of GHC (7.7.20130114).--Now use branched type family instances to allow for promotion of functions-with overlapping patterns.--Permit promotion of functions with constraints by omitting constraints.--0.8.3--------Update to work with latest version of GHC (7.7.20121031).--Removed use of Any to simulate kind classes; now using KindOf and OfKind-from GHC.TypeLits.--Made compatible with GHC.TypeLits.--0.8.2--------Added this changelog--Update to work with latest version of GHC (7.6.1). (There was a change to-Template Haskell).--Moved library into Data.Singletons.--0.8.1--------Update to work with latest version of GHC. (There was a change to-Template Haskell).--Updated dependencies in cabal to include the newer version of TH.--0.8------Initial public release
+ CHANGES.md view
@@ -0,0 +1,96 @@+Changelog for singletons project+================================++0.9.0+-----++Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.++Change module structure significantly. If you want to derive your own+singletons, you should import `Data.Singletons.TH`. The module+`Data.Singletons` now exports functions only for the *use* of singletons.++New modules `Data.Singletons.Bool`, `...Maybe`, `...Either`, and `...List`+are just like their equivalents from `Data.`, except for `List`, which is+quite lacking in features.++For singleton equality, use `Data.Singletons.Eq`.++For propositional singleton equality, use `Data.Singletons.Decide`.++New module `Data.Singletons.Prelude` is meant to mirror the Haskell Prelude,+but with singleton definitions.++Streamline representation of singletons, resulting in *exponential* speedup+at execution. (This has not been rigorously measured, but the data structures+are now *exponentially* smaller.)++Add internal support for TypeLits, because the TypeLits module no longer+exports singleton definitions.++Add support for existential singletons, through the `toSing` method of+`SingKind`.++Remove the `SingE` class, bundling its functionality into `SingKind`.+Thus, the `SingRep` synonym has also been removed.++Name change: `KindIs` becomes `KProxy`.++Add support for singletonizing calls to `error`.++Add support for singletonizing empty data definitions.++0.8.6+-----++Make compatible with GHC HEAD, but HEAD reports core lint errors sometimes.++0.8.5+-----++Bug fix to make singletons compatible with GHC 7.6.1.++Added git info to cabal file.++0.8.4+-----++Update to work with latest version of GHC (7.7.20130114).++Now use branched type family instances to allow for promotion of functions+with overlapping patterns.++Permit promotion of functions with constraints by omitting constraints.++0.8.3+-----++Update to work with latest version of GHC (7.7.20121031).++Removed use of Any to simulate kind classes; now using KindOf and OfKind+from GHC.TypeLits.++Made compatible with GHC.TypeLits.++0.8.2+-----++Added this changelog++Update to work with latest version of GHC (7.6.1). (There was a change to+Template Haskell).++Moved library into Data.Singletons.++0.8.1+-----++Update to work with latest version of GHC. (There was a change to+Template Haskell).++Updated dependencies in cabal to include the newer version of TH.++0.8+---++Initial public release
Data/Singletons.hs view
@@ -1,123 +1,127 @@-{- Data/Singletons.hs--(c) Richard Eisenberg 2013-eir@cis.upenn.edu--This is the public interface file to the singletons library. Please-see the accompanying README file for more information. Haddock is-not currently compatible with the features used here, so the documentation-is all in the README file and /Dependently typed programming with singletons/,-available at <http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>--}+{-# LANGUAGE MagicHash, RankNTypes, PolyKinds, GADTs, DataKinds,+ FlexibleContexts, CPP, TypeFamilies #-} -{-# LANGUAGE TypeFamilies, GADTs, KindSignatures, TemplateHaskell,- DataKinds, PolyKinds, TypeOperators, MultiParamTypeClasses,- FlexibleContexts, RankNTypes, UndecidableInstances,- FlexibleInstances, ScopedTypeVariables, CPP- #-}-{-# OPTIONS_GHC -fwarn-incomplete-patterns -fno-warn-unused-binds #-}--- We make unused bindings for (||), (&&), and not.+-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- 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+-- <http://www.cis.upenn.edu/~eir/packages/singletons/README.html> and the+-- original paper presenting this library, available at+-- <http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>.+--+---------------------------------------------------------------------------- module Data.Singletons (- KindIs(..), Sing(..), SingI(..), SingE(..), SingRep, KindOf, Demote,- Any,- (:==), (:==:),- SingInstance(..), SingKind(singInstance),- sTrue, sFalse, SBool, sNothing, sJust, SMaybe, sLeft, sRight, SEither,- sTuple0, sTuple2, sTuple3, sTuple4, sTuple5, sTuple6, sTuple7,- STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7,- Not, sNot, (:&&), (%:&&), (:||), (%:||), (:&&:), (:||:), (:/=), (:/=:),- SEq((%==%), (%/=%)), (%:==), (%:/=),- If, sIf, - sNil, sCons, SList, (:++), (%:++), Head, Tail,- cases, bugInGHC,- genSingletons, singletons, genPromotions, promote,- promoteEqInstances, promoteEqInstance, singEqInstance, singEqInstances- ) where--import Prelude hiding ((++))-import Data.Singletons.Singletons-import Data.Singletons.Promote-import Data.Singletons.Exports-import Language.Haskell.TH-import Data.Singletons.Util-import GHC.Exts (Any)---- provide a few useful singletons...-$(genSingletons [''Bool, ''Maybe, ''Either, ''[]])-$(genSingletons [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])+ -- * Main singleton definitions+ + Sing,+ -- | See also 'Data.Singletons.Prelude.Sing' for exported constructors+ + SingI(..), SingKind(..), --- ... with some functions over Booleans-$(singletons [d|- not :: Bool -> Bool- not False = True- not True = False+ -- * Working with singletons+ KindOf, Demote,+ SingInstance(..), SomeSing(..),+ singInstance, withSingI, withSomeSing, singByProxy, - (&&) :: Bool -> Bool -> Bool- False && _ = False- True && a = a+#if __GLASGOW_HASKELL__ >= 707+ singByProxy#,+#endif+ withSing, singThat, - (||) :: Bool -> Bool -> Bool- False || a = a- True || _ = True- |])+ -- * Auxiliary functions+ bugInGHC, Error, sError,+ KProxy(..), Proxy(..)+ ) where -type family (a :: k) :==: (b :: k) :: Bool-type a :== b = a :==: b -- :== and :==: are synonyms+import Data.Singletons.Core+import Unsafe.Coerce+import GHC.TypeLits (Symbol) -type a :/=: b = Not (a :==: b)-type a :/= b = a :/=: b+#if __GLASGOW_HASKELL__ >= 707+import GHC.Exts ( Proxy# )+import Data.Proxy+#else+import Data.Singletons.Types+#endif --- the singleton analogue of @Eq@-class (kparam ~ KindParam) => SEq (kparam :: KindIs k) where- (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)- (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)- a %/=% b = sNot (a %==% b)+-- | A 'SingInstance' wraps up a 'SingI' instance for explicit handling.+data SingInstance (a :: k) where+ SingInstance :: SingI a => SingInstance a -(%:==) :: forall (a :: k) (b :: k). SEq (KindParam :: KindIs k)- => Sing a -> Sing b -> Sing (a :==: b)-(%:==) = (%==%)+-- dirty implementation of explicit-to-implicit conversion+newtype DI a = Don'tInstantiate (SingI a => SingInstance a) -(%:/=) :: forall (a :: k) (b :: k). SEq (KindParam :: KindIs k)- => Sing a -> Sing b -> Sing (a :/=: b)-(%:/=) = (%/=%)+-- | Get an implicit singleton (a 'SingI' instance) from an explicit one.+singInstance :: forall (a :: k). Sing a -> SingInstance a+singInstance s = with_sing_i SingInstance+ where+ with_sing_i :: (SingI a => SingInstance a) -> SingInstance a+ with_sing_i si = unsafeCoerce (Don'tInstantiate si) s -$(singEqInstances [''Bool, ''Maybe, ''Either, ''[]])-$(singEqInstances [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])+-- | Convenience function for creating a context with an implicit singleton+-- available.+withSingI :: Sing n -> (SingI n => r) -> r+withSingI sn r =+ case singInstance sn of+ SingInstance -> r --- singleton conditional-sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)-sIf STrue b _ = b-sIf SFalse _ c = c+-- | Convert a normal datatype (like 'Bool') to a singleton for that datatype,+-- passing it into a continuation.+withSomeSing :: SingKind ('KProxy :: KProxy k)+ => DemoteRep ('KProxy :: KProxy k) -- ^ The original datatype+ -> (forall (a :: k). Sing a -> r) -- ^ Function expecting a singleton+ -> r+withSomeSing x f =+ case toSing x of+ SomeSing x' -> f x' --- symmetric syntax synonyms-type a :&&: b = a :&& b-type a :||: b = a :|| b+-- | A convenience function useful when we need to name a singleton value+-- multiple times. Without this function, each use of 'sing' could potentially+-- refer to a different singleton, and one has to use type signatures (often+-- with @ScopedTypeVariables@) to ensure that they are the same.+withSing :: SingI a => (Sing a -> b) -> b+withSing f = f sing -$(singletons [d|- (++) :: [a] -> [a] -> [a]- [] ++ a = a- (h:t) ++ a = h:(t ++ a)- |])+-- | A convenience function that names a singleton satisfying a certain+-- property. If the singleton does not satisfy the property, then the function+-- returns 'Nothing'. The property is expressed in terms of the underlying+-- representation of the singleton.+singThat :: forall (a :: k). (SingKind ('KProxy :: KProxy k), SingI a)+ => (Demote a -> Bool) -> Maybe (Sing a)+singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing --- allows for automatic checking of all constructors in a GADT for instance--- inference-cases :: Name -> Q Exp -> Q Exp -> Q Exp-cases tyName expq bodyq = do- info <- reifyWithWarning tyName- case info of- TyConI (DataD _ _ _ ctors _) -> buildCases ctors- TyConI (NewtypeD _ _ _ ctor _) -> buildCases [ctor]- _ -> fail $ "Using <<cases>> with something other than a type constructor: "- ++ (show tyName)- where buildCases :: [Con] -> Q Exp- buildCases ctors =- caseE expq (map ((flip (flip match (normalB bodyq)) []) . conToPat) ctors)+-- | Allows creation of a singleton when a proxy is at hand.+singByProxy :: SingI a => proxy a -> Sing a+singByProxy _ = sing - conToPat :: Con -> Q Pat- conToPat = ctor1Case- (\name tys -> conP name (replicate (length tys) wildP))+#if __GLASGOW_HASKELL__ >= 707+-- | Allows creation of a singleton when a @proxy#@ is at hand.+singByProxy# :: SingI a => Proxy# a -> Sing a+singByProxy# _ = sing+#endif --- useful when suppressing GHC's warnings about incomplete pattern matches+-- | GHC 7.8 sometimes warns about incomplete pattern matches when no such+-- patterns are possible, due to GADT constraints.+-- See the bug report at <https://ghc.haskell.org/trac/ghc/ticket/3927>.+-- In such cases, it's useful to have a catch-all pattern that then has+-- 'bugInGHC' as its right-hand side. bugInGHC :: forall a. a bugInGHC = error "Bug encountered in GHC -- this should never happen"++-- | The promotion of 'error'+type family Error (str :: Symbol) :: k++-- | The singleton for 'error'+sError :: Sing (str :: Symbol) -> a+sError sstr = error (fromSing sstr)
+ Data/Singletons/Bool.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE TemplateHaskell, DataKinds, PolyKinds, TypeFamilies, TypeOperators,+ GADTs, CPP #-}++#if __GLASGOW_HASKELL__ < 707+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Bool+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines functions and datatypes relating to the singleton for 'Bool',+-- including a singletons version of all the definitions in @Data.Bool@.+--+-- Because many of these definitions are produced by Template Haskell,+-- it is not possible to create proper Haddock documentation. Please look+-- up the corresponding operation in @Data.Bool@. Also, please excuse+-- the apparent repeated variable names. This is due to an interaction+-- between Template Haskell and Haddock.+--+----------------------------------------------------------------------------++module Data.Singletons.Bool (+ -- * The 'Bool' singleton+ + Sing(SFalse, STrue),+ -- | Though Haddock doesn't show it, the 'Sing' instance above declares+ -- constructors+ --+ -- > SFalse :: Sing False+ -- > STrue :: Sing True+ + SBool,+ -- | 'SBool' is a kind-restricted synonym for 'Sing': @type SBool (a :: Bool) = Sing a@+ + -- * Conditionals+ If, sIf,++ -- * Singletons from @Data.Bool@+ Not, sNot, (:&&), (:||), (%:&&), (%:||),++ -- | The following are derived from the function 'bool' in @Data.Bool@. The extra+ -- underscore is to avoid name clashes with the type 'Bool'.+ Bool_, sBool_, Otherwise, sOtherwise+ ) where++import Data.Singletons.Core+import Data.Singletons.Singletons++#if __GLASGOW_HASKELL__ >= 707+import Data.Type.Bool++type a :&& b = a && b+type a :|| b = a || b++sNot :: SBool a -> SBool (Not a)+sNot SFalse = STrue+sNot STrue = SFalse++(%:&&) :: SBool a -> SBool b -> SBool (a :&& b)+SFalse %:&& _ = SFalse+STrue %:&& a = a++(%:||) :: SBool a -> SBool b -> SBool (a :|| b)+SFalse %:|| a = a+STrue %:|| _ = STrue++#else++$(singletonsOnly [d|+ not :: Bool -> Bool+ not False = True+ not True = False++ (&&) :: Bool -> Bool -> Bool+ False && _ = False+ True && x = x++ (||) :: Bool -> Bool -> Bool+ False || x = x+ True || _ = True+ |])++-- | Type-level "If". @If True a b@ ==> @a@; @If False a b@ ==> @b@+type family If (a :: Bool) (b :: k) (c :: k) :: k+type instance If 'True b c = b+type instance If 'False b c = c++#endif++-- | Conditional over singletons+sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)+sIf STrue b _ = b+sIf SFalse _ c = c+++-- ... with some functions over Booleans+$(singletonsOnly [d|+ bool_ :: a -> a -> Bool -> a+ bool_ fls _tru False = fls+ bool_ _fls tru True = tru++ otherwise :: Bool+ otherwise = True+ |])+
+ Data/Singletons/Core.hs view
@@ -0,0 +1,144 @@+{- Data/Singletons/Core.hs++(c) Richard Eisenberg 2013+eir@cis.upenn.edu++This (internal) module contains the main class definitions for singletons,+re-exported from various places.++-}++{-# LANGUAGE CPP, RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies,+ FlexibleContexts, TemplateHaskell, ScopedTypeVariables,+ UndecidableInstances, TypeOperators, FlexibleInstances #-}+#if __GLASGOW_HASKELL__ >= 707+{-# LANGUAGE EmptyCase #-}+#else+ -- optimizing instances of SDecide cause GHC to die (#8467)+{-# OPTIONS_GHC -O0 #-}+#endif++module Data.Singletons.Core where++import Data.Singletons.Util+import Data.Singletons.Singletons+import GHC.TypeLits (Nat, Symbol)+import Data.Singletons.Types+import Unsafe.Coerce++#if __GLASGOW_HASKELL__ >= 707+import GHC.TypeLits (KnownNat, KnownSymbol, natVal, symbolVal)+import Data.Proxy+import Data.Type.Equality+#else+import qualified GHC.TypeLits as TypeLits+#endif++-- | Convenient synonym to refer to the kind of a type variable:+-- @type KindOf (a :: k) = ('KProxy :: KProxy k)@+type KindOf (a :: k) = ('KProxy :: KProxy k)++-- | The singleton kind-indexed data family.+data family Sing (a :: k)++-- | A 'SingI' constraint is essentially an implicitly-passed singleton.+-- If you need to satisfy this constraint with an explicit singleton, please+-- see 'withSingI'.+class SingI (a :: k) where+ -- | Produce the singleton explicitly. You will likely need the @ScopedTypeVariables@+ -- extension to use this method the way you want.+ sing :: Sing a++-- | The 'SingKind' class is essentially a /kind/ class. It classifies all kinds+-- for which singletons are defined. The class supports converting between a singleton+-- type and the base (unrefined) type which it is built from.+class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where+ -- | Get a base type from a proxy for the promoted kind. For example,+ -- @DemoteRep ('KProxy :: KProxy Bool)@ will be the type @Bool@.+ type DemoteRep kparam :: *++ -- | Convert a singleton to its unrefined version.+ fromSing :: Sing (a :: k) -> DemoteRep kparam++ -- | Convert an unrefined type to an existentially-quantified singleton type.+ toSing :: DemoteRep kparam -> SomeSing kparam++-- | Convenient abbreviation for 'DemoteRep':+-- @type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)@+type Demote (a :: k) = DemoteRep ('KProxy :: KProxy k)++-- | An /existentially-quantified/ singleton. This type is useful when you want a+-- singleton type, but there is no way of knowing, at compile-time, what the type+-- index will be. To make use of this type, you will generally have to use a+-- pattern-match:+--+-- > foo :: Bool -> ...+-- > foo b = case toSing b of+-- > SomeSing sb -> {- fancy dependently-typed code with sb -}+--+-- An example like the one above may be easier to write using 'withSomeSing'.+data SomeSing (kproxy :: KProxy k) where+ SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)+ +-- some useful singletons+$(genSingletons basicTypes)++-- define singletons for TypeLits++newtype instance Sing (n :: Nat) = SNat Integer+#if __GLASGOW_HASKELL__ >= 707+instance KnownNat n => SingI n where+ sing = SNat (natVal (Proxy :: Proxy n))+#else+instance TypeLits.SingRep n Integer => SingI (n :: Nat) where+ sing = SNat (TypeLits.fromSing (TypeLits.sing :: TypeLits.Sing n))+#endif+instance SingKind ('KProxy :: KProxy Nat) where+ type DemoteRep ('KProxy :: KProxy Nat) = Integer+ fromSing (SNat n) = n+ toSing n = SomeSing (SNat n)++newtype instance Sing (n :: Symbol) = SSym String+#if __GLASGOW_HASKELL__ >= 707+instance KnownSymbol n => SingI n where+ sing = SSym (symbolVal (Proxy :: Proxy n))+#else+instance TypeLits.SingRep n String => SingI (n :: Symbol) where+ sing = SSym (TypeLits.fromSing (TypeLits.sing :: TypeLits.Sing n))+#endif+instance SingKind ('KProxy :: KProxy Symbol) where+ type DemoteRep ('KProxy :: KProxy Symbol) = String+ fromSing (SSym n) = n+ toSing s = SomeSing (SSym s)+ +-- we need to decare SDecide and its instances here to avoid making+-- the EqualityT instance an orphan++-- | Members of the 'SDecide' "kind" class support decidable equality. Instances+-- of this class are generated alongside singleton definitions for datatypes that+-- derive an 'Eq' instance.+class (kparam ~ 'KProxy) => SDecide (kparam :: KProxy k) where+ -- | Compute a proof or disproof of equality, given two singletons.+ (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)++$(singDecideInstances basicTypes)++-- We need SDecide instances for the TypeLits singletons+instance SDecide ('KProxy :: KProxy Nat) where+ (SNat n) %~ (SNat m)+ | n == m = Proved $ unsafeCoerce Refl+ | otherwise = Disproved (\_ -> error errStr)+ where errStr = "Broken Nat singletons"+ +instance SDecide ('KProxy :: KProxy Symbol) where+ (SSym n) %~ (SSym m)+ | n == m = Proved $ unsafeCoerce Refl+ | otherwise = Disproved (\_ -> error errStr)+ where errStr = "Broken Symbol singletons"++instance SDecide ('KProxy :: KProxy k) => TestEquality (Sing :: k -> *) where+ testEquality a b =+ case a %~ b of+ Proved Refl -> Just Refl+ Disproved _ -> Nothing+
Data/Singletons/CustomStar.hs view
@@ -1,45 +1,105 @@-{- Data/Singletons/CustomStar.hs--(c) Richard Eisenbeg 2013-eir@cis.upenn.edu+{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, CPP, TemplateHaskell #-} -This file implements singletonStar, which generates a datatype Rep and associated-singleton from a list of types. The promoted version of Rep is kind * and the-Haskell types themselves. This is still very experimental, so expect unusual-results!--} -{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, CPP #-}-{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}+-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.CustomStar+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This file implements 'singletonStar', which generates a datatype @Rep@ and associated+-- singleton from a list of types. The promoted version of @Rep@ is kind @*@ and the+-- Haskell types themselves. This is still very experimental, so expect unusual+-- results!+--+---------------------------------------------------------------------------- -module Data.Singletons.CustomStar where+module Data.Singletons.CustomStar ( singletonStar ) where import Language.Haskell.TH+import Language.Haskell.TH.Syntax ( Quasi(..) ) import Data.Singletons.Util import Data.Singletons.Promote import Data.Singletons.Singletons import Control.Monad --- Produce a representation and singleton for the collection of types given-singletonStar :: [Name] -> Q [Dec]+#if __GLASGOW_HASKELL__ >= 707+import Data.Singletons.Core+import Data.Singletons.Types+import Data.Singletons.Eq+import Unsafe.Coerce+import Data.Type.Equality+#endif++{-+The SEq instance here is tricky.+The problem is that, in GHC 7.8+, the instance of type-level (==) for *+is not recursive. Thus, it's impossible, say, to get (Maybe a == Maybe b) ~ False+from (a == b) ~ False.++There are a few ways forward:+ 1) Define SEq to use our own Boolean (==) operator, instead of the built-in one.+ This would work, but feels wrong.+ 2) Use unsafeCoerce.+We do #2.++Also to note: because these problems don't exist in GHC 7.6, the generation of+Eq and Decide for 7.6 is entirely normal.++Note that mkCustomEqInstances makes the SDecide and SEq instances in GHC 7.8+,+but the type-level (==) instance in GHC 7.6. This is perhaps poor design, but+it reduces the amount of CPP noise.+-}++-- | Produce a representation and singleton for the collection of types given.+--+-- A datatype @Rep@ is created, with one constructor per type in the declared+-- universe. When this type is promoted by the singletons library, the+-- constructors become full types in @*@, not just promoted data constructors.+-- +-- For example,+-- +-- > $(singletonStar [''Nat, ''Bool, ''Maybe])+-- +-- generates the following:+-- +-- > data Rep = Nat | Bool | Maybe Rep deriving (Eq, Show, Read)+-- +-- and its singleton. However, because @Rep@ is promoted to @*@, the singleton+-- is perhaps slightly unexpected:+-- +-- > data instance Sing (a :: *) where+-- > SNat :: Sing Nat+-- > SBool :: Sing Bool+-- > SMaybe :: SingRep a => Sing a -> Sing (Maybe a)+-- +-- The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,+-- @Bool@, and @Maybe@, not just promoted data constructors.+-- +-- Please note that this function is /very/ experimental. Use at your own risk.+singletonStar :: Quasi q+ => [Name] -- ^ A list of Template Haskell @Name@s for types+ -> q [Dec] singletonStar names = do kinds <- mapM getKind names ctors <- zipWithM (mkCtor True) names kinds let repDecl = DataD [] repName [] ctors- [mkName "Eq", mkName "Show", mkName "Read"]+ [''Eq, ''Show, ''Read] fakeCtors <- zipWithM (mkCtor False) names kinds-#if __GLASGOW_HASKELL__ >= 707- eqInstances <- mkEqTypeInstance StarT fakeCtors-#else- eqInstances <- mapM mkEqTypeInstance- [(c1, c2) | c1 <- fakeCtors, c2 <- fakeCtors]-#endif+ eqInstances <- mkCustomEqInstances fakeCtors singletonDecls <- singDataD True [] repName [] fakeCtors- [mkName "Eq", mkName "Show", mkName "Read"]+ [''Show, ''Read+#if __GLASGOW_HASKELL__ < 707+ , ''Eq+#endif+ ] return $ repDecl : eqInstances ++ singletonDecls where -- get the kinds of the arguments to the tycon with the given name- getKind :: Name -> Q [Kind]+ getKind :: Quasi q => Name -> q [Kind] getKind name = do info <- reifyWithWarning name case info of@@ -59,7 +119,7 @@ -- first parameter is whether this is a real ctor (with a fresh name) -- or a fake ctor (when the name is actually a Haskell type)- mkCtor :: Bool -> Name -> [Kind] -> Q Con+ mkCtor :: Quasi q => Bool -> Name -> [Kind] -> q Con mkCtor real name args = do (types, vars) <- evalForPair $ mapM kindToType args let ctor = NormalC ((if real then reinterpret else id) name)@@ -69,7 +129,7 @@ else return ctor -- demote a kind back to a type, accumulating any unbound parameters- kindToType :: Kind -> QWithAux [Name] Type+ kindToType :: Quasi q => Kind -> QWithAux [Name] q Type kindToType (ForallT _ _ _) = fail "Explicit forall encountered in kind" kindToType (AppT k1 k2) = do t1 <- kindToType k1@@ -93,3 +153,30 @@ fail $ "Cannot make a representation of a type that has " ++ "an argument of kind Constraint" kindToType (LitT _) = fail "Literal encountered at the kind level"++mkCustomEqInstances :: Quasi q => [Con] -> q [Dec]+mkCustomEqInstances ctors = do+#if __GLASGOW_HASKELL__ >= 707+ let ctorVar = error "Internal error: Equality instance inspected ctor var"+ sCtors <- evalWithoutAux $ mapM (singCtor ctorVar) ctors+ decideInst <- mkEqualityInstance StarT sCtors sDecideClassDesc++ a <- qNewName "a"+ b <- qNewName "b"+ let eqInst = InstanceD+ []+ (AppT (ConT ''SEq) (kindParam StarT))+ [FunD '(%:==)+ [Clause [VarP a, VarP b]+ (NormalB $+ CaseE (foldExp (VarE '(%~)) [VarE a, VarE b])+ [ Match (ConP 'Proved [ConP 'Refl []])+ (NormalB $ ConE 'STrue) []+ , Match (ConP 'Disproved [WildP])+ (NormalB $ AppE (VarE 'unsafeCoerce)+ (ConE 'SFalse)) []+ ]) []]]+ return [decideInst, eqInst]+#else+ mapM mkEqTypeInstance [(c1, c2) | c1 <- ctors, c2 <- ctors]+#endif
+ Data/Singletons/Decide.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE CPP #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Decide+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines the class 'SDecide', allowing for decidable equality over singletons.+--+----------------------------------------------------------------------------++module Data.Singletons.Decide (+ -- * The SDecide class+ SDecide(..),++ -- * Supporting definitions+ (:~:)(..), Void, Refuted, Decision(..)+ ) where++import Data.Singletons.Types+import Data.Singletons.Core+import Data.Singletons.Void++#if __GLASGOW_HASKELL__ >= 707+import Data.Type.Equality+#endif
+ Data/Singletons/Either.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies, GADTs,+ DataKinds, PolyKinds, RankNTypes, UndecidableInstances, CPP #-}++#if __GLASGOW_HASKELL__ < 707+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Either+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines functions and datatypes relating to the singleton for 'Either',+-- including a singletons version of all the definitions in @Data.Either@.+--+-- Because many of these definitions are produced by Template Haskell,+-- it is not possible to create proper Haddock documentation. Please look+-- up the corresponding operation in @Data.Either@. Also, please excuse+-- the apparent repeated variable names. This is due to an interaction+-- between Template Haskell and Haddock.+--+----------------------------------------------------------------------------++module Data.Singletons.Either (+ -- * The 'Either' singleton+ Sing(SLeft, SRight),+ -- | Though Haddock doesn't show it, the 'Sing' instance above declares+ -- constructors+ --+ -- > SLeft :: Sing a -> Sing (Left a)+ -- > SRight :: Sing b -> Sing (Right b)+ + SEither,+ -- | 'SEither' is a kind-restricted synonym for 'Sing':+ -- @type SEither (a :: Either x y) = Sing a@++ -- * Singletons from @Data.Either@+ Either_, sEither_,+ -- | The preceding two definitions are derived from the function 'either' in+ -- @Data.Either@. The extra underscore is to avoid name clashes with the type+ -- 'Either'.+ + Lefts, sLefts, Rights, sRights,+ PartitionEithers, sPartitionEithers, IsLeft, sIsLeft, IsRight, sIsRight+ ) where++import Data.Singletons.Core+import Data.Singletons.TH+import Data.Singletons.List++$(singletonsOnly [d|+ -- | Case analysis for the 'Either' type.+ -- If the value is @'Left' a@, apply the first function to @a@;+ -- if it is @'Right' b@, apply the second function to @b@.+ either_ :: (a -> c) -> (b -> c) -> Either a b -> c+ either_ f _ (Left x) = f x+ either_ _ g (Right y) = g y++ -- | Extracts from a list of 'Either' all the 'Left' elements+ -- All the 'Left' elements are extracted in order.++ lefts :: [Either a b] -> [a]+ lefts [] = []+ lefts (Left x : xs) = x : lefts xs+ lefts (Right _ : xs) = lefts xs++ -- | Extracts from a list of 'Either' all the 'Right' elements+ -- All the 'Right' elements are extracted in order.++ rights :: [Either a b] -> [b]+ rights [] = []+ rights (Left _ : xs) = rights xs+ rights (Right x : xs) = x : rights xs++ -- | Partitions a list of 'Either' into two lists+ -- All the 'Left' elements are extracted, in order, to the first+ -- component of the output. Similarly the 'Right' elements are extracted+ -- to the second component of the output.++ partitionEithers :: [Either a b] -> ([a],[b])+ partitionEithers es = partitionEithers_aux ([], []) es++ partitionEithers_aux :: ([a],[b]) -> [Either a b] -> ([a],[b])+ partitionEithers_aux (as,bs) [] = (reverse as,reverse bs)+ partitionEithers_aux (as,bs) (Left a : es) =+ partitionEithers_aux (a : as, bs) es+ partitionEithers_aux (as,bs) (Right b : es) =+ partitionEithers_aux (as, b : bs) es++ -- | Return `True` if the given value is a `Left`-value, `False` otherwise.+ --+ -- /Since: 4.7.0.0/+ isLeft :: Either a b -> Bool+ isLeft (Left _) = True+ isLeft (Right _) = False++ -- | Return `True` if the given value is a `Right`-value, `False` otherwise.+ --+ -- /Since: 4.7.0.0/+ isRight :: Either a b -> Bool+ isRight (Left _) = False+ isRight (Right _) = True+ |])
+ Data/Singletons/Eq.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE TypeOperators, DataKinds, PolyKinds, TypeFamilies,+ RankNTypes, FlexibleContexts, TemplateHaskell,+ UndecidableInstances, GADTs, CPP #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Eq+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines the SEq singleton version of the Eq type class.+--+-----------------------------------------------------------------------------++module Data.Singletons.Eq (+ SEq(..),+ type (==), (:==), (:/=)+ ) where++import Data.Singletons.Util+import Data.Singletons.Bool+import Data.Singletons.Singletons+import Data.Singletons.Core++#if __GLASGOW_HASKELL__ >= 707+import Data.Proxy+import Data.Type.Equality++-- | A re-export of the type-level @(==)@ that conforms to the singletons naming+-- convention.+type a :== b = a == b++#else+import Data.Singletons.Types+import Data.Singletons.Promote++type family (a :: k) :== (b :: k) :: Bool+type a == b = a :== b++#endif++type a :/= b = Not (a :== b)++-- | The singleton analogue of 'Eq'. Unlike the definition for 'Eq', it is required+-- that instances define a body for '(%:==)'. You may also supply a body for '(%:/=)'.+class (kparam ~ 'KProxy) => SEq (kparam :: KProxy k) where+ -- | Boolean equality on singletons+ (%:==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :== b)++ -- | Boolean disequality on singletons+ (%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/= b)+ a %:/= b = sNot (a %:== b)++#if __GLASGOW_HASKELL__ < 707+$(promoteEqInstances basicTypes)+#endif+ +$(singEqInstancesOnly basicTypes)
− Data/Singletons/Exports.hs
@@ -1,65 +0,0 @@-{- Data/Singletons/Exports.hs--(c) Richard Eienberg 2013-eir@cis.upenn.edu--This file contains the fundamental datatype definitions for the singletons-package. These are all re-exported in Data/Singletons.hs--}--{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, RankNTypes, FlexibleContexts,- FlexibleInstances, UndecidableInstances, TypeOperators, GADTs,- CPP #-}--module Data.Singletons.Exports (- KindIs(..), Sing, SingI(..), SingE(..), SingRep, KindOf, Demote,-- SingInstance(..), SingKind(..), If, Head, Tail- ) where--#if __GLASGOW_HASKELL__ >= 707--import GHC.TypeLits ( KindIs(..), Sing, SingI(..), SingE(..),- SingRep, KindOf, Demote )--#else---- Kind-level proxy-data KindIs (k :: *) = KindParam---- Access the kind of a type variable-type KindOf (a :: k) = (KindParam :: KindIs k)---- Declarations of singleton structures-data family Sing (a :: k)-class SingI (a :: k) where- sing :: Sing a-class (kparam ~ KindParam) => SingE (kparam :: KindIs k) where- type DemoteRep kparam :: *- fromSing :: Sing (a :: k) -> DemoteRep kparam---- SingRep is a synonym for (SingI, SingE)-class (SingI a, SingE (KindOf a)) => SingRep (a :: k)-instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)---- Abbreviation for DemoteRep-type Demote (a :: k) = DemoteRep (KindParam :: KindIs k)--#endif--data SingInstance (a :: k) where- SingInstance :: SingRep a => SingInstance a-class (kparam ~ KindParam) => SingKind (kparam :: KindIs k) where- singInstance :: forall (a :: k). Sing a -> SingInstance a---- type-level conditional-type family If (a :: Bool) (b :: k) (c :: k) :: k-type instance If 'True b c = b-type instance If 'False b c = c---- operate on type-level lists-type family Head (a :: [k]) :: k-type instance Head (h ': t) = h--type family Tail (a :: [k]) :: [k]-type instance Tail (h ': t) = t
+ Data/Singletons/List.hs view
@@ -0,0 +1,70 @@+{-# LANGUAGE CPP, TypeOperators, DataKinds, PolyKinds, TypeFamilies,+ TemplateHaskell, GADTs, UndecidableInstances #-}++#if __GLASGOW_HASKELL__ < 707+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.List+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines functions and datatypes relating to the singleton for '[]',+-- including a singletons version of a few of the definitions in @Data.List@.+--+-- Because many of these definitions are produced by Template Haskell,+-- it is not possible to create proper Haddock documentation. Please look+-- up the corresponding operation in @Data.List@. Also, please excuse+-- the apparent repeated variable names. This is due to an interaction+-- between Template Haskell and Haddock.+--+----------------------------------------------------------------------------++module Data.Singletons.List (+ -- * The singleton for lists+ Sing(SNil, SCons),+ -- | Though Haddock doesn't show it, the 'Sing' instance above declares+ -- constructors+ --+ -- > SNil :: Sing '[]+ -- > SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)++ SList,+ -- | 'SList' is a kind-restricted synonym for 'Sing': @type SList (a :: [k]) = Sing a@+ + Head, Tail, sHead, sTail,+ (:++), (%:++),+ Reverse, sReverse+ ) where++import Data.Singletons.Core+import Data.Singletons+import Data.Singletons.Singletons++$(singletonsOnly [d|+ (++) :: [a] -> [a] -> [a]+ [] ++ a = a+ (h:t) ++ a = h:(t ++ a)++ head :: [a] -> a+ head (a : _) = a+ head [] = error "Data.Singletons.List.head: empty list"++ tail :: [a] -> [a]+ tail (_ : t) = t+ tail [] = error "Data.Singletons.List.tail: empty list"++ reverse :: [a] -> [a]+ reverse list = reverse_aux [] list++ reverse_aux :: [a] -> [a] -> [a]+ reverse_aux acc [] = acc+ reverse_aux acc (h : t) = reverse_aux (h : acc) t+ |])++
+ Data/Singletons/Maybe.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeFamilies,+ DataKinds, PolyKinds, UndecidableInstances, GADTs,+ RankNTypes, CPP #-}++#if __GLASGOW_HASKELL__ < 707+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Maybe+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines functions and datatypes relating to the singleton for 'Maybe',+-- including a singletons version of all the definitions in @Data.Maybe@.+--+-- Because many of these definitions are produced by Template Haskell,+-- it is not possible to create proper Haddock documentation. Please look+-- up the corresponding operation in @Data.Maybe@. Also, please excuse+-- the apparent repeated variable names. This is due to an interaction+-- between Template Haskell and Haddock.+--+----------------------------------------------------------------------------+++module Data.Singletons.Maybe (+ -- The 'Maybe' singleton+ + Sing(SNothing, SJust),+ -- | Though Haddock doesn't show it, the 'Sing' instance above declares+ -- constructors+ --+ -- > SNothing :: Sing Nothing+ -- > SJust :: Sing a -> Sing (Just a)++ SMaybe,+ -- | 'SBool' is a kind-restricted synonym for 'Sing': @type SMaybe (a :: Maybe k) = Sing a@++ -- * Singletons from @Data.Maybe@++ Maybe_, sMaybe_,+ -- | The preceding two definitions are derived from the function 'maybe' in+ -- @Data.Maybe@. The extra underscore is to avoid name clashes with the type+ -- 'Maybe'.+ + IsJust, sIsJust, IsNothing, sIsNothing,+ FromJust, sFromJust, FromMaybe, sFromMaybe, MaybeToList, sMaybeToList,+ ListToMaybe, sListToMaybe, CatMaybes, sCatMaybes, MapMaybe, sMapMaybe+ ) where++import Data.Singletons.Core+import Data.Singletons+import Data.Singletons.TH+import Data.Singletons.List++$(singletonsOnly [d|+ -- | The 'maybe' function takes a default value, a function, and a 'Maybe'+ -- value. If the 'Maybe' value is 'Nothing', the function returns the+ -- default value. Otherwise, it applies the function to the value inside+ -- the 'Just' and returns the result.+ maybe_ :: b -> (a -> b) -> Maybe a -> b+ maybe_ n _ Nothing = n+ maybe_ _ f (Just x) = f x++ -- | The 'isJust' function returns 'True' iff its argument is of the+ -- form @Just _@.+ isJust :: Maybe a -> Bool+ isJust Nothing = False+ isJust (Just _) = True++ -- | The 'isNothing' function returns 'True' iff its argument is 'Nothing'.+ isNothing :: Maybe a -> Bool+ isNothing Nothing = True+ isNothing (Just _) = False++ -- | The 'fromJust' function extracts the element out of a 'Just' and+ -- throws an error if its argument is 'Nothing'.+ fromJust :: Maybe a -> a+ fromJust Nothing = error "Maybe.fromJust: Nothing" -- yuck+ fromJust (Just x) = x++ -- | The 'fromMaybe' function takes a default value and and 'Maybe'+ -- value. If the 'Maybe' is 'Nothing', it returns the default values;+ -- otherwise, it returns the value contained in the 'Maybe'.+ fromMaybe :: a -> Maybe a -> a+ fromMaybe d Nothing = d+ fromMaybe _ (Just v) = v++ -- | The 'maybeToList' function returns an empty list when given+ -- 'Nothing' or a singleton list when not given 'Nothing'.+ maybeToList :: Maybe a -> [a]+ maybeToList Nothing = []+ maybeToList (Just x) = [x]++ -- | The 'listToMaybe' function returns 'Nothing' on an empty list+ -- or @'Just' a@ where @a@ is the first element of the list.+ listToMaybe :: [a] -> Maybe a+ listToMaybe [] = Nothing+ listToMaybe (a:_) = Just a++ -- | The 'catMaybes' function takes a list of 'Maybe's and returns+ -- a list of all the 'Just' values. + catMaybes :: [Maybe a] -> [a]+ catMaybes [] = []+ catMaybes (Just x : xs) = x : catMaybes xs+ catMaybes (Nothing : xs) = catMaybes xs++ -- | The 'mapMaybe' function is a version of 'map' which can throw+ -- out elements. In particular, the functional argument returns+ -- something of type @'Maybe' b@. If this is 'Nothing', no element+ -- is added on to the result list. If it just @'Just' b@, then @b@ is+ -- included in the result list.+ mapMaybe :: (a -> Maybe b) -> [a] -> [b]+ mapMaybe _ [] = []+ mapMaybe f (x:xs) = maybeToList (f x) ++ (mapMaybe f xs)+ |])
+ Data/Singletons/Prelude.hs view
@@ -0,0 +1,102 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Prelude+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Mimics the Haskell Prelude, but with singleton types. Includes the basic+-- singleton definitions. Note: This is currently very incomplete!+--+-- Because many of these definitions are produced by Template Haskell, it is+-- not possible to create proper Haddock documentation. Also, please excuse+-- the apparent repeated variable names. This is due to an interaction between+-- Template Haskell and Haddock.+--+----------------------------------------------------------------------------++module Data.Singletons.Prelude (+ -- * Basic singleton definitions+ module Data.Singletons,+ + Sing(SFalse, STrue, SNil, SCons, SJust, SNothing, SLeft, SRight, SLT, SEQ, SGT,+ STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7),+ -- | Though Haddock doesn't show it, the 'Sing' instance above includes+ -- the following instances+ --+ -- > data instance Sing (a :: Bool) where+ -- > SFalse :: Sing False+ -- > STrue :: Sing True+ -- >+ -- > data instance Sing (a :: [k]) where+ -- > SNil :: Sing '[]+ -- > SCons :: Sing (h :: k) -> Sing (t :: [k]) -> Sing (h ': t)+ -- >+ -- > data instance Sing (a :: Maybe k) where+ -- > SNothing :: Sing Nothing+ -- > SJust :: Sing (a :: k) -> Sing (Just a)+ -- >+ -- > data instance Sing (a :: Either x y) where+ -- > SLeft :: Sing (a :: x) -> Sing (Left a)+ -- > SRight :: Sing (b :: y) -> Sing (Right b)+ -- >+ -- > data instance Sing (a :: Ordering) where+ -- > SLT :: Sing LT+ -- > SEQ :: Sing EQ+ -- > SGT :: Sing GT+ -- >+ -- > data instance Sing (a :: ()) where+ -- > STuple0 :: Sing '()+ -- >+ -- > data instance Sing (z :: (a, b)) where+ -- > STuple2 :: Sing a -> Sing b -> Sing '(a, b)+ -- >+ -- > data instance Sing (z :: (a, b, c)) where+ -- > STuple3 :: Sing a -> Sing b -> Sing c -> Sing '(a, b, c)+ -- >+ -- > data instance Sing (z :: (a, b, c, d)) where+ -- > STuple4 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing '(a, b, c, d)+ -- >+ -- > data instance Sing (z :: (a, b, c, d, e)) where+ -- > STuple5 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing e -> Sing '(a, b, c, d, e)+ -- >+ -- > data instance Sing (z :: (a, b, c, d, e, f)) where+ -- > STuple6 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing e -> Sing f+ -- > -> Sing '(a, b, c, d, e, f)+ -- >+ -- > data instance Sing (z :: (a, b, c, d, e, f, g)) where+ -- > STuple7 :: Sing a -> Sing b -> Sing c -> Sing d -> Sing e -> Sing f+ -- > -> Sing g -> Sing '(a, b, c, d, e, f, g)++ -- * Singleton type synonyms++ -- | These synonyms are all kind-restricted synonyms of 'Sing'.+ -- For example 'SBool' requires an argument of kind 'Bool'.+ SBool, SList, SMaybe, SEither,+ STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7,++ -- * Functions working with 'Bool'+ If, sIf, Not, sNot, (:&&), (:||), (%:&&), (%:||),++ -- * Functions working with lists+ Head, Tail, (:++), (%:++),++ -- * Singleton equality+ module Data.Singletons.Eq,++ -- * Other datatypes+ Maybe_, sMaybe_,+ Either_, sEither_,+ Fst, sFst, Snd, sSnd, Curry, sCurry, Uncurry, sUncurry+ ) where++import Data.Singletons+import Data.Singletons.Bool+import Data.Singletons.List+import Data.Singletons.Maybe+import Data.Singletons.Either+import Data.Singletons.Tuple+import Data.Singletons.Eq+import Data.Singletons.Core
Data/Singletons/Promote.hs view
@@ -12,29 +12,32 @@ module Data.Singletons.Promote where -import Language.Haskell.TH+import Language.Haskell.TH hiding ( Q, cxt )+import Language.Haskell.TH.Syntax ( falseName, trueName, Quasi(..) ) import Data.Singletons.Util-import Data.Singletons.Exports import GHC.Exts (Any)+import GHC.TypeLits (Symbol) import Prelude hiding (exp) import qualified Data.Map as Map import qualified Data.Set as Set import Control.Monad-import Control.Monad.Writer hiding (Any) import Data.List -anyTypeName, falseName, trueName, boolName, andName, tyEqName, repName, ifName,- headName, tailName :: Name+anyTypeName, boolName, andName, tyEqName, repName, ifName,+ headName, tailName, symbolName :: Name anyTypeName = ''Any-falseName = 'False-trueName = 'True boolName = ''Bool andName = mkName "&&"-tyEqName = mkName ":==:"+#if __GLASGOW_HASKELL__ >= 707+tyEqName = mkName "=="+#else+tyEqName = mkName ":=="+#endif repName = mkName "Rep"-ifName = ''If-headName = ''Head-tailName = ''Tail+ifName = mkName "If"+headName = mkName "Head"+tailName = mkName "Tail"+symbolName = ''Symbol falseTy :: Type falseTy = promoteDataCon falseName@@ -57,14 +60,7 @@ tailTyFam :: Type tailTyFam = ConT tailName -genPromotions :: [Name] -> Q [Dec]-genPromotions names = do- checkForRep names- infos <- mapM reifyWithWarning names- decls <- mapM promoteInfo infos- return $ concat decls--promoteInfo :: Info -> Q [Dec]+promoteInfo :: Quasi q => Info -> q [Dec] promoteInfo (ClassI _dec _instances) = fail "Promotion of class info not supported" promoteInfo (ClassOpI _name _ty _className _fixity) =@@ -83,11 +79,13 @@ fail "Promotion of type variable info not supported" promoteDataCon :: Name -> Type-promoteDataCon name =- if isTupleName name- then PromotedTupleT (tupleDegree $ nameBase name)- else PromotedT name+promoteDataCon name+ | Just degree <- tupleNameDegree_maybe name+ = PromotedTupleT degree + | otherwise+ = PromotedT name+ promoteValName :: Name -> Name promoteValName n | nameBase n == "undefined" = anyTypeName@@ -96,16 +94,19 @@ promoteVal :: Name -> Type promoteVal = ConT . promoteValName -promoteType :: Type -> Q Kind+promoteType :: Quasi q => Type -> q Kind -- We don't need to worry about constraints: they are used to express -- static guarantees at runtime. But, because we don't need to do -- anything special to keep static guarantees at compile time, we don't -- need to promote them. promoteType (ForallT _tvbs _ ty) = promoteType ty -- ForallKinds promoteType (VarT name) = return $ VarT name-promoteType (ConT name) = return $ if (nameBase name) == "TypeRep" ||- (nameBase name) == (nameBase repName)- then StarT else ConT name+promoteType (ConT name) = return $+ case nameBase name of+ "TypeRep" -> StarT+ "String" -> ConT symbolName+ x | x == nameBase repName -> StarT+ | otherwise -> ConT name promoteType (TupleT n) = return $ TupleT n promoteType (UnboxedTupleT _n) = fail "Promotion of unboxed tuples not supported" promoteType ArrowT = return ArrowT@@ -128,21 +129,28 @@ -- a table to keep track of variable->type mappings type TypeTable = Map.Map Name Type --- Promote each declaration in a splice-promote :: Q [Dec] -> Q [Dec]+-- | Promote every declaration given to the type level, retaining the originals.+promote :: Quasi q => q [Dec] -> q [Dec] promote qdec = do decls <- qdec (promDecls, _) <- promoteDecs decls return $ decls ++ promDecls -checkForRep :: [Name] -> Q ()+-- | Promote each declaration, discarding the originals.+promoteOnly :: Quasi q => q [Dec] -> q [Dec]+promoteOnly qdec = do+ decls <- qdec+ (promDecls, _) <- promoteDecs decls+ return promDecls++checkForRep :: Quasi q => [Name] -> q () checkForRep names = when (any ((== nameBase repName) . nameBase) names) (fail $ "A data type named <<Rep>> is a special case.\n" ++ "Promoting it will not work as expected.\n" ++ "Please choose another name for your data type.") -checkForRepInDecls :: [Dec] -> Q ()+checkForRepInDecls :: Quasi q => [Dec] -> q () checkForRepInDecls decls = checkForRep (map extractNameFromDec decls) where extractNameFromDec :: Dec -> Name@@ -166,7 +174,7 @@ -- parameters before producing the type family declaration. -- At this point, any function written without a type signature is rejected -- and removed.-promoteDecs :: [Dec] -> Q ([Dec], [Name])+promoteDecs :: Quasi q => [Dec] -> q ([Dec], [Name]) promoteDecs decls = do checkForRepInDecls decls let vartbl = Map.empty@@ -182,24 +190,24 @@ #endif (Set.fromList names) noTypeSigsPro = map promoteValName noTypeSigs- newDecls' = foldl (\decls name ->- filter (not . (containsName name)) decls)+ newDecls' = foldl (\bad_decls name ->+ filter (not . (containsName name)) bad_decls) (concat newDecls) (noTypeSigs ++ noTypeSigsPro)- mapM_ (\n -> reportWarning $ "No type binding for " ++ (show (nameBase n)) ++- "; removing all declarations including it")+ mapM_ (\n -> qReportWarning $ "No type binding for " ++ (show (nameBase n)) +++ "; removing all declarations including it") noTypeSigs return (newDecls' ++ moreNewDecls, noTypeSigs) --- produce instances for (:==:) from the given types-promoteEqInstances :: [Name] -> Q [Dec]+-- | Produce instances for '(:==)' (type-level equality) from the given types+promoteEqInstances :: Quasi q => [Name] -> q [Dec] promoteEqInstances = concatMapM promoteEqInstance --- produce instance for (:==:) from the given type-promoteEqInstance :: Name -> Q [Dec]+-- | Produce an instance for '(:==)' (type-level equality) from the given type+promoteEqInstance :: Quasi q => Name -> q [Dec] promoteEqInstance name = do (_tvbs, cons) <- getDataD "I cannot make an instance of (:==:) for it." name #if __GLASGOW_HASKELL__ >= 707- vars <- replicateM (length _tvbs) (newName "k")+ vars <- replicateM (length _tvbs) (qNewName "k") let tyvars = map VarT vars kind = foldType (ConT name) tyvars inst_decs <- mkEqTypeInstance kind cons@@ -212,28 +220,30 @@ #if __GLASGOW_HASKELL__ >= 707 -- produce a closed type family helper and the instance--- for (:==:) over the given list of ctors-mkEqTypeInstance :: Kind -> [Con] -> Q [Dec]+-- for (:==) over the given list of ctors+mkEqTypeInstance :: Quasi q => Kind -> [Con] -> q [Dec] mkEqTypeInstance kind cons = do helperName <- newUniqueName "Equals"- aName <- newName "a"- bName <- newName "b"- closedFam <- closedTypeFamilyKindD helperName- [ KindedTV aName kind- , KindedTV bName kind ]- boolTy- (map mk_branch cons ++ [false_case])- let eqInst = TySynInstD tyEqName (TySynEqn [ SigT (VarT aName) kind+ aName <- qNewName "a"+ bName <- qNewName "b"+ true_branches <- mapM mk_branch cons+ false_branch <- false_case+ let closedFam = ClosedTypeFamilyD helperName+ [ KindedTV aName kind+ , KindedTV bName kind ]+ (Just boolTy)+ (true_branches ++ [false_branch])+ eqInst = TySynInstD tyEqName (TySynEqn [ SigT (VarT aName) kind , SigT (VarT bName) kind ] (foldType (ConT helperName) [VarT aName, VarT bName])) return [closedFam, eqInst] - where mk_branch :: Con -> Q TySynEqn+ where mk_branch :: Quasi q => Con -> q TySynEqn mk_branch con = do let (name, numArgs) = extractNameArgs con- lnames <- replicateM numArgs (newName "a")- rnames <- replicateM numArgs (newName "b")+ lnames <- replicateM numArgs (qNewName "a")+ rnames <- replicateM numArgs (qNewName "b") let lvars = map VarT lnames rvars = map VarT rnames ltype = foldType (PromotedT name) lvars@@ -242,10 +252,10 @@ result = tyAll results return $ TySynEqn [ltype, rtype] result - false_case :: Q TySynEqn+ false_case :: Quasi q => q TySynEqn false_case = do- lvar <- newName "a"- rvar <- newName "b"+ lvar <- qNewName "a"+ rvar <- qNewName "b" return $ TySynEqn [SigT (VarT lvar) kind, SigT (VarT rvar) kind] falseTy tyAll :: [Type] -> Type -- "all" at the type level@@ -255,14 +265,14 @@ #else --- produce the type instance for (:==:) for the given pair of constructors-mkEqTypeInstance :: (Con, Con) -> Q Dec+-- produce the type instance for (:==) for the given pair of constructors+mkEqTypeInstance :: Quasi q => (Con, Con) -> q Dec mkEqTypeInstance (c1, c2) = if c1 == c2 then do let (name, numArgs) = extractNameArgs c1- lnames <- replicateM numArgs (newName "a")- rnames <- replicateM numArgs (newName "b")+ lnames <- replicateM numArgs (qNewName "a")+ rnames <- replicateM numArgs (qNewName "b") let lvars = map VarT lnames rvars = map VarT rnames return $ TySynInstD@@ -274,8 +284,8 @@ else do let (lname, lNumArgs) = extractNameArgs c1 (rname, rNumArgs) = extractNameArgs c2- lnames <- replicateM lNumArgs (newName "a")- rnames <- replicateM rNumArgs (newName "b")+ lnames <- replicateM lNumArgs (qNewName "a")+ rnames <- replicateM rNumArgs (qNewName "b") return $ TySynInstD tyEqName [foldType (PromotedT lname) (map VarT lnames),@@ -295,20 +305,20 @@ #else type PromoteTable = Map.Map Name Int #endif-type PromoteQ = QWithAux PromoteTable+type PromoteQ q = QWithAux PromoteTable q -- used when a type is declared as a type synonym, not a type family -- no need to declare "type family ..." for these typeSynonymFlag :: Int typeSynonymFlag = -1 -promoteDec :: TypeTable -> Dec -> PromoteQ [Dec]+promoteDec :: Quasi q => TypeTable -> Dec -> PromoteQ q [Dec] promoteDec vars (FunD name clauses) = do let proName = promoteValName name vars' = Map.insert name (promoteVal name) vars numArgs = getNumPats (head clauses) -- count the parameters -- Haskell requires all clauses to have the same number of parameters- (eqns, instDecls) <- lift $ evalForPair $+ (eqns, instDecls) <- evalForPair $ mapM (promoteClause vars' proName) clauses #if __GLASGOW_HASKELL__ >= 707 addBinding name (numArgs, eqns) -- remember the number of parameters and the eqns@@ -324,16 +334,16 @@ when (length decs > 0) (fail $ "Promotion of global variable with <<where>> clause " ++ "not yet supported")- (rhs, decls) <- lift $ evalForPair $ promoteBody vars body- (lhss, decls') <- lift $ evalForPair $ promoteTopLevelPat pat+ (rhs, decls) <- evalForPair $ promoteBody vars body+ (lhss, decls') <- evalForPair $ promoteTopLevelPat pat if any (flip containsName rhs) (map lhsName lhss) then -- definition is recursive. This means an infinite value. fail "Promotion of infinite terms not yet supported" else do -- definition is not recursive; just use "type" decls #if __GLASGOW_HASKELL__ >= 707- mapM (flip addBinding (typeSynonymFlag, [])) (map lhsRawName lhss)+ mapM_ (flip addBinding (typeSynonymFlag, [])) (map lhsRawName lhss) #else- mapM (flip addBinding typeSynonymFlag) (map lhsRawName lhss)+ mapM_ (flip addBinding typeSynonymFlag) (map lhsRawName lhss) #endif return $ (map (\(LHS _ nm hole) -> TySynD nm [] (hole rhs)) lhss) ++ decls ++ decls'@@ -362,6 +372,8 @@ promoteDec _vars (NewtypeInstD _cxt _name _tys _ctors _derivings) = fail "Promotion of newtype instances not yet supported" #if __GLASGOW_HASKELL__ >= 707+promoteDec _vars (RoleAnnotD _name _roles) =+ return [] -- silently ignore role annotations, as they're harmless here promoteDec _vars (ClosedTypeFamilyD _name _tvs _mkind _eqns) = fail "Promotion of closed type families not yet supported" promoteDec _vars (TySynInstD _name _eqn) =@@ -371,25 +383,25 @@ fail "Promotion of type synonym instances not yet supported" -- only need to check if the datatype derives Eq. The rest is automatic.-promoteDataD :: TypeTable -> Cxt -> Name -> [TyVarBndr] -> [Con] ->- [Name] -> PromoteQ [Dec]+promoteDataD :: Quasi q => TypeTable -> Cxt -> Name -> [TyVarBndr] -> [Con] ->+ [Name] -> PromoteQ q [Dec] promoteDataD _vars _cxt _name _tvbs ctors derivings = if any (\n -> (nameBase n) == "Eq") derivings then do #if __GLASGOW_HASKELL__ >= 707- kvs <- replicateM (length _tvbs) (lift $ newName "k")- inst_decs <- lift $ mkEqTypeInstance (foldType (ConT _name) (map VarT kvs)) ctors+ kvs <- replicateM (length _tvbs) (qNewName "k")+ inst_decs <- mkEqTypeInstance (foldType (ConT _name) (map VarT kvs)) ctors return inst_decs #else let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]- lift $ mapM mkEqTypeInstance pairs+ mapM mkEqTypeInstance pairs #endif else return [] -- the actual promotion is automatic -- second pass through declarations to deal with type signatures -- returns the new declarations and the list of names that have been -- processed-promoteDec' :: PromoteTable -> Dec -> Q ([Dec], [Name])+promoteDec' :: Quasi q => PromoteTable -> Dec -> q ([Dec], [Name]) promoteDec' tab (SigD name ty) = case Map.lookup name tab of Nothing -> fail $ "Type declaration is missing its binding: " ++ (show name) #if __GLASGOW_HASKELL__ >= 707@@ -404,7 +416,7 @@ let ks = unravel k (argKs, resultKs) = splitAt numArgs ks -- divide by uniformity resultK <- ravel resultKs -- rebuild the arrow kind- tyvarNames <- mapM newName (replicate (length argKs) "a")+ tyvarNames <- mapM qNewName (replicate (length argKs) "a") #if __GLASGOW_HASKELL__ >= 707 return ([ClosedTypeFamilyD (promoteValName name) (zipWith KindedTV tyvarNames argKs)@@ -421,7 +433,7 @@ let ks = unravel k2 in k1 : ks unravel k = [k] - ravel :: [Kind] -> Q Kind+ ravel :: Quasi q => [Kind] -> q Kind ravel [] = fail "Internal error: raveling nil" ravel [k] = return k ravel (h:t) = do@@ -430,14 +442,14 @@ promoteDec' _ _ = return ([], []) #if __GLASGOW_HASKELL__ >= 707-promoteClause :: TypeTable -> Name -> Clause -> QWithDecs TySynEqn+promoteClause :: Quasi q => TypeTable -> Name -> Clause -> QWithDecs q TySynEqn #else-promoteClause :: TypeTable -> Name -> Clause -> QWithDecs Dec+promoteClause :: Quasi q => TypeTable -> Name -> Clause -> QWithDecs q Dec #endif promoteClause vars _name (Clause pats body []) = do -- promoting the patterns creates variable bindings. These are passed -- to the function promoted the RHS- (types, vartbl) <- lift $ evalForPair $ mapM promotePat pats+ (types, vartbl) <- evalForPair $ mapM promotePat pats let vars' = Map.union vars vartbl ty <- promoteBody vars' body #if __GLASGOW_HASKELL__ >= 707@@ -459,7 +471,7 @@ -- because type families have type patterns as their LHS. However, -- it is not possible to use type patterns at the top level, so we -- have to use other techniques.-promoteTopLevelPat :: Pat -> QWithDecs [TopLevelLHS]+promoteTopLevelPat :: Quasi q => Pat -> QWithDecs q [TopLevelLHS] promoteTopLevelPat (LitP _) = fail "Cannot declare a global literal." promoteTopLevelPat (VarP name) = return [LHS name (promoteValName name) id] promoteTopLevelPat (TupP pats) = case length pats of@@ -472,23 +484,23 @@ -- to promote a constructor pattern, we need to create extraction type -- families to pull out the individual arguments of the constructor promoteTopLevelPat (ConP name pats) = do- ctorInfo <- lift $ reifyWithWarning name- (ctorType, argTypes) <- lift $ extractTypes ctorInfo+ ctorInfo <- reifyWithWarning name+ (ctorType, argTypes) <- extractTypes ctorInfo when (length argTypes /= length pats) $ fail $ "Inconsistent data constructor pattern: " ++ (show name) ++ " " ++ (show pats)- kind <- lift $ promoteType ctorType- argKinds <- lift $ mapM promoteType argTypes- extractorNames <- lift $ replicateM (length pats) (newUniqueName "Extract")+ kind <- promoteType ctorType+ argKinds <- mapM promoteType argTypes+ extractorNames <- replicateM (length pats) (newUniqueName "Extract") - varName <- lift $ newName "a"- zipWithM (\nm arg -> addElement $ FamilyD TypeFam+ varName <- qNewName "a"+ zipWithM_ (\nm arg -> addElement $ FamilyD TypeFam nm [KindedTV varName kind] (Just arg))- extractorNames argKinds- componentNames <- lift $ replicateM (length pats) (newName "a")- zipWithM (\extractorName componentName ->+ extractorNames argKinds+ componentNames <- replicateM (length pats) (qNewName "a")+ zipWithM_ (\extractorName componentName -> addElement $ mkTyFamInst extractorName [foldType (promoteDataCon name) (map VarT componentNames)]@@ -504,13 +516,13 @@ (hole . (AppT (ConT extractor)))) lhslist) promotedPats extractorNames- where extractTypes :: Info -> Q (Type, [Type])+ where extractTypes :: Quasi q => Info -> q (Type, [Type]) extractTypes (DataConI datacon _dataconTy tyname _fixity) = do tyinfo <- reifyWithWarning tyname extractTypesHelper datacon tyinfo extractTypes _ = fail "Internal error: unexpected Info in extractTypes" - extractTypesHelper :: Name -> Info -> Q (Type, [Type])+ extractTypesHelper :: Quasi q => Name -> Info -> q (Type, [Type]) extractTypesHelper datacon (TyConI (DataD _cxt tyname tvbs cons _derivs)) = let mcon = find ((== datacon) . fst . extractNameArgs) cons in@@ -533,10 +545,10 @@ promoteTopLevelPat (ParensP _) = fail "Unresolved infix constructors not supported" promoteTopLevelPat (TildeP pat) = do- lift $ reportWarning "Lazy pattern converted into regular pattern in promotion"+ qReportWarning "Lazy pattern converted into regular pattern in promotion" promoteTopLevelPat pat promoteTopLevelPat (BangP pat) = do- lift $ reportWarning "Strict pattern converted into regular pattern in promotion"+ qReportWarning "Strict pattern converted into regular pattern in promotion" promoteTopLevelPat pat promoteTopLevelPat (AsP _name _pat) = fail "Promotion of aliased patterns at top level not yet supported"@@ -555,20 +567,20 @@ LHS raw nm (hole . (AppT headTyFam) . extractFn)) lhss)) id promotedPats promoteTopLevelPat (SigP pat _) = do- lift $ reportWarning $ "Promotion of explicit type annotation in pattern " +++ qReportWarning $ "Promotion of explicit type annotation in pattern " ++ "not yet supported." promoteTopLevelPat pat promoteTopLevelPat (ViewP _ _) = fail "Promotion of view patterns not yet supported" -type TypesQ = QWithAux TypeTable+type TypesQ q = QWithAux TypeTable q -- promotes a term pattern into a type pattern, accumulating variable -- binding in the auxiliary TypeTable-promotePat :: Pat -> TypesQ Type-promotePat (LitP lit) = fail $ "Promoting literals not supported: " ++ (show lit)+promotePat :: Quasi q => Pat -> TypesQ q Type+promotePat (LitP lit) = promoteLit lit promotePat (VarP name) = do- tyVar <- lift $ newName (nameBase name)+ tyVar <- qNewName (nameBase name) addBinding name (VarT tyVar) return $ VarT tyVar promotePat (TupP pats) = do@@ -585,42 +597,42 @@ promotePat (UInfixP _ _ _) = fail "Unresolved infix constructions not supported" promotePat (ParensP _) = fail "Unresolved infix constructions not supported" promotePat (TildeP pat) = do- lift $ reportWarning "Lazy pattern converted into regular pattern in promotion"+ qReportWarning "Lazy pattern converted into regular pattern in promotion" promotePat pat promotePat (BangP pat) = do- lift $ reportWarning "Strict pattern converted into regular pattern in promotion"+ qReportWarning "Strict pattern converted into regular pattern in promotion" promotePat pat promotePat (AsP name pat) = do ty <- promotePat pat addBinding name ty return ty promotePat WildP = do- name <- lift $ newName "z"+ name <- qNewName "z" return $ VarT name promotePat (RecP _ _) = fail "Promotion of record patterns not yet supported" promotePat (ListP pats) = do types <- mapM promotePat pats return $ foldr (\h t -> AppT (AppT PromotedConsT h) t) PromotedNilT types promotePat (SigP pat _) = do- lift $ reportWarning $ "Promotion of explicit type annotation in pattern " +++ qReportWarning $ "Promotion of explicit type annotation in pattern " ++ "not yet supported" promotePat pat promotePat (ViewP _ _) = fail "View patterns not yet supported" -- promoting a body may produce auxiliary declarations. Accumulate these.-type QWithDecs = QWithAux [Dec]+type QWithDecs q = QWithAux [Dec] q -promoteBody :: TypeTable -> Body -> QWithDecs Type+promoteBody :: Quasi q => TypeTable -> Body -> QWithDecs q Type promoteBody vars (NormalB exp) = promoteExp vars exp promoteBody _vars (GuardedB _) = fail "Promoting guards in patterns not yet supported" -promoteExp :: TypeTable -> Exp -> QWithDecs Type+promoteExp :: Quasi q => TypeTable -> Exp -> QWithDecs q Type promoteExp vars (VarE name) = case Map.lookup name vars of Just ty -> return ty Nothing -> return $ promoteVal name promoteExp _vars (ConE name) = return $ promoteDataCon name-promoteExp _vars (LitE _lit) = fail "Promotion of literal expressions not supported"+promoteExp _vars (LitE lit) = promoteLit lit promoteExp vars (AppE exp1 exp2) = do ty1 <- promoteExp vars exp1 ty2 <- promoteExp vars exp2@@ -667,3 +679,11 @@ fail "Promotion of record construction not yet supported" promoteExp _vars (RecUpdE _exp _fields) = fail "Promotion of record updates not yet supported"++promoteLit :: Monad m => Lit -> m Type+promoteLit (IntegerL n)+ | n >= 0 = return $ LitT (NumTyLit n)+ | otherwise = fail ("Promoting negative integers not supported: " ++ (show n))+promoteLit (StringL str) = return $ LitT (StrTyLit str)+promoteLit lit =+ fail ("Only string and natural number literals can be promoted: " ++ show lit)
Data/Singletons/Singletons.hs view
@@ -6,20 +6,26 @@ This file contains functions to refine constructs to work with singleton types. It is an internal module to the singletons package. -}-{-# LANGUAGE PatternGuards, TemplateHaskell, CPP #-}+{-# LANGUAGE TemplateHaskell, CPP, TupleSections #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} module Data.Singletons.Singletons where -import Language.Haskell.TH-import Data.Singletons.Exports+import Prelude hiding ( exp )+import Language.Haskell.TH hiding ( cxt )+import Language.Haskell.TH.Syntax (falseName, trueName, Quasi(..)) import Data.Singletons.Util import Data.Singletons.Promote import qualified Data.Map as Map import Control.Monad-import Control.Monad.Writer-import Data.List+import Control.Applicative+import Data.Singletons.Types +#if __GLASGOW_HASKELL__ >= 707+import Data.Proxy+import Data.Type.Equality+#endif+ -- map to track bound variables type ExpTable = Map.Map Name Exp @@ -30,32 +36,38 @@ -- a list of argument types extracted from a type application type TypeContext = [Type] -singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName,- demoteName, singKindClassName, singInstanceMethName, singInstanceTyConName,- singInstanceDataConName, sEqClassName, sEqMethName, sconsName, snilName,- smartSconsName, smartSnilName, sIfName, undefinedName, kindParamName,- ofKindName :: Name-singFamilyName = ''Sing-isSingletonName = ''SingI-forgettableName = ''SingE-comboClassName = ''SingRep-witnessName = 'sing-forgetName = 'fromSing-demoteName = ''DemoteRep-singKindClassName = ''SingKind-singInstanceMethName = 'singInstance-singInstanceTyConName = ''SingInstance-singInstanceDataConName = 'SingInstance+singFamilyName, singIName, singMethName, demoteRepName, singKindClassName, + sEqClassName, sEqMethName, sconsName, snilName, sIfName, undefinedName,+ kProxyDataName, kProxyTypeName, someSingTypeName, someSingDataName,+ nilName, consName, sListName, eqName, sDecideClassName, sDecideMethName,+ provedName, disprovedName, reflName, toSingName, fromSingName, listName :: Name+singFamilyName = mkName "Sing"+singIName = mkName "SingI"+singMethName = mkName "sing"+toSingName = mkName "toSing"+fromSingName = mkName "fromSing"+demoteRepName = mkName "DemoteRep"+singKindClassName = mkName "SingKind" sEqClassName = mkName "SEq"-sEqMethName = mkName "%==%"-sconsName = mkName "SCons"-snilName = mkName "SNil"-smartSconsName = mkName "sCons"-smartSnilName = mkName "sNil"+sEqMethName = mkName "%:==" sIfName = mkName "sIf" undefinedName = 'undefined-kindParamName = 'KindParam-ofKindName = ''KindIs+sconsName = mkName "SCons"+snilName = mkName "SNil" +kProxyDataName = 'KProxy+kProxyTypeName = ''KProxy+someSingTypeName = mkName "SomeSing"+someSingDataName = mkName "SomeSing"+nilName = '[]+consName = '(:)+listName = ''[]+sListName = mkName "SList"+eqName = ''Eq+sDecideClassName = mkName "SDecide"+sDecideMethName = mkName "%~"+provedName = 'Proved+disprovedName = 'Disproved+reflName = 'Refl mkTupleName :: Int -> Name mkTupleName n = mkName $ "STuple" ++ (show n)@@ -66,32 +78,21 @@ singKindConstraint :: Kind -> Pred singKindConstraint k = ClassP singKindClassName [kindParam k] -singInstanceMeth :: Exp-singInstanceMeth = VarE singInstanceMethName--singInstanceTyCon :: Type-singInstanceTyCon = ConT singInstanceTyConName--singInstanceDataCon :: Exp-singInstanceDataCon = ConE singInstanceDataConName--singInstancePat :: Pat-singInstancePat = ConP singInstanceDataConName []- demote :: Type-demote = ConT demoteName+demote = ConT demoteRepName singDataConName :: Name -> Name-singDataConName nm = case nameBase nm of- "[]" -> snilName- ":" -> sconsName- tuple | isTupleString tuple -> mkTupleName (tupleDegree tuple)- _ -> prefixUCName "S" ":%" nm+singDataConName nm+ | nm == nilName = snilName+ | nm == consName = sconsName+ | Just degree <- tupleNameDegree_maybe nm = mkTupleName degree+ | otherwise = prefixUCName "S" ":%" nm singTyConName :: Name -> Name-singTyConName name | nameBase name == "[]" = mkName "SList"- | isTupleName name = mkTupleName (tupleDegree $ nameBase name)- | otherwise = prefixUCName "S" ":%" name+singTyConName name+ | name == listName = sListName+ | Just degree <- tupleNameDegree_maybe name = mkTupleName degree+ | otherwise = prefixUCName "S" ":%" name singClassName :: Name -> Name singClassName = singTyConName@@ -99,12 +100,6 @@ singDataCon :: Name -> Exp singDataCon = ConE . singDataConName -smartConName :: Name -> Name-smartConName = locase . singDataConName--smartCon :: Name -> Exp-smartCon = VarE . smartConName- singValName :: Name -> Name singValName n | nameBase n == "undefined" = undefinedName@@ -114,17 +109,20 @@ singVal = VarE . singValName kindParam :: Kind -> Type-kindParam k = SigT (ConT kindParamName) (AppT (ConT ofKindName) k)+kindParam k = SigT (ConT kProxyDataName) (AppT (ConT kProxyTypeName) k) --- generate singleton definitions from an ADT-genSingletons :: [Name] -> Q [Dec]+-- | Generate singleton definitions from a type that is already defined.+-- For example, the singletons package itself uses+--+-- > $(genSingletons [''Bool, ''Maybe, ''Either, ''[]])+--+-- to generate singletons for Prelude types.+genSingletons :: Quasi q => [Name] -> q [Dec] genSingletons names = do checkForRep names- infos <- mapM reifyWithWarning names- decls <- mapM singInfo infos- return $ concat decls+ concatMapM (singInfo <=< reifyWithWarning) names -singInfo :: Info -> Q [Dec]+singInfo :: Quasi q => Info -> q [Dec] singInfo (ClassI _dec _instances) = fail "Singling of class info not supported" singInfo (ClassOpI _name _ty _className _fixity) =@@ -145,93 +143,72 @@ -- refine a constructor. the first parameter is the type variable that -- the singleton GADT is parameterized by -- runs in the QWithDecs monad because auxiliary declarations are produced-singCtor :: Type -> Con -> QWithDecs Con +singCtor :: Quasi q => Type -> Con -> QWithDecs q Con singCtor a = ctorCases+ -- monomorphic case (\name types -> do let sName = singDataConName name sCon = singDataCon name pCon = promoteDataCon name- indexNames <- lift $ replicateM (length types) (newName "n")+ indexNames <- replicateM (length types) (qNewName "n") let indices = map VarT indexNames- kinds <- lift $ mapM promoteType types- args <- lift $ buildArgTypes types indices+ kinds <- mapM promoteType types+ args <- buildArgTypes types indices let tvbs = zipWith KindedTV indexNames kinds- bareKindVars = filter isVarK kinds+ kindedIndices = zipWith SigT indices kinds -- SingI instance- addElement $ InstanceD ((map singKindConstraint bareKindVars) ++- (map (ClassP comboClassName . return) indices))- (AppT (ConT isSingletonName)- (foldType pCon (zipWith SigT indices kinds)))- [ValD (VarP witnessName)+ addElement $ InstanceD (map (ClassP singIName . listify) indices)+ (AppT (ConT singIName)+ (foldType pCon kindedIndices))+ [ValD (VarP singMethName) (NormalB $ foldExp sCon (replicate (length types)- (VarE witnessName)))+ (VarE singMethName))) []] - -- smart constructor type signature- smartConType <- lift $ conTypesToFunType indexNames args kinds- (AppT singFamily (foldType pCon indices))- addElement $ SigD (smartConName name) (liftOutForalls smartConType)- - -- smart constructor- let vars = map VarE indexNames- smartConBody = mkSingInstances vars (foldExp (singDataCon name) vars)- addElement $ FunD (smartConName name)- [Clause (map VarP indexNames)- (NormalB smartConBody)- []]- return $ ForallC tvbs- ((EqualP a (foldType (promoteDataCon name) indices)) :- (map (ClassP comboClassName . return) indices) ++- (map singKindConstraint bareKindVars))- (NormalC sName $ map (\ty -> (NotStrict,ty)) args))+ [EqualP a (foldType pCon indices)]+ (NormalC sName $ map (NotStrict,) args))++ -- polymorphic case (\_tvbs cxt ctor -> case cxt of _:_ -> fail "Singling of constrained constructors not yet supported"- [] -> singCtor a ctor)- where buildArgTypes :: [Type] -> [Type] -> Q [Type]+ [] -> singCtor a ctor) -- polymorphic constructors are handled just+ -- like monomorphic ones -- the polymorphism in+ -- the kind is automatic+ where buildArgTypes :: Quasi q => [Type] -> [Type] -> q [Type] buildArgTypes types indices = do- typeFns <- mapM (singType False) types+ typeFns <- mapM singType types return $ zipWith id typeFns indices - conTypesToFunType :: [Name] -> [Type] -> [Kind] -> Type -> Q Type- conTypesToFunType [] [] [] ret = return ret- conTypesToFunType (nm : nmtail) (ty : tytail) (k : ktail) ret = do- rhs <- conTypesToFunType nmtail tytail ktail ret - let innerty = AppT (AppT ArrowT ty) rhs- return $ ForallT [KindedTV nm k]- (if isVarK k then [singKindConstraint k] else [])- innerty- conTypesToFunType _ _ _ _ =- fail "Internal error in conTypesToFunType"-- mkSingInstances :: [Exp] -> Exp -> Exp- mkSingInstances [] exp = exp- mkSingInstances (var:tail) exp =- CaseE (AppE singInstanceMeth var)- [Match singInstancePat (NormalB $ mkSingInstances tail exp) []]+-- | Make promoted and singleton versions of all declarations given, retaining+-- the original declarations.+-- See <http://www.cis.upenn.edu/~eir/packages/singletons/README.html> for+-- further explanation.+singletons :: Quasi q => q [Dec] -> q [Dec]+singletons = (>>= singDecs True) --- refine the declarations given-singletons :: Q [Dec] -> Q [Dec]-singletons qdec = do- decls <- qdec- singDecs decls+-- | Make promoted and singleton versions of all declarations given, discarding+-- the original declarations.+singletonsOnly :: Quasi q => q [Dec] -> q [Dec]+singletonsOnly = (>>= singDecs False) -singDecs :: [Dec] -> Q [Dec]-singDecs decls = do+-- first parameter says whether or not to include original decls+singDecs :: Quasi q => Bool -> [Dec] -> q [Dec]+singDecs originals decls = do (promDecls, badNames) <- promoteDecs decls -- need to remove the bad names returned from promoteDecs newDecls <- mapM singDec (filter (\dec -> not $ or (map (\f -> f dec) (map containsName badNames))) decls)- return $ decls ++ promDecls ++ (concat newDecls)+ return $ (if originals then (decls ++) else id) $ promDecls ++ (concat newDecls) -singDec :: Dec -> Q [Dec]+singDec :: Quasi q => Dec -> q [Dec] singDec (FunD name clauses) = do let sName = singValName name vars = Map.singleton name (VarE sName)- liftM return $ funD sName (map (singClause vars) clauses)+ listify <$> FunD sName <$> (mapM (singClause vars) clauses) singDec (ValD _ (GuardedB _) _) = fail "Singling of definitions of values with a pattern guard not yet supported" singDec (ValD _ _ (_:_)) =@@ -253,11 +230,11 @@ singDec (InstanceD _cxt _ty _decs) = fail "Singling of class instance not yet supported" singDec (SigD name ty) = do- tyTrans <- singType True ty+ tyTrans <- singType ty return [SigD (singValName name) (tyTrans (promoteVal name))] singDec (ForeignD fgn) = let name = extractName fgn in do- reportWarning $ "Singling of foreign functions not supported -- " +++ qReportWarning $ "Singling of foreign functions not supported -- " ++ (show name) ++ " ignored" return [] where extractName :: Foreign -> Name@@ -267,7 +244,7 @@ | isUpcase name = return [InfixD fixity (singDataConName name)] | otherwise = return [InfixD fixity (singValName name)] singDec (PragmaD _prag) = do- reportWarning "Singling of pragmas not supported"+ qReportWarning "Singling of pragmas not supported" return [] singDec (FamilyD _flavour _name _tvbs _mkind) = fail "Singling of type and data families not yet supported"@@ -276,6 +253,8 @@ singDec (NewtypeInstD _cxt _name _tys _ctor _derivings) = fail "Singling of newtype instances not yet supported" #if __GLASGOW_HASKELL__ >= 707+singDec (RoleAnnotD _name _roles) =+ return [] -- silently ignore role annotations, as they're harmless singDec (ClosedTypeFamilyD _name _tvs _mkind _eqns) = fail "Singling of closed type families not yet supported" singDec (TySynInstD _name _eqns) =@@ -284,94 +263,185 @@ #endif fail "Singling of type family instances not yet supported" --- create instances of SEq for each type in the list-singEqInstances :: [Name] -> Q [Dec]+-- | Create instances of 'SEq' and type-level '(:==)' for each type in the list+singEqInstances :: Quasi q => [Name] -> q [Dec] singEqInstances = concatMapM singEqInstance --- create instance of SEq for the given *singleton* type-singEqInstance :: Name -> Q [Dec]+-- | Create instance of 'SEq' and type-level '(:==)' for the given type+singEqInstance :: Quasi q => Name -> q [Dec] singEqInstance name = do promotion <- promoteEqInstance name- (tvbs, cons) <- getDataD "I cannot make an instance of SEq for it." name+ dec <- singEqualityInstance sEqClassDesc name+ return $ dec : promotion++-- | Create instances of 'SEq' (only -- no instance for '(:==)', which 'SEq' generally+-- relies on) for each type in the list+singEqInstancesOnly :: Quasi q => [Name] -> q [Dec]+singEqInstancesOnly = concatMapM singEqInstanceOnly++-- | Create instances of 'SEq' (only -- no instance for '(:==)', which 'SEq' generally+-- relies on) for the given type+singEqInstanceOnly :: Quasi q => Name -> q [Dec]+singEqInstanceOnly name = listify <$> singEqualityInstance sEqClassDesc name++-- | Create instances of 'SDecide' for each type in the list+singDecideInstances :: Quasi q => [Name] -> q [Dec]+singDecideInstances = concatMapM singDecideInstance++-- | Create instance of SDecide for the given type+singDecideInstance :: Quasi q => Name -> q [Dec]+singDecideInstance name = listify <$> singEqualityInstance sDecideClassDesc name++-- generalized function for creating equality instances+singEqualityInstance :: Quasi q => EqualityClassDesc q -> Name -> q Dec+singEqualityInstance desc@(_, className, _) name = do+ (tvbs, cons) <- getDataD ("I cannot make an instance of " +++ show className ++ " for it.") name let tyvars = map (VarT . extractTvbName) tvbs kind = foldType (ConT name) tyvars- aName <- newName "a"+ aName <- qNewName "a" let aVar = VarT aName scons <- mapM (evalWithoutAux . singCtor aVar) cons- dec <- mkSingEqInstance kind scons- return $ dec : promotion+ mkEqualityInstance kind scons desc --- create an SEq instance for singletons of the given kind,--- with the given *singleton* constructors -mkSingEqInstance :: Kind -> [Con] -> Q Dec-mkSingEqInstance k ctors = do+-- making the SEq instance and the SDecide instance are rather similar,+-- so we generalize+type EqualityClassDesc q = ((Con, Con) -> q Clause, Name, Name)+sEqClassDesc, sDecideClassDesc :: Quasi q => EqualityClassDesc q+sEqClassDesc = (mkEqMethClause, sEqClassName, sEqMethName)+sDecideClassDesc = (mkDecideMethClause, sDecideClassName, sDecideMethName)++-- pass the *singleton* constructors, not the originals+mkEqualityInstance :: Quasi q => Kind -> [Con]+ -> EqualityClassDesc q -> q Dec+mkEqualityInstance k ctors (mkMeth, className, methName) = do let ctorPairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ]- sEqMethClauses <- mapM mkEqMethClause ctorPairs- return $ InstanceD (map (\k -> ClassP sEqClassName [kindParam k])- (getBareKinds ctors))- (AppT (ConT sEqClassName)+ methClauses <- if null ctors+ then mkEmptyMethClauses+ else mapM mkMeth ctorPairs+ return $ InstanceD (map (\kvar -> ClassP className [kindParam kvar])+ (getKindVars k))+ (AppT (ConT className) (kindParam k))- [FunD sEqMethName sEqMethClauses]- where mkEqMethClause :: (Con, Con) -> Q Clause- mkEqMethClause (c1, c2) =- if c1 == c2- then do- let (name, numArgs) = extractNameArgs c1- lnames <- replicateM numArgs (newName "a")- rnames <- replicateM numArgs (newName "b")- let lpats = map VarP lnames- rpats = map VarP rnames- lvars = map VarE lnames- rvars = map VarE rnames- return $ Clause- [ConP name lpats, ConP name rpats]- (NormalB $- allExp (zipWith (\l r -> foldExp (VarE sEqMethName) [l, r])- lvars rvars))- []- else do- let (lname, lNumArgs) = extractNameArgs c1- (rname, rNumArgs) = extractNameArgs c2- return $ Clause- [ConP lname (replicate lNumArgs WildP),- ConP rname (replicate rNumArgs WildP)]- (NormalB (singDataCon falseName))- []+ [FunD methName methClauses]+ where getKindVars :: Kind -> [Kind]+ getKindVars (AppT l r) = getKindVars l ++ getKindVars r+ getKindVars (VarT x) = [VarT x]+ getKindVars (ConT _) = []+ getKindVars StarT = []+ getKindVars other =+ error ("getKindVars sees an unusual kind: " ++ show other) - getBareKinds :: [Con] -> [Kind]- getBareKinds = foldl (\res -> ctorCases- (\_ _ -> res) -- must be a constant constructor- (\tvbs _ _ -> union res (filter isVarK $ map extractTvbKind tvbs)))- []+ mkEmptyMethClauses :: Quasi q => q [Clause]+ mkEmptyMethClauses = do+ a <- qNewName "a"+ return [Clause [VarP a, WildP] (NormalB (CaseE (VarE a) emptyMatches)) []] - allExp :: [Exp] -> Exp+mkEqMethClause :: Quasi q => (Con, Con) -> q Clause+mkEqMethClause (c1, c2)+ | lname == rname = do+ lnames <- replicateM lNumArgs (qNewName "a")+ rnames <- replicateM lNumArgs (qNewName "b")+ let lpats = map VarP lnames+ rpats = map VarP rnames+ lvars = map VarE lnames+ rvars = map VarE rnames+ return $ Clause+ [ConP lname lpats, ConP rname rpats]+ (NormalB $+ allExp (zipWith (\l r -> foldExp (VarE sEqMethName) [l, r])+ lvars rvars))+ []+ | otherwise =+ return $ Clause+ [ConP lname (replicate lNumArgs WildP),+ ConP rname (replicate rNumArgs WildP)]+ (NormalB (singDataCon falseName))+ []+ where allExp :: [Exp] -> Exp allExp [] = singDataCon trueName allExp [one] = one allExp (h:t) = AppE (AppE (singVal andName) h) (allExp t) + (lname, lNumArgs) = extractNameArgs c1+ (rname, rNumArgs) = extractNameArgs c2++mkDecideMethClause :: Quasi q => (Con, Con) -> q Clause+mkDecideMethClause (c1, c2)+ | lname == rname = + if lNumArgs == 0+ then return $ Clause [ConP lname [], ConP rname []]+ (NormalB (AppE (ConE provedName) (ConE reflName))) []+ else do+ lnames <- replicateM lNumArgs (qNewName "a")+ rnames <- replicateM lNumArgs (qNewName "b")+ contra <- qNewName "contra"+ let lpats = map VarP lnames+ rpats = map VarP rnames+ lvars = map VarE lnames+ rvars = map VarE rnames+ return $ Clause+ [ConP lname lpats, ConP rname rpats]+ (NormalB $+ CaseE (mkTupleExp $+ zipWith (\l r -> foldExp (VarE sDecideMethName) [l, r])+ lvars rvars)+ ((Match (mkTuplePat (replicate lNumArgs+ (ConP provedName [ConP reflName []])))+ (NormalB $ AppE (ConE provedName) (ConE reflName))+ []) :+ [Match (mkTuplePat (replicate i WildP +++ ConP disprovedName [VarP contra] :+ replicate (lNumArgs - i - 1) WildP))+ (NormalB $ AppE (ConE disprovedName)+ (LamE [ConP reflName []]+ (AppE (VarE contra)+ (ConE reflName))))+ [] | i <- [0..lNumArgs-1] ]))+ []+ + | otherwise =+ return $ Clause+ [ConP lname (replicate lNumArgs WildP),+ ConP rname (replicate rNumArgs WildP)]+ (NormalB (AppE (ConE disprovedName) (LamCaseE emptyMatches)))+ []++ where+ (lname, lNumArgs) = extractNameArgs c1+ (rname, rNumArgs) = extractNameArgs c2+ -- the first parameter is True when we're refining the special case "Rep" -- and false otherwise. We wish to consider the promotion of "Rep" to be * -- not a promoted data constructor.-singDataD :: Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> Q [Dec]+singDataD :: Quasi q => Bool -> Cxt -> Name -> [TyVarBndr] -> [Con] -> [Name] -> q [Dec] singDataD rep cxt name tvbs ctors derivings | (_:_) <- cxt = fail "Singling of constrained datatypes is not supported" | otherwise = do- aName <- newName "a"+ aName <- qNewName "z" let a = VarT aName let tvbNames = map extractTvbName tvbs k <- promoteType (foldType (ConT name) (map VarT tvbNames)) (ctors', ctorInstDecls) <- evalForPair $ mapM (singCtor a) ctors -- instance for SingKind+ fromSingClauses <- mapM mkFromSingClause ctors+ toSingClauses <- mapM mkToSingClause ctors let singKindInst =- InstanceD []+ InstanceD (map (singKindConstraint . VarT) tvbNames) (AppT (ConT singKindClassName) (kindParam k))- [FunD singInstanceMethName- (map mkSingInstanceClause ctors')]+ [ mkTyFamInst demoteRepName+ [kindParam k]+ (foldType (ConT name)+ (map (AppT demote . kindParam . VarT) tvbNames))+ , FunD fromSingName (fromSingClauses `orIfEmpty` emptyMethod aName)+ , FunD toSingName (toSingClauses `orIfEmpty` emptyMethod aName) ] -- SEq instance- sEqInst <- mkSingEqInstance k ctors'+ sEqInsts <- if elem eqName derivings+ then mapM (mkEqualityInstance k ctors') [sEqClassDesc, sDecideClassDesc]+ else return [] -- e.g. type SNat (a :: Nat) = Sing a let kindedSynInst =@@ -379,44 +449,52 @@ [KindedTV aName k] (AppT singFamily a) - -- SingE instance- forgetClauses <- mapM mkForgetClause ctors- let singEInst =- InstanceD []- (AppT (ConT forgettableName) (kindParam k))- [mkTyFamInst demoteName- [kindParam k]- (foldType (ConT name)- (map (\kv -> AppT demote (kindParam (VarT kv)))- tvbNames)),- FunD forgetName- forgetClauses]-- return $ (if (any (\n -> (nameBase n) == "Eq") derivings)- then (sEqInst :)- else id) $- (DataInstD [] singFamilyName [SigT a k] ctors' []) :- singEInst :- kindedSynInst :- singKindInst :- ctorInstDecls- where mkSingInstanceClause :: Con -> Clause- mkSingInstanceClause = ctor1Case- (\nm tys ->- Clause [ConP nm (replicate (length tys) WildP)]- (NormalB singInstanceDataCon) [])+ return $ (DataInstD [] singFamilyName [SigT a k] ctors' []) :+ kindedSynInst :+ singKindInst :+ sEqInsts +++ ctorInstDecls+ where -- in the Rep case, the names of the constructors are in the wrong scope+ -- (they're types, not datacons), so we have to reinterpret them.+ mkConName :: Name -> Name+ mkConName = if rep then reinterpret else id - mkForgetClause :: Con -> Q Clause- mkForgetClause c = do- let (name, numArgs) = extractNameArgs c- varNames <- replicateM numArgs (newName "a")- return $ Clause [ConP (singDataConName name) (map VarP varNames)]+ mkFromSingClause :: Quasi q => Con -> q Clause+ mkFromSingClause c = do+ let (cname, numArgs) = extractNameArgs c+ varNames <- replicateM numArgs (qNewName "b")+ return $ Clause [ConP (singDataConName cname) (map VarP varNames)] (NormalB $ foldExp- (ConE $ (if rep then reinterpret else id) name)- (map (AppE (VarE forgetName) . VarE) varNames))+ (ConE $ mkConName cname)+ (map (AppE (VarE fromSingName) . VarE) varNames)) [] -singKind :: Kind -> Q (Kind -> Kind)+ mkToSingClause :: Quasi q => Con -> q Clause+ mkToSingClause = ctor1Case $ \cname types -> do+ varNames <- mapM (const $ qNewName "b") types+ svarNames <- mapM (const $ qNewName "c") types+ promoted <- mapM promoteType types+ let recursiveCalls = zipWith mkRecursiveCall varNames promoted+ return $+ Clause [ConP (mkConName cname) (map VarP varNames)]+ (NormalB $+ multiCase recursiveCalls+ (map (ConP someSingDataName . listify . VarP)+ svarNames)+ (AppE (ConE someSingDataName)+ (foldExp (ConE (singDataConName cname))+ (map VarE svarNames))))+ []++ mkRecursiveCall :: Name -> Kind -> Exp+ mkRecursiveCall var_name ki =+ SigE (AppE (VarE toSingName) (VarE var_name))+ (AppT (ConT someSingDataName) (kindParam ki))++ emptyMethod :: Name -> [Clause]+ emptyMethod n = [Clause [VarP n] (NormalB $ CaseE (VarE n) emptyMatches) []]++singKind :: Quasi q => Kind -> q (Kind -> Kind) singKind (ForallT _ _ _) = fail "Singling of explicitly quantified kinds not yet supported" singKind (VarT _) = fail "Singling of kind variables not yet supported"@@ -428,7 +506,7 @@ singKind (AppT (AppT ArrowT k1) k2) = do k1fn <- singKind k1 k2fn <- singKind k2- k <- newName "k"+ k <- qNewName "k" return $ \f -> AppT (AppT ArrowT (k1fn (VarT k))) (k2fn (AppT f (VarT k))) singKind (AppT _ _) = fail "Singling of kind applications not yet supported" singKind (SigT _ _) =@@ -441,10 +519,9 @@ singKind StarT = return $ \k -> AppT (AppT ArrowT k) StarT singKind ConstraintT = fail "Singling of constraint kinds not yet supported" --- the first parameter is whether or not this type occurs in a positive position-singType :: Bool -> Type -> Q TypeFn-singType pos ty = do -- replace with singTypeRec [] pos ty after GHC bug #??? is fixed- sTypeFn <- singTypeRec [] pos ty+singType :: Quasi q => Type -> q TypeFn+singType ty = do -- replace with singTypeRec [] ty after GHC bug #??? is fixed+ sTypeFn <- singTypeRec [] ty return $ \inner_ty -> liftOutForalls $ sTypeFn inner_ty -- the lifts all foralls to the top-level@@ -467,67 +544,57 @@ mk_fun_ty (arg1:args) res = AppT (AppT ArrowT arg1) (mk_fun_ty args res) -- the first parameter is the list of types the current type is applied to--- the second parameter is whether or not this type occurs in a positive position-singTypeRec :: TypeContext -> Bool -> Type -> Q TypeFn-singTypeRec (_:_) _pos (ForallT _ _ _) =+singTypeRec :: Quasi q => TypeContext -> Type -> q TypeFn+singTypeRec (_:_) (ForallT _ _ _) = fail "I thought this was impossible in Haskell. Email me at eir@cis.upenn.edu with your code if you see this message."-singTypeRec [] pos (ForallT _ [] ty) = -- Sing makes handling foralls automatic- singTypeRec [] pos ty-singTypeRec ctx pos (ForallT _tvbs cxt innerty) = do+singTypeRec [] (ForallT _ [] ty) = -- Sing makes handling foralls automatic+ singTypeRec [] ty+singTypeRec ctx (ForallT _tvbs cxt innerty) = do cxt' <- singContext cxt- innerty' <- singTypeRec ctx pos innerty+ innerty' <- singTypeRec ctx innerty return $ \ty -> ForallT [] cxt' (innerty' ty)-singTypeRec (_:_) _pos (VarT _) =+singTypeRec (_:_) (VarT _) = fail "Singling of type variables of arrow kinds not yet supported"-singTypeRec [] _pos (VarT _name) = +singTypeRec [] (VarT _name) = return $ \ty -> AppT singFamily ty-singTypeRec _ctx _pos (ConT _name) = -- we don't need to process the context with Sing+singTypeRec _ctx (ConT _name) = -- we don't need to process the context with Sing return $ \ty -> AppT singFamily ty-singTypeRec _ctx _pos (TupleT _n) = -- just like ConT+singTypeRec _ctx (TupleT _n) = -- just like ConT return $ \ty -> AppT singFamily ty-singTypeRec _ctx _pos (UnboxedTupleT _n) =+singTypeRec _ctx (UnboxedTupleT _n) = fail "Singling of unboxed tuple types not yet supported"-singTypeRec ctx pos ArrowT = case ctx of+singTypeRec ctx ArrowT = case ctx of [ty1, ty2] -> do- t <- newName "t"- sty1 <- singTypeRec [] (not pos) ty1- sty2 <- singTypeRec [] pos ty2+ t <- qNewName "t"+ sty1 <- singTypeRec [] ty1+ sty2 <- singTypeRec [] ty2 k1 <- promoteType ty1- -- need a SingKind constraint on all kind variables that appear- -- outside of any kind constructor in a negative position (to the- -- left of an odd number of arrows)- let polykinds = extractPolyKinds (not pos) k1 return (\f -> ForallT [KindedTV t k1]- (map (\k -> ClassP singKindClassName [kindParam k]) polykinds)+ [] (AppT (AppT ArrowT (sty1 (VarT t))) (sty2 (AppT f (VarT t)))))- where extractPolyKinds :: Bool -> Kind -> [Kind]- extractPolyKinds pos (AppT (AppT ArrowT k1) k2) =- (extractPolyKinds (not pos) k1) ++ (extractPolyKinds pos k2)- extractPolyKinds False (VarT k) = [VarT k]- extractPolyKinds _ _ = [] _ -> fail "Internal error in Sing: converting ArrowT with improper context"-singTypeRec _ctx _pos ListT =+singTypeRec _ctx ListT = return $ \ty -> AppT singFamily ty-singTypeRec ctx pos (AppT ty1 ty2) =- singTypeRec (ty2 : ctx) pos ty1 -- recur with the ty2 in the applied context-singTypeRec _ctx _pos (SigT _ty _knd) =+singTypeRec ctx (AppT ty1 ty2) =+ singTypeRec (ty2 : ctx) ty1 -- recur with the ty2 in the applied context+singTypeRec _ctx (SigT _ty _knd) = fail "Singling of types with explicit kinds not yet supported"-singTypeRec _ctx _pos (LitT _) = fail "Singling of type-level literals not yet supported"-singTypeRec _ctx _pos (PromotedT _) =+singTypeRec _ctx (LitT _) = fail "Singling of type-level literals not yet supported"+singTypeRec _ctx (PromotedT _) = fail "Singling of promoted data constructors not yet supported"-singTypeRec _ctx _pos (PromotedTupleT _) =+singTypeRec _ctx (PromotedTupleT _) = fail "Singling of type-level tuples not yet supported"-singTypeRec _ctx _pos PromotedNilT = fail "Singling of promoted nil not yet supported"-singTypeRec _ctx _pos PromotedConsT = fail "Singling of type-level cons not yet supported"-singTypeRec _ctx _pos StarT = fail "* used as type"-singTypeRec _ctx _pos ConstraintT = fail "Constraint used as type"+singTypeRec _ctx PromotedNilT = fail "Singling of promoted nil not yet supported"+singTypeRec _ctx PromotedConsT = fail "Singling of type-level cons not yet supported"+singTypeRec _ctx StarT = fail "* used as type"+singTypeRec _ctx ConstraintT = fail "Constraint used as type" -- refine a constraint context-singContext :: Cxt -> Q Cxt+singContext :: Quasi q => Cxt -> q Cxt singContext = mapM singPred -singPred :: Pred -> Q Pred+singPred :: Quasi q => Pred -> q Pred singPred (ClassP name tys) = do kis <- mapM promoteType tys let sName = singClassName name@@ -535,18 +602,18 @@ singPred (EqualP _ty1 _ty2) = fail "Singling of type equality constraints not yet supported" -singClause :: ExpTable -> Clause -> Q Clause+singClause :: Quasi q => ExpTable -> Clause -> q Clause singClause vars (Clause pats (NormalB exp) []) = do (sPats, vartbl) <- evalForPair $ mapM (singPat Parameter) pats let vars' = Map.union vartbl vars- sBody <- normalB $ singExp vars' exp+ sBody <- NormalB <$> singExp vars' exp return $ Clause sPats sBody [] singClause _ (Clause _ (GuardedB _) _) = fail "Singling of guarded patterns not yet supported" singClause _ (Clause _ _ (_:_)) = fail "Singling of <<where>> declarations not yet supported" -type ExpsQ = QWithAux ExpTable+type ExpsQ q = QWithAux ExpTable q -- we need to know where a pattern is to anticipate when -- GHC's brain might explode@@ -557,7 +624,7 @@ | Statement deriving Eq -checkIfBrainWillExplode :: PatternContext -> ExpsQ ()+checkIfBrainWillExplode :: Quasi q => PatternContext -> ExpsQ q () checkIfBrainWillExplode CaseStatement = return () checkIfBrainWillExplode Statement = return () checkIfBrainWillExplode Parameter = return ()@@ -566,13 +633,13 @@ "do expression: GHC's brain will explode if you try. (Do try it!)" -- convert a pattern, building up the lexical scope as we go-singPat :: PatternContext -> Pat -> ExpsQ Pat+singPat :: Quasi q => PatternContext -> Pat -> ExpsQ q Pat singPat _patCxt (LitP _lit) = fail "Singling of literal patterns not yet supported" singPat patCxt (VarP name) =- let newName = if patCxt == TopLevel then singValName name else name in do- addBinding name (VarE newName)- return $ VarP newName+ let new = if patCxt == TopLevel then singValName name else name in do+ addBinding name (VarE new)+ return $ VarP new singPat patCxt (TupP pats) = singPat patCxt (ConP (tupleDataName (length pats)) pats) singPat _patCxt (UnboxedTupP _pats) =@@ -593,9 +660,9 @@ pat' <- singPat patCxt pat return $ BangP pat' singPat patCxt (AsP name pat) = do- let newName = if patCxt == TopLevel then singValName name else name in do+ let new = if patCxt == TopLevel then singValName name else name in do pat' <- singPat patCxt pat- addBinding name (VarE newName)+ addBinding name (VarE new) return $ AsP name pat' singPat _patCxt WildP = return WildP singPat _patCxt (RecP _name _fields) =@@ -609,13 +676,12 @@ singPat _patCxt (ViewP _exp _pat) = fail "Singling of view patterns not yet supported" -singExp :: ExpTable -> Exp -> Q Exp+singExp :: Quasi q => ExpTable -> Exp -> q Exp singExp vars (VarE name) = case Map.lookup name vars of Just exp -> return exp Nothing -> return (singVal name)-singExp _vars (ConE name) = return $ smartCon name-singExp _vars (LitE _lit) =- fail "Singling of literal expressions not yet supported"+singExp _vars (ConE name) = return $ singDataCon name+singExp _vars (LitE lit) = singLit lit singExp vars (AppE exp1 exp2) = do exp1' <- singExp vars exp1 exp2' <- singExp vars exp2@@ -661,11 +727,14 @@ fail "Singling of ranges not yet supported" singExp vars (ListE exps) = do sExps <- mapM (singExp vars) exps- return $ foldr (\x -> (AppE (AppE (VarE smartSconsName) x)))- (VarE smartSnilName) sExps+ return $ foldr (\x -> (AppE (AppE (ConE sconsName) x)))+ (ConE snilName) sExps singExp _vars (SigE _exp _ty) = fail "Singling of annotated expressions not yet supported" singExp _vars (RecConE _name _fields) = fail "Singling of record construction not yet supported" singExp _vars (RecUpdE _exp _fields) = fail "Singling of record updates not yet supported"++singLit :: Quasi q => Lit -> q Exp+singLit lit = SigE (VarE singMethName) <$> (AppT singFamily <$> (promoteLit lit))
+ Data/Singletons/TH.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE ExplicitNamespaces, CPP #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.TH+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module contains everything you need to derive your own singletons via+-- Template Haskell.+--+-- TURN ON @-XScopedTypeVariables@ IN YOUR MODULE IF YOU WANT THIS TO WORK.+--+----------------------------------------------------------------------------++module Data.Singletons.TH (+ -- * Primary Template Haskell generation functions+ singletons, singletonsOnly, genSingletons,+ promote, promoteOnly,++ -- ** Functions to generate equality instances+ promoteEqInstances, promoteEqInstance,+ singEqInstances, singEqInstance,+ singEqInstancesOnly, singEqInstanceOnly,+ singDecideInstances, singDecideInstance,++ -- ** Utility function+ cases,++ -- * Basic singleton definitions+ Sing, SingI(..), SingKind(..), KindOf, Demote,+ + -- * Auxiliary definitions+ -- | These definitions might be mentioned in code generated by Template Haskell,+ -- so they must be in scope.+ + type (==), If, sIf, (:&&), SEq(..), + Any, + SDecide(..), (:~:)(..), Void, Refuted, Decision(..),+ KProxy(..), SomeSing(..)+ ) where++import Data.Singletons.Singletons+import Data.Singletons.Promote+import Data.Singletons.Core+import Data.Singletons.Bool+import Data.Singletons.Eq+import Data.Singletons.Types+import Data.Singletons.Void++import GHC.Exts+import Language.Haskell.TH+import Language.Haskell.TH.Syntax ( Quasi(..) )+import Language.Haskell.TH.Desugar+import Data.Singletons.Util+import Control.Applicative++#if __GLASGOW_HASKELL__ >= 707+import Data.Type.Equality+import Data.Proxy+#endif++-- | The function 'cases' generates a case expression where each right-hand side+-- is identical. This may be useful if the type-checker requires knowledge of which+-- constructor is used to satisfy equality or type-class constraints, but where+-- each constructor is treated the same.+cases :: Quasi q+ => Name -- ^ The head of the type of the scrutinee. (Like @''Maybe@ or @''Bool@.)+ -> q Exp -- ^ The scrutinee, in a Template Haskell quote+ -> q Exp -- ^ The body, in a Template Haskell quote+ -> q Exp+cases tyName expq bodyq = do+ info <- reifyWithWarning tyName+ case info of+ TyConI (DataD _ _ _ ctors _) -> buildCases ctors+ TyConI (NewtypeD _ _ _ ctor _) -> buildCases [ctor]+ _ -> fail $ "Using <<cases>> with something other than a type constructor: "+ ++ (show tyName)+ where buildCases ctors =+ CaseE <$> expq <*>+ mapM (\con -> Match (conToPat con) <$>+ (NormalB <$> bodyq) <*> pure []) ctors++ conToPat :: Con -> Pat+ conToPat = ctor1Case+ (\name tys -> ConP name (map (const WildP) tys))
+ Data/Singletons/Tuple.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DataKinds, PolyKinds,+ RankNTypes, TypeFamilies, GADTs, CPP #-}++#if __GLASGOW_HASKELL__ < 707+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}+#endif++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Tuple+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines functions and datatypes relating to the singleton for tuples,+-- including a singletons version of all the definitions in @Data.Tuple@.+--+-- Because many of these definitions are produced by Template Haskell,+-- it is not possible to create proper Haddock documentation. Please look+-- up the corresponding operation in @Data.Tuple@. Also, please excuse+-- the apparent repeated variable names. This is due to an interaction+-- between Template Haskell and Haddock.+--+----------------------------------------------------------------------------++module Data.Singletons.Tuple (+ -- * Singleton definitions+ -- | See 'Data.Singletons.Prelude.Sing' for more info.+ Sing(STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7),+ STuple0, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7,++ -- * Singletons from @Data.Tuple@+ Fst, sFst, Snd, sSnd, Curry, sCurry, Uncurry, sUncurry, Swap, sSwap+ ) where++import Data.Singletons.Core+import Data.Singletons.TH++$(singletonsOnly [d|+ -- | Extract the first component of a pair.+ fst :: (a,b) -> a+ fst (x,_) = x++ -- | Extract the second component of a pair.+ snd :: (a,b) -> b+ snd (_,y) = y++ -- | 'curry' converts an uncurried function to a curried function.+ curry :: ((a, b) -> c) -> a -> b -> c+ curry f x y = f (x, y)++ -- | 'uncurry' converts a curried function to a function on pairs.+ uncurry :: (a -> b -> c) -> ((a, b) -> c)+ uncurry f p = f (fst p) (snd p)++ -- | Swap the components of a pair.+ swap :: (a,b) -> (b,a)+ swap (a,b) = (b,a)+ |])
Data/Singletons/TypeRepStar.hs view
@@ -1,31 +1,98 @@-{- Data/Singletons/TypeRepStar.hs+{-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances,+ GADTs, UndecidableInstances, ScopedTypeVariables, DataKinds,+ MagicHash, CPP, TypeOperators #-}+{-# OPTIONS_GHC -fno-warn-orphans #-} -(c) Richard Eisenberg 2013-eir@cis.upenn.edu+-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.TypeRepStar+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module defines singleton instances making 'Typeable' the singleton for+-- the kind @*@. The definitions don't fully line up with what is expected+-- within the singletons library, so expect unusual results!+--+---------------------------------------------------------------------------- -This file contains the definitions for considering TypeRep to be the demotion-of *. This is still highly experimental, so expect unusual results!+module Data.Singletons.TypeRepStar (+ Sing(STypeRep)+ -- | Here is the definition of the singleton for @*@:+ --+ -- > data instance Sing (a :: *) where+ -- > STypeRep :: Typeable a => Sing a+ --+ -- Instances for 'SingI', 'SingKind', 'SEq', 'SDecide', and 'TestCoercion' are+ -- also supplied.+ ) where --}+import Data.Singletons.Core+import Data.Singletons.Types+import Data.Singletons.Eq+import Data.Typeable+import Unsafe.Coerce -{-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances,- GADTs, UndecidableInstances, ScopedTypeVariables, DataKinds #-}+#if __GLASGOW_HASKELL__ >= 707+import GHC.Exts ( Proxy# )+import Data.Type.Coercion+import Data.Proxy+#else -module Data.Singletons.TypeRepStar where+eqT :: (Typeable a, Typeable b) => Maybe (a :~: b)+eqT = gcast Refl -import Data.Singletons-import Data.Typeable+type instance (a :: *) :== (a :: *) = True +#endif+ data instance Sing (a :: *) where STypeRep :: Typeable a => Sing a -sTypeRep :: forall (a :: *). Typeable a => Sing a-sTypeRep = STypeRep- instance Typeable a => SingI (a :: *) where sing = STypeRep-instance SingE (KindParam :: KindIs *) where- type DemoteRep (KindParam :: KindIs *) = TypeRep+instance SingKind ('KProxy :: KProxy *) where+ type DemoteRep ('KProxy :: KProxy *) = TypeRep fromSing (STypeRep :: Sing a) = typeOf (undefined :: a)-instance SingKind (KindParam :: KindIs *) where- singInstance STypeRep = SingInstance+ toSing = dirty_mk_STypeRep++instance SEq ('KProxy :: KProxy *) where+ (STypeRep :: Sing a) %:== (STypeRep :: Sing b) =+ case (eqT :: Maybe (a :~: b)) of+ Just Refl -> STrue+ Nothing -> unsafeCoerce SFalse+ -- the Data.Typeable interface isn't strong enough+ -- to enable us to define this without unsafeCoerce++instance SDecide ('KProxy :: KProxy *) where+ (STypeRep :: Sing a) %~ (STypeRep :: Sing b) =+ case (eqT :: Maybe (a :~: b)) of+ Just Refl -> Proved Refl+ Nothing -> Disproved (\Refl -> error "Data.Typeable.eqT failed")++#if __GLASGOW_HASKELL__ >= 707+-- TestEquality instance already defined, but we need this one:+instance TestCoercion Sing where+ testCoercion (STypeRep :: Sing a) (STypeRep :: Sing b) =+ case (eqT :: Maybe (a :~: b)) of+ Just Refl -> Just Coercion+ Nothing -> Nothing+#endif++-- everything below here is private and dirty. Don't look!+ +newtype DI = Don'tInstantiate (Typeable a => Sing a)+dirty_mk_STypeRep :: TypeRep -> SomeSing ('KProxy :: KProxy *)+dirty_mk_STypeRep rep =+#if __GLASGOW_HASKELL__ >= 707+ let justLikeTypeable :: Proxy# a -> TypeRep+ justLikeTypeable _ = rep+ in+#else+ let justLikeTypeable :: a -> TypeRep+ justLikeTypeable _ = rep+ in+#endif+ unsafeCoerce (Don'tInstantiate STypeRep) justLikeTypeable
+ Data/Singletons/Types.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE PolyKinds, TypeOperators, GADTs, RankNTypes, TypeFamilies,+ CPP, DataKinds #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Singletons.Types+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- Defines and exports types that are useful when working with singletons.+-- Some of these are re-exports from @Data.Type.Equality@.+--+----------------------------------------------------------------------------+++module Data.Singletons.Types (+ Refuted, Decision(..),+#if __GLASGOW_HASKELL__ < 707+ KProxy(..), Proxy(..),+ (:~:)(..), gcastWith, TestEquality(..)+#endif+ ) where++import Data.Singletons.Void++#if __GLASGOW_HASKELL__ < 707++-- now in Data.Proxy+data KProxy (a :: *) = KProxy+data Proxy a = Proxy++-- now in Data.Type.Equality+data a :~: b where+ Refl :: a :~: a++gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r+gcastWith Refl x = x++class TestEquality (f :: k -> *) where+ testEquality :: f a -> f b -> Maybe (a :~: b)++#endif++-- | Because we can never create a value of type 'Void', a function that type-checks+-- at @a -> Void@ shows that objects of type @a@ can never exist. Thus, we say that+-- @a@ is 'Refuted'+type Refuted a = (a -> Void)++-- | A 'Decision' about a type @a@ is either a proof of existence or a proof that @a@+-- cannot exist.+data Decision a = Proved a -- ^ Witness for @a@+ | Disproved (Refuted a) -- ^ Proof that no @a@ exists
Data/Singletons/Util.hs view
@@ -7,15 +7,24 @@ Users of the package should not need to consult this file. -} -{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, TypeSynonymInstances, FlexibleInstances, RankNTypes,+ TemplateHaskell, GeneralizedNewtypeDeriving,+ MultiParamTypeClasses #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} -module Data.Singletons.Util where+module Data.Singletons.Util (+ module Data.Singletons.Util,+ module Language.Haskell.TH.Desugar )+ where -import Language.Haskell.TH+import Prelude hiding ( exp )+import Language.Haskell.TH hiding ( Q )+import Language.Haskell.TH.Syntax ( Quasi(..) )+import Language.Haskell.TH.Desugar ( reifyWithWarning, getDataD ) import Data.Char import Data.Data import Control.Monad+import Control.Applicative import Control.Monad.Writer import qualified Data.Map as Map import Data.Generics@@ -28,41 +37,48 @@ TySynInstD name lhs rhs #endif +-- The list of types that singletons processes by default+basicTypes :: [Name]+basicTypes = [ ''Bool+ , ''Maybe+ , ''Either+ , ''Ordering+ , ''[]+ , ''()+ , ''(,)+ , ''(,,)+ , ''(,,,)+ , ''(,,,,)+ , ''(,,,,,)+ , ''(,,,,,,)+ ]+ -- like newName, but even more unique (unique across different splices) -- TH doesn't allow "newName"s to work at the top-level, so we have to -- do this trick to ensure the Extract functions are unique-newUniqueName :: String -> Q Name+newUniqueName :: Quasi q => String -> q Name newUniqueName str = do- n <- newName str+ n <- qNewName str return $ mkName $ show n --- reify a declaration, warning the user about splices if the reify fails-reifyWithWarning :: Name -> Q Info-reifyWithWarning name = recover- (fail $ "Looking up " ++ (show name) ++ " in the list of available " ++- "declarations failed.\nThis lookup fails if the declaration " ++- "referenced was made in the same Template\nHaskell splice as the use " ++- "of the declaration. If this is the case, put\nthe reference to " ++- "the declaration in a new splice.")- (reify name)---- check if a string is the name of a tuple-isTupleString :: String -> Bool-isTupleString s =- (length s > 1) &&- (head s == '(') &&- (last s == ')') &&- ((length (takeWhile (== ',') (tail s))) == ((length s) - 2))---- check if a name is a tuple name-isTupleName :: Name -> Bool-isTupleName = isTupleString . nameBase+-- like reportWarning, but generalized to any Quasi+qReportWarning :: Quasi q => String -> q ()+qReportWarning = qReport False -- extract the degree of a tuple-tupleDegree :: String -> Int-tupleDegree "()" = 0-tupleDegree s = length s - 1+tupleDegree_maybe :: String -> Maybe Int+tupleDegree_maybe s = do+ '(' : s1 <- return s + (commas, ")") <- return $ span (== ',') s1+ let degree+ | "" <- commas = 0+ | otherwise = length commas + 1+ return degree +-- extract the degree of a tuple name+tupleNameDegree_maybe :: Name -> Maybe Int+tupleNameDegree_maybe = tupleDegree_maybe . nameBase+ -- reduce the four cases of a 'Con' to just two: monomorphic and polymorphic -- and convert 'StrictType' to 'Type' ctorCases :: (Name -> [Type] -> a) -> ([TyVarBndr] -> Cxt -> Con -> a) -> Con -> a@@ -126,24 +142,16 @@ then mkName (pre ++ str) else mkName (tyPre ++ str) --- extract the name from a TyVarBndr-extractTvbName :: TyVarBndr -> Name-extractTvbName (PlainTV n) = n-extractTvbName (KindedTV n _) = n-#if __GLASGOW_HASKELL__ >= 707-extractTvbName (RoledTV n _) = n-extractTvbName (KindedRoledTV n _ _) = n-#endif- -- extract the kind from a TyVarBndr. Returns '*' by default. extractTvbKind :: TyVarBndr -> Kind extractTvbKind (PlainTV _) = StarT -- FIXME: This seems wrong. extractTvbKind (KindedTV _ k) = k-#if __GLASGOW_HASKELL__ >= 707-extractTvbKind (RoledTV _ _) = StarT -- FIXME: This seems wrong.-extractTvbKind (KindedRoledTV _ k _) = k-#endif +-- extract the name from a TyVarBndr.+extractTvbName :: TyVarBndr -> Name+extractTvbName (PlainTV n) = n+extractTvbName (KindedTV n _) = n+ -- apply a type to a list of types foldType :: Type -> [Type] -> Type foldType = foldl AppT@@ -157,28 +165,98 @@ isVarK (VarT _) = True isVarK _ = False +-- tuple up a list of expressions+mkTupleExp :: [Exp] -> Exp+mkTupleExp [x] = x+mkTupleExp xs = TupE xs++-- tuple up a list of patterns+mkTuplePat :: [Pat] -> Pat+mkTuplePat [x] = x+mkTuplePat xs = TupP xs++-- choose the first non-empty list+orIfEmpty :: [a] -> [a] -> [a]+orIfEmpty [] x = x+orIfEmpty x _ = x++-- an empty list of matches, compatible with GHC 7.6.3+emptyMatches :: [Match]+#if __GLASGOW_HASKELL__ >= 707+emptyMatches = []+#else+emptyMatches = [Match WildP (NormalB (AppE (VarE 'error) (LitE (StringL errStr)))) []]+ where errStr = "Empty case reached -- this should be impossible"+#endif++-- build a pattern match over several expressions, each with only one pattern+multiCase :: [Exp] -> [Pat] -> Exp -> Exp+multiCase [] [] body = body+multiCase scruts pats body =+ CaseE (mkTupleExp scruts)+ [Match (mkTuplePat pats) (NormalB body) []]+ -- a monad transformer for writing a monoid alongside returning a Q-type QWithAux m = WriterT m Q+newtype QWithAux m q a = QWA { runQWA :: WriterT m q a }+ deriving (Functor, Applicative, Monad, MonadTrans) +instance (Monoid m, Monad q) => MonadWriter m (QWithAux m q) where+ writer = QWA . writer+ tell = QWA . tell+ listen = QWA . listen . runQWA+ pass = QWA . pass . runQWA++-- make a Quasi instance for easy lifting+instance (Quasi q, Monoid m) => Quasi (QWithAux m q) where+ qNewName = lift `comp1` qNewName+ qReport = lift `comp2` qReport+ qLookupName = lift `comp2` qLookupName+ qReify = lift `comp1` qReify+ qReifyInstances = lift `comp2` qReifyInstances+ qLocation = lift qLocation+ qRunIO = lift `comp1` qRunIO+ qAddDependentFile = lift `comp1` qAddDependentFile+#if __GLASGOW_HASKELL__ >= 707+ qReifyRoles = lift `comp1` qReifyRoles+ qReifyAnnotations = lift `comp1` qReifyAnnotations+ qReifyModule = lift `comp1` qReifyModule+ qAddTopDecls = lift `comp1` qAddTopDecls+ qAddModFinalizer = lift `comp1` qAddModFinalizer+ qGetQ = lift qGetQ+ qPutQ = lift `comp1` qPutQ+#endif + + qRecover exp handler = do+ (result, aux) <- lift $ qRecover (evalForPair exp) (evalForPair handler)+ tell aux+ return result++-- helper functions for composition+comp1 :: (b -> c) -> (a -> b) -> a -> c+comp1 = (.)++comp2 :: (c -> d) -> (a -> b -> c) -> a -> b -> d+comp2 f g a b = f (g a b)+ -- run a computation with an auxiliary monoid, discarding the monoid result-evalWithoutAux :: QWithAux m a -> Q a-evalWithoutAux = liftM fst . runWriterT+evalWithoutAux :: Quasi q => QWithAux m q a -> q a+evalWithoutAux = liftM fst . runWriterT . runQWA -- run a computation with an auxiliary monoid, returning only the monoid result-evalForAux :: QWithAux m a -> Q m-evalForAux = execWriterT+evalForAux :: Quasi q => QWithAux m q a -> q m+evalForAux = execWriterT . runQWA -- run a computation with an auxiliary monoid, return both the result -- of the computation and the monoid result-evalForPair :: QWithAux m a -> Q (a, m)-evalForPair = runWriterT+evalForPair :: Quasi q => QWithAux m q a -> q (a, m)+evalForPair = runWriterT . runQWA -- in a computation with an auxiliary map, add a binding to the map-addBinding :: Ord k => k -> v -> QWithAux (Map.Map k v) ()+addBinding :: (Quasi q, Ord k) => k -> v -> QWithAux (Map.Map k v) q () addBinding k v = tell (Map.singleton k v) -- in a computation with an auxiliar list, add an element to the list-addElement :: elt -> QWithAux [elt] ()+addElement :: Quasi q => elt -> QWithAux [elt] q () addElement elt = tell [elt] -- does a TH structure contain a name?@@ -191,19 +269,6 @@ bss <- mapM fn list return $ concat bss --- extract the tyvars and constructors from a name of a type,--- printing out the string upon failure-getDataD :: String -> Name -> Q ([TyVarBndr], [Con])-getDataD error name = do- info <- reifyWithWarning name- dec <- case info of- TyConI dec -> return dec- _ -> badDeclaration- case dec of- DataD _cxt _name tvbs cons _derivings -> return (tvbs, cons)- NewtypeD _cxt _name tvbs con _derivings -> return (tvbs, [con])- _ -> badDeclaration- where badDeclaration =- fail $ "The name (" ++ (show name) ++ ") refers to something " ++- "other than a datatype. " ++ error-+-- make a one-element list+listify :: a -> [a]+listify = return
+ Data/Singletons/Void.hs view
@@ -0,0 +1,78 @@+{- Data/Singletons/Void.hs++ A reimplementation of a Void type, copied shamelessly from Edward Kmett's void+ package, but without inducing a dependency.++-}++{-# LANGUAGE CPP, Trustworthy, DeriveDataTypeable, DeriveGeneric, StandaloneDeriving #-}++-----------------------------------------------------------------------------+-- |+-- Copyright : (C) 2008-2013 Edward Kmett+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module is a reimplementation of Edward Kmett's @void@ package.+-- It is included within singletons to avoid depending on @void@ and all the+-- packages that depends on (including @text@). If this causes problems for+-- you (that singletons has its own 'Void' type), please let me (Richard Eisenberg)+-- know at @eir@ at @cis.upenn.edu@.+--+----------------------------------------------------------------------------+module Data.Singletons.Void+ ( Void+ , absurd+ , vacuous+ , vacuousM+ ) where++import Control.Monad (liftM)+import Data.Ix+import Data.Data+import GHC.Generics+import Control.Exception++-- | A logically uninhabited data type.+newtype Void = Void Void+ deriving (Data, Typeable, Generic)++instance Eq Void where+ _ == _ = True++instance Ord Void where+ compare _ _ = EQ++instance Show Void where+ showsPrec _ = absurd++-- | Reading a 'Void' value is always a parse error, considering 'Void' as+-- a data type with no constructors.+instance Read Void where+ readsPrec _ _ = []++-- | Since 'Void' values logically don't exist, this witnesses the logical+-- reasoning tool of \"ex falso quodlibet\".+absurd :: Void -> a+absurd a = a `seq` spin a where+ spin (Void b) = spin b++-- | If 'Void' is uninhabited then any 'Functor' that holds only values of type 'Void'+-- is holding no values.+vacuous :: Functor f => f Void -> f a+vacuous = fmap absurd++-- | If 'Void' is uninhabited then any 'Monad' that holds values of type 'Void'+-- is holding no values.+vacuousM :: Monad m => m Void -> m a+vacuousM = liftM absurd++instance Ix Void where+ range _ = []+ index _ = absurd+ inRange _ = absurd+ rangeSize _ = 0++instance Exception Void
− README
@@ -1,441 +0,0 @@-singletons-==========--This is the README file for the singletons library. This file contains all the-documentation for the definitions and functions in the library. As of the time-of this writing (January 16, 2013), haddock has not quite caught up with GHC in-handling kind-polymorphic code, and the HEAD version of haddock cannot process-Template Haskell. Thus, the documentation is in here. In the future, it will-be generated by haddock.--The singletons library was written by Richard Eisenberg, eir@cis.upenn.edu.-See also /Dependently typed programming with singletons/, available at-<http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>------------------------------------Purpose of the singletons library------------------------------------The library contains a definition of /singleton types/, which allow-programmers to use dependently typed techniques to enforce rich constraints-among the types in their programs. See the paper cited above for a-more thorough introduction.----------------Compatibility----------------The singletons library requires GHC version 7.6.1 or greater.-Any code that uses the singleton generation primitives will also need-to enable a long list of GHC extensions. This list includes, but-is not necessarily limited to, the following:--* TemplateHaskell-* TypeFamilies-* GADTs-* KindSignatures-* DataKinds-* PolyKinds-* TypeOperators-* FlexibleContexts-* RankNTypes-* UndecidableInstances-* FlexibleInstances--In addition, @ScopedTypeVariables@ is often very helpful.-----------------------------------Functions to generate singletons-----------------------------------There are four top-level functions used to generate the singleton definitions.-These functions should all be used within top-level Template Haskell splices.-See #supported-features# for a list of what Haskell constructs are supported.--These functions are all defined in Data.Singletons.---genPromotion :: [Name] -> Q [Dec]--Takes a list of names of types and promotes them to the kind level. Although-@DataKinds@ does this promotion automaticlly, the manual promotion also-handles generating instances of @:==:@, Boolean equality at the type level,-for type that derive @Eq@.--To use:--> $(genPromotion [''Bool, ''Maybe])---genSingletons :: [Name] -> Q [Dec]--Takes a list of names of types and generates singleton type definitions-for them.--To use:--> $(genSingletons [''Bool, ''Maybe])---promote :: Q [Dec] -> Q [Dec]--Promotes the declarations given.--To use:--> $(promote [d|-> data Nat = Zero | Succ Nat-> pred :: Nat -> Nat-> pred Zero = Zero-> pred (Succ n) = n-> |])---singletons :: Q [Dec] -> Q [Dec]--Generates singletons from the definitions given. Because singleton generation-requires promotion, this also promotes all of the definitions given.--To use:-> $(singletons [d|-> data Nat = Zero | Succ Nat-> pred :: Nat -> Nat-> pred Zero = Zero-> pred (Succ n) = n-> |])------------------------------------------Definitions used to support singletons-----------------------------------------Please refer to the paper cited above for a more in-depth explanation of these-definitions.--------NOTE: The original paper used a trick with the GHC primitive 'Any' to simulate-kind classes and to perform other shenanigans. 'Any' is like undefined at the-type level. GHC has evolved to prevent pattern-matching on 'Any', which is a-Good Thing. This means that some of singletons's uses of 'Any' were invalid.-These were replaced with a kind-level proxy, defined thus:--data OfKind (k :: *) = KindParam-type KindOf (a :: k) = (KindParam :: OfKind k)--The parameter must be explicitly kinded to * to prevent polymorphism, because-only monomorphic types are promoted to kinds. This definition should only be-used at the kind level.--------Many of the definitions were developed in tandem with Iavor Diatchki, the-maintainer of type-level literals in GHC. In GHC 7.7+, the singletons library-imports many of these definitions from GHC.TypeLits.---data family Sing (a :: k)--The data family of singleton types. A new instance of this data family is-generated for every new singleton type.---class SingI (a :: k) where- sing :: Sing a--A class used to pass singleton values implicitly. The 'sing' method produces-an explicit singleton value.---class (kparam ~ KindParam) => SingE (kparam :: OfKind k) where- type DemoteRep kparam :: *- fromSing :: Sing (a :: k) -> DemoteRep kparam--This class is used to convert a singleton value back to a value in the-original, unrefined ADT. The 'fromSing' method converts, say, a-singleton @Nat@ back to an ordinary @Nat@. The 'DemoteRep' associated-kind-indexed type family maps a proxy of the kind @Nat@-back to the type @Nat@.---class (SingI a, SingE (KindOf a)) => SingRep (a :: k)-instance (SingI a, SingE (KindOf a)) => SingRep (a :: k)--'SingRep' is a synonym for @('SingI' a, 'SingE' (KindOf a))@.---type family (a :: k) :==: (b :: k) :: Bool-type a :== b = a :==: b-type a :/=: b = Not (a :==: b)-type a :/= b = a :/=: b--These are two equivalent forms of Boolean equality and inequality at the type-level. When promoted a datatype that derives @Eq@, instances of this type-family are generated.--data SingInstance (a :: k) where- SingInstance :: SingRep a => SingInstance a-class (kparam ~ KindParam) => SingKind (kparam :: OfKind k) where- singInstance :: forall (a :: k). Sing a -> SingInstance a--The 'SingKind' class allows for easy access to implicit parameters. The-intuition here is that for any kind @k@ with an associated singleton definition,-@SingKind (KindParam :: OfKind k)@ is defined.---class (kparam ~ KindParam) => SEq (kparam :: OfKind k) where- (%==%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :==: b)- (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b)--This is the equivalent of @Eq@ for singletons. It computes singleton Boolean-equality. Alternate spellings of the functions are provided: (%:==) is the-same as (%==%) and (%:/=) is the same as (%/=%). These synonyms are provided-for compatibility with generated code.---type family If (a :: Bool) (b :: k) (c :: k) :: k--This type family is a Boolean conditional at the type level. Note that type--level computation is *strict* in GHC. Thus, you cannot use If to check a-termination condition in a recursive type family -- the type checker will-loop if you try. Corollary: you cannot use plain old 'if' to check a-termination condition in a term-level function you wish to promote or refine-into a singleton.---sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)--This function is a conditional for singletons.---type family Head (a :: [k]) :: k--Returns the head of a type-level list. Gets stuck when given @'[]@.---type family Tail (a :: [k]) :: [k]--Returns the tail of a type-level list. Gets stuck when given @'[]@.---------------------------Other utility functions--------------------------cases :: Name -- the type of the scrutinee- -> Q Exp -- the scrutinee- -> Q Exp -- the body of each branch- -> Q Exp -- the resulting expression--It is sometimes necessary to get GHC to do case analysis on all possible-types for a given type parameter. No matter what the type variable is, though,-the resulting action is the same. This normally takes the form of a case-statement where every branch has the same expression. The 'cases' function-generates such a case statement. For example,--> $(cases ''Bool [| not foo |] [| doSomething foo |])--expands to--> case not foo of-> True -> doSomething foo-> False -> doSomething foo---bugInGHC :: forall a. a--Currently, GHC will issue a warning for an incomplete pattern match, even-when all omitted cases can be statically proven to be impossible. For example:--> safePred :: Sing (Succ n) -> Sing n-> safePred (SSucc n) = n--With @-fwarn-incomplete-patterns@ (which we highly recommend using), GHC-warns that the pattern match is incomplete. The solution? Suppress the warning-with a wildcard pattern, using 'bugInGHC':--> safePred _ = bugInGHC--The 'bugInGHC' function just calls @error@ with an appropriate message. --------------------------Pre-defined singletons-------------------------The singletons library defines a number of singleton types and functions-by default:--* @Bool@-* @Maybe@-* @Either@-* @()@-* tuples up to length 7-* @not@, @&&@, @||@-* lists-* @++@-----------On names-----------The singletons library has to produce new names for the new constructs it-generates. Here are some examples showing how this is done:--original datatype: Nat-promoted kind: Nat-singleton type: SNat (which is really a synonym for @Sing@)--original datatype: (:/\:)-promoted kind: (:/\:)-singleton type: (:%/\:)--original constructor: Zero-promoted type: 'Zero-singleton constructor: SZero-smart constructor: sZero (see paper cited above for more info)--original constructor: :+:-promoted type: ':+:-singleton constructor: :%+:-smart constructor: %:+:--original value: pred-promoted type: Pred-singleton value: sPred--original value: +-promoted type: :+-singleton value: %:+---Special names----------------There are some special cases:--original datatype: []-singleton type: SList--original constructor: []-singleton constructor: SNil-smart constructor: sNil--original constructor: :-singleton constructor: SCons-smart constructor: sCons--original datatype: (,)-singleton type: STuple2--original constructor: (,)-singleton constructor: STuple2-smart constructor: sTuple2--All tuples (including the 0-tuple, unit) are treated similarly.--original value: undefined-promoted type: Any-singleton value: undefined--------------------------------Supported Haskell constructs------------------------------#supported-features#--The following constructs are fully supported:--* variables-* tuples-* constructors-* if statements-* infix expressions-* !, ~, and _ patterns-* aliased patterns (except at top-level)-* lists-* (+) sections-* (x +) sections-* undefined-* deriving Eq-* class constraints--The following constructs will be coming soon:--* unboxed tuples-* records-* scoped type variables-* overlapping patterns-* pattern guards-* (+ x) sections-* case-* let-* list comprehensions--The following constructs are problematic and are not planned to be-implemented:--* literals-* lambda expressions-* do-* arithmetic sequences--See the paper cited above for reasons why these are problematic.--As described briefly in the paper, the singletons generation mechanism does not-currently work for higher-order datatypes (though higher-order functions are-just peachy). So, if you have a declaration such as--> data Foo = Bar (Bool -> Maybe Bool)--, its singleton will not work correctly. It turns out that getting this to work-requires fairly thorough changes to the whole singleton generation scheme.-Please shout (to eir@cis.upenn.edu) if you have a compelling use case for this-and I can take a look at it. No promises, though.----------------Support for *----------------The built-in Haskell promotion mechanism does not yet have a full story around-the kind * (the kind of types that have values). Ideally, promoting some form-of TypeRep would yield *, but the implementation of TypeRep would have to be-updated for this to really work out. In the meantime, users who wish to-experiment with this feature have two options:--1) The module Data.Singletons.TypeRepStar has all the definitions possible for-making * the promoted version of TypeRep, as TypeRep is currently implemented.-The singleton associated with TypeRep has one constructor:--> data instance Sing (a :: *) where-> STypeRep :: Typeable a => Sing a--Thus, an implicit TypeRep is stored in the singleton constructor. However,-any datatypes that store TypeReps will not generally work as expected; the-built-in promotion mechanism will not promote TypeRep to *.--2) The module Singletons.CustomStar allows the programmer to define a subset-of types with which to work. A datatype @Rep@ is created, with one constructor-per type in the declared universe. When this type is promoted by the singletons-library, the constructors become full types in *, not just promoted data-constructors. The universe is specified with the @singletonStar@ function.--For example,--> $(singletonStar [''Nat, ''Bool, ''Maybe])--generates the following:--> data Rep = Nat | Bool | Maybe Rep deriving (Eq, Show, Read)--and its singleton. However, because @Rep@ is promoted to @*@, the singleton-is perhaps slightly unexpected:--> data instance Sing (a :: *) where-> SNat :: Sing Nat-> SBool :: Sing Bool-> SMaybe :: SingRep a => Sing a -> Sing (Maybe a)--The unexpected part is that @Nat@, @Bool@, and @Maybe@ above are the real @Nat@,-@Bool@, and @Maybe@, not just promoted data constructors.---Please note that support for * is *very* experimental. Use at your own risk.
+ README.md view
@@ -0,0 +1,302 @@+singletons 0.9.0+================++This is the README file for the singletons library. This file contains all the+documentation for the definitions and functions in the library.++The singletons library was written by Richard Eisenberg, eir@cis.upenn.edu.+See also _Dependently typed programming with singletons_, available+[here](http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf).++Purpose of the singletons library+---------------------------------++The library contains a definition of _singleton types_, which allow+programmers to use dependently typed techniques to enforce rich constraints+among the types in their programs. See the paper cited above for a+more thorough introduction.++Compatibility+-------------++The singletons library requires GHC version 7.6.3 or greater.+Any code that uses the singleton generation primitives will also need+to enable a long list of GHC extensions. This list includes, but+is not necessarily limited to, the following:++* `ScopedTypeVariables` (absolutely required)+* `TemplateHaskell`+* `TypeFamilies`+* `GADTs`+* `KindSignatures`+* `DataKinds`+* `PolyKinds`+* `TypeOperators`+* `FlexibleContexts`+* `RankNTypes`+* `UndecidableInstances`+* `FlexibleInstances`+* `EmptyCase` (for GHC 7.8)+++Functions to generate singletons+--------------------------------++The top-level functions used to generate singletons are documented in the+`Data.Singletons.TH` module. The most common case is just calling `singletons`,+which I'll describe here:++ singletons :: Q [Dec] -> Q [Dec]++Generates singletons from the definitions given. Because singleton generation+requires promotion, this also promotes all of the definitions given to the+type level.++To use:+ $(singletons [d|+ data Nat = Zero | Succ Nat+ pred :: Nat -> Nat+ pred Zero = Zero+ pred (Succ n) = n+ |])++Definitions used to support singletons+--------------------------------------++Please refer to the paper cited above for a more in-depth explanation of these+definitions. Many of the definitions were developed in tandem with Iavor Diatchki.++ data family Sing (a :: k)++The data family of singleton types. A new instance of this data family is+generated for every new singleton type.++ class SingI (a :: k) where+ sing :: Sing a++A class used to pass singleton values implicitly. The `sing` method produces+an explicit singleton value.++ data SomeSing (kproxy :: KProxy k) where+ SomeSing :: Sing (a :: k) -> SomeSing ('KProxy :: KProxy k)++The `SomeSing` type wraps up an _existentially-quantified_ singleton. Note that+the type parameter `a` does not appear in the `SomeSing` type. Thus, this type+can be used when you have a singleton, but you don't know at compile time what+it will be. `SomeSing ('KProxy :: KProxy Thing)` is isomorphic to `Thing`.++ class (kparam ~ 'KProxy) => SingKind (kparam :: KProxy k) where+ type DemoteRep kparam :: *+ fromSing :: Sing (a :: k) -> DemoteRep kparam+ toSing :: DemoteRep kparam -> SomeSing kparam+ +This class is used to convert a singleton value back to a value in the+original, unrefined ADT. The `fromSing` method converts, say, a+singleton `Nat` back to an ordinary `Nat`. The `toSing` method produces+an existentially-quantified singleton, wrapped up in a `SomeSing`.+The `DemoteRep` associated+kind-indexed type family maps a proxy of the kind `Nat`+back to the type `Nat`. ++ data SingInstance (a :: k) where+ SingInstance :: SingI a => SingInstance a+ singInstance :: Sing a -> SingInstance a++Sometimes you have an explicit singleton (a `Sing`) where you need an implicit+one (a dictionary for `SingI`). The `SingInstance` type simply wraps a `SingI`+dictionary, and the `singInstance` function produces this dictionary from an+explicit singleton. The `singInstance` function runs in constant time, using+a little magic.+++Equality classes+----------------++There are two different notions of equality applicable to singletons: Boolean+equality and propositional equality.++* Boolean equality is implemented in the type family `(:==)` (which is actually+a synonym for the type family `(==)` from `Data.Type.Equality`) and the class+`SEq`. See the `Data.Singletons.Eq` module for more information.++* Propositional equality is implemented through the constraint `(~)`, the type+`(:~:)`, and the class `SDecide`. See modules `Data.Type.Equality` and+`Data.Singletons.Decide` for more information.++Which one do you need? That depends on your application. Boolean equality has+the advantage that your program can take action when two types do _not_ equal,+while propositional equality has the advantage that GHC can use the equality+of types during type inference.++Instances of both `SEq` and `SDecide` are generated when `singletons` is called+on a datatype that has `deriving Eq`. You can also generate these instances+directly through functions exported from `Data.Singletons.TH`.+++Pre-defined singletons+----------------------++The singletons library defines a number of singleton types and functions+by default:++* `Bool`+* `Maybe`+* `Either`+* `Ordering`+* `()`+* tuples up to length 7+* lists++These are all available through `Data.Singletons.Prelude`. Functions that+operate on these singletons are available from modules such as `Data.Singletons.Bool`+and `Data.Singletons.Maybe`.+++On names+--------++The singletons library has to produce new names for the new constructs it+generates. Here are some examples showing how this is done:++original datatype: `Nat`+promoted kind: `Nat`+singleton type: `SNat` (which is really a synonym for `Sing`)++original datatype: `:/\:`+promoted kind: `:/\:`+singleton type: `:%/\:`++original constructor: `Zero`+promoted type: `'Zero` (you can use `Zero` when unambiguous)+singleton constructor: `SZero`++original constructor: `:+:`+promoted type: `':+:`+singleton constructor: `:%+:`++original value: `pred`+promoted type: `Pred`+singleton value: `sPred`++original value: `+`+promoted type: `:+`+singleton value: `%:+`+++Special names+-------------++There are some special cases:++original datatype: `[]`+singleton type: `SList`++original constructor: `[]`+singleton constructor: `SNil`++original constructor: `:`+singleton constructor: `SCons`++original datatype: `(,)`+singleton type: `STuple2`++original constructor: `(,)`+singleton constructor: `STuple2`++All tuples (including the 0-tuple, unit) are treated similarly.++original value: `undefined`+promoted type: `Any`+singleton value: `undefined`+++Supported Haskell constructs+----------------------------++The following constructs are fully supported:++* variables+* tuples+* constructors+* if statements+* infix expressions+* !, ~, and _ patterns+* aliased patterns (except at top-level)+* lists+* (+) sections+* (x +) sections+* undefined+* error+* deriving Eq+* class constraints+* literals (for `Nat` and `Symbol`)++The following constructs will be coming soon:++* unboxed tuples+* records+* scoped type variables+* overlapping patterns+* pattern guards+* (+ x) sections+* case+* let+* list comprehensions+* lambda expressions+* do+* arithmetic sequences++As described briefly in the paper, the singletons generation mechanism does not+currently work for higher-order datatypes (though higher-order functions are+just peachy). So, if you have a declaration such as++ data Foo = Bar (Bool -> Maybe Bool)++its singleton will not work correctly. It turns out that getting this to work+requires fairly thorough changes to the whole singleton generation scheme.+Please shout (to eir@cis.upenn.edu) if you have a compelling use case for this+and I can take a look at it. No promises, though.++Support for `*`+---------------++The built-in Haskell promotion mechanism does not yet have a full story around+the kind `*` (the kind of types that have values). Ideally, promoting some form+of `TypeRep` would yield `*`, but the implementation of TypeRep would have to be+updated for this to really work out. In the meantime, users who wish to+experiment with this feature have two options:++1) The module `Data.Singletons.TypeRepStar` has all the definitions possible for+making `*` the promoted version of `TypeRep`, as `TypeRep` is currently implemented.+The singleton associated with `TypeRep` has one constructor:++ data instance Sing (a :: *) where+ STypeRep :: Typeable a => Sing a++Thus, an implicit `TypeRep` is stored in the singleton constructor. However,+any datatypes that store `TypeRep`s will not generally work as expected; the+built-in promotion mechanism will not promote `TypeRep` to `*`.++2) The module `Data.Singletons.CustomStar` allows the programmer to define a subset+of types with which to work. See the Haddock documentation for the function+`singletonStar` for more info.++Changes from earlier versions+-----------------------------++singletons 0.9 contains a bit of an API change from previous versions. Here is+a summary:++* There are no more "smart" constructors. Those were necessary because each+singleton used to carry both explicit and implicit versions of any children+nodes. However, this leads to exponential overhead! Now, the magic (i.e., a+use of `unsafeCoerce`) in `singInstance` gets rid of the need for storing+implicit singletons. The smart constructors did some of the work of managing+the stored implicits, so they are no longer needed.++* `SingE` and `SingRep` are gone. If you need to carry an implicit singleton,+use `SingI`. Otherwise, you probably want `SingKind`.++* The Template Haskell functions are now exported from `Data.Singletons.TH`.++* The Prelude singletons are now exported from `Data.Singletons.Prelude`.
singletons.cabal view
@@ -1,6 +1,6 @@ name: singletons-version: 0.8.6-cabal-version: >= 1.8+version: 0.9.0+cabal-version: >= 1.10 synopsis: A framework for generating singleton types homepage: http://www.cis.upenn.edu/~eir/packages/singletons category: Dependent Types@@ -8,7 +8,7 @@ maintainer: Richard Eisenberg <eir@cis.upenn.edu> bug-reports: https://github.com/goldfirere/singletons/issues stability: experimental-extra-source-files: README, CHANGES+extra-source-files: README.md, CHANGES.md license: BSD3 license-file: LICENSE build-type: Simple@@ -20,25 +20,57 @@ at the Haskell Symposium, 2012. (<http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf>) - As of this release date, Haddock was not able to properly process the code- and produce documentation. Hence, all of the documentation is in the- README file distributed with the package. This README is also accessible- from the project home page.+ The Haddock documentation does not build with the Haddock distributed with+ GHC 7.6.x, but it does build with HEAD. Please see links from the project+ homepage to find the built documentation. source-repository this type: git location: https://github.com/goldfirere/singletons.git- tag: v0.8.6- subdir: devel+ tag: v0.9.0 library build-depends: - base >= 4 && < 5,+ base >= 4.6 && < 5, mtl >= 2.1.1, template-haskell, containers >= 0.5,- syb >= 0.3- exposed-modules: Data.Singletons, Data.Singletons.CustomStar,- Data.Singletons.TypeRepStar- other-modules: Data.Singletons.Promote, Data.Singletons.Singletons,- Data.Singletons.Util, Data.Singletons.Exports+ syb >= 0.3,+ th-desugar >= 1.2+ default-language: Haskell2010+ exposed-modules: Data.Singletons,+ Data.Singletons.CustomStar,+ Data.Singletons.TypeRepStar,+ Data.Singletons.List,+ Data.Singletons.Bool,+ Data.Singletons.Maybe,+ Data.Singletons.Either,+ Data.Singletons.Tuple+ Data.Singletons.TH,+ Data.Singletons.Eq,+ Data.Singletons.Prelude,+ Data.Singletons.Types,+ Data.Singletons.Decide,+ Data.Singletons.Void++ other-modules: Data.Singletons.Promote,+ Data.Singletons.Singletons,+ Data.Singletons.Util,+ Data.Singletons.Core++-- This DOES NOT WORK with GHC HEAD because of -dynamic-too problems+-- test-suite compile+-- type: exitcode-stdio-1.0+-- ghc-options: -Wall -Werror -main-is Test.Main+-- default-language: Haskell2010+-- main-is: Test/Main.hs++-- build-depends:+-- base >= 4.6 && < 5,+-- constraints >= 0.3,+-- containers >= 0.5,+-- syb >= 0.3,+-- mtl >= 2.1.1,+-- th-desugar >= 1.2,+-- template-haskell+