th-kinds 0.1.1 → 0.2

raw patch · 3 files changed

+236/−152 lines, 3 filesdep +th-orphansdep ~template-haskellnew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: th-orphans

Dependency ranges changed: template-haskell

API changes (from Hackage documentation)

Files

• Language/Haskell/TH/KindInference.hs +163/−101
• Language/Haskell/TH/Unification.hs +49/−43
• th-kinds.cabal +24/−8

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-}  -- | A module to infer the kind of a given type within Template Haskell. -- Warning: this implements its own kind inference system, and is therefore@@ -7,14 +8,12 @@  -- import Control.Monad import Control.Monad.Trans-import Data.Ord-import Debug.Trace-import Data.Map((!))-import Data.Set+import Data.Set hiding (foldr) import Control.Monad.State.Strict import Text.ParserCombinators.ReadP hiding (get)  import Language.Haskell.TH hiding (AppE)+import Language.Haskell.TH.Instances () import Language.Haskell.TH.Unification import Language.Haskell.TH.PprLib hiding (empty, char) import qualified Language.Haskell.TH.PprLib as Ppr@@ -22,138 +21,178 @@ type KindUTerm = Term KindFunc Type KindAtom type KindUT = UnifT KindFunc Type KindAtom -instance Ord Type where-	compare = comparing show- type LoopKillerT = StateT (Set Name)-data KindFunc = KindArrow deriving (Eq, Show)-data KindAtom = Star deriving (Eq, Show)+data KindFunc = KindArrow deriving (Eq, Ord, Show)+data KindAtom = Star deriving (Eq, Ord, Show)  -- | Returns either an error message or the 'Kind' of the type referred to by the specified name. -- Works with datas, newtypes, type synonyms, type classes, data families, and type families. --  -- Note: There has been a bug observed in Template Haskell relating to the parsing of types.  This -- assumes that bug has been fixed, requiring GHC at least 6.12.2.-inferKind :: Name -> Q (Either String Kind)-inferKind name = do-	ans <- solveUnification defaultKind (evalStateT (infer (ConT name)) empty)-	either (return . Left) (\ (x, sol) -> return (Right $ termToK (subTerm defaultKind sol x))) ans+class InferKind t where+    inferKind :: t -> Q (Either String Kind) +instance InferKind Name where+    inferKind name = inferKind (ConT name)++instance InferKind Type where+    inferKind typ = do+      ans <- solveUnification defaultKind (evalStateT (infer typ) empty)+      either (return . Left) (\ (x, sol) -> return (Right $ termToK (subTerm defaultKind sol x))) ans+ defaultKind :: Explicit KindFunc KindAtom defaultKind = AtomE Star  termToK :: Explicit KindFunc KindAtom -> Kind+#if MIN_VERSION_template_haskell(2,8,0)+-- Kind became a synonym of Type here+termToK (AppE ~KindArrow t1 t2) = termToK t1 `AppT` termToK t2+#else termToK (AppE ~KindArrow t1 t2) = termToK t1 `ArrowK` termToK t2-termToK (AtomE ~Star) = StarK+#endif+termToK (AtomE ~Star) = StarT  infer :: Type -> LoopKillerT (KindUT Q) KindUTerm infer (TupleT n) = return (tupleKind n star) infer ArrowT = return (tupleKind 2 star) infer ListT = return (tupleKind 1 star) infer (AppT f x) = do-	fK <- infer f-	xK <- infer x-	let var = Var (AppT f x)-	unify fK (xK ->- var)-	return var+        fK <- infer f+        xK <- infer x+        let var = Var (AppT f x)+        unify fK (xK ->- var)+        return var infer (SigT t k) = do-	tK <- infer t-	unify tK (kToTerm k)-	return tK+        tK <- infer t+        unify tK (kToTerm k)+        return tK infer (ForallT bdrs cxt t) = do-	mapM_ handleBdr bdrs-	mapM_ handleCxt cxt-	infer t+        mapM_ handleBdr bdrs+        mapM_ handleCxt cxt+        infer t infer t@VarT{} = return $ Var t infer (ConT t) = do-	examine (Just t) t-	return (tyCon t)+        examine (Just t) t+        return (tyCon t)+infer t = error $ "inferKind - unimplemented: " ++ pprint t  matchUnboxedTuple :: ReadP Int matchUnboxedTuple = do-	string "(#"-	munchComma 1-	where	munchComma k = k `seq` ((do-			char ','-			munchComma (k+1)) <++ (do-			string "#)"-			return k))+        string "(#"+        munchComma 1+        where   munchComma k = k `seq` ((do+                        char ','+                        munchComma (k+1)) <++ (do+                        string "#)"+                        return k))  examine :: Maybe Name -> Name -> LoopKillerT (KindUT Q) () examine name0 name = do      mUnify name0 (tyVar name)      case [n | (n, "") <- readP_to_S matchUnboxedTuple (nameBase name)] of-	(n:_)	-> unify (tyVar name) (tupleKind n star)-	_	-> do-	  inf <- lift $ lift $ reify name-	  case inf of-		  ClassI dec	-> examineDec name0 dec-		  TyConI dec	-> examineDec name0 dec-		  PrimTyConI name n _ -> unify (tyVar name) (tupleKind n star)-		  TyVarI name typ -> do-		  	kind <- infer typ-			unify (tyVar name) kind-		  _ -> return ()-	+        (n:_)   -> unify (tyVar name) (tupleKind n star)+        _       -> do+          inf <- lift $ lift $ reify name+          case inf of+#if MIN_VERSION_template_haskell(2,5,0)+                  ClassI dec _is -> examineDec name0 dec+#else+                  ClassI dec    -> examineDec name0 dec+#endif+                  TyConI dec    -> examineDec name0 dec+                  PrimTyConI name n _ -> unify (tyVar name) (tupleKind n star)+                  TyVarI name typ -> do+                        kind <- infer typ+                        unify (tyVar name) kind+                  FamilyI dec insts -> do+                        examineDec name0 dec+                  _ -> return ()+ mUnify :: Maybe Name -> KindUTerm -> LoopKillerT (KindUT Q) ()-mUnify name0 k = case name0 of -	Just name0	-> unify (tyCon name0) k-	_		-> return ()+mUnify name0 k = case name0 of+        Just name0      -> unify (tyCon name0) k+        _               -> return ()  examineDec :: Maybe Name -> Dec -> LoopKillerT (KindUT Q) ()+#if MIN_VERSION_template_haskell(2,11,0)+examineDec name0 (DataD cxt name bdrs mK cons _) = do+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          mapM_ handleCxt cxt+          args <- mapM handleBdr bdrs+          unify (tyCon name) (foldr (->-) (maybe star kToTerm mK) args)+          mUnify name0 (tyCon name)+          mapM_ handleCon cons+examineDec name0 (NewtypeD cxt name bdrs mK con _) = do+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          mapM_ handleCxt cxt+          args <- mapM handleBdr bdrs+          unify (tyCon name) (foldr (->-) (maybe star kToTerm mK) args)+          mUnify name0 (tyCon name)+          handleCon con+#else examineDec name0 (DataD cxt name bdrs cons _) = do-	visited <- get-	unless (name `member` visited) $ do-	  modify (insert name)-	  mapM_ handleCxt cxt-	  args <- mapM handleBdr bdrs-	  unify (tyCon name) (foldr (->-) star args)-	  mUnify name0 (tyCon name)-	  mapM_ handleCon cons+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          mapM_ handleCxt cxt+          args <- mapM handleBdr bdrs+          unify (tyCon name) (foldr (->-) star args)+          mUnify name0 (tyCon name)+          mapM_ handleCon cons examineDec name0 (NewtypeD cxt name bdrs con _) = do-	visited <- get-	unless (name `member` visited) $ do-	  modify (insert name)-	  mapM_ handleCxt cxt-	  args <- mapM handleBdr bdrs-	  unify (tyCon name) (foldr (->-) star args)-	  mUnify name0 (tyCon name)-	  handleCon con+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          mapM_ handleCxt cxt+          args <- mapM handleBdr bdrs+          unify (tyCon name) (foldr (->-) star args)+          mUnify name0 (tyCon name)+          handleCon con+#endif examineDec name0 (ClassD cxt name bdrs _ _) = do-	visited <- get-	unless (name `member` visited) $ do-	  modify (insert name)-	  mapM_ handleCxt cxt-	  args <- mapM handleBdr bdrs-	  unify (tyCon name) (foldr (->-) star args)-	  mUnify name0 (tyCon name)+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          mapM_ handleCxt cxt+          args <- mapM handleBdr bdrs+          unify (tyCon name) (foldr (->-) star args)+          mUnify name0 (tyCon name)+#if MIN_VERSION_template_haskell(2,11,0)+examineDec name0 (DataFamilyD name bdrs mK) = do+#else examineDec name0 (FamilyD _ name bdrs mK) = do-	visited <- get-	unless (name `member` visited) $ do-	  modify (insert name)-	  mapM_ handleBdr bdrs-	  unify (tyCon name) (maybe star kToTerm mK)-	  mUnify name0 (tyCon name)+#endif+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          args <- mapM handleBdr bdrs+          unify (tyCon name) (foldr (->-) (maybe star kToTerm mK) args)+          mUnify name0 (tyCon name) examineDec name0 (TySynD name bdrs typ) = do-	visited <- get-	unless (name `member` visited) $ do-	  modify (insert name)-	  args <- mapM handleBdr bdrs-	  kind <- infer typ-	  unify (tyCon name) (foldr (->-) kind args)-	  mUnify name0 (tyCon name)+        visited <- get+        unless (name `member` visited) $ do+          modify (insert name)+          args <- mapM handleBdr bdrs+          kind <- infer typ+          unify (tyCon name) (foldr (->-) kind args)+          mUnify name0 (tyCon name) examineDec _ _ = return ()  handleCon :: Con -> LoopKillerT (KindUT Q) () handleCon (NormalC _ ts) = mapM_ (\ (_, t) -> infer t >>= unify star) ts handleCon (RecC _ ts) = mapM_ (\ (_, _, t) -> infer t >>= unify star) ts handleCon (InfixC (_, t1) _ (_, t2)) = do-	infer t1 >>= unify star-	infer t2 >>= unify star+        infer t1 >>= unify star+        infer t2 >>= unify star handleCon (ForallC bdrs cxt con) = do-	mapM_ handleBdr bdrs-	mapM_ handleCxt cxt-	handleCon con+        mapM_ handleBdr bdrs+        mapM_ handleCxt cxt+        handleCon con  tyCon :: Name -> KindUTerm tyCon = Var . ConT@@ -164,22 +203,45 @@ handleBdr :: TyVarBndr -> LoopKillerT (KindUT Q) KindUTerm handleBdr (PlainTV n) = return (tyVar n) handleBdr (KindedTV n k) = do-	unify (tyVar n) (kToTerm k)-	return (tyVar n)+        unify (tyVar n) (kToTerm k)+        return (tyVar n)  handleCxt :: Pred -> LoopKillerT (KindUT Q) ()+#if MIN_VERSION_template_haskell(2,10,0)+handleCxt typ =+        case unfoldInstance typ of+          Just (name, args) -> do+            kinds <- mapM infer args+            unify (Var (ConT name)) (foldr (->-) star kinds)+            examine (Just name) name+        where+          unfoldInstance :: Type -> Maybe (Name, [Type])+          unfoldInstance (ConT name) = Just (name, [])+          unfoldInstance (AppT t1 t2) = maybe Nothing (\ (name, types) -> Just (name, types ++ [t2])) (unfoldInstance t1)+          unfoldInstance _ = Nothing+handleCxt (AppT (AppT EqualityT t1) t2) = do+        k1 <- infer t1+        k2 <- infer t2+        unify k1 k2+#else handleCxt (ClassP name args) = do-	kinds <- mapM infer args-	unify (Var (ConT name)) (foldr (->-) star kinds)-	examine (Just name) name+        kinds <- mapM infer args+        unify (Var (ConT name)) (foldr (->-) star kinds)+        examine (Just name) name handleCxt (EqualP t1 t2) = do-	k1 <- infer t1-	k2 <- infer t2-	unify k1 k2+        k1 <- infer t1+        k2 <- infer t2+        unify k1 k2+#endif  kToTerm :: Kind -> KindUTerm+#if MIN_VERSION_template_haskell(2,8,0)+kToTerm (AppT a b) = kToTerm a ->- kToTerm b+kToTerm StarT = star+#else kToTerm (ArrowK a b) = kToTerm a ->- kToTerm b kToTerm StarK = star+#endif  (->-) :: KindUTerm -> KindUTerm -> KindUTerm (->-) = App KindArrow@@ -191,7 +253,7 @@ tupleKind n k = foldr (->-) k (replicate n star)  instance (Ppr a, Ppr b) => Ppr (Either a b) where-	ppr (Left x) = text "Left" <+> parens (ppr x)-	ppr (Right x) = text "Right" <+> parens (ppr x)+        ppr (Left x) = text "Left" <+> parens (ppr x)+        ppr (Right x) = text "Right" <+> parens (ppr x) instance Ppr Char where-	ppr = Ppr.char+        ppr = Ppr.char

