th-kinds (empty) → 0.0.0

raw patch · 5 files changed

+301/−0 lines, 5 filesdep +basedep +containersdep +mtlsetup-changed

Dependencies added: base, containers, mtl, template-haskell

Files

• LICENSE +2/−0
• Language/Haskell/TH/KindInference.hs +208/−0
• Language/Haskell/TH/Unification.hs +70/−0
• Setup.lhs +4/−0
• th-kinds.cabal +17/−0

@@ -0,0 +1,2 @@+Copyright Louis Wasserman 2010+BSD license

@@ -0,0 +1,208 @@++-- | A module to infer the kind of a given type within Template Haskell.+-- Warning: this implements its own kind inference system, and is therefore+-- not guaranteed to work on all esoteric types.  (That said, I have no examples+-- where it doesn't work.)+module Language.Haskell.TH.KindInference (inferKind) where++-- import Control.Monad+import Control.Monad.Trans+import Data.Ord+import Debug.Trace+import Data.Map((!))+import Data.Set+import Control.Monad.State+import Text.ParserCombinators.ReadP hiding (get)++import Language.Haskell.TH hiding (AppE)+import Language.Haskell.TH.Unification+import Language.Haskell.TH.PprLib hiding (empty, char)+import qualified Language.Haskell.TH.PprLib as Ppr++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)++-- | 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 is still present, and fixes it.+inferKind :: Name -> Q (Either String Kind)+inferKind name = do+	ans <- solveUnification (evalStateT (infer (ConT name)) empty)+	either (return . Left) (\ (x, sol) -> return (Right $ termToK (subTerm sol x))) ans++termToK :: Explicit KindFunc KindAtom -> Kind+termToK (AppE ~KindArrow t1 t2) = termToK t1 `ArrowK` termToK t2+termToK (AtomE ~Star) = StarK++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)+	lift $ unify fK (xK `kindArrow` var)+	return var+infer (SigT t k) = do+	tK <- infer t+	lift $ unify tK (kToTerm k)+	return tK+infer (ForallT bdrs cxt t) = do+	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)++matchUnboxedTuple :: ReadP Int+matchUnboxedTuple = do+	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 = case [n | (n, "") <- readP_to_S matchUnboxedTuple (nameBase name)] of+	(n:_)	-> do	lift $ unify (tyVar name) (tupleKind n star)+			mUnify name0 (tyVar name)+	_	-> do+	  inf <- lift $ lift $ reify name+	  case inf of+		  ClassI dec	-> examineDec name0 dec+		  TyConI dec	-> examineDec name0 dec+		  PrimTyConI name n _ -> do+			  lift $ unify (tyVar name) (tupleKind n star)+			  mUnify name0 (tyVar name)+		  TyVarI name typ	-> do+		  			  kind <- infer typ+					  lift $ unify (tyVar name) kind+					  mUnify name0 (tyVar name)+		  _		-> return ()+	+mUnify :: Maybe Name -> KindUTerm -> LoopKillerT (KindUT Q) ()+mUnify name0 k = case name0 of +	Just name0	-> lift $ unify (tyCon name0) k+	_		-> return ()++examineDec :: Maybe Name -> Dec -> LoopKillerT (KindUT Q) ()+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+	  lift $ unify (tyCon name) (foldr kindArrow 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+	  lift $ unify (tyCon name) (foldr kindArrow star args)+	  mUnify name0 (tyCon name)+	  handleCon con+examineDec name0 (ClassD cxt name bdrs _ _) = do+	visited <- get+	unless (name `member` visited) $ do+	  modify (insert name)+	  mapM_ handleCxt cxt+	  args <- mapM handleBdr bdrs+	  lift $ unify (tyCon name) (foldr kindArrow star args)+	  mUnify name0 (tyCon name)+examineDec name0 (FamilyD _ name bdrs mK) = do+	visited <- get+	unless (name `member` visited) $ do+	  modify (insert name)+	  args <- mapM handleBdr bdrs+	  lift $ unify (tyCon name) (maybe star kToTerm mK)+	  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+	  lift $ unify (tyCon name) (foldr kindArrow kind args)+	  mUnify name0 (tyCon name)+examineDec _ _ = return ()++handleCon :: Con -> LoopKillerT (KindUT Q) ()+handleCon (NormalC _ ts) = mapM_ (\ (_, t) -> do+	k <- infer t+	lift $ unify k star) ts+handleCon (RecC _ ts) = mapM_ (\ (_, _, t) -> do+	k <- infer t+	lift $ unify k star) ts+handleCon (InfixC (_, t1) _ (_, t2)) = do+	k1 <- infer t1+	k2 <- infer t2+	lift $ unify k1 star+	lift $ unify k2 star+handleCon (ForallC bdrs cxt con) = do+	mapM_ handleBdr bdrs+	mapM_ handleCxt cxt+	handleCon con++tyCon :: Name -> KindUTerm+tyCon = Var . ConT++tyVar :: Name -> KindUTerm+tyVar = Var . VarT++handleBdr :: TyVarBndr -> LoopKillerT (KindUT Q) KindUTerm+handleBdr (PlainTV n) = return (tyVar n)+handleBdr (KindedTV n k) = do+	lift $ unify (tyVar n) (kToTerm k)+	return (tyVar n)++handleCxt :: Pred -> LoopKillerT (KindUT Q) ()+handleCxt (ClassP name args) = do+	kinds <- mapM infer args+	lift $ unify (Var (ConT name)) (foldr kindArrow star kinds)+	examine (Just name) name+handleCxt (EqualP t1 t2) = do+	k1 <- infer t1+	k2 <- infer t2+	lift $ unify k1 k2++kToTerm :: Kind -> KindUTerm+kToTerm = kToTerm' . fixKind where+	kToTerm' (ArrowK a b) = kToTerm' a `kindArrow` kToTerm' b+	kToTerm' StarK = star++fixKind :: Kind -> Kind+fixKind k = loop k StarK where+	loop StarK k = k+	loop (ArrowK k1 k2) k = loop k1 (loop k2 StarK `ArrowK` k)++kindArrow :: KindUTerm -> KindUTerm -> KindUTerm+kindArrow = App KindArrow++star :: KindUTerm+star = Atom Star++tupleKind :: Int -> KindUTerm -> KindUTerm+tupleKind n k = foldr kindArrow 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)+instance Ppr Char where+	ppr = Ppr.char

