diff --git a/CHANGES b/CHANGES deleted file mode 100644 --- a/CHANGES +++ /dev/null @@ -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 diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 --- /dev/null +++ b/CHANGES.md @@ -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 diff --git a/Data/Singletons.hs b/Data/Singletons.hs --- a/Data/Singletons.hs +++ b/Data/Singletons.hs @@ -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 --} +{-# 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 +-- and the +-- original paper presenting this library, available at +-- . +-- +---------------------------------------------------------------------------- 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 <> 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 . +-- 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) diff --git a/Data/Singletons/Bool.hs b/Data/Singletons/Bool.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Bool.hs @@ -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 + |]) + diff --git a/Data/Singletons/Core.hs b/Data/Singletons/Core.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Core.hs @@ -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 + diff --git a/Data/Singletons/CustomStar.hs b/Data/Singletons/CustomStar.hs --- a/Data/Singletons/CustomStar.hs +++ b/Data/Singletons/CustomStar.hs @@ -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 diff --git a/Data/Singletons/Decide.hs b/Data/Singletons/Decide.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Decide.hs @@ -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 diff --git a/Data/Singletons/Either.hs b/Data/Singletons/Either.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Either.hs @@ -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 + |]) diff --git a/Data/Singletons/Eq.hs b/Data/Singletons/Eq.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Eq.hs @@ -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) diff --git a/Data/Singletons/Exports.hs b/Data/Singletons/Exports.hs deleted file mode 100644 --- a/Data/Singletons/Exports.hs +++ /dev/null @@ -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 diff --git a/Data/Singletons/List.hs b/Data/Singletons/List.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/List.hs @@ -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 + |]) + + diff --git a/Data/Singletons/Maybe.hs b/Data/Singletons/Maybe.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Maybe.hs @@ -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) + |]) diff --git a/Data/Singletons/Prelude.hs b/Data/Singletons/Prelude.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Prelude.hs @@ -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 diff --git a/Data/Singletons/Promote.hs b/Data/Singletons/Promote.hs --- a/Data/Singletons/Promote.hs +++ b/Data/Singletons/Promote.hs @@ -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 <> 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 <> 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) diff --git a/Data/Singletons/Singletons.hs b/Data/Singletons/Singletons.hs --- a/Data/Singletons/Singletons.hs +++ b/Data/Singletons/Singletons.hs @@ -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 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 <> 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)) diff --git a/Data/Singletons/TH.hs b/Data/Singletons/TH.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/TH.hs @@ -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 <> 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)) diff --git a/Data/Singletons/Tuple.hs b/Data/Singletons/Tuple.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Tuple.hs @@ -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) + |]) diff --git a/Data/Singletons/TypeRepStar.hs b/Data/Singletons/TypeRepStar.hs --- a/Data/Singletons/TypeRepStar.hs +++ b/Data/Singletons/TypeRepStar.hs @@ -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 diff --git a/Data/Singletons/Types.hs b/Data/Singletons/Types.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Types.hs @@ -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 diff --git a/Data/Singletons/Util.hs b/Data/Singletons/Util.hs --- a/Data/Singletons/Util.hs +++ b/Data/Singletons/Util.hs @@ -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 diff --git a/Data/Singletons/Void.hs b/Data/Singletons/Void.hs new file mode 100644 --- /dev/null +++ b/Data/Singletons/Void.hs @@ -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 diff --git a/README b/README deleted file mode 100644 --- a/README +++ /dev/null @@ -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 - - ---------------------------------- -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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`. diff --git a/singletons.cabal b/singletons.cabal --- a/singletons.cabal +++ b/singletons.cabal @@ -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 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. () - 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 +