@@ -1,67 +1,73 @@-{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE CPP, UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}  module Language.Haskell.TH.Unification (subTerm, Term(..), MonadUnify(..), UnifT, Explicit(..), solveUnification) where +#if __GLASGOW_HASKELL__ < 710+import Control.Applicative (Applicative)+#endif import Control.Monad-import Data.Map hiding (map)+import Data.Map as Map hiding (map)+import Data.Set as Set (Set, insert, map, minView) import Control.Monad.State.Strict-import Control.Monad.Error+import Control.Monad.Except -data Term f v a = App f (Term f v a) (Term f v a) | Atom a | Var v deriving (Eq, Show)-data Explicit f a = AppE f (Explicit f a) (Explicit f a) | AtomE a deriving (Eq, Show)+data Term f v a = App f (Term f v a) (Term f v a) | Atom a | Var v deriving (Eq, Ord, Show)+data Explicit f a = AppE f (Explicit f a) (Explicit f a) | AtomE a deriving (Eq, Ord, Show) type Solution f v a = Map v (Explicit f a) -data Constraint f v a = Term f v a :==: Term f v a-type Constraints f v a = [Constraint f v a]+data Constraint f v a = Term f v a :==: Term f v a deriving (Eq, Ord, Show)+type Constraints f v a = Set (Constraint f v a) -newtype UnifT f v a m x = UnifT (StateT (Constraints f v a) (ErrorT String m) x)+newtype UnifT f v a m x = UnifT (StateT (Constraints f v a) (ExceptT String m) x)+deriving instance Functor m => Functor (UnifT f v a m)+deriving instance (Monad m, Functor m) => Applicative (UnifT f v a m) deriving instance (Monad m) => Monad (UnifT f v a m) deriving instance (Monad m) => MonadState (Constraints f v a) (UnifT f v a m)  class Monad m => MonadUnify u m | m -> u where-	unify :: u -> u -> m ()+        unify :: u -> u -> m () -instance Monad m => MonadUnify (Term f v a) (UnifT f v a m) where-	a `unify` b = modify ((a :==: b):)+instance (Monad m, Ord a, Ord v, Ord f) => MonadUnify (Term f v a) (UnifT f v a m) where+        a `unify` b = modify (Set.insert (a :==: b))  instance MonadUnify u m => MonadUnify u (StateT s m) where-	a `unify` b = lift (a `unify` b)+        a `unify` b = lift (a `unify` b)  instance MonadTrans (UnifT f v a) where-	lift = UnifT . lift . lift+        lift = UnifT . lift . lift -runUnification :: (Ord v, Eq f, Eq a, Monad m) => UnifT f v a m x -> m (Either String (Constraints f v a))-runUnification (UnifT m) = runErrorT (execStateT m [])+runUnification :: (Ord a, Ord v, Ord f, Eq f, Eq a, Monad m) => UnifT f v a m x -> m (Either String (Constraints f v a))+runUnification (UnifT m) = runExceptT (execStateT m mempty) -solveUnification :: (Ord v, Eq f, Eq a, Monad m) => Explicit f a -> UnifT f v a m x -> m (Either String (x, Solution f v a))-solveUnification def (UnifT m) = runErrorT (evalStateT m' [])-	where	m' = do	x <- m-			ans <- solve def =<< get-			return (x, ans)+solveUnification :: (Ord a, Ord v, Ord f, Eq f, Eq a, Monad m) => Explicit f a -> UnifT f v a m x -> m (Either String (x, Solution f v a))+solveUnification def (UnifT m) = runExceptT (evalStateT m' mempty)+        where   m' = do x <- m+                        ans <- solve def =<< get+                        return (x, ans) -solve :: (Ord v, Eq f, Eq a, Monad m) => Explicit f a -> Constraints f v a -> m (Solution f v a)-solve def (constr:constrs) = case constr of-	Var x :==: Var y-		| x == y	-> solve def constrs-	Var x :==: t-		-> subSol def x t `liftM` solve def (substitute x t constrs)-	t :==: Var y-		-> subSol def y t `liftM` solve def (substitute y t constrs)-	Atom a :==: Atom b-		| a == b	-> solve def constrs-		| otherwise	-> fail "Mismatched atoms"-	App f1 x1 y1 :==: App f2 x2 y2-		| f1 == f2	-> solve def ([x1 :==: x2, y1 :==: y2] ++ constrs)-		| otherwise	-> fail "Mismatched functions"-	_	-> fail "Function matched to atom"-solve _ [] = return empty+solve :: (Ord a, Ord v, Ord f, Eq f, Eq a, Monad m) => Explicit f a -> Constraints f v a -> m (Solution f v a)+solve def constrs0 = case Set.minView constrs0 of+        Just (Var x :==: Var y, constrs)+                | x == y        -> solve def constrs+        Just (Var x :==: t, constrs)+                -> subSol def x t `liftM` solve def (substitute x t constrs)+        Just (t :==: Var y, constrs)+                -> subSol def y t `liftM` solve def (substitute y t constrs)+        Just (Atom a :==: Atom b, constrs)+                | a == b        -> solve def constrs+                | otherwise     -> fail "Mismatched atoms"+        Just (App f1 x1 y1 :==: App f2 x2 y2, constrs)+                | f1 == f2      -> solve def (Set.insert (x1 :==: x2) (Set.insert (y1 :==: y2) constrs))+                | otherwise     -> fail "Mismatched functions"+        Just (_, _)             -> fail "Function matched to atom"+        Nothing -> return empty -substitute :: (Ord v, Eq f, Eq a) => v -> Term f v a -> Constraints f v a -> Constraints f v a-substitute v t = map (\ (x :==: y) -> sub x :==: sub y) where-	sub (Var v')-		| v == v'	= t-	sub (App f x y) = App f (sub x) (sub y)-	sub t' = t'+substitute :: (Ord a, Ord v, Ord f, Eq f, Eq a) => v -> Term f v a -> Constraints f v a -> Constraints f v a+substitute v t = Set.map (\ (x :==: y) -> sub x :==: sub y) where+        sub (Var v')+                | v == v'       = t+        sub (App f x y) = App f (sub x) (sub y)+        sub t' = t'  subTerm :: Ord v => Explicit f a -> Solution f v a -> Term f v a -> Explicit f a subTerm def sol (Var v) = findWithDefault def v sol@@ -69,4 +75,4 @@ subTerm _ _ (Atom a) = AtomE a  subSol :: (Ord v, Eq f, Eq a) => Explicit f a -> v -> Term f v a -> Solution f v a -> Solution f v a-subSol def v t sol = insert v (subTerm def sol t) sol+subSol def v t sol = Map.insert v (subTerm def sol t) sol