@@ -0,0 +1,70 @@+{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}++module Language.Haskell.TH.Unification (subTerm, Term(..), UnifT, Explicit(..), unify, solveUnification) where++import Control.Monad+import Data.Map hiding (map)+import Control.Monad.State.Strict+import Control.Monad.Error++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)+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]++newtype UnifT f v a m x = UnifT (StateT (Constraints f v a) (ErrorT String m) x)+deriving instance (Monad m) => Monad (UnifT f v a m)+deriving instance (Monad m) => MonadState (Constraints f v a) (UnifT f v a m)++instance MonadTrans (UnifT f v a) where+	lift = UnifT . lift . lift++unify :: (Monad m) => Term f v a -> Term f v a -> UnifT f v a m ()+a `unify` b = modify ((a :==: b):)++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 [])++solveUnification :: (Ord v, Eq f, Eq a, Monad m) => UnifT f v a m x -> m (Either String (x, Solution f v a))+solveUnification (UnifT m) = runErrorT (evalStateT m' [])+	where	m' = do	x <- m+			ans <- solve =<< get+			return (x, ans)++solve :: (Ord v, Eq f, Eq a, Monad m) => Constraints f v a -> m (Solution f v a)+solve (constr:constrs) = case constr of+	Var x :==: Var y+		| x == y	-> solve constrs+	Var x :==: t+		-> subSol x t `liftM` solve (substitute x t constrs)+	t :==: Var y+		-> subSol y t `liftM` solve (substitute y t constrs)+	Atom a :==: Atom b+		| a == b	-> solve constrs+		| otherwise	-> fail "Mismatched atoms"+	App f1 x1 y1 :==: App f2 x2 y2+		| f1 /= f2	-> fail "Mismatched functions"+		| otherwise	-> solve ([x1 :==: x2, y1 :==: y2] ++ constrs)+	_	-> fail "Function matched to atom"+solve [] = 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'++subTerm :: Ord v => Solution f v a -> Term f v a -> Explicit f a+subTerm sol (Var v) = sol ! v+subTerm sol (App f x y) = AppE f (subTerm sol x) (subTerm sol y)+subTerm _ (Atom a) = AtomE a++subSol :: (Ord v, Eq f, Eq a) => v -> Term f v a -> Solution f v a -> Solution f v a+subSol v t sol = insert v (subTerm sol t) sol+	+-- test :: UnifT Char String String IO ()+-- test = do	App 'f' (App 'g' (Var "A") (Var "A")) (Var "A") `unify`+-- 			App 'f' (Var "B") (Atom "xyz")

@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain

@@ -0,0 +1,17 @@+Name:		th-kinds+Version:	0.0.0+Category:	Template Haskell+Author:		Louis Wasserman+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.+Maintainer:	Louis Wasserman <wasserman.louis@gmail.com>+Build-type:	Simple+build-depends:   template-haskell >= 2.4.0.0 , base >= 4 && < 5, containers >= 0.3, mtl++exposed-modules:+      Language.Haskell.TH.KindInference+other-modules:+      Language.Haskell.TH.Unification