open-typerep (empty) → 0.1
raw patch · 8 files changed
+748/−0 lines, 8 filesdep +basedep +constraintsdep +criterionsetup-changed
Dependencies added: base, constraints, criterion, open-typerep, syntactic, tagged
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- benchmarks/Dynamic.hs +57/−0
- examples/Simple.hs +28/−0
- open-typerep.cabal +123/−0
- src/Data/TypeRep.hs +61/−0
- src/Data/TypeRep/Internal.hs +414/−0
- src/Data/TypeRep/Sub.hs +33/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Emil Axelsson++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * 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.++ * Neither the name of Emil Axelsson nor the names of other+ 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+OWNER 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ benchmarks/Dynamic.hs view
@@ -0,0 +1,57 @@+{-# OPTIONS_GHC -fcontext-stack=100 #-}++import Criterion.Main+import Criterion.Config+import Data.Monoid++import Data.TypeRep++import qualified Data.Dynamic as Base -- For comparison++++type Types = BoolType :+: IntType :+: ListType++type Types2 = CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: CharType :+: BoolType :+: IntType+ -- 30 terms++dynList :: Int -> [Dynamic Types]+dynList n = concat [[toDyn i, toDyn (even i)] | i <- [0..n]]++dynList2 :: Int -> [Dynamic Types2]+dynList2 n = concat [[toDyn i, toDyn (even i)] | i <- [0..n]]++dynListBase :: Int -> [Base.Dynamic]+dynListBase n = concat [[Base.toDyn i, Base.toDyn (even i)] | i <- [0..n]]++dynSum :: [Dynamic Types] -> Int+dynSum ds = sum [i | d <- ds, Just i <- [fromDyn d]]++dynSum2 :: [Dynamic Types2] -> Int+dynSum2 ds = sum [i | d <- ds, Just i <- [fromDyn d]]++dynSumBase :: [Base.Dynamic] -> Int+dynSumBase ds = sum [i | d <- ds, Just i <- [Base.fromDynamic d]]++testDyn :: Int -> Int+testDyn = dynSum . dynList++testDyn2 :: Int -> Int+testDyn2 = dynSum2 . dynList2++testDynBase :: Int -> Int+testDynBase = dynSumBase . dynListBase++main :: IO ()+main = defaultMainWith (defaultConfig {cfgSummaryFile = Last $ Just "bench-results/dynamic.csv"}) (return ())+ [ bgroup "size=1000"+ [ bench "testDyn" $ nf testDyn 1000+ , bench "testDyn2" $ nf testDyn2 1000+ , bench "testDynBase" $ nf testDynBase 1000+ ]+ , bgroup "size=2000"+ [ bench "testDyn" $ nf testDyn 2000+ , bench "testDyn2" $ nf testDyn2 2000+ , bench "testDynBase" $ nf testDynBase 2000+ ]+ ]
+ examples/Simple.hs view
@@ -0,0 +1,28 @@+import Control.Monad++import Data.TypeRep++type MyUniverse = IntType :+: BoolType++hlist :: [Dynamic MyUniverse]+hlist = [toDyn True, toDyn (1 :: Int)]+ -- Prints: [True,1]++addDyn :: (TypeEq ts ts, PWitness Num ts ts) => Dynamic ts -> Dynamic ts -> Maybe (Dynamic ts)+addDyn (Dyn ta a) (Dyn tb b) = do+ Dict <- typeEq ta tb+ Dict <- pwit pNum ta+ return (Dyn ta (a+b))+++test1 = toDyn (1 :: Int) `addDyn` toDyn (2 :: Int)+ -- Prints: Just 3++main = do+ unless t1 $ fail "Test 1 failed"+ unless t2 $ fail "Test 2 failed"+ putStrLn "All tests passed"+ where+ t1 = show hlist == "[True,1]"+ t2 = show (test1 :: Maybe (Dynamic MyUniverse)) == "Just 3"+
+ open-typerep.cabal view
@@ -0,0 +1,123 @@+name: open-typerep+version: 0.1+synopsis: Open type representations and dynamic types+description: This package uses Data Types à la Carte to provide open type representations+ and dynamic types/coercions for open type universes.+ .+ Example 1 (dynamic types):+ .+ > type MyUniverse = IntType :+: BoolType+ >+ > hlist :: [Dynamic MyUniverse]+ > hlist = [toDyn True, toDyn (1 :: Int)]+ .+ > *Main> hlist+ > [True,1]+ .+ Note that if we were using "Data.Dynamic", it would just print+ .+ > [<<Bool>>,<<Int>>]+ .+ Example 2 (dynamically typed addition):+ .+ > addDyn :: (TypeEq ts ts, PWitness Num ts ts) => Dynamic ts -> Dynamic ts -> Maybe (Dynamic ts)+ > addDyn (Dyn ta a) (Dyn tb b) = do+ > Dict <- typeEq ta tb+ > Dict <- pwit pNum ta+ > return (Dyn ta (a+b))+ .+ "Data.Dynamic" could only do this monomorphically, for one 'Num' type at a+ time.+author: Emil Axelsson+maintainer: emax@chalmers.se+copyright: Copyright (c) 2014, Emil Axelsson+license: BSD3+license-file: LICENSE+homepage: https://github.com/emilaxelsson/open-typerep+bug-reports: https://github.com/emilaxelsson/open-typerep/issues+category: Dependent Types+stability: experimental+build-type: Simple+cabal-version: >=1.10+tested-with: GHC==7.6.2, GHC==7.8.2++extra-source-files:+ examples/*.hs++source-repository head+ type: git+ location: https://github.com/emilaxelsson/open-typerep++library+ hs-source-dirs: src++ exposed-modules:+ Data.TypeRep+ Data.TypeRep.Internal++ other-modules:+ Data.TypeRep.Sub++ build-depends:+ base >=4 && <5,+ constraints >=0.3,+ syntactic >=2.0,+ tagged >=0.4++ default-language: Haskell2010++ default-extensions:+ FlexibleContexts+ FlexibleInstances+ GADTs+ MultiParamTypeClasses+ ScopedTypeVariables+ TypeFamilies+ TypeOperators++ other-extensions:+ UndecidableInstances,+ OverlappingInstances++test-suite examples+ type: exitcode-stdio-1.0++ hs-source-dirs: examples++ main-is: Simple.hs++ default-language: Haskell2010++ build-depends:+ open-typerep,+ base++ default-language: Haskell2010++ default-extensions:+ FlexibleContexts+ GADTs+ TypeOperators++benchmark dynamic-bench+ type: exitcode-stdio-1.0++ hs-source-dirs: benchmarks++ main-is: Dynamic.hs++ build-depends:+ base,+ criterion,+ open-typerep++ default-language: Haskell2010++ default-extensions:+ FlexibleInstances+ GADTs+ MultiParamTypeClasses+ TypeOperators++ other-extensions:+ TemplateHaskell
+ src/Data/TypeRep.hs view
@@ -0,0 +1,61 @@+-- | Open type representations and dynamic types++module Data.TypeRep+ ( -- * Helper types+ module Data.Constraint+ , module Data.Proxy+ , module Data.Syntactic+ -- * Type representations+ , Typeable+ , TypeRep+ , TypeEq+ , typeEq+ , matchCon+ , matchConM+ , Witness+ , PWitness+ , wit+ , pwit+ -- * Dynamic types+ , cast+ , gcast+ , Dynamic (..)+ , toDyn+ , fromDyn+ , dynToInteger+ -- * Type class witnessing+ , Any+ , witTypeable+ , pwitTypeable+ , pAny+ , pEq+ , pOrd+ , pShow+ , pNum+ , pIntegral+ , BoolType+ , CharType+ , IntType+ , FloatType+ , ListType+ , FunType+ , boolType+ , charType+ , intType+ , floatType+ , listType+ , funType+ -- * Sub-universes+ , module Data.TypeRep.Sub+ ) where++++import Data.Constraint (Dict (..))+import Data.Proxy (Proxy (..))++import Data.Syntactic ((:+:), Project (..), (:<:) (..), E (..))++import Data.TypeRep.Internal+import Data.TypeRep.Sub+
+ src/Data/TypeRep/Internal.hs view
@@ -0,0 +1,414 @@+{-# LANGUAGE UndecidableInstances #-}++-- | Open type representations and dynamic types++module Data.TypeRep.Internal where++++import Data.Constraint (Dict (..))+import Data.Proxy (Proxy (..))++import Data.Syntactic++++----------------------------------------------------------------------------------------------------+-- * Type representations+----------------------------------------------------------------------------------------------------++-- | 'Full'-indexed type representation+type TR = AST++-- | This class provides reification of type @a@ in a universe @t@. @`Typeable` t a@ means that @a@+-- is in the type universe represented by @t@.+class Typeable t a+ where+ typeRep' :: TR t (Full a)++-- | Representation of type @a@ in a type universe @t@+--+-- This type can also be seen as a witness that @a@ is a member of @t@ (i.e. @`Typeable` t a@); see+-- 'witTypeable'.+newtype TypeRep t a = TypeRep { unTypeRep :: TR t (Full a) }+ -- The newtype is mainly because 'TR' cannot be partially applied++instance Render t => Show (TypeRep t a)+ where+ show = render . desugar++instance Syntactic (TypeRep t a)+ where+ type Domain (TypeRep t a) = t+ type Internal (TypeRep t a) = a+ desugar = unTypeRep+ sugar = TypeRep++-- | Reification of type @a@ in a type universe @t@+typeRep :: Typeable t a => TypeRep t a+typeRep = TypeRep typeRep'++-- | Equality on type representations+class TypeEq t u+ where+ typeEqSym+ :: (t sig1, Args (AST u) sig1)+ -> (t sig2, Args (AST u) sig2)+ -> Maybe (Dict (DenResult sig1 ~ DenResult sig2))++instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t+ where+ typeEqSym (InjL t1, as1) (InjL t2, as2) = typeEqSym (t1,as1) (t2,as2)+ typeEqSym (InjR t1, as1) (InjR t2, as2) = typeEqSym (t1,as1) (t2,as2)+ typeEqSym _ _ = Nothing++instance TypeEq t t => TypeEq (AST t) t+ where+ typeEqSym (Sym t1, as1) (Sym t2, as2) = typeEqSym (t1,as1) (t2,as2)+ typeEqSym (s1 :$ a1, as1) (s2 :$ a2, as2) = typeEqSym (s1, a1 :* as1) (s2, a2 :* as2)++instance TypeEq Empty t+ where+ typeEqSym = error "typeEqSym: Empty"++-- | Equality on type representations+typeEq :: forall t a b . TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))+typeEq (TypeRep s1) (TypeRep s2) = typeEqSym (s1, Nil :: Args (AST t) (Full a)) (s2, Nil)++-- | Type constructor matching. This function makes it possible to match on type representations+-- without dealing with the underlying 'AST' representation.+--+-- For example, to check that a 'TypeRep' represents the type @a -> Int@ for some @a@:+--+-- > is_atoi :: (TypeEq t t, IntType :<: t) => TypeRep t a -> Bool+-- > is_atoi t+-- > | [E ta, E tb] <- matchCon t+-- > , Just _ <- typeEq ta intType = True+-- > | otherwise = False+matchCon :: TypeRep t c -> [E (TypeRep t)]+matchCon = simpleMatch (\_ -> foldrArgs (\t -> (E (TypeRep t) :)) []) . unTypeRep++-- | Monadic version of 'matchCon'+--+-- > matchConM = return . matchCon+--+-- 'matchConM' is convenient when matching types in a monad, e.g.:+--+-- > do ...+-- > [E ta, E tb] <- matchConM t+-- > Dict <- typeEq ta tb+-- > ...+matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]+matchConM = return . matchCon++-- | Witness a type constraint for a reified type+class Witness p t u+ where+ witSym :: t sig -> Args (AST u) sig -> Dict (p (DenResult sig))++instance (Witness p t1 t, Witness p t2 t) => Witness p (t1 :+: t2) t+ where+ witSym (InjL s) as = witSym s as+ witSym (InjR s) as = witSym s as++instance Witness p t t => Witness p (AST t) t+ where+ witSym (Sym s) as = witSym s as+ witSym (s :$ a) as = witSym s (a :* as)++-- | Partially witness a type constraint for a reified type+class PWitness p t u+ where+ pwitSym :: t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))+ pwitSym _ _ = Nothing++instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t+ where+ pwitSym (InjL s) as = pwitSym s as+ pwitSym (InjR s) as = pwitSym s as++instance PWitness p t t => PWitness p (AST t) t+ where+ pwitSym (Sym s) as = pwitSym s as+ pwitSym (s :$ a) as = pwitSym s (a :* as)++-- | Default implementation of 'pwitSym' for types that have a 'Witness' instance+pwitSymDefault :: Witness p t u => t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))+pwitSymDefault t = Just . witSym t++-- | Witness a type constraint for a reified type+wit :: forall p t a . Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)+wit _ (TypeRep a) = witSym a (Nil :: Args (AST t) (Full a))++-- | Partially witness a type constraint for a reified type+pwit :: forall p t a . PWitness p t t => Proxy p -> TypeRep t a -> Maybe (Dict (p a))+pwit _ (TypeRep a) = pwitSym a (Nil :: Args (AST t) (Full a))++++----------------------------------------------------------------------------------------------------+-- * Dynamic types+----------------------------------------------------------------------------------------------------++-- | Safe cast (does not use @unsafeCoerce@)+cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> a -> Maybe b+cast _ a = do+ Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)+ return a++-- | Safe generalized cast (does not use @unsafeCoerce@)+gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Maybe (c b)+gcast _ a = do+ Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)+ return a++-- | Dynamic type parameterized on a type universe+data Dynamic t+ where+ Dyn :: TypeRep t a -> a -> Dynamic t++toDyn :: Typeable t a => a -> Dynamic t+toDyn = Dyn typeRep++fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Maybe a+fromDyn (Dyn t a) = do+ Dict <- typeEq t (typeRep :: TypeRep t a)+ return a++instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)+ where+ Dyn ta a == Dyn tb b+ | Just Dict <- typeEq ta tb+ , Dict <- wit pEq ta+ = a == b+ _ == _ = False++instance Witness Show t t => Show (Dynamic t)+ where+ show (Dyn t a) | Dict <- wit pShow t = show a++++----------------------------------------------------------------------------------------------------+-- * Specific types/classes+----------------------------------------------------------------------------------------------------++-- | The universal class+class Any a+instance Any a++-- | Witness a 'Typeable' constraint for a reified type+witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)+witTypeable = wit Proxy++-- | Partially witness a 'Typeable' constraint for a reified type+pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Maybe (Dict (Typeable t a))+pwitTypeable = pwit Proxy++pAny :: Proxy Any+pAny = Proxy++pEq :: Proxy Eq+pEq = Proxy++pOrd :: Proxy Ord+pOrd = Proxy++pShow :: Proxy Show+pShow = Proxy++pNum :: Proxy Num+pNum = Proxy++pIntegral :: Proxy Integral+pIntegral = Proxy++data BoolType a where BoolType :: BoolType (Full Bool)+data CharType a where CharType :: CharType (Full Char)+data IntType a where IntType :: IntType (Full Int)+data FloatType a where FloatType :: FloatType (Full Float)+data ListType a where ListType :: ListType (a :-> Full [a])+data FunType a where FunType :: FunType (a :-> b :-> Full (a -> b))++instance Render BoolType where renderSym BoolType = "Bool"+instance Render CharType where renderSym CharType = "Char"+instance Render IntType where renderSym IntType = "Int"+instance Render FloatType where renderSym FloatType = "Float"++instance Render ListType+ where+ renderSym ListType = "[]"+ renderArgs [a] ListType = "[" ++ a ++ "]"++instance Render FunType+ where+ renderSym FunType = "(->)"+ renderArgs [a,b] FunType = a ++ " -> " ++ b++boolType :: (Syntactic a, BoolType :<: Domain a, Internal a ~ Bool) => a+boolType = sugarSym BoolType++charType :: (Syntactic a, CharType :<: Domain a, Internal a ~ Char) => a+charType = sugarSym CharType++intType :: (Syntactic a, IntType :<: Domain a, Internal a ~ Int) => a+intType = sugarSym IntType++floatType :: (Syntactic a, FloatType :<: Domain a, Internal a ~ Float) => a+floatType = sugarSym FloatType++listType+ :: ( Syntactic list+ , Syntactic elem+ , Domain list ~ Domain elem+ , ListType :<: Domain list+ , Internal list ~ [Internal elem]+ , elem ~ c e+ , list ~ c l+ -- These last equalities are used to help type inference by forcing the representations+ -- to use the same type constructor (e.g. 'TR' or 'TypeRep')+ )+ => elem -> list+listType = sugarSym ListType++funType+ :: ( Syntactic fun+ , Syntactic a+ , Syntactic b+ , Domain fun ~ Domain a+ , Domain fun ~ Domain b+ , FunType :<: Domain fun+ , Internal fun ~ (Internal a -> Internal b)+ , a ~ c x+ , b ~ c y+ , fun ~ c z+ )+ => a -> b -> fun+funType = sugarSym FunType++instance (BoolType :<: t) => Typeable t Bool where typeRep' = boolType+instance (CharType :<: t) => Typeable t Char where typeRep' = charType+instance (IntType :<: t) => Typeable t Int where typeRep' = intType+instance (FloatType :<: t) => Typeable t Float where typeRep' = floatType+instance (ListType :<: t, Typeable t a) => Typeable t [a] where typeRep' = listType typeRep'+instance (FunType :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b) where typeRep' = funType typeRep' typeRep'++instance TypeEq BoolType t where typeEqSym (BoolType, Nil) (BoolType, Nil) = Just Dict+instance TypeEq CharType t where typeEqSym (CharType, Nil) (CharType, Nil) = Just Dict+instance TypeEq IntType t where typeEqSym (IntType, Nil) (IntType, Nil) = Just Dict+instance TypeEq FloatType t where typeEqSym (FloatType, Nil) (FloatType, Nil) = Just Dict++instance TypeEq t t => TypeEq ListType t+ where+ typeEqSym (ListType, a :* Nil) (ListType, b :* Nil) = do+ Dict <- typeEq (TypeRep a) (TypeRep b)+ return Dict++instance TypeEq t t => TypeEq FunType t+ where+ typeEqSym (FunType, a1 :* b1 :* Nil) (FunType, a2 :* b2 :* Nil) = do+ Dict <- typeEq (TypeRep a1) (TypeRep a2)+ Dict <- typeEq (TypeRep b1) (TypeRep b2)+ return Dict++instance (BoolType :<: t) => Witness (Typeable t) BoolType t where witSym BoolType Nil = Dict+instance (CharType :<: t) => Witness (Typeable t) CharType t where witSym CharType Nil = Dict+instance (IntType :<: t) => Witness (Typeable t) IntType t where witSym IntType Nil = Dict+instance (FloatType :<: t) => Witness (Typeable t) FloatType t where witSym FloatType Nil = Dict++instance (ListType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) ListType t+ where+ witSym ListType (a :* Nil)+ | Dict <- witTypeable (TypeRep a) = Dict++instance (FunType :<: t, Witness (Typeable t) t t) => Witness (Typeable t) FunType t+ where+ witSym FunType (a :* b :* Nil)+ | Dict <- witTypeable (TypeRep a)+ , Dict <- witTypeable (TypeRep b)+ = Dict++instance (BoolType :<: t) => PWitness (Typeable t) BoolType t where pwitSym = pwitSymDefault+instance (CharType :<: t) => PWitness (Typeable t) CharType t where pwitSym = pwitSymDefault+instance (IntType :<: t) => PWitness (Typeable t) IntType t where pwitSym = pwitSymDefault+instance (FloatType :<: t) => PWitness (Typeable t) FloatType t where pwitSym = pwitSymDefault+instance (ListType :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) ListType t where pwitSym ListType (a :* Nil) = do Dict <- pwitTypeable (TypeRep a); return Dict+instance (FunType :<: t, PWitness (Typeable t) t t) => PWitness (Typeable t) FunType t where pwitSym FunType (a :* b :* Nil) = do Dict <- pwitTypeable (TypeRep a); Dict <- pwitTypeable (TypeRep b); return Dict++instance Witness Any BoolType t where witSym _ _ = Dict+instance Witness Any CharType t where witSym _ _ = Dict+instance Witness Any IntType t where witSym _ _ = Dict+instance Witness Any FloatType t where witSym _ _ = Dict+instance Witness Any ListType t where witSym _ _ = Dict+instance Witness Any FunType t where witSym _ _ = Dict++instance PWitness Any BoolType t where pwitSym _ _ = Just Dict+instance PWitness Any CharType t where pwitSym _ _ = Just Dict+instance PWitness Any IntType t where pwitSym _ _ = Just Dict+instance PWitness Any FloatType t where pwitSym _ _ = Just Dict+instance PWitness Any ListType t where pwitSym _ _ = Just Dict+instance PWitness Any FunType t where pwitSym _ _ = Just Dict++instance Witness Eq BoolType t where witSym BoolType Nil = Dict+instance Witness Eq CharType t where witSym CharType Nil = Dict+instance Witness Eq IntType t where witSym IntType Nil = Dict+instance Witness Eq FloatType t where witSym FloatType Nil = Dict+instance Witness Eq t t => Witness Eq ListType t where witSym ListType (a :* Nil) | Dict <- wit pEq (TypeRep a) = Dict++instance PWitness Eq BoolType t where pwitSym = pwitSymDefault+instance PWitness Eq CharType t where pwitSym = pwitSymDefault+instance PWitness Eq IntType t where pwitSym = pwitSymDefault+instance PWitness Eq FloatType t where pwitSym = pwitSymDefault+instance PWitness Eq t t => PWitness Eq ListType t where pwitSym ListType (a :* Nil) = do Dict <- pwit pEq (TypeRep a); return Dict+instance PWitness Eq FunType t++instance Witness Ord BoolType t where witSym BoolType Nil = Dict+instance Witness Ord CharType t where witSym CharType Nil = Dict+instance Witness Ord IntType t where witSym IntType Nil = Dict+instance Witness Ord FloatType t where witSym FloatType Nil = Dict+instance Witness Ord t t => Witness Ord ListType t where witSym ListType (a :* Nil) | Dict <- wit pOrd (TypeRep a) = Dict++instance PWitness Ord BoolType t where pwitSym = pwitSymDefault+instance PWitness Ord CharType t where pwitSym = pwitSymDefault+instance PWitness Ord IntType t where pwitSym = pwitSymDefault+instance PWitness Ord FloatType t where pwitSym = pwitSymDefault+instance PWitness Ord t t => PWitness Ord ListType t where pwitSym ListType (a :* Nil) = do Dict <- pwit pOrd (TypeRep a); return Dict+instance PWitness Ord FunType t++instance Witness Show BoolType t where witSym BoolType Nil = Dict+instance Witness Show CharType t where witSym CharType Nil = Dict+instance Witness Show IntType t where witSym IntType Nil = Dict+instance Witness Show FloatType t where witSym FloatType Nil = Dict+instance Witness Show t t => Witness Show ListType t where witSym ListType (a :* Nil) | Dict <- wit pShow (TypeRep a) = Dict++instance PWitness Show BoolType t where pwitSym = pwitSymDefault+instance PWitness Show CharType t where pwitSym = pwitSymDefault+instance PWitness Show IntType t where pwitSym = pwitSymDefault+instance PWitness Show FloatType t where pwitSym = pwitSymDefault+instance PWitness Show t t => PWitness Show ListType t where pwitSym ListType (a :* Nil) = do Dict <- pwit pShow (TypeRep a); return Dict+instance PWitness Show FunType t++instance Witness Num IntType t where witSym IntType Nil = Dict+instance Witness Num FloatType t where witSym FloatType Nil = Dict++instance PWitness Num BoolType t+instance PWitness Num CharType t+instance PWitness Num IntType t where pwitSym = pwitSymDefault+instance PWitness Num FloatType t where pwitSym = pwitSymDefault+instance PWitness Num ListType t+instance PWitness Num FunType t++instance Witness Integral IntType t where witSym IntType Nil = Dict++instance PWitness Integral BoolType t+instance PWitness Integral CharType t+instance PWitness Integral IntType t where pwitSym = pwitSymDefault+instance PWitness Integral FloatType t+instance PWitness Integral ListType t+instance PWitness Integral FunType t++dynToInteger :: PWitness Integral t t => Dynamic t -> Maybe Integer+dynToInteger (Dyn tr a)+ | Just Dict <- pwit pIntegral tr = Just (toInteger a)+dynToInteger _ = Nothing+
+ src/Data/TypeRep/Sub.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE OverlappingInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-- | This module is only to limit the scope of the @OverlappingInstances@ flag++module Data.TypeRep.Sub where++++import Data.Syntactic++import Data.TypeRep.Internal++++-- | Sub-universe relation+--+-- In general, a universe @t@ is a sub-universe of @u@ if @u@ has the form+--+-- > t1 :+: t2 :+: ... :+: t+class SubUniverse sub sup+ where+ -- | Cast a type representation to a larger universe+ weakenUniverse :: TypeRep sub a -> TypeRep sup a++instance SubUniverse t t+ where+ weakenUniverse = id++instance (SubUniverse sub sup', sup ~ (t :+: sup')) => SubUniverse sub sup+ where+ weakenUniverse = sugar . mapAST InjR . desugar . weakenUniverse+