@@ -1,17 +1,33 @@ Name:		th-kinds-Version:	0.1.1+Version:	0.2 Category:	Template Haskell Author:		Louis Wasserman+Maintainer:     David Fox <dsf@seereason.com>+Homepage:       https://github.com/ddssff/th-kinds+Bug-Reports:    https://github.com/ddssff/th-kinds/issues License:	BSD3 License-file:	LICENSE Stability:	experimental Synopsis:	Automated kind inference in Template Haskell.-Description:	Given the name of a Haskell type, typeclass, type family, or any of the above, determines its kind.+Description:	Given the name of a Haskell type, typeclass, type family, or any of the above, determine its kind. Maintainer:	Louis Wasserman <wasserman.louis@gmail.com>-Build-type:	Simple-build-depends:   template-haskell == 2.4.0.1 , base >= 4 && < 5, containers >= 0.3, mtl+Build-Type:	Simple+Cabal-Version:  >= 1.22 -exposed-modules:-      Language.Haskell.TH.KindInference-other-modules:-      Language.Haskell.TH.Unification+Library+  Default-Language: Haskell2010+  Hs-Source-Dirs: .+  Build-Depends:+    template-haskell,+    th-orphans,+    base >= 4 && < 5,+    containers >= 0.3,+    mtl+  Exposed-Modules:+    Language.Haskell.TH.KindInference+  Other-Modules:+    Language.Haskell.TH.Unification++source-repository head+  type:     git+  location: https://github.com/ddssff/th-kinds