diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,27 @@ +Copyright (c) 2012, Richard Eisenberg +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, +this list of conditions and the following disclaimer in the documentation +and/or other materials provided with the distribution. + +3. Neither the name of the author nor the names of its contributors may be +used to endorse or promote products derived from this software without +specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -0,0 +1,404 @@ +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 (June 2, 2012), 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.5.20120529 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 Singletons.Lib. + + +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-dpeth explanation of these +definitions. + + +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 SingE (a :: k) where + type Demote a :: * + fromSing :: Sing a -> Demote (Any :: k) + +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 'Demote' associated +kind-indexed type family maps, for example, types of the kind @Nat@ +back to the type @Nat@. + + +class (SingI a, SingE a) => SingRep a +instance (SingI a, SingE a) => SingRep a + +'SingRep' is a synonym for @('SingI' a, 'SingE' 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 (b ~ Any) => SingKind (b :: 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 (Any :: k)@ is defined. + + +class (t ~ Any) => SEq (t :: 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. + + +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 +---------------------------- + +The following constructs are fully supported: + +* variables +* tuples +* constructors +* infix expressions +* !, ~, and _ patterns +* aliased patterns (except at top-level) +* lists +* (+) sections +* (x +) sections +* undefined +* deriving Eq + +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. + + +------------- +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 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 expected 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/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Singletons/CustomStar.hs b/Singletons/CustomStar.hs new file mode 100644 --- /dev/null +++ b/Singletons/CustomStar.hs @@ -0,0 +1,91 @@ +{- Singletons/CustomStar.hs + +(c) Richard Eisenbeg 2012 +eir@cis.upenn.edu + +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! +-} + +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module Singletons.CustomStar where + +import Language.Haskell.TH +import Singletons.Util +import Singletons.Promote +import Singletons.Singletons +import Control.Monad + +-- Produce a representation and singleton for the collection of types given +singletonStar :: [Name] -> 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"] + fakeCtors <- zipWithM (mkCtor False) names kinds + eqTypeInstances <- mapM mkEqTypeInstance [ (c1, c2) | c1 <- fakeCtors, + c2 <- fakeCtors ] + singletonDecls <- singDataD True [] repName [] fakeCtors + [mkName "Eq", mkName "Show", mkName "Read"] + return $ repDecl : + eqTypeInstances ++ + singletonDecls + where -- get the kinds of the arguments to the tycon with the given name + getKind :: Name -> Q [Kind] + getKind name = do + info <- reifyWithWarning name + case info of + TyConI (DataD (_:_) _ _ _ _) -> + fail "Cannot make a representation of a constrainted data type" + TyConI (DataD [] _ tvbs _ _) -> + return $ map extractTvbKind tvbs + TyConI (NewtypeD (_:_) _ _ _ _) -> + fail "Cannot make a representation of a constrainted newtype" + TyConI (NewtypeD [] _ tvbs _ _) -> + return $ map extractTvbKind tvbs + TyConI (TySynD _ tvbs _) -> + return $ map extractTvbKind tvbs + PrimTyConI _ n _ -> + return $ replicate n StarT + _ -> fail $ "Invalid thing for representation: " ++ (show name) + + -- 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 real name args = do + (types, vars) <- evalForPair $ mapM kindToType args + let ctor = NormalC ((if real then reinterpret else id) name) + (map (\ty -> (NotStrict, ty)) types) + if length vars > 0 + then return $ ForallC (map PlainTV vars) [] ctor + else return ctor + + -- demote a kind back to a type, accumulating any unbound parameters + kindToType :: Kind -> QWithAux [Name] Type + kindToType (ForallT _ _ _) = fail "Explicit forall encountered in kind" + kindToType (AppT k1 k2) = do + t1 <- kindToType k1 + t2 <- kindToType k2 + return $ AppT t1 t2 + kindToType (SigT _ _) = fail "Sort signature encountered in kind" + kindToType (VarT n) = do + addElement n + return $ VarT n + kindToType (ConT n) = return $ ConT n + kindToType (PromotedT _) = fail "Promoted type used as a kind" + kindToType (TupleT n) = return $ TupleT n + kindToType (UnboxedTupleT _) = fail "Unboxed tuple kind encountered" + kindToType ArrowT = return ArrowT + kindToType ListT = return ListT + kindToType (PromotedTupleT _) = fail "Promoted tuple kind encountered" + kindToType PromotedNilT = fail "Promoted nil kind encountered" + kindToType PromotedConsT = fail "Promoted cons kind encountered" + kindToType StarT = return $ ConT repName + kindToType ConstraintT = + fail $ "Cannot make a representation of a type that has " ++ + "an argument of kind Constraint" + kindToType (LitT _) = fail "Literal encountered at the kind level" diff --git a/Singletons/Lib.hs b/Singletons/Lib.hs new file mode 100644 --- /dev/null +++ b/Singletons/Lib.hs @@ -0,0 +1,158 @@ +{- Singletons/Lib.hs + +(c) Richard Eisenberg 2012 +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 TypeFamilies, GADTs, KindSignatures, TemplateHaskell, + DataKinds, PolyKinds, TypeOperators, MultiParamTypeClasses, + FlexibleContexts, RankNTypes, UndecidableInstances, + FlexibleInstances, ScopedTypeVariables + #-} + +module Singletons.Lib ( + Any, + Demote, Sing(..), SingI, sing, SingE, fromSing, SingRep, (:==), (:==:), + 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, + ) where + +import Prelude hiding ((++)) +import Singletons.Singletons +import Singletons.Promote +import Language.Haskell.TH +import GHC.Exts +import Singletons.Util + +-- Declarations of singleton structures +data family Sing (a :: k) +class SingI (a :: k) where + sing :: Sing a +class SingE (a :: k) where + type Demote a :: * + fromSing :: Sing a -> Demote (Any :: k) + +-- SingRep is a synonym for (SingI, SingE) +class (SingI a, SingE a) => SingRep a +instance (SingI a, SingE a) => SingRep a + +type family (a :: k) :==: (b :: k) :: Bool +type a :== b = a :==: b -- :== and :==: are synonyms + +data SingInstance (a :: k) where + SingInstance :: SingRep a => SingInstance a +class (b ~ Any) => SingKind (b :: k) where + singInstance :: forall (a :: k). Sing a -> SingInstance a + +-- provide a few useful singletons... +$(genSingletons [''Bool, ''Maybe, ''Either, ''[]]) +$(genSingletons [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)]) + +-- ... with some functions over Booleans +$(singletons [d| + not :: Bool -> Bool + not False = True + not True = False + + (&&) :: Bool -> Bool -> Bool + False && a = False + True && a = a + + (||) :: Bool -> Bool -> Bool + False || a = a + True || a = True + |]) + +-- symmetric syntax synonyms +type a :&&: b = a :&& b +type a :||: b = a :|| b + +type a :/=: b = Not (a :==: b) +type a :/= b = a :/=: b + +-- the singleton analogue of @Eq@ +class (t ~ Any) => SEq (t :: 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) + (%:==) = (%==%) + (%:/=) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b) + a %:/= b = sNot (a %==% b) + (%/=%) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a :/=: b) + (%/=%) = (%:/=) + +-- 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 + +-- singleton conditional +sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c) +sIf STrue b c = b +sIf SFalse b c = c + +type instance '[] :==: '[] = True +type instance '[] :==: (h ': t) = False +type instance (h ': t) :==: '[] = False +type instance (h ': t) :==: (h' ': t') = (h :==: h') :&&: (t :==: t') + +instance SEq (Any :: k) => SEq (Any :: [k]) where + SNil %==% SNil = STrue + SNil %==% (SCons _ _) = SFalse + (SCons _ _) %==% SNil = SFalse + (SCons a b) %==% (SCons a' b') = (a %==% a') %:&& (b %==% b') + +type family Head (a :: [k]) :: k +type instance Head (h ': t) = h + +type family Tail (a :: [k]) :: [k] +type instance Tail (h ': t) = t + +-- must handle (++) by hand because of bug in module interface system +-- when kind-polymorphic code is produced by Template Haskell +(++) :: [a] -> [a] -> [a] +[] ++ a = a +(h:t) ++ a = h:(t ++ a) + +type family (a :: [k]) :++ (b :: [k]) :: [k] +type instance '[] :++ a = a +type instance (h ': t) :++ a = (h ': (t :++ a)) + +(%:++) :: Sing a -> Sing b -> Sing (a :++ b) +SNil %:++ a = a +(SCons h t) %:++ a = sCons h (t %:++ a) + +-- 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) + + conToPat :: Con -> Q Pat + conToPat = ctor1Case + (\name tys -> conP name (replicate (length tys) wildP)) + +-- useful when suppressing GHC's warnings about incomplete pattern matches +bugInGHC :: forall a. a +bugInGHC = error "Bug encountered in GHC -- this should never happen" diff --git a/Singletons/Promote.hs b/Singletons/Promote.hs new file mode 100644 --- /dev/null +++ b/Singletons/Promote.hs @@ -0,0 +1,544 @@ +{- Singletons/Promote.hs + +(c) Richard Eisenberg 2012 +eir@cis.upenn.edu + +This file contains functions to promote term-level constructs to the +type level. It is an internal module to the singletons package. +-} + +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module Singletons.Promote where + +import Language.Haskell.TH +import Singletons.Util +import Prelude hiding (exp) +import qualified Data.Map as Map +import qualified Data.Set as Set +import Control.Monad +import Data.Maybe +import Control.Monad.Writer +import Data.List + +anyTypeName, falseName, trueName, andName, tyEqName, repName, ifName, + headName, tailName :: Name +anyTypeName = mkName "Any" +falseName = mkName "False" +trueName = mkName "True" +andName = mkName "&&" +tyEqName = mkName ":==:" +repName = mkName "Rep" +ifName = mkName "If" +headName = mkName "Head" +tailName = mkName "Tail" + +falseTy :: Type +falseTy = promoteDataCon falseName + +trueTy :: Type +trueTy = promoteDataCon trueName + +andTy :: Type +andTy = promoteVal andName + +ifTyFam :: Type +ifTyFam = ConT ifName + +headTyFam :: Type +headTyFam = ConT headName + +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 (ClassI dec instances) = + fail "Promotion of class info not supported" +promoteInfo (ClassOpI name ty className fixity) = + fail "Promotion of class members info not supported" +promoteInfo (TyConI dec) = evalWithoutAux $ promoteDec Map.empty dec +promoteInfo (FamilyI dec instances) = + fail "Promotion of type family info not yet supported" -- KindFams +promoteInfo (PrimTyConI name numArgs unlifted) = + fail "Promotion of primitive type constructors not supported" +promoteInfo (DataConI name ty tyname fixity) = + fail $ "Promotion of individual constructors not supported; " ++ + "promote the type instead" +promoteInfo (VarI name ty mdec fixity) = + fail "Promotion of value info not supported" +promoteInfo (TyVarI name ty) = + fail "Promotion of type variable info not supported" + +promoteDataCon :: Name -> Type +promoteDataCon name = + if isTupleName name + then PromotedTupleT (tupleDegree $ nameBase name) + else PromotedT name + +promoteValName :: Name -> Name +promoteValName n + | nameBase n == "undefined" = anyTypeName + | otherwise = upcase n + +promoteVal :: Name -> Type +promoteVal = ConT . promoteValName + +promoteType :: Type -> Q Kind +promoteType (ForallT tvbs [] ty) = promoteType ty -- ForallKinds +promoteType (ForallT _ (_:_) _) = fail "Cannot promote type with constrained variables" +promoteType (VarT name) = return $ VarT name +promoteType (ConT name) = return $ if (nameBase name) == "TypeRep" || + (nameBase name) == (nameBase repName) + then StarT else ConT name +promoteType (TupleT n) = return $ TupleT n +promoteType (UnboxedTupleT n) = fail "Promotion of unboxed tuples not supported" +promoteType ArrowT = return ArrowT +promoteType ListT = return ListT +promoteType (AppT (AppT ArrowT (ForallT (_:_) _ _)) _) = + fail "Cannot promote types of rank above 1." +promoteType (AppT ty1 ty2) = do + k1 <- promoteType ty1 + k2 <- promoteType ty2 + return $ AppT k1 k2 +promoteType (SigT ty _) = fail "Cannot promote type of kind other than *" +promoteType (LitT _) = fail "Cannot promote a type-level literal" +promoteType (PromotedT _) = fail "Cannot promote a promoted data constructor" +promoteType (PromotedTupleT _) = fail "Cannot promote tuples that are already promoted" +promoteType PromotedNilT = fail "Cannot promote a nil that is already promoted" +promoteType PromotedConsT = fail "Cannot promote a cons that is already promoted" +promoteType StarT = fail "* used as a type" +promoteType ConstraintT = fail "Constraint used as a type" + +-- 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 qdec = do + decls <- qdec + (promDecls, _) <- promoteDecs decls + return $ decls ++ promDecls + +checkForRep :: [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 decls = + checkForRep (map extractNameFromDec decls) + where extractNameFromDec :: Dec -> Name + extractNameFromDec (DataD _ name _ _ _) = name + extractNameFromDec (NewtypeD _ name _ _ _) = name + extractNameFromDec (TySynD name _ _) = name + extractNameFromDec (FamilyD _ name _ _) = name + extractNameFromDec _ = mkName "NotRep" + +-- Promote a list of declarations; returns the promoted declarations +-- and a list of names of declarations without accompanying type signatures. +-- (This list is needed by singletons to strike such definitions.) + +-- Promoting declarations proceeds in two stages: +-- 1) Promote everything except type signatures +-- 2) Promote type signatures. This must be done in a second pass because +-- a function type signature gets promoted to a type family declaration. +-- Although function signatures do not differentiate between uniform parameters +-- and non-uniform parameters, type family declarations do. We need +-- to process a function's definition to get the count of non-uniform +-- 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 decls = do + checkForRepInDecls decls + let vartbl = Map.empty + (newDecls, numArgsTable) <- evalForPair $ mapM (promoteDec vartbl) decls + (declss, namess) <- mapAndUnzipM (promoteDec' numArgsTable) decls + let moreNewDecls = concat declss + names = concat namess + noTypeSigs = Set.toList $ Set.difference (Map.keysSet $ + Map.filter (>= 0) numArgsTable) + (Set.fromList names) + noTypeSigsPro = map promoteValName noTypeSigs + newDecls' = foldl (\decls name -> + filter (not . (containsName name)) decls) + (concat newDecls) (noTypeSigs ++ noTypeSigsPro) + mapM_ (\n -> report False $ "No type binding for " ++ (show (nameBase n)) ++ + "; removing all declarations including it") + noTypeSigs + return (newDecls' ++ moreNewDecls, noTypeSigs) + +-- produce the type instance for (:==:) for the given pair of constructors +mkEqTypeInstance :: (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") + let lvars = map VarT lnames + rvars = map VarT rnames + return $ TySynInstD + tyEqName + [foldType (PromotedT name) lvars, + foldType (PromotedT name) rvars] + (tyAll (zipWith (\l r -> foldType (ConT tyEqName) [l, r]) + lvars rvars)) + else do + let (lname, lNumArgs) = extractNameArgs c1 + (rname, rNumArgs) = extractNameArgs c2 + lnames <- replicateM lNumArgs (newName "a") + rnames <- replicateM rNumArgs (newName "b") + return $ TySynInstD + tyEqName + [foldType (PromotedT lname) (map VarT lnames), + foldType (PromotedT rname) (map VarT rnames)] + falseTy + where tyAll :: [Type] -> Type -- "all" at the type level + tyAll [] = trueTy + tyAll [one] = one + tyAll (h:t) = foldType andTy [h, (tyAll t)] + +-- keeps track of the number of non-uniform parameters to promoted values +type NumArgsTable = Map.Map Name Int +type NumArgsQ = QWithAux NumArgsTable + +-- 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 -> NumArgsQ [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 + instDecls <- lift $ mapM (promoteClause vars' proName) clauses + addBinding name numArgs -- remember the number of parameters + return $ concat instDecls + where getNumPats :: Clause -> Int + getNumPats (Clause pats _ _) = length pats +promoteDec vars (ValD pat body decs) = do + -- see also the comment for promoteTopLevelPat + 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 + if any (flip containsName rhs) (map lhsName lhss) + then do -- definition is recursive. use type families & require ty sigs + mapM (flip addBinding 0) (map lhsRawName lhss) + return $ (map (\(LHS _ nm hole) -> TySynInstD nm [] (hole rhs)) lhss) ++ + decls ++ decls' + else do -- definition is not recursive; just use "type" decls + mapM (flip addBinding typeSynonymFlag) (map lhsRawName lhss) + return $ (map (\(LHS _ nm hole) -> TySynD nm [] (hole rhs)) lhss) ++ + decls ++ decls' +promoteDec vars (DataD cxt name tvbs ctors derivings) = + promoteDataD vars cxt name tvbs ctors derivings +promoteDec vars (NewtypeD cxt name tvbs ctor derivings) = + promoteDataD vars cxt name tvbs [ctor] derivings +promoteDec vars (TySynD name tvbs ty) = + fail "Promotion of type synonym declaration not yet supported" +promoteDec vars (ClassD cxt name tvbs fundeps decs) = + fail "Promotion of class declaration not yet supported" +promoteDec vars (InstanceD cxt ty decs) = + fail "Promotion of instance declaration not yet supported" +promoteDec vars (SigD name ty) = return [] -- handle in promoteDec' +promoteDec vars (ForeignD fgn) = + fail "Promotion of foreign function declaration not yet supported" +promoteDec vars (InfixD fixity name) + | isUpcase name = return [] -- automatic: promoting a type or data ctor + | otherwise = return [InfixD fixity (promoteValName name)] -- value +promoteDec vars (PragmaD prag) = + fail "Promotion of pragmas not yet supported" +promoteDec vars (FamilyD flavour name tvbs mkind) = + fail "Promotion of type and data families not yet supported" +promoteDec vars (DataInstD cxt name tys ctors derivings) = + fail "Promotion of data instances not yet supported" +promoteDec vars (NewtypeInstD cxt name tys ctors derivings) = + fail "Promotion of newtype instances not yet supported" +promoteDec vars (TySynInstD name tys ty) = + 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] -> NumArgsQ [Dec] +promoteDataD vars cxt name tvbs ctors derivings = + if any (\n -> (nameBase n) == "Eq") derivings + then do + let pairs = [ (c1, c2) | c1 <- ctors, c2 <- ctors ] + lift $ mapM mkEqTypeInstance pairs + 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' :: NumArgsTable -> Dec -> Q ([Dec], [Name]) +promoteDec' nat (SigD name ty) = case Map.lookup name nat of + Nothing -> fail $ "Type declaration is missing its binding: " ++ (show name) + Just numArgs -> + -- if there are no args, then use a type synonym, not a type family + -- in the type synonym case, we ignore the type signature + if numArgs == typeSynonymFlag then return $ ([], [name]) else do + k <- promoteType ty + 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") + return ([FamilyD TypeFam + (promoteValName name) + (zipWith KindedTV tyvarNames argKs) + (Just resultK)], [name]) + where unravel :: Kind -> [Kind] -- get argument kinds from an arrow kind + unravel (AppT (AppT ArrowT k1) k2) = + let ks = unravel k2 in k1 : ks + unravel k = [k] + + ravel :: [Kind] -> Q Kind + ravel [] = fail "Internal error: raveling nil" + ravel [k] = return k + ravel (h:t) = do + k <- ravel t + return $ (AppT (AppT ArrowT h) k) +promoteDec' _ _ = return ([], []) + +promoteClause :: TypeTable -> Name -> Clause -> Q [Dec] +promoteClause vars name (Clause pats body []) = do + -- promoting the patterns creates variable bindings. These are passed + -- to the function promoted the RHS + (types, vartbl) <- evalForPair $ mapM promotePat pats + let vars' = Map.union vars vartbl + (ty, decls) <- evalForPair $ promoteBody vars' body + return $ decls ++ [TySynInstD name types ty] +promoteClause _ _ (Clause _ _ (_:_)) = + fail "A <> clause in a function definition is not yet supported" + +-- the LHS of a top-level expression is a name and "type with hole" +-- the hole is filled in by the RHS +data TopLevelLHS = LHS { lhsRawName :: Name -- the unpromoted name + , lhsName :: Name + , lhsHole :: Type -> Type + } + +-- Treatment of top-level patterns is different from other patterns +-- 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 (LitP _) = fail "Cannot declare a global literal." +promoteTopLevelPat (VarP name) = return [LHS name (promoteValName name) id] +promoteTopLevelPat (TupP pats) = case length pats of + 0 -> return [] -- unit as LHS of pattern... ignore + 1 -> fail "1-tuple encountered during top-level pattern promotion" + n -> promoteTopLevelPat (ConP (tupleDataName n) pats) +promoteTopLevelPat (UnboxedTupP _) = + fail "Promotion of unboxed tuples not supported" + +-- 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 + when (length argTypes /= length pats) $ + fail $ "Inconsistent data constructor pattern: " ++ (show name) ++ " " ++ + (show pats) + kind <- lift $ promoteType ctorType + argKinds <- lift $ mapM promoteType argTypes + extractorNamesRaw <- lift $ replicateM (length pats) (newName "Extract") + + -- 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 + let extractorNames = map (mkName . show) extractorNamesRaw + varName <- lift $ newName "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 -> + addElement $ TySynInstD extractorName + [foldType (promoteDataCon name) + (map VarT componentNames)] + (VarT componentName)) + extractorNames componentNames + + -- now we have the extractor families. Use the appropriate families + -- in the "holes" + promotedPats <- mapM promoteTopLevelPat pats + return $ concat $ + zipWith (\lhslist extractor -> + map (\(LHS raw nm hole) -> LHS raw nm + (hole . (AppT (ConT extractor)))) + lhslist) + promotedPats extractorNames + where extractTypes :: 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 datacon + (TyConI (DataD _cxt tyname tvbs cons _derivs)) = + let mcon = find ((== datacon) . fst . extractNameArgs) cons in + case mcon of + Nothing -> fail $ "Internal error reifying " ++ (show datacon) + Just con -> return (foldType (ConT tyname) + (map (VarT . extractTvbName) tvbs), + extractConArgs con) + extractTypesHelper datacon + (TyConI (NewtypeD cxt tyname tvbs con derivs)) = + extractTypesHelper datacon (TyConI (DataD cxt tyname tvbs [con] derivs)) + extractTypesHelper datacon _ = + fail $ "Cannot promote data constructor " ++ (show datacon) + + extractConArgs :: Con -> [Type] + extractConArgs = ctor1Case (\_ tys -> tys) +promoteTopLevelPat (InfixP l name r) = promoteTopLevelPat (ConP name [l, r]) +promoteTopLevelPat (UInfixP _ _ _) = + fail "Unresolved infix constructors not supported" +promoteTopLevelPat (ParensP _) = + fail "Unresolved infix constructors not supported" +promoteTopLevelPat (TildeP pat) = do + lift $ report False "Lazy pattern converted into regular pattern in promotion" + promoteTopLevelPat pat +promoteTopLevelPat (BangP pat) = do + lift $ report False "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" +promoteTopLevelPat WildP = return [] +promoteTopLevelPat (RecP _ _) = + fail "Promotion of record patterns at top level not yet supported" + +-- must do a similar trick as what is in the ConP case, but this is easier +-- because Lib defined Head and Tail +promoteTopLevelPat (ListP pats) = do + promotedPats <- mapM promoteTopLevelPat pats + return $ concat $ snd $ + mapAccumL (\extractFn lhss -> + ((AppT tailTyFam) . extractFn, + map (\(LHS raw nm hole) -> + LHS raw nm (hole . (AppT headTyFam) . extractFn)) lhss)) + id promotedPats +promoteTopLevelPat (SigP pat _) = do + lift $ report False $ "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 + +-- 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 (VarP name) = do + tyVar <- lift $ newName (nameBase name) + addBinding name (VarT tyVar) + return $ VarT tyVar +promotePat (TupP pats) = do + types <- mapM promotePat pats + let baseTup = PromotedTupleT (length types) + tup = foldType baseTup types + return tup +promotePat (UnboxedTupP _) = fail "Unboxed tuples not supported" +promotePat (ConP name pats) = do + types <- mapM promotePat pats + let tyCon = foldType (promoteDataCon name) types + return tyCon +promotePat (InfixP pat1 name pat2) = promotePat (ConP name [pat1, pat2]) +promotePat (UInfixP _ _ _) = fail "Unresolved infix constructions not supported" +promotePat (ParensP _) = fail "Unresolved infix constructions not supported" +promotePat (TildeP pat) = do + lift $ report False "Lazy pattern converted into regular pattern in promotion" + promotePat pat +promotePat (BangP pat) = do + lift $ report False "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" + 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 $ report False $ "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] + +promoteBody :: TypeTable -> Body -> QWithDecs 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 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 (AppE exp1 exp2) = do + ty1 <- promoteExp vars exp1 + ty2 <- promoteExp vars exp2 + return $ AppT ty1 ty2 +promoteExp vars (InfixE mexp1 exp mexp2) = + case (mexp1, mexp2) of + (Nothing, Nothing) -> promoteExp vars exp + (Just exp1, Nothing) -> promoteExp vars (AppE exp exp1) + (Nothing, Just exp2) -> + fail "Promotion of right-only sections not yet supported" + (Just exp1, Just exp2) -> promoteExp vars (AppE (AppE exp exp1) exp2) +promoteExp vars (UInfixE _ _ _) = + fail "Promotion of unresolved infix operators not supported" +promoteExp vars (ParensE _) = fail "Promotion of unresolved parens not supported" +promoteExp vars (LamE pats exp) = + fail "Promotion of lambda expressions not yet supported" +promoteExp vars (TupE exps) = do + tys <- mapM (promoteExp vars) exps + let tuple = PromotedTupleT (length tys) + tup = foldType tuple tys + return tup +promoteExp vars (UnboxedTupE _) = fail "Promotion of unboxed tuples not supported" +promoteExp vars (CondE bexp texp fexp) = do + tys <- mapM (promoteExp vars) [bexp, texp, fexp] + return $ foldType ifTyFam tys +promoteExp vars (LetE decs exp) = + fail "Promotion of let statements not yet supported" +promoteExp vars (CaseE exp matches) = + fail "Promotion of case statements not yet supported" +promoteExp vars (DoE stmts) = fail "Promotion of do statements not supported" +promoteExp vars (CompE stmts) = + fail "Promotion of list comprehensions not yet supported" +promoteExp vars (ArithSeqE _) = fail "Promotion of ranges not supported" +promoteExp vars (ListE exps) = do + tys <- mapM (promoteExp vars) exps + return $ foldr (\ty lst -> AppT (AppT PromotedConsT ty) lst) PromotedNilT tys +promoteExp vars (SigE exp ty) = + fail "Promotion of explicit type annotations not yet supported" +promoteExp vars (RecConE name fields) = + fail "Promotion of record construction not yet supported" +promoteExp vars (RecUpdE exp fields) = + fail "Promotion of record updates not yet supported" diff --git a/Singletons/Singletons.hs b/Singletons/Singletons.hs new file mode 100644 --- /dev/null +++ b/Singletons/Singletons.hs @@ -0,0 +1,599 @@ +{- Singletons/Singletons.hs + +(c) Richard Eisenberg 2012 +eir@cis.upenn.edu + +This file contains functions to refine constructs to work with singleton +types. It is an internal module to the singletons package. +-} + +{-# OPTIONS_GHC -fwarn-incomplete-patterns #-} + +module Singletons.Singletons where + +import Language.Haskell.TH.Lib +import Language.Haskell.TH.Syntax hiding (lift) +import Singletons.Util +import Singletons.Promote +import qualified Data.Map as Map +import Control.Monad +import Control.Monad.Writer +import Data.List + +-- map to track bound variables +type ExpTable = Map.Map Name Exp + +-- translating a type gives a type with a hole in it, +-- represented here as a function +type TypeFn = Type -> Type + +-- a list of argument types extracted from a type application +type TypeContext = [Type] + +singFamilyName, isSingletonName, forgettableName, comboClassName, witnessName, + demoteName, singKindClassName, singInstanceMethName, singInstanceName, + sEqClassName, sEqMethName, sconsName, snilName, smartSconsName, + smartSnilName, sIfName, undefinedName :: Name +singFamilyName = mkName "Sing" +isSingletonName = mkName "SingI" +forgettableName = mkName "SingE" +comboClassName = mkName "SingRep" +witnessName = mkName "sing" +forgetName = mkName "fromSing" +demoteName = mkName "Demote" +singKindClassName = mkName "SingKind" +singInstanceMethName = mkName "singInstance" +singInstanceName = mkName "SingInstance" +sEqClassName = mkName "SEq" +sEqMethName = mkName "%==%" +sconsName = mkName "SCons" +snilName = mkName "SNil" +smartSconsName = mkName "sCons" +smartSnilName = mkName "sNil" +sIfName = mkName "sIf" +undefinedName = mkName "undefined" + +mkTupleName :: Int -> Name +mkTupleName n = mkName $ "STuple" ++ (show n) + +singFamily :: Type +singFamily = ConT singFamilyName + +singKindConstraint :: Kind -> Pred +singKindConstraint k = ClassP singKindClassName [SigT anyType k] + +singInstanceMeth :: Exp +singInstanceMeth = VarE singInstanceMethName + +singInstanceTyCon :: Type +singInstanceTyCon = ConT singInstanceName + +singInstanceDataCon :: Exp +singInstanceDataCon = ConE singInstanceName + +singInstancePat :: Pat +singInstancePat = ConP singInstanceName [] + +demote :: Type +demote = ConT demoteName + +anyType :: Type +anyType = ConT anyTypeName + +singDataConName :: Name -> Name +singDataConName nm = case nameBase nm of + "[]" -> snilName + ":" -> sconsName + tuple | isTupleString tuple -> mkTupleName (tupleDegree tuple) + _ -> prefixUCName "S" ":%" nm + +singTyConName :: Name -> Name +singTyConName name | nameBase name == "[]" = mkName "SList" + | isTupleName name = mkTupleName (tupleDegree $ nameBase name) + | otherwise = prefixUCName "S" ":%" name + +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 + | otherwise = (prefixLCName "s" "%") $ upcase n + +singVal :: Name -> Exp +singVal = VarE . singValName + +-- generate singleton definitions from an ADT +genSingletons :: [Name] -> Q [Dec] +genSingletons names = do + checkForRep names + infos <- mapM reifyWithWarning names + decls <- mapM singInfo infos + return $ concat decls + +singInfo :: Info -> Q [Dec] +singInfo (ClassI dec instances) = + fail "Singling of class info not supported" +singInfo (ClassOpI name ty className fixity) = + fail "Singling of class members info not supported" +singInfo (TyConI dec) = singDec dec +singInfo (FamilyI dec instances) = + fail "Singling of type family info not yet supported" -- KindFams +singInfo (PrimTyConI name numArgs unlifted) = + fail "Singling of primitive type constructors not supported" +singInfo (DataConI name ty tyname fixity) = + fail $ "Singling of individual constructors not supported; " ++ + "single the type instead" +singInfo (VarI name ty mdec fixity) = + fail "Singling of value info not supported" +singInfo (TyVarI name ty) = + fail "Singling of type variable info not supported" + +-- 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 a = ctorCases + (\name types -> do + let sName = singDataConName name + sCon = singDataCon name + pCon = promoteDataCon name + indexNames <- lift $ replicateM (length types) (newName "n") + let indices = map VarT indexNames + kinds <- lift $ mapM promoteType types + args <- lift $ buildArgTypes types indices + let tvbs = zipWith KindedTV indexNames kinds + bareKindVars = filter isVarK 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) + (NormalB $ foldExp sCon (replicate (length types) + (VarE witnessName))) + []] + + -- smart constructor type signature + smartConType <- lift $ conTypesToFunType indexNames args kinds + (AppT singFamily (foldType pCon indices)) + addElement $ SigD (smartConName name) 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)) + (\tvbs cxt ctor -> case cxt of + _:_ -> fail "Singling of constrained constructors not yet supported" + [] -> singCtor a ctor) + where buildArgTypes :: [Type] -> [Type] -> Q [Type] + buildArgTypes types indices = do + typeFns <- mapM (singType False) 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) []] + +-- refine the declarations given +singletons :: Q [Dec] -> Q [Dec] +singletons qdec = do + decls <- qdec + singDecs decls + +singDecs :: [Dec] -> Q [Dec] +singDecs 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) + +singDec :: 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) +singDec (ValD _ (GuardedB _) _) = + fail "Singling of definitions of values with a pattern guard not yet supported" +singDec (ValD _ _ (_:_)) = + fail "Singling of definitions of values with a <> clause not yet supported" +singDec (ValD pat (NormalB exp) []) = do + (sPat, vartbl) <- evalForPair $ singPat TopLevel pat + sExp <- singExp vartbl exp + return [ValD sPat (NormalB sExp) []] +singDec (DataD (_:_) _ _ _ _) = + fail "Singling of constrained datatypes not supported" +singDec (DataD cxt name tvbs ctors derivings) = + singDataD False cxt name tvbs ctors derivings +singDec (NewtypeD cxt name tvbs ctor derivings) = + singDataD False cxt name tvbs [ctor] derivings +singDec (TySynD name tvbs ty) = + fail "Singling of type synonyms not yet supported" +singDec (ClassD cxt name tvbs fundeps decs) = + fail "Singling of class declaration not yet supported" +singDec (InstanceD cxt ty decs) = + fail "Singling of class instance not yet supported" +singDec (SigD name ty) = do + tyTrans <- singType True ty + return [SigD (singValName name) (tyTrans (promoteVal name))] +singDec (ForeignD fgn) = + let name = extractName fgn in do + report False $ "Singling of foreign functions not supported -- " ++ + (show name) ++ " ignored" + return [] + where extractName :: Foreign -> Name + extractName (ImportF _ _ _ n _) = n + extractName (ExportF _ _ n _) = n +singDec (InfixD fixity name) + | isUpcase name = return [InfixD fixity (singDataConName name)] + | otherwise = return [InfixD fixity (singValName name)] +singDec (PragmaD prag) = + let name = extractName prag in do + report False $ "Singling of pragmas not supported -- " ++ + (show name) ++ " ignored" + return [] + where extractName :: Pragma -> Name + extractName (InlineP n _) = n + extractName (SpecialiseP n _ _) = n +singDec (FamilyD flavour name tvbs mkind) = + fail "Singling of type and data families not yet supported" +singDec (DataInstD cxt name tys ctors derivings) = + fail "Singling of data instances not yet supported" +singDec (NewtypeInstD cxt name tys ctor derivings) = + fail "Singling of newtype instances not yet supported" +singDec (TySynInstD name tys ty) = + fail "Singling of type family instances not yet supported" + +-- 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 rep cxt name tvbs ctors derivings = do + aName <- newName "a" + 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 + let singKindInst = + InstanceD [] + (AppT (ConT singKindClassName) + (SigT anyType k)) + [FunD singInstanceMethName + (map mkSingInstanceClause ctors')] + + -- SEq instance + let ctorPairs = [ (c1, c2) | c1 <- ctors', c2 <- ctors' ] + sEqMethClauses <- mapM mkEqMethClause ctorPairs + let sEqInst = + InstanceD (map (\k -> ClassP sEqClassName [SigT anyType k]) + (getBareKinds ctors')) + (AppT (ConT sEqClassName) + (SigT anyType k)) + [FunD sEqMethName sEqMethClauses] + + -- e.g. type SNat (a :: Nat) = Sing a + let kindedSynInst = + TySynD (singTyConName name) + [KindedTV aName k] + (AppT singFamily a) + + -- SingE instance + forgetClauses <- mapM mkForgetClause ctors + let singEInst = + InstanceD [] + (AppT (ConT forgettableName) (SigT a k)) + [TySynInstD demoteName [a] + (foldType (ConT name) + (map (\kv -> AppT demote (SigT anyType (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) []) + + 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)) + [] + + 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)] + (NormalB $ foldExp + (ConE $ (if rep then reinterpret else id) name) + (map (AppE (VarE forgetName) . VarE) varNames)) + [] + + getBareKinds :: [Con] -> [Kind] + getBareKinds = foldl (\res -> ctorCases + (\_ _ -> res) -- must be a constant constructor + (\tvbs _ _ -> union res (filter isVarK $ map extractTvbKind tvbs))) + [] + + allExp :: [Exp] -> Exp + allExp [] = singDataCon trueName + allExp [one] = one + allExp (h:t) = AppE (AppE (singVal andName) h) (allExp t) + +singKind :: 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" +singKind (ConT _) = fail "Singling of named kinds not yet supported" +singKind (TupleT _) = fail "Singling of tuple kinds not yet supported" +singKind (UnboxedTupleT _) = fail "Unboxed tuple used as kind" +singKind ArrowT = fail "Singling of unsaturated arrow kinds not yet supported" +singKind ListT = fail "Singling of list kinds not yet supported" +singKind (AppT (AppT ArrowT k1) k2) = do + k1fn <- singKind k1 + k2fn <- singKind k2 + k <- newName "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 _ _) = + fail "Singling of explicitly annotated kinds not yet supported" +singKind (LitT _) = fail "Type literal used as kind" +singKind (PromotedT _) = fail "Promoted data constructor used as kind" +singKind (PromotedTupleT _) = fail "Promoted tuple used as kind" +singKind PromotedNilT = fail "Promoted nil used as kind" +singKind PromotedConsT = fail "Promoted cons used as kind" +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 = singTypeRec [] + +-- 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 ctx pos (ForallT tvbs (_:_) ty) = + fail "Singling of constrained functions not yet supported" +singTypeRec (_:_) pos (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 (_:_) pos (VarT _) = + fail "Singling of type variables of arrow kinds not yet supported" +singTypeRec [] pos (VarT name) = + return $ \ty -> AppT singFamily ty +singTypeRec ctx pos (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 + return $ \ty -> AppT singFamily ty +singTypeRec ctx pos (UnboxedTupleT n) = + fail "Singling of unboxed tuple types not yet supported" +singTypeRec ctx pos ArrowT = case ctx of + [ty1, ty2] -> do + t <- newName "t" + sty1 <- singTypeRec [] (not pos) ty1 + sty2 <- singTypeRec [] pos 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 [SigT anyType 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 = + 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) = + 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 _) = + fail "Singling of promoted data constructors not yet supported" +singTypeRec ctx pos (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" + +singClause :: 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 + 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 + +-- we need to know where a pattern is to anticipate when +-- GHC's brain might explode +data PatternContext = LetBinding + | CaseStatement + | TopLevel + | Parameter + | Statement + deriving Eq + +checkIfBrainWillExplode :: PatternContext -> ExpsQ () +checkIfBrainWillExplode CaseStatement = return () +checkIfBrainWillExplode Statement = return () +checkIfBrainWillExplode Parameter = return () +checkIfBrainWillExplode _ = + fail $ "Can't use a singleton pattern outside of a case-statement or\n" ++ + "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 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 +singPat patCxt (TupP pats) = + singPat patCxt (ConP (tupleDataName (length pats)) pats) +singPat patCxt (UnboxedTupP pats) = + fail "Singling of unboxed tuples not supported" +singPat patCxt (ConP name pats) = do + checkIfBrainWillExplode patCxt + pats' <- mapM (singPat patCxt) pats + return $ ConP (singDataConName name) pats' +singPat patCxt (InfixP pat1 name pat2) = singPat patCxt (ConP name [pat1, pat2]) +singPat patCxt (UInfixP _ _ _) = + fail "Singling of unresolved infix patterns not supported" +singPat patCxt (ParensP _) = + fail "Singling of unresolved paren patterns not supported" +singPat patCxt (TildeP pat) = do + pat' <- singPat patCxt pat + return $ TildeP pat' +singPat patCxt (BangP pat) = do + 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 + pat' <- singPat patCxt pat + addBinding name (VarE newName) + return $ AsP name pat' +singPat patCxt WildP = return WildP +singPat patCxt (RecP name fields) = + fail "Singling of record patterns not yet supported" +singPat patCxt (ListP pats) = do + checkIfBrainWillExplode patCxt + sPats <- mapM (singPat patCxt) pats + return $ foldr (\elt lst -> ConP sconsName [elt, lst]) (ConP snilName []) sPats +singPat patCxt (SigP pat ty) = + fail "Singling of annotated patterns not yet supported" +singPat patCxt (ViewP exp pat) = + fail "Singling of view patterns not yet supported" + +singExp :: 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 (AppE exp1 exp2) = do + exp1' <- singExp vars exp1 + exp2' <- singExp vars exp2 + return $ AppE exp1' exp2' +singExp vars (InfixE mexp1 exp mexp2) = + case (mexp1, mexp2) of + (Nothing, Nothing) -> singExp vars exp + (Just exp1, Nothing) -> singExp vars (AppE exp exp1) + (Nothing, Just exp2) -> + fail "Singling of right-only sections not yet supported" + (Just exp1, Just exp2) -> singExp vars (AppE (AppE exp exp1) exp2) +singExp vars (UInfixE _ _ _) = + fail "Singling of unresolved infix expressions not supported" +singExp vars (ParensE _) = + fail "Singling of unresolved paren expressions not supported" +singExp vars (LamE pats exp) = do + (pats', vartbl) <- evalForPair $ mapM (singPat Parameter) pats + let vars' = Map.union vartbl vars -- order matters; union is left-biased + singExp vars' exp +singExp vars (TupE exps) = do + sExps <- mapM (singExp vars) exps + sTuple <- singExp vars (ConE (tupleDataName (length exps))) + return $ foldExp sTuple sExps +singExp vars (UnboxedTupE exps) = + fail "Singling of unboxed tuple not supported" +singExp vars (CondE bexp texp fexp) = do + exps <- mapM (singExp vars) [bexp, texp, fexp] + return $ foldExp (VarE sIfName) exps +singExp vars (LetE decs exp) = + fail "Singling of let expressions not yet supported" +singExp vars (CaseE exp matches) = + fail "Singling of case expressions not yet supported" +singExp vars (DoE stmts) = + fail "Singling of do expressions not yet supported" +singExp vars (CompE stmts) = + fail "Singling of list comprehensions not yet supported" +singExp vars (ArithSeqE range) = + 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 +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" diff --git a/Singletons/TypeRepStar.hs b/Singletons/TypeRepStar.hs new file mode 100644 --- /dev/null +++ b/Singletons/TypeRepStar.hs @@ -0,0 +1,31 @@ +{- Singletons/TypeRepStar.hs + +(c) Richard Eisenberg 2012 +eir@cis.upenn.edu + +This file contains the definitions for considering TypeRep to be the demotion +of *. This is still highly experimental, so expect unusual results! + +-} + +{-# LANGUAGE RankNTypes, TypeFamilies, KindSignatures, FlexibleInstances, + GADTs, UndecidableInstances, ScopedTypeVariables #-} + +module Singletons.TypeRepStar where + +import Singletons.Lib +import Data.Typeable + +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 (a :: *) where + type Demote a = TypeRep + fromSing STypeRep = typeOf (undefined :: a) +instance SingKind (Any :: *) where + singInstance STypeRep = SingInstance diff --git a/Singletons/Util.hs b/Singletons/Util.hs new file mode 100644 --- /dev/null +++ b/Singletons/Util.hs @@ -0,0 +1,163 @@ +{- Singletons/Util.hs + +(c) Richard Eisenberg 2012 +eir@cis.upenn.edu + +This file contains helper functions internal to the singletons package. +Users of the package should not need to consult this file. +-} + +module Singletons.Util where + +import Language.Haskell.TH +import Language.Haskell.TH.Syntax +import Data.Char +import Data.Maybe +import Data.Data +import Data.List +import Control.Monad +import Control.Monad.Writer +import qualified Data.Map as Map +import Data.Generics + +-- 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 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 + +-- extract the degree of a tuple +tupleDegree :: String -> Int +tupleDegree "()" = 0 +tupleDegree s = length s - 1 + +-- 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 +ctorCases genFun forallFun ctor = case ctor of + NormalC name stypes -> genFun name (map snd stypes) + RecC name vstypes -> genFun name (map (\(_,_,ty) -> ty) vstypes) + InfixC (_,ty1) name (_,ty2) -> genFun name [ty1, ty2] + ForallC [] [] ctor' -> ctorCases genFun forallFun ctor' + ForallC tvbs cx ctor' -> forallFun tvbs cx ctor' + +-- reduce the four cases of a 'Con' to just 1: a polymorphic Con is treated +-- as a monomorphic one +ctor1Case :: (Name -> [Type] -> a) -> Con -> a +ctor1Case mono = ctorCases mono (\_ _ ctor -> ctor1Case mono ctor) + +-- extract the name and number of arguments to a constructor +extractNameArgs :: Con -> (Name, Int) +extractNameArgs = ctor1Case (\name tys -> (name, length tys)) + +-- reinterpret a name. This is useful when a Name has an associated +-- namespace that we wish to forget +reinterpret :: Name -> Name +reinterpret = mkName . nameBase + +-- is an identifier uppercase? +isUpcase :: Name -> Bool +isUpcase n = let first = head (nameBase n) in isUpper first || first == ':' + +-- make an identifier uppercase +upcase :: Name -> Name +upcase n = + let str = nameBase n + first = head str in + if isLetter first + then mkName ((toUpper first) : tail str) + else mkName (':' : str) + +-- make an identifier lowercase +locase :: Name -> Name +locase n = + let str = nameBase n + first = head str in + if isLetter first + then mkName ((toLower first) : tail str) + else mkName (tail str) -- remove the ":" + +-- put an uppercase prefix on a name. Takes two prefixes: one for identifiers +-- and one for symbols +prefixUCName :: String -> String -> Name -> Name +prefixUCName pre tyPre n = case (nameBase n) of + (':' : rest) -> mkName (tyPre ++ rest) + alpha -> mkName (pre ++ alpha) + +-- put a lowercase prefix on a name. Takes two prefixes: one for identifiers +-- and one for symbols +prefixLCName :: String -> String -> Name -> Name +prefixLCName pre tyPre n = + let str = nameBase n + first = head str in + if isLetter first + 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 + +-- extract the kind from a TyVarBndr. Returns '*' by default. +extractTvbKind :: TyVarBndr -> Kind +extractTvbKind (PlainTV _) = StarT -- FIXME: This seems wrong. +extractTvbKind (KindedTV _ k) = k + +-- apply a type to a list of types +foldType :: Type -> [Type] -> Type +foldType = foldl AppT + +-- apply an expression to a list of expressions +foldExp :: Exp -> [Exp] -> Exp +foldExp = foldl AppE + +-- is a kind a variable? +isVarK :: Kind -> Bool +isVarK (VarT _) = True +isVarK _ = False + +-- a monad transformer for writing a monoid alongside returning a Q +type QWithAux m = WriterT m Q + +-- run a computation with an auxiliary monoid, discarding the monoid result +evalWithoutAux :: QWithAux m a -> Q a +evalWithoutAux = liftM fst . runWriterT + +-- run a computation with an auxiliary monoid, returning only the monoid result +evalForAux :: QWithAux m a -> Q m +evalForAux = execWriterT + +-- 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 + +-- in a computation with an auxiliary map, add a binding to the map +addBinding :: Ord k => k -> v -> QWithAux (Map.Map k v) () +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 elt = tell [elt] + +-- does a TH structure contain a name? +containsName :: Data a => Name -> a -> Bool +containsName n = everything (||) (mkQ False (== n)) + diff --git a/singletons.cabal b/singletons.cabal new file mode 100644 --- /dev/null +++ b/singletons.cabal @@ -0,0 +1,37 @@ +name: singletons +version: 0.8 +cabal-version: >= 1.8 +synopsis: A framework for generating singleton types +homepage: http://www.cis.upenn.edu/~eir/packages/singletons +category: Dependent Types +author: Richard Eisenberg +maintainer: Richard Eisenberg +stability: experimental +extra-source-files: README +license: BSD3 +license-file: LICENSE +build-type: Simple +description: + This library generates singleton types, promoted functions, and singleton + functions using Template Haskell. It is useful for programmers who wish + to use dependently typed programming techniques. The library was originally + presented in /Dependently typed programming with singletons/, submitted + to 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. + +library + build-depends: + base >= 4 && < 5, + mtl >= 2.1.1, + template-haskell, + containers >= 0.5, + syb >= 0.3 + exposed-modules: Singletons.Lib, Singletons.CustomStar, + Singletons.TypeRepStar + other-modules: Singletons.Promote, Singletons.Singletons, + Singletons.Util