packages feed

hindley-milner-type-check (empty) → 0.1.0.0

raw patch · 15 files changed

+2278/−0 lines, 15 filesdep +basedep +containersdep +data-fixsetup-changed

Dependencies added: base, containers, data-fix, deepseq, deriving-compat, dlist, hindley-milner-type-check, mtl, prettyprinter, tasty, tasty-hunit, text

Files

+ LICENSE view
@@ -0,0 +1,29 @@+Copyright MIT license +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 Anton Kholomiov 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
+ hindley-milner-type-check.cabal view
@@ -0,0 +1,93 @@+name:                   hindley-milner-type-check+version:                0.1.0.0+synopsis:               Type inference for Hindley-Milner based languages+description:+    This package contains an implemention of Hindley-Milner inference algorithm.+    It supports reporting of source code locations for errors.+    Language for type inference is labda-calculus augmented with primitive+    functions, let-expressions,  case-expressions and bottom.++    See github repo for tutorial and test-cases for examples.+++license:                MIT+license-file:           LICENSE+author:                 Anton Kholomiov, Aleksey Khudyakov+maintainer:             anton.kholomiov@gmail.com+category:               Language+build-type:             Simple+cabal-version:          >=1.22++source-repository head+  type:                 git+  location:             https://github.com/anton-k/hindley-milner-type-check++library+  ghc-options:  -Wall+  exposed-modules:+    Type.Check.HM,+    Type.Check.HM.Infer,+    Type.Check.HM.Lang+    Type.Check.HM.Pretty,+    Type.Check.HM.Subst,+    Type.Check.HM.Term,+    Type.Check.HM.Type,+    Type.Check.HM.TypeError,+    Type.Check.HM.TyTerm++  other-modules:++  -- Other library packages from which modules are imported.+  build-depends: base                      >=4.8 && <5+               , deepseq                   >=1.4+               , containers                >=0.5+               , deriving-compat+               , data-fix                  >=0.3+               , dlist+               , mtl+               , prettyprinter+               , text++  -- Directories containing source files.+  hs-source-dirs:       src++  -- Base language which the package is written in.+  default-language:     Haskell2010++  default-extensions:+    DeriveDataTypeable+    DeriveFunctor,+    DeriveFoldable,+    DeriveTraversable,+    DeriveGeneric,+    FlexibleContexts,+    FlexibleInstances,+    GeneralizedNewtypeDeriving,+    LambdaCase,+    MultiParamTypeClasses,+    OverloadedStrings,+    RankNTypes+    RecordWildCards,+    ScopedTypeVariables,+    StandaloneDeriving,+    TemplateHaskell,+    TupleSections,+    TypeFamilies,+    TypeSynonymInstances++test-suite hindley-milner-tests+  Type:                exitcode-stdio-1.0+  Ghc-options:         -Wall -threaded -rtsopts+  Default-Language:    Haskell2010+  Build-Depends:       base              >=4.9 && <5+                     , hindley-milner-type-check+                     , containers+                     , text+                     , data-fix                  >=0.3+                     , tasty+                     , tasty-hunit+                     , prettyprinter+  hs-source-dirs:      test+  Main-is:             Main.hs+  Other-modules:       TM.SKI+                     , TM.NumLang
+ src/Type/Check/HM.hs view
@@ -0,0 +1,28 @@+-- | This module exports all useful functions of the library+module Type.Check.HM (+  -- * Language definition+  module Type.Check.HM.Lang,++  -- * Types+  module Type.Check.HM.Type,++  -- * Terms+  module Type.Check.HM.Term,++  -- * Typed terms+  module Type.Check.HM.TyTerm,++  -- * Inference+  module Type.Check.HM.Infer,++  -- * Errors+  module Type.Check.HM.TypeError,+) where++import Type.Check.HM.Infer+import Type.Check.HM.Lang+import Type.Check.HM.Pretty      as X()+import Type.Check.HM.Term+import Type.Check.HM.Type+import Type.Check.HM.TypeError+import Type.Check.HM.TyTerm
+ src/Type/Check/HM/Infer.hs view
@@ -0,0 +1,620 @@+-- | Defines type-inference algorithm.+--+-- For type inference we have to define instance of the Lang class:+--+-- > data NoPrim+-- >   deriving (Show)+-- >+-- > data TestLang+-- >+-- > instance Lang TestLang where+-- >   type Src  TestLang = ()              -- ^ define type for source code locations+-- >   type Var  TestLang = Text            -- ^ define type for variables+-- >   type Prim TestLang = NoPrim          -- ^ define type for primitive operators+-- >   getPrimType _ = error "No primops"   -- ^ reports types for primitives+--+-- Also we define context for type inference that holds types for all known variables+-- Often it defines types for all global variables or functions that are external.+--+-- > context = Context $ Map.fromList [...]+--+-- Then we can use inference to derive type for given term with @inferType@ or+-- we can derive types for all sub-expressions of given term with @inferTerm@.+-- See module in the test "TM.Infer" for examples of the usage.+--+-- > termI,termK :: Term NoPrim () Text+-- >+-- > -- I combinator+-- > termI = lamE () "x" $ varE () "x"+-- > -- K combinator+-- > termK = lamE () "x" $ lamE () "y" $ varE () "x"+-- >+-- > -- Let's infer types+-- > typeI = inferType mempty termI+-- > typeK = inferType mempty termK+--+-- There are functions to check that two types unify (@unifyTypes@) or that one type+-- is subtype of another one (@subtypeOf@).+module Type.Check.HM.Infer(+  -- * Context+    Context(..)+  , insertCtx+  , lookupCtx+  , ContextOf+  -- * Inference+  , inferType+  , inferTerm+  , subtypeOf+  , unifyTypes+  -- * Utils+  , closeSignature+) where++import Control.Monad.Identity++import Control.Applicative+import Control.Arrow (second)+import Control.Monad.Except+import Control.Monad.State.Strict++import Data.Bifunctor (bimap)+import Data.Fix+import Data.Function (on)+import Data.Map.Strict (Map)+import Data.Maybe++import Type.Check.HM.Lang+import Type.Check.HM.Term+import Type.Check.HM.Subst+import Type.Check.HM.Type+import Type.Check.HM.TypeError+import Type.Check.HM.TyTerm++import qualified Data.Map.Strict as M+import qualified Data.Set as S+import qualified Data.List as L++-- | Context holds map of proven signatures for free variables in the expression.+newtype Context loc v = Context { unContext :: Map v (Signature loc v) }+  deriving (Show, Eq, Semigroup, Monoid)++-- | Type synonym for context.+type ContextOf q = Context (Src q) (Var q)++instance CanApply Context where+  apply subst = Context . fmap (apply subst) . unContext++-- | Insert signature into context+insertCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v+insertCtx v sign (Context ctx) = Context $ M.insert v sign ctx++-- | Lookup signature by name in the context of inferred terms.+lookupCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)+lookupCtx v (Context ctx) = M.lookup v ctx++-- | Wrapper with ability to generate fresh names+data Name v+  = Name v+  | FreshName !Int+  deriving (Show, Eq, Ord)++fromNameVar :: Name v -> Either (TypeError loc v) v+fromNameVar = \case+  Name v      -> Right v+  FreshName _ -> Left FreshNameFound++instance IsVar a => IsVar (Name a) where+  prettyLetters = fmap Name (prettyLetters :: [a])++-- Synonyms to simplify typing+type Context' loc v = Context (Origin loc) (Name v)+type Type' loc v = Type (Origin loc) (Name v)+type Signature' loc v = Signature (Origin loc) (Name v)+type Subst' loc v = Subst (Origin loc) (Name v)+type Bind' loc v a = Bind (Origin loc) (Name v) a+type VarSet' loc v = VarSet (Origin loc) (Name v)++type ContextOf' q = Context (Origin (Src q)) (Name (Var q))+type TypeOf' q = Type (Origin (Src q)) (Name (Var q))+type TermOf' q = Term (Prim q) (Origin (Src q)) (Name (Var q))+type TyTermOf' q = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))+type SignatureOf' q = Signature (Origin (Src q)) (Name (Var q))+type SubstOf' q = Subst (Origin (Src q)) (Name (Var q))+type BindOf' q a = Bind (Origin (Src q)) (Name (Var q)) a+type CaseAltOf' q = CaseAlt (Origin (Src q)) (Name (Var q))++-- | We leave in the context only terms that are truly needed.+-- To check the term we need only variables that are free in the term.+-- So we can safely remove everything else and speed up lookup times.+restrictContext :: Ord v => Term prim loc v -> Context loc v -> Context loc v+restrictContext t (Context ctx) = Context $ M.intersection ctx fv+  where+    fv = M.fromList $ fmap (, ()) $ S.toList $ freeVars t++wrapContextNames :: Ord v => Context loc v -> Context loc (Name v)+wrapContextNames = fmapCtx Name+  where+    fmapCtx f (Context m) = Context $ M.mapKeys f $ M.map (fmap f) m++wrapTermNames :: Term prim loc v -> Term prim loc (Name v)+wrapTermNames = fmap Name++markProven :: Context loc v -> Context (Origin loc) v+markProven = Context . M.map (mapLoc Proven) . unContext++markUserCode :: Term prim loc v -> Term prim (Origin loc) v+markUserCode = mapLoc UserCode++chooseUserOrigin :: Show a => Origin a -> Origin a -> a+chooseUserOrigin x y = case (x, y) of+  (UserCode a, _) -> a+  (_, UserCode a) -> a+  _               -> fromOrigin x++-- | Type-tag for source locations to distinguish proven types from those+-- that have to be checked.+--+-- We use it on unification failure to show source locations in the user code and not in the+-- expression that is already was proven.+data Origin a+  = Proven a+  -- ^ Proven source code location+  | UserCode a+  -- ^ User source code (we type-check it)+  deriving (Show, Functor)++fromOrigin :: Origin a -> a+fromOrigin = \case+  Proven   a -> a+  UserCode a -> a++instance Eq a => Eq (Origin a) where+  (==) = (==) `on` fromOrigin++instance Ord a => Ord (Origin a) where+  compare = compare `on` fromOrigin++instance HasLoc a => HasLoc (Origin a) where+  type Loc (Origin a) = Loc a+  getLoc = getLoc . fromOrigin++-- | Type-inference monad.+-- Contains integer counter for fresh variables and possibility to report type-errors.+newtype InferM loc var a = InferM (StateT Int (Except (TypeError loc (Name var))) a)+  deriving (Functor, Applicative, Monad, MonadState Int, MonadError (TypeError loc (Name var)))++-- | Runs inference monad.+runInferM :: InferM loc var a -> Either (TypeError loc (Name var)) a+runInferM (InferM m) = runExcept $ evalStateT m 0++type InferOf q = InferM (Src q) (Var q) (Out (Prim q) (Src q) (Var q))++-- | Type-inference function.+-- We provide a context of already proven type-signatures and term to infer the type.+inferType :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TypeOf q)+inferType ctx term = fmap termType $ inferTerm ctx term++-- | Infers types for all subexpressions of the given term.+-- We provide a context of already proven type-signatures and term to infer the type.+inferTerm :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TyTermOf q)+inferTerm ctx term = join $+  bimap (fromTypeErrorNameVar . normaliseType) ((\(_, tyTerm) -> toTyTerm tyTerm)) $+    runInferM $ infer (wrapContextNames $ markProven $ restrictContext term ctx) (wrapTermNames $ markUserCode term)+  where+    toTyTerm = fromTyTermNameVar . normaliseType . mapLoc fromOrigin++type Out prim loc var = ( Subst (Origin loc) (Name var)+                        , TyTerm prim (Origin loc) (Name var)+                        )++infer :: Lang q => ContextOf' q -> TermOf' q -> InferOf q+infer ctx (Term (Fix x)) = case x of+  Var loc v           -> inferVar ctx loc v+  Prim loc p          -> inferPrim loc p+  App loc a b         -> inferApp ctx loc (Term a) (Term b)+  Lam loc v r         -> inferLam ctx loc v (Term r)+  Let loc v a         -> inferLet ctx loc (fmap Term v) (Term a)+  LetRec loc vs a     -> inferLetRec ctx loc (fmap (fmap Term) vs) (Term a)+  AssertType loc a ty -> inferAssertType ctx loc (Term a) ty+  Constr loc ty tag   -> inferConstr loc ty tag+  Case loc e alts     -> inferCase ctx loc (Term e) (fmap (fmap Term) alts)+  Bottom loc          -> inferBottom loc++inferVar :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q+inferVar ctx loc v = {- trace (unlines ["VAR", ppShow ctx, ppShow v]) $ -}+  case M.lookup v (unContext ctx) of+    Nothing  -> throwError $ NotInScopeErr (fromOrigin loc) v+    Just sig -> do ty <- newInstance $ setLoc loc sig+                   return (mempty, tyVarE ty loc v)++inferPrim :: Lang q => Origin (Src q) -> Prim q -> InferOf q+inferPrim loc prim =+  return (mempty, tyPrimE ty loc prim)+  where+    ty = fmap Name $ mapLoc UserCode $ getPrimType prim++inferApp :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q+inferApp ctx loc f a = {- fmap (\res -> trace (unlines ["APP", ppCtx ctx, ppShow' f, ppShow' a, ppShow' $ snd res]) res) $-} do+  tvn <- fmap (varT loc) $ freshVar+  res <- inferTerms ctx [f, a]+  case res of+    (phi, [(tf, f'), (ta, a')]) -> fmap (\subst ->+                                            let ty   = apply subst tvn+                                                term = tyAppE ty loc (apply subst f') (apply subst a')+                                            in  (subst, term)) $ unify phi tf (arrowT loc ta tvn)+    _               -> error "Impossible has happened!"++inferLam :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q+inferLam ctx loc x body = do+  tvn <- freshVar+  (phi, bodyTyTerm) <- infer (ctx1 tvn) body+  let ty = arrowT loc (apply phi (varT loc tvn)) (termType bodyTyTerm)+  return (phi, tyLamE ty loc x bodyTyTerm)+  where+    ctx1 tvn = insertCtx x (newVar loc tvn) ctx++inferLet :: Lang q => ContextOf' q -> Origin (Src q) -> BindOf' q (TermOf' q) -> TermOf' q -> InferOf q+inferLet ctx loc v body = do+  (phi, rhsTyTerm) <- infer ctx $ bind'rhs v+  let tBind = termType rhsTyTerm+  ctx1 <- addDecls [fmap (const tBind) v] (apply phi ctx)+  (subst, bodyTerm) <- infer ctx1 body+  let subst1 = phi <> subst+      tyBind = v { bind'rhs = apply subst1 rhsTyTerm }+  return ( subst1+         , apply subst1 $ tyLetE (termType bodyTerm) loc tyBind bodyTerm+         )++inferLetRec :: forall q . Lang q+  => ContextOf' q -> Origin (Src q) -> [BindOf' q (TermOf' q)] -> TermOf' q+  -> InferOf q+inferLetRec ctx topLoc vs body = do+  lhsCtx <- getTypesLhs vs+  (phi, rhsTyTerms) <- inferTerms (ctx <> Context (M.fromList lhsCtx)) exprBinds+  let (tBinds, bindsTyTerms) = unzip rhsTyTerms+  (ctx1, lhsCtx1, subst) <- unifyRhs ctx lhsCtx phi tBinds+  inferBody bindsTyTerms ctx1 lhsCtx1 subst body+  where+    exprBinds = fmap bind'rhs vs+    locBinds  = fmap bind'loc vs++    getTypesLhs :: [BindOf' q (TermOf' q)] -> InferM (Src q) (Var q) [(Name (Var q), SignatureOf' q)]+    getTypesLhs lhs = mapM (\b -> fmap ((bind'lhs b, ) . newVar (bind'loc b)) freshVar) lhs++    unifyRhs context lhsCtx phi tBinds =+      fmap (\subst -> (context1, lhsCtx1, subst)) $ unifyl phi ts tBinds+      where+        context1 = apply phi context+        lhsCtx1  = fmap (second $ apply phi) lhsCtx+        ts = fmap (oldBvar . snd) lhsCtx1++    oldBvar = foldFix go . unSignature+      where+        go  = \case+          MonoT t       -> t+          ForAllT _ _ t -> t++    inferBody termBinds context lhsCtx subst expr = do+      ctx1 <- addDecls (zipWith (\loc (v, ty) -> Bind loc v ty) locBinds $ fmap (second $ oldBvar . apply subst) lhsCtx) $ apply subst context+      (phi, bodyTerm) <- infer ctx1 expr+      let tyBinds = zipWith (\bind rhs -> bind { bind'rhs = rhs }) vs termBinds+      return (subst <> phi, tyLetRecE (termType bodyTerm) topLoc tyBinds bodyTerm)++inferAssertType :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q+inferAssertType ctx loc a ty = do+  (phi, aTyTerm) <- infer ctx a+  subst <- genSubtypeOf phi ty (termType aTyTerm)+  let subst' = phi <> subst+  return (subst', apply subst' $ tyAssertTypeE loc aTyTerm ty)++inferConstr :: Lang q => Origin (Src q) -> TypeOf' q -> Name (Var q) -> InferOf q+inferConstr loc ty tag = do+  vT <- newInstance $ typeToSignature ty+  return (mempty, tyConstrE loc vT tag)++inferCase :: forall q . Lang q+  => ContextOf' q -> Origin (Src q) -> TermOf' q -> [CaseAltOf' q (TermOf' q)]+  -> InferOf q+inferCase ctx loc e caseAlts = do+  (phi, tyTermE) <- infer ctx e+  (psi, tRes, tyAlts) <- inferAlts phi (termType tyTermE) $ caseAlts+  return ( psi+         , apply psi $ tyCaseE tRes loc (apply psi tyTermE) $ fmap (applyAlt psi) tyAlts)+  where+    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)])+    inferAlts substE tE alts =+      fmap (\(subst, _, tRes, as) -> (subst, tRes, L.reverse as)) $ foldM go (substE, tE, tE, []) alts+      where+        go (subst, tyTop, _, res) alt = do+          (phi, tRes, alt1) <- inferAlt (applyAlt subst alt)+          let subst1 = subst <> phi+          subst2 <- unify subst1 (apply subst1 tyTop) (apply subst1 $ caseAlt'constrType alt1)+          return (subst2, apply subst2 tyTop, apply subst2 tRes, applyAlt subst2 alt1 : res)+++    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q))+    inferAlt preAlt = do+      alt <- newCaseAltInstance preAlt+      let argVars = fmap  (\ty -> (snd $ typed'value ty, (fst $ typed'value ty, typed'type ty))) $ caseAlt'args alt+          ctx1 = Context (M.fromList $ fmap (second $ monoT . snd) argVars) <> ctx+      (subst, tyTermRhs) <- infer ctx1 $ caseAlt'rhs alt+      let args = fmap (\(v, (argLoc, tv)) -> Typed (apply subst tv) (argLoc, v)) argVars+          alt' = alt+                  { caseAlt'rhs = tyTermRhs+                  , caseAlt'args = args+                  , caseAlt'constrType = apply subst $ caseAlt'constrType alt+                  }+      return (subst, termType tyTermRhs, alt')++    newCaseAltInstance :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))+    newCaseAltInstance alt = do+      tv <- newInstance $ typeToSignature $ getCaseType alt+      let (argsT, resT)= splitFunT tv+      return $ alt+        { caseAlt'constrType = resT+        , caseAlt'args = zipWith (\aT ty -> ty { typed'type = aT }) argsT $ caseAlt'args alt+        }++    getCaseType :: CaseAltOf' q (TermOf' q) -> TypeOf' q+    getCaseType CaseAlt{..} = funT (fmap typed'type caseAlt'args) caseAlt'constrType++    splitFunT :: TypeOf' q -> ([TypeOf' q], TypeOf' q)+    splitFunT arrT = go [] arrT+      where+        go argsT (Type (Fix t)) = case t of+          ArrowT _loc a b -> go (Type a : argsT) (Type b)+          other           -> (reverse argsT, Type $ Fix other)+++    funT :: [TypeOf' q] -> TypeOf' q -> TypeOf' q+    funT argsT resT = foldr (\a b -> arrowT (getLoc a) a b) resT argsT++    applyAlt subst alt@CaseAlt{..} = alt+      { caseAlt'constrType = apply subst caseAlt'constrType+      , caseAlt'args       = fmap applyTyped caseAlt'args+      , caseAlt'rhs        = apply subst caseAlt'rhs+      }+      where+        applyTyped ty@Typed{..} = ty { typed'type = apply subst $ typed'type }++inferBottom :: Lang q => Origin (Src q) -> InferOf q+inferBottom loc = do+  ty <- fmap (varT loc) freshVar+  return (mempty, tyBottomE ty loc)++newInstance :: IsVar v => Signature loc (Name v) -> InferM loc' v (Type loc (Name v))+newInstance = fmap (uncurry apply) . foldFixM go . unSignature+  where+    go = \case+      MonoT ty -> return (mempty, ty)+      ForAllT loc v (Subst m, ty) -> fmap (\nv -> (Subst $ M.insert v (varT loc nv) m, ty)) freshVar++newVar :: loc -> v -> Signature loc v+newVar loc tvn = monoT $ varT loc tvn++freshVar :: IsVar v => InferM loc v (Name v)+freshVar = do+  n <- get+  put $ n + 1+  return $ FreshName n++inferTerms :: Lang q+  => ContextOf' q+  -> [TermOf' q]+  -> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])+inferTerms ctx ts = case ts of+  []   -> return $ (mempty, [])+  a:as -> do+    (phi, termA) <- infer ctx a+    let ta = termType termA+    (psi, tas) <- inferTerms (apply phi ctx) as+    return ( phi <> psi+           , (apply psi ta, apply psi termA) : tas+           )++-- | Unification function. Checks weather two types unify.+-- First argument is current substitution.+unify :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+  => Subst' loc v+  -> Type' loc v+  -> Type' loc v+  -> m (Subst' loc v)+unify phi (Type (Fix x)) (Type (Fix y)) = {- trace (unlines ["UNIFY", ppShow tx, ppShow ty]) $ -}+  case (x, y) of+    (VarT loc tvn, t) ->+        let phiTvn = applyVar phi loc tvn+            phiT   = apply phi (Type (Fix t))+        in  if phiTvn `eqIgnoreLoc` varT loc tvn+              then extend phi loc tvn phiT+              else unify phi phiTvn phiT+    (a, VarT locB v) -> unify phi (varT locB v) (Type $ Fix a) -- (conT locA name $ fmap Type ts)+    (ConT locA n xs, ConT locB m ys) ->+      if n == m+        then unifyl phi (fmap Type xs) (fmap Type ys)+        else unifyErr locA locB+    (ArrowT _ a1 a2, ArrowT _ b1 b2) -> unifyl phi (fmap Type [a1, a2]) (fmap Type [b1, b2])+    (TupleT locA xs, TupleT locB ys) ->+      if length xs == length ys+        then unifyl phi (fmap Type xs) (fmap Type ys)+        else unifyErr locA locB+    (ListT _ a, ListT _ b) -> unify phi (Type a) (Type b)+    (a, b) -> unifyErr (getLoc $ Type $ Fix a) (getLoc $ Type $ Fix b)+  where+    unifyErr locA locB = throwError $+      UnifyErr (chooseUserOrigin locA locB)+               (mapLoc fromOrigin $ Type (Fix x))+               (mapLoc fromOrigin $ Type (Fix y))++eqIgnoreLoc :: Eq v => Type loc v -> Type loc v -> Bool+eqIgnoreLoc = (==) `on` mapLoc (const ())++applyVar :: IsVar v => Subst' loc v -> Origin loc -> Name v -> Type' loc v+applyVar (Subst subst) loc v = fromMaybe (varT loc v) $ M.lookup v subst++extend+  :: (IsVar v, MonadError (TypeError loc (Name v)) m)+  => Subst' loc v -> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)+extend phi loc tvn ty+  | varT loc tvn `eqIgnoreLoc` ty = return phi+  | memberVarSet tvn (tyVars ty)  = throwError $ OccursErr (fromOrigin loc) (mapLoc fromOrigin ty)+  | otherwise                     = return $ phi <> delta tvn ty++unifyl :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+  => Subst' loc v+  -> [Type' loc v]+  -> [Type' loc v]+  -> m (Subst' loc v)+unifyl subst as bs = foldr go (return subst) $ zip as bs+  where+    go (a, b) eSubst = (\t -> unify t a b) =<< eSubst++-- | Checks if first argument one type is subtype of the second one.+subtypeOf :: (IsVar v, Show loc, Eq loc)+  => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)+subtypeOf a b =+  join $ bimap (fromTypeErrorNameVar . normaliseType) (fromSubstNameVar . fromSubstOrigin) $+    genSubtypeOf mempty (fmap Name $ mapLoc Proven a) (fmap Name $ mapLoc UserCode b)++genSubtypeOf :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+  => Subst' loc v+  -> Type' loc v+  -> Type' loc v+  -> m (Subst' loc v)+genSubtypeOf phi tx@(Type (Fix x)) ty@(Type (Fix y)) = case (x, y) of+  (_, VarT _ _) -> unify phi tx ty+  (ConT locA n xs, ConT locB m ys) ->+    if n == m+      then subtypeOfL phi (fmap Type xs) (fmap Type ys)+      else subtypeErr locA locB+  (ArrowT _ a1 a2, ArrowT _ b1 b2) -> subtypeOfL phi (fmap Type [a1, a2]) (fmap Type [b1, b2])+  (TupleT locA as, TupleT locB bs) ->+    if length as == length bs+      then subtypeOfL phi (fmap Type as) (fmap Type bs)+      else subtypeErr locA locB+  (ListT _ a, ListT _ b) -> genSubtypeOf phi (Type a) (Type b)+  (VarT locA _, _) -> subtypeErr locA (getLoc ty)+  _ -> subtypeErr (getLoc tx) (getLoc ty)+  where+    subtypeErr locA locB = throwError+      $ SubtypeErr (chooseUserOrigin locA locB) (mapLoc fromOrigin tx) (mapLoc fromOrigin ty)++subtypeOfL :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)+  => Subst' loc v+  -> [Type' loc v]+  -> [Type' loc v]+  -> m (Subst' loc v)+subtypeOfL subst as bs = foldr go (return subst) $ zip as bs+  where+    go (a, b) eSubst = (\t -> genSubtypeOf t a b) =<< eSubst++addDecls :: IsVar v+  => [Bind (Origin loc) (Name v) (Type' loc v)]+  -> Context' loc v+  -> InferM loc v (Context' loc v)+addDecls vs ctx =+  foldM  (\c b -> addDecl unknowns b c) ctx vs+  where+    unknowns = foldMap tyVars $ unContext ctx++addDecl :: forall loc v . IsVar v+  => VarSet' loc v+  -> Bind' loc v (Type' loc v)+  -> Context' loc v+  -> InferM loc v (Context' loc v)+addDecl unknowns b ctx = do+  scheme <- toScheme unknowns (bind'rhs b)+  return $ Context . M.insert (bind'lhs b) scheme . unContext $ ctx+  where+    toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)+    toScheme uVars ty = do+      (subst, newVars) <- fmap (\xs -> (toSubst xs, fmap (\((loc, _), v) -> (loc, v)) xs)) $+          mapM (\sv -> fmap ((sv, )) freshVar) $ varSetToList schematicVars+      return $ foldr (uncurry forAllT) (monoT (apply subst ty)) newVars+      where+        schematicVars = tyVars ty `differenceVarSet` uVars++    toSubst = Subst . M.fromList . fmap (\((loc, v), a) -> (v, varT loc a))++-------------------------------------------------------+-- pretty letters for variables in the result type++-- | Converts variable names to human-readable format.+normaliseType :: (HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) => m loc (Name v) -> m loc (Name v)+normaliseType ty = apply (normaliseSubst ty) ty++normaliseSubst :: (HasTypeVars m, Show loc, Eq loc, IsVar v) => m loc v -> Subst loc v+normaliseSubst x =+  Subst $ M.fromList $+    zipWith (\(nameA, loc) nameB -> (nameA, varT loc nameB)) (tyVarsInOrder x) prettyLetters++------------------------------------------------+--++-- | Checks weather two types unify. If they do it returns substitution that unifies them.+unifyTypes :: (Show loc, IsVar v, Eq loc) => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)+unifyTypes a b =+  join $ bimap (fromTypeErrorNameVar . normaliseType) (fromSubstNameVar . fromSubstOrigin) $+    unify mempty (fmap Name $ mapLoc Proven a) (fmap Name $ mapLoc UserCode b)++------------------------------------------------+-- recover name and origin wrappers++fromTypeErrorNameVar :: TypeError loc (Name var) -> TypeError loc var+fromTypeErrorNameVar = either id id . \case+    OccursErr loc ty     -> fmap (OccursErr loc) (fromTypeNameVar ty)+    UnifyErr loc tA tB   -> liftA2 (UnifyErr loc) (fromTypeNameVar tA) (fromTypeNameVar tB)+    SubtypeErr loc tA tB -> liftA2 (SubtypeErr loc) (fromTypeNameVar tA) (fromTypeNameVar tB)+    NotInScopeErr loc v  -> fmap (NotInScopeErr loc) $ fromNameVar v+    EmptyCaseExpr loc    -> pure $ EmptyCaseExpr loc+    FreshNameFound       -> pure FreshNameFound++fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)+fromTypeNameVar (Type x) = fmap Type $ foldFixM go x+  where+    go :: TypeF loc (Name var) (Fix (TypeF loc var)) -> Either (TypeError loc var) (Fix (TypeF loc var))+    go = \case+      VarT loc v     -> fmap (Fix . VarT loc) $ fromNameVar v+      ConT loc v as  -> fmap (\con -> Fix $ ConT loc con as) $ fromNameVar v+      ArrowT loc a b -> pure $ Fix $ ArrowT loc a b+      TupleT loc as  -> pure $ Fix $ TupleT loc as+      ListT loc as   -> pure $ Fix $ ListT loc as++fromTyTermNameVar :: TyTerm prim loc (Name var) -> Either (TypeError loc var) (TyTerm prim loc var)+fromTyTermNameVar (TyTerm x) = fmap TyTerm $ foldFixM go x+  where+    go (Ann annTy term) = liftA2 (\t val -> Fix $ Ann t val) (fromTypeNameVar annTy) $ case term of+      Var loc v           -> fmap (Var loc) $ fromNameVar v+      Prim loc p          -> pure $ Prim loc p+      App loc a b         -> pure $ App loc a b+      Lam loc v a         -> fmap (\arg -> Lam loc arg a) $ fromNameVar v+      Let loc bind a      -> fmap (\b -> Let loc b a) $ fromBind bind+      LetRec loc binds a  -> fmap (\bs -> LetRec loc bs a) $ mapM fromBind binds+      AssertType loc a ty -> fmap (AssertType loc a) $ fromTypeNameVar ty+      Constr loc t v      -> liftA2 (Constr loc) (fromTypeNameVar t) (fromNameVar v)+      Bottom loc          -> pure $ Bottom loc+      Case loc e alts     -> fmap (Case loc e) $ mapM fromAlt alts++    fromBind b = fmap (\a -> b { bind'lhs = a }) $ fromNameVar $ bind'lhs b++    fromAlt alt@CaseAlt{..} =+      liftA3 (\tag args constrType -> alt { caseAlt'tag = tag, caseAlt'args = args, caseAlt'constrType = constrType })+        (fromNameVar caseAlt'tag)+        (mapM fromTyped caseAlt'args)+        (fromTypeNameVar caseAlt'constrType)++    fromTyped Typed{..} = liftA2 Typed (fromTypeNameVar typed'type) (mapM fromNameVar typed'value)++fromSubstNameVar :: Ord v => Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)+fromSubstNameVar (Subst m) = fmap (Subst . M.fromList) $ mapM uncover $ M.toList m+  where+    uncover (v, ty) = liftA2 (,) (fromNameVar v) (fromTypeNameVar ty)++fromSubstOrigin :: Ord v => Subst (Origin loc) v -> Subst loc v+fromSubstOrigin = Subst . M.map (mapLoc fromOrigin) . unSubst++-- | Substitutes all type arguments with given types.+closeSignature :: Ord var => [Type loc var] -> Signature loc var -> Type loc var+closeSignature argTys sig = apply (Subst $ M.fromList $ zip argNames argTys) monoTy+  where+    (argNames, monoTy) = splitSignature sig+
+ src/Type/Check/HM/Lang.hs view
@@ -0,0 +1,68 @@+{-# Language TypeFamilyDependencies #-}+-- | Main class for the library that defines common types and primitives for the language.+module Type.Check.HM.Lang(+  -- * Lang+    Lang(..)+  , TypeOf+  , TermOf+  , TyTermOf+  , SubstOf+  , ErrorOf+) where++import Type.Check.HM.Term+import Type.Check.HM.Subst+import Type.Check.HM.Type+import Type.Check.HM.TypeError+import Type.Check.HM.TyTerm++-- | Main class to define inference API.+-- For type inference we have to define instance of the Lang class:+--+-- > data NoPrim+-- >   deriving (Show)+-- >+-- > data TestLang+-- >+-- > instance Lang TestLang where+-- >   type Src  TestLang = ()+-- >   type Var  TestLang = Text+-- >   type Prim TestLang = NoPrim+-- >   getPrimType _ = error "No primops"+--+class+  ( IsVar (Var q)+  , Show (Src q)+  , Show (Prim q)+  , Eq (Src q)+  ) => Lang q where++  -- | Variables for our language. Notice that this type should be injective in relation to type of @Lang@.+  -- We need to have unique type of variables for each language definition.+  type Var q = r | r -> q++  -- | Source code locations+  type Src q++  -- | Primitives+  type Prim q++  -- | Reports type for primitive.+  getPrimType :: Prim q -> TypeOf q++-- | Types of our language+type TypeOf q = Type (Src q) (Var q)++-- | |Terms of our language+type TermOf q = Term (Prim q) (Src q) (Var q)++-- | Typed terms of our language+type TyTermOf q = TyTerm (Prim q) (Src q) (Var q)++-- | Type errors of our language+type ErrorOf q = TypeError (Src q) (Var q)++-- | Type substitutions+type SubstOf q = Subst (Src q) (Var q)++
+ src/Type/Check/HM/Pretty.hs view
@@ -0,0 +1,184 @@+{-# OPTIONS_GHC -Wno-orphans #-}+-- | Pretty printer for types and terms.+module Type.Check.HM.Pretty(+    HasPrefix(..)+  , PrintCons(..)+  , OpFix(..)+  , Fixity(..)+) where++import Data.Bool+import Data.Fix+import Data.Maybe+import Data.Text (Text)+import Data.Text.Prettyprint.Doc++import Type.Check.HM.Type+import Type.Check.HM.Term++-- | Class to querry fixity of infix operations.+class IsVar v => HasPrefix v where+  getFixity :: v -> Maybe OpFix++instance HasPrefix Text where+  getFixity = const Nothing++instance HasPrefix String where+  getFixity = const Nothing++instance HasPrefix Int where+  getFixity = const Nothing++-- | This class is useful to define the way to print special cases+-- like constructors for tuples or lists.+class PrintCons v where+  printCons :: v -> [Doc ann] -> Doc ann++instance PrintCons Text where+  printCons name args = hsep $ pretty name : args++isPrefix :: HasPrefix v => v -> Bool+isPrefix = isNothing . getFixity++isInfix :: HasPrefix v => v -> Bool+isInfix  = not . isPrefix++instance (Pretty v, PrintCons v, HasPrefix v) => Pretty (Signature loc v) where+  pretty = foldFix go . unSignature+    where+      go = \case+        ForAllT _ _ r -> r+        MonoT ty      -> pretty ty++instance (HasPrefix v, PrintCons v, Pretty v) => Pretty (Type loc v) where+  pretty = go False initCtx . unType+    where+      go :: Bool -> FixityContext v -> Fix (TypeF loc v) -> Doc ann+      go isArrPrev ctx (Fix expr) = case expr of+        VarT _ name   -> pretty name+        ConT _ name [a, b] | isInfix name -> fromBin name a b+        ConT _ name as -> fromCon isArrPrev name as+        ArrowT _ a b -> fromArrow a b+        TupleT _ as -> fromTuple as+        ListT _ a -> fromList a+        where+          fromCon isArr name args = maybeParens (not (null args) && not isArr && needsParens ctx OpFunAp) $+            printCons name $ fmap (go False (FcRight OpFunAp)) args++          fromBin op a b = maybeParens (needsParens ctx (Op op)) $ hsep+            [ go True (FcLeft $ Op op) a+            , pretty op+            , go True (FcRight $ Op op) b+            ]++          fromArrow a b = maybeParens (needsParens ctx ArrowOp) $ hsep+            [ go True (FcLeft ArrowOp ) a+            , "->"+            , go True (FcRight ArrowOp) b+            ]++          fromTuple as = parens $ hsep $ punctuate comma $ fmap (pretty . Type) as++          fromList a = brackets $ pretty $ Type a++      initCtx = FcNone++maybeParens :: Bool -> Doc ann -> Doc ann+maybeParens cond = bool id parens cond++needsParens :: HasPrefix v => FixityContext v -> Operator v -> Bool+needsParens = \case+  FcNone      -> const False+  FcLeft ctx  -> fcLeft ctx+  FcRight ctx -> fcRight ctx+  where+    fcLeft ctxt op+      | comparePrec ctxt op == PoLT = False+      | comparePrec ctxt op == PoGT = True+      | comparePrec ctxt op == PoNC = True+      -- otherwise the two operators have the same precedence+      | fixity ctxt /= fixity op = True+      | fixity ctxt == FixLeft = False+      | otherwise = True++    fcRight ctxt op+      | comparePrec ctxt op == PoLT = False+      | comparePrec ctxt op == PoGT = True+      | comparePrec ctxt op == PoNC = True+      -- otherwise the two operators have the same precedence+      | fixity ctxt /= fixity op = True+      | fixity ctxt == FixRight = False+      | otherwise = True++data PartialOrdering = PoLT | PoGT | PoEQ | PoNC+  deriving Eq++-- | Defines fixity type and order of infix operation+data OpFix = OpFix+  { opFix'fixity :: !Fixity+  -- ^ fixity type+  , opFix'prec   :: !Int+  -- ^ fixity order+  }++-- | Infix operation can be left or right associative or associativity is not known.+data Fixity = FixLeft | FixRight | FixNone+  deriving Eq++data Operator v = OpFunAp | Op v | ArrowOp+  deriving (Eq, Ord)++data FixityContext v = FcNone | FcLeft (Operator v) | FcRight (Operator v)++{-+initEnv :: FixityEnv+initEnv = Map.fromList+  [ (Op "->", OpFix FixRight 2) ]+-}++getFixityEnv :: HasPrefix v => Operator v -> Maybe OpFix+getFixityEnv = \case+  OpFunAp -> Nothing+  Op v    -> getFixity v+  ArrowOp -> Just $ OpFix FixRight 2++comparePrec :: HasPrefix v => Operator v -> Operator v -> PartialOrdering+comparePrec a b = case (getFixityEnv a, getFixityEnv b) of+  (Just opA, Just opB) -> toPo (opFix'prec opA) (opFix'prec opB)+  _                    -> PoNC+  where+    toPo m n+      | m < n     = PoLT+      | m > n     = PoGT+      | otherwise = PoEQ+++fixity :: HasPrefix v => Operator v -> Fixity+fixity op = maybe FixNone opFix'fixity $ getFixityEnv op++---------------------------------------++instance (HasPrefix v, PrintCons v, Pretty v, Pretty prim) => Pretty (Term prim loc v) where+  pretty (Term x) = foldFix prettyTermF x+    where+      prettyTermF = \case+        Var _ v            -> pretty v+        Prim _ p           -> pretty p+        App _ a b          -> parens $ hsep [a, b]+        Lam _ v a          -> parens $ hsep [hcat ["\\", pretty v], "->", a]+        Let _ v a          -> onLet [v] a+        LetRec _ vs a      -> onLet vs a+        AssertType _ r sig -> parens $ hsep [r, "::", pretty sig]+        Constr _ _ tag     -> pretty tag+        Case _ e alts      -> vcat [ hsep ["case", e, "of"], indent 4 $ vcat $ fmap onAlt alts]+        Bottom _           -> "_|_"+        where+          onLet vs body =+            vcat [ hsep ["let", indent 4 $ vcat $ fmap (\Bind{..} -> hsep [pretty bind'lhs, "=", bind'rhs]) vs]+                 , hsep ["in ", body]]++          onAlt CaseAlt{..} = hsep+            [ pretty caseAlt'tag, hsep $ fmap (pretty . snd . typed'value) caseAlt'args+            , "->"+            , caseAlt'rhs ]+
+ src/Type/Check/HM/Subst.hs view
@@ -0,0 +1,49 @@+-- | Capture-avoiding substitutions.+module Type.Check.HM.Subst(+    CanApply(..)+  , Subst(..)+  , delta+  , applyToVar+) where++import Data.Fix+import qualified Data.Map.Strict as M++import Type.Check.HM.Type++-- | Substitutions of type variables for monomorphic types.+newtype Subst loc v = Subst { unSubst :: M.Map v (Type loc v) }+  deriving (Eq, Ord, Monoid)++instance Ord v => Semigroup (Subst loc v) where+  (Subst ma) <> sb@(Subst mb) = Subst $ fmap (apply sb) ma <> M.difference mb ma++-- | Singleton substitution.+delta :: v -> Type loc v -> Subst loc v+delta v = Subst . M.singleton v++applyToVar :: Ord v => Subst loc v -> v -> Maybe (Type loc v)+applyToVar (Subst m) v = M.lookup v m++---------------------------------------------------------------++-- | Class for application of substitutions to various types.+class CanApply f where+  apply :: Ord v => Subst loc v -> f loc v -> f loc v++instance CanApply Type where+  apply (Subst s) = foldFix go . unType+    where+      go = \case+        VarT loc v -> case M.lookup v s of+          Nothing -> varT loc v+          Just t  -> t+        ConT loc name args -> conT loc name args+        ArrowT loc a b     -> arrowT loc a b+        TupleT loc as      -> tupleT loc as+        ListT loc a        -> listT loc a++instance CanApply Signature where+  apply (Subst s) (Signature (Fix expr)) = case expr of+    MonoT t     -> monoT $ apply (Subst s) t+    ForAllT loc x t -> forAllT loc x $ apply (Subst $ M.delete x s) (Signature t)
+ src/Type/Check/HM/Term.hs view
@@ -0,0 +1,232 @@+-- | This module contains the abstract syntax tree of the term language.+module Type.Check.HM.Term(+    Term(..)+  , TermF(..)+  , CaseAlt(..)+  , Bind(..)+  , varE+  , primE+  , appE+  , lamE+  , letE+  , letRecE+  , assertTypeE+  , caseE+  , constrE+  , bottomE+  , freeVars+) where++import Control.Arrow++import Data.Data+import Data.Fix+import Data.Set (Set)+import Data.Eq.Deriving+import Data.Ord.Deriving+import Text.Show.Deriving++import Type.Check.HM.Subst+import Type.Check.HM.Type++import qualified Data.Set as S++-- | Term functor. The arguments are+-- @loc@ for source code locations, @v@ for variables, @r@ for recurion.+data TermF prim loc v r+    = Var loc v                       -- ^ Variables.+    | Prim loc prim                   -- ^ Primitives.+    | App loc r r                     -- ^ Applications.+    | Lam loc v r                     -- ^ Abstractions.+    | Let loc (Bind loc v r) r        -- ^ Let bindings.+    | LetRec loc [Bind loc v r] r     -- ^ Recursive  let bindings+    | AssertType loc r (Type loc v)   -- ^ Assert type.+    | Case loc r [CaseAlt loc v r]    -- ^ case alternatives+    | Constr loc (Type loc v) v       -- ^ constructor with tag and arity, also we should provide the type+                                      --   of constructor as a function for a type-checker+    | Bottom loc                      -- ^ value of any type that means failed program.+    deriving (Show, Eq, Functor, Foldable, Traversable, Data)++-- | Case alternatives+data CaseAlt loc v a = CaseAlt+  { caseAlt'loc   :: loc+  -- ^ source code location+  , caseAlt'tag   :: v+  -- ^ tag of the constructor+  , caseAlt'args  :: [Typed loc v (loc, v)]+  -- ^ arguments of the pattern matching+  , caseAlt'constrType :: Type loc v+  -- ^ type of the result expression, they should be the same for all cases+  , caseAlt'rhs   :: a+  -- ^ right-hand side of the case-alternative+  }+  deriving (Show, Eq, Functor, Foldable, Traversable, Data)++-- | Local variable definition.+--+-- > let lhs = rhs in ...+data Bind loc var r = Bind+  { bind'loc :: loc             -- ^ Source code location+  , bind'lhs :: var             -- ^ Variable name+  , bind'rhs :: r               -- ^ Definition (right-hand side)+  } deriving (Show, Eq, Functor, Foldable, Traversable, Data)++$(deriveShow1 ''TermF)+$(deriveEq1   ''TermF)+$(deriveOrd1  ''TermF)+$(deriveShow1 ''Bind)+$(deriveEq1   ''Bind)+$(deriveOrd1  ''Bind)+$(deriveShow1 ''CaseAlt)+$(deriveEq1   ''CaseAlt)+$(deriveOrd1  ''CaseAlt)++-- | The type of terms.+newtype Term prim loc v = Term { unTerm :: Fix (TermF prim loc v) }+  deriving (Show, Eq, Data)++instance Functor (Term prim loc) where+  fmap f (Term x) =  Term $ foldFix go x+    where+      go = \case+        Var loc v    -> Fix $ Var loc (f v)+        Prim loc p   -> Fix $ Prim loc p+        App loc a b  -> Fix $ App loc a b+        Lam loc v a  -> Fix $ Lam loc (f v) a+        Let loc v a  -> Fix $ Let loc (v { bind'lhs = f $ bind'lhs v }) a+        LetRec loc vs a -> Fix $ LetRec loc (fmap (\b ->  b { bind'lhs = f $ bind'lhs b }) vs) a+        AssertType loc r sig -> Fix $ AssertType loc r (fmap f sig)+        Case loc a alts -> Fix $ Case loc a $ fmap (mapAlt f) alts+        Constr loc ty v -> Fix $ Constr loc (fmap f ty) (f v)+        Bottom loc -> Fix $ Bottom loc++      mapAlt g alt@CaseAlt{..} = alt+        { caseAlt'tag  = f caseAlt'tag+        , caseAlt'args = fmap (mapTyped g) caseAlt'args+        , caseAlt'constrType = fmap f caseAlt'constrType+        }++      mapTyped g Typed{..} = Typed (fmap f typed'type) (second g typed'value)++-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.+varE :: loc -> var -> Term prim loc var+varE loc = Term . Fix . Var loc++-- | `primE` @loc prim@ constructs a primitive with source code at @loc@.+primE :: loc -> prim -> Term prim loc var+primE loc = Term . Fix . Prim loc++-- | 'appE' @loc a b@ constructs an application of @a@ to @b@ with source code at @loc@.+appE :: loc -> Term prim loc v -> Term prim loc v -> Term prim loc v+appE loc (Term l) (Term r) = Term $ Fix $ App loc l r++-- | 'lamE' @loc x e@ constructs an abstraction of @x@ over @e@ with source code at @loc@.+lamE :: loc -> v -> Term prim loc v -> Term prim loc v+lamE loc x (Term e) = Term $ Fix $ Lam loc x e++-- | 'letE' @loc binds e@ constructs a binding of @binds@ in @e@ with source code at @loc@.+-- No recursive bindings.+letE :: loc -> Bind loc v (Term prim loc v) -> Term prim loc v -> Term prim loc v+letE loc bind (Term e) = Term $ Fix $ Let loc (fmap unTerm bind) e++-- | 'letRecE' @loc binds e@ constructs a recursive binding of @binds@ in @e@ with source code at @loc@.+letRecE :: loc -> [Bind loc v (Term prim loc v)] -> Term prim loc v -> Term prim loc v+letRecE loc binds (Term e) = Term $ Fix $ LetRec loc (fmap (fmap unTerm) binds) e++-- | 'assertTypeE' @loc term ty@ constructs assertion of the type @ty@ to @term@.+assertTypeE :: loc -> Term prim loc v -> Type loc v -> Term prim loc v+assertTypeE loc (Term a) ty = Term $ Fix $ AssertType loc a ty++-- | 'caseE' @loc expr alts@ constructs case alternatives expression.+caseE :: loc -> Term prim loc v -> [CaseAlt loc v (Term prim loc v)] -> Term prim loc v+caseE loc (Term e) alts = Term $ Fix $ Case loc e $ fmap (fmap unTerm) alts++-- | 'constrE' @loc ty tag arity@ constructs constructor tag expression.+constrE :: loc -> Type loc v -> v -> Term prim loc v+constrE loc ty tag = Term $ Fix $ Constr loc ty tag++-- | 'bottomE' @loc@ constructs bottom value.+bottomE :: loc -> Term prim loc v+bottomE loc = Term $ Fix $ Bottom loc++--------------------------------------------------------------------------------++instance HasLoc (Term prim loc v) where+  type Loc (Term prim loc v) = loc++  getLoc (Term (Fix x)) = case x of+    Var loc _   -> loc+    Prim loc _  -> loc+    App loc _ _ -> loc+    Lam loc _ _ -> loc+    Let loc _ _ -> loc+    LetRec loc _ _ -> loc+    AssertType loc _ _ -> loc+    Constr loc _ _ -> loc+    Case loc _ _ -> loc+    Bottom loc -> loc++instance LocFunctor (Term prim) where+  mapLoc f (Term x) = Term $ foldFix go x+    where+      go = \case+        Var loc v    -> Fix $ Var (f loc) v+        Prim loc p   -> Fix $ Prim (f loc) p+        App loc a b  -> Fix $ App (f loc) a b+        Lam loc v a  -> Fix $ Lam (f loc) v a+        Let loc v a  -> Fix $ Let (f loc) (v { bind'loc = f $ bind'loc v }) a+        LetRec loc vs a -> Fix $ LetRec (f loc) (fmap (\b ->  b { bind'loc = f $ bind'loc b }) vs) a+        AssertType loc r sig -> Fix $ AssertType (f loc) r (mapLoc f sig)+        Constr loc ty v -> Fix $ Constr (f loc) (mapLoc f ty) v+        Case loc e alts -> Fix $ Case (f loc) e (fmap mapAlt alts)+        Bottom loc -> Fix $ Bottom (f loc)++      mapAlt alt@CaseAlt{..} = alt+        { caseAlt'loc  = f caseAlt'loc+        , caseAlt'args = fmap mapTyped caseAlt'args+        , caseAlt'constrType = mapLoc f caseAlt'constrType+        }++      mapTyped (Typed ty val) = Typed (mapLoc f ty) (first f val)++-- | Get free variables of the term.+freeVars :: Ord v => Term lprim oc v -> Set v+freeVars = foldFix go . unTerm+  where+    go = \case+      Var    _ v          -> S.singleton v+      Prim   _ _          -> mempty+      App    _ a b        -> mappend a b+      Lam    _ v a        -> S.delete v a+      Let    _ bind body  -> let lhs = S.singleton $ bind'lhs bind+                             in  mappend (bind'rhs bind)+                                         (body `S.difference` lhs)+      LetRec _ binds body -> let lhs = S.fromList $ fmap bind'lhs binds+                             in  (mappend (freeBinds binds) body) `S.difference` lhs+      AssertType _ a _    -> a+      Case _ e alts       -> mappend e (foldMap freeVarAlts alts)+      Constr _ _ _        -> mempty+      Bottom _            -> mempty++    freeBinds = foldMap bind'rhs++    freeVarAlts CaseAlt{..} = caseAlt'rhs `S.difference` (S.fromList $ fmap (snd . typed'value) caseAlt'args)++instance TypeFunctor (Term prim) where+  mapType f (Term term) = Term $ foldFix go term+    where+      go = \case+        Constr loc ty cons       -> Fix $ Constr loc (f ty) cons+        Case loc e alts          -> Fix $ Case loc e $ fmap applyAlt alts+        other                    -> Fix other++      applyAlt alt@CaseAlt{..} = alt+        { caseAlt'args       = fmap applyTyped caseAlt'args+        , caseAlt'constrType = f caseAlt'constrType+        }++      applyTyped ty@Typed{..} = ty { typed'type = f typed'type }++instance CanApply (Term prim) where+  apply subst term = mapType (apply subst) term+
+ src/Type/Check/HM/TyTerm.hs view
@@ -0,0 +1,147 @@+-- | This module contains type annotations for terms of the language.+module Type.Check.HM.TyTerm(+    Ann(..)+  , TyTerm(..)+  , termType+  , tyVarE+  , tyPrimE+  , tyAppE+  , tyLamE+  , tyLetE+  , tyLetRecE+  , tyAssertTypeE+  , tyCaseE+  , tyConstrE+  , tyBottomE+  , mapType+) where++import Control.Arrow++import Data.Fix+import Data.Containers.ListUtils (nubOrdOn)+import Data.Foldable+import Data.Eq.Deriving+import Data.Ord.Deriving+import Text.Show.Deriving++import Type.Check.HM.Subst+import Type.Check.HM.Type+import Type.Check.HM.Term++import qualified Data.DList as D++-- | Type to annotate nodes of AST.+-- We use it for type annotations.+data Ann note f a = Ann+  { ann'note  :: note+  , ann'value :: f a+  } deriving (Show, Eq, Functor, Foldable, Traversable)++$(deriveShow1 ''Ann)+$(deriveEq1   ''Ann)+$(deriveOrd1  ''Ann)+++-- | Terms with type annotations for all subexpressions.+newtype TyTerm prim loc v = TyTerm { unTyTerm :: Fix (Ann (Type loc v) (TermF prim loc v)) }+  deriving (Show, Eq)++termType :: TyTerm prim loc v -> Type loc v+termType (TyTerm (Fix (Ann ty _))) = ty++-- tyTerm :: Type loc v -> TermF loc var (Ann () ) -> TyTerm loc var+tyTerm :: Type loc v -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))) -> TyTerm prim loc v+tyTerm ty x = TyTerm $ Fix $ Ann ty x++-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.+tyVarE :: Type loc var -> loc -> var -> TyTerm prim loc var+tyVarE ty loc var =  tyTerm ty $ Var loc var++-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.+tyPrimE :: Type loc var -> loc -> prim -> TyTerm prim loc var+tyPrimE ty loc prim =  tyTerm ty $ Prim loc prim++-- | 'appE' @loc a b@ constructs an application of @a@ to @b@ with source code at @loc@.+tyAppE :: Type loc v -> loc -> TyTerm prim loc v -> TyTerm prim loc v -> TyTerm prim loc v+tyAppE ty loc (TyTerm l) (TyTerm r) = tyTerm ty $ App loc l r++-- | 'lamE' @loc x e@ constructs an abstraction of @x@ over @e@ with source code at @loc@.+tyLamE :: Type loc v -> loc -> v -> TyTerm prim loc v -> TyTerm prim loc v+tyLamE ty loc x (TyTerm e) = tyTerm ty $ Lam loc x e++-- | 'letE' @loc binds e@ constructs a binding of @binds@ in @e@ with source code at @loc@.+-- No recursive bindings.+tyLetE :: Type loc v -> loc -> Bind loc v (TyTerm prim loc v) -> TyTerm prim loc v -> TyTerm prim loc v+tyLetE ty loc bind (TyTerm e) = tyTerm ty $ Let loc (fmap unTyTerm bind) e++-- | 'letRecE' @loc binds e@ constructs a recursive binding of @binds@ in @e@ with source code at @loc@.+tyLetRecE :: Type loc v -> loc -> [Bind loc v (TyTerm prim loc v)] -> TyTerm prim loc v -> TyTerm prim loc v+tyLetRecE ty loc binds (TyTerm e) = tyTerm ty $ LetRec loc (fmap (fmap unTyTerm) binds) e++-- | 'assertTypeE' @loc term ty@ constructs assertion of the type @ty@ to @term@.+tyAssertTypeE :: loc -> TyTerm prim loc v -> Type loc v -> TyTerm prim loc v+tyAssertTypeE loc (TyTerm a) ty = tyTerm ty $ AssertType loc a ty++-- | 'caseE' @loc expr alts@ constructs case alternatives expression.+tyCaseE :: Type loc v -> loc -> TyTerm prim loc v -> [CaseAlt loc v (TyTerm prim loc v)] -> TyTerm prim loc v+tyCaseE ty loc (TyTerm e) alts = tyTerm ty $ Case loc e $ fmap (fmap unTyTerm) alts++-- | 'constrE' @loc ty tag arity@ constructs constructor tag expression.+tyConstrE :: loc -> Type loc v -> v -> TyTerm prim loc v+tyConstrE loc ty tag = tyTerm ty $ Constr loc ty tag++-- | 'bottomE' @loc@ constructs bottom value.+tyBottomE :: Type loc v -> loc -> TyTerm prim loc v+tyBottomE ty loc = tyTerm ty $ Bottom loc++instance LocFunctor (TyTerm prim) where+  mapLoc f (TyTerm x) = TyTerm $ foldFix go x+    where+      go (Ann annTy term) = Fix $ Ann (mapLoc f annTy) $ case term of+        Var loc v    -> Var (f loc) v+        Prim loc p   -> Prim (f loc) p+        App loc a b  -> App (f loc) a b+        Lam loc v a  -> Lam (f loc) v a+        Let loc v a  -> Let (f loc) (v { bind'loc = f $ bind'loc v }) a+        LetRec loc vs a -> LetRec (f loc) (fmap (\b ->  b { bind'loc = f $ bind'loc b }) vs) a+        AssertType loc r sig -> AssertType (f loc) r (mapLoc f sig)+        Constr loc ty v -> Constr (f loc) (mapLoc f ty) v+        Case loc e alts -> Case (f loc) e (fmap (mapAlt f) alts)+        Bottom loc -> Bottom (f loc)++      mapAlt g alt@CaseAlt{..} = alt+        { caseAlt'loc  = g caseAlt'loc+        , caseAlt'args = fmap (mapTyped g) caseAlt'args+        , caseAlt'constrType = mapLoc g caseAlt'constrType+        }++      mapTyped g (Typed ty val) = Typed (mapLoc g ty) (first g val)++instance TypeFunctor (TyTerm prim) where+  mapType f (TyTerm x) = TyTerm $ foldFix go x+    where+      go (Ann ty term) = Fix $ Ann (f ty) $+        case term of+          Constr loc cty cons -> Constr loc (f cty) cons+          Case loc e alts          -> Case loc e $ fmap applyAlt alts+          other                    -> other++      applyAlt alt@CaseAlt{..} = alt+        { caseAlt'args       = fmap applyTyped caseAlt'args+        , caseAlt'constrType = f caseAlt'constrType+        }++      applyTyped ty@Typed{..} = ty { typed'type = f typed'type }++instance CanApply (TyTerm prim) where+  apply subst term = mapType (apply subst) term++instance HasTypeVars (TyTerm prim) where+  tyVars (TyTerm x) = foldFix (\(Ann ty term) -> tyVars ty <> fold term) x++  tyVarsInOrder (TyTerm x) =+    nubOrdOn fst $ D.toList $ foldFix (\(Ann ty term) -> D.fromList (tyVarsInOrder ty) <> fold term) x+++
+ src/Type/Check/HM/Type.hs view
@@ -0,0 +1,370 @@+-- | This module contains the abstract syntax of Hindley-Milner types.+module Type.Check.HM.Type (+    IsVar(..),+    HasLoc(..),+    DefLoc(..),+    -- * Monomorphic types.+    TypeF(..),+    Type(..),+    varT,+    conT,+    arrowT,+    tupleT,+    listT,+    -- * Typed values+    Typed(..),++    -- * Polymorphic types.+    SignatureF(..),+    Signature(..),+    forAllT,+    monoT,+    stripSignature,+    splitSignature,+    typeToSignature,+    getTypeVars,++    VarSet(..),+    differenceVarSet,+    varSetToList,+    memberVarSet,++    HasTypeVars(..),+    LocFunctor(..),+    setLoc,+    TypeFunctor(..),++    extractFunType,+    extractArrow,++    isMono,+    isPoly+) where++--------------------------------------------------------------------------------++import Control.DeepSeq (NFData(..))+import Control.Monad++import Data.Containers.ListUtils (nubOrdOn)+import Data.Data+import Data.Eq.Deriving+import Data.Ord.Deriving+import Data.Fix+import Data.Foldable+import Data.Function (on)+import Data.Map.Strict (Map)+import Data.Monoid+import Data.String+import Data.Tuple (swap)+import Data.Text (Text)++import GHC.Generics++import qualified Data.List as L+import qualified Data.Map.Strict as M++import Text.Show.Deriving++--------------------------------------------------------------------------------++-- | Class to get source code location.+class HasLoc f where+  -- | Type for source code location+  type Loc f :: *++  -- | Get the source code location.+  getLoc :: f -> Loc f++-- | Type class for default location+class DefLoc f where+  defLoc :: f++-- | Functions we need for variables to do type-inference.+class (Show v, Ord v) => IsVar v where+  -- | Canonical leters for pretty output+  prettyLetters :: [v]++instance IsVar String where+  prettyLetters = stringPrettyLetters++instance IsVar Text where+  prettyLetters = stringPrettyLetters++instance IsVar Int where+  prettyLetters = [0..]++stringPrettyLetters :: IsString a => [a]+stringPrettyLetters = fmap fromString $ [1..] >>= flip replicateM ['a'..'z']++instance DefLoc () where+  defLoc = ()++-- | Type functor. Arguments are+--+-- * @loc@ - source code locations+--+-- * @var@ - variable name+--+-- * @r@ - recursion+--+-- There are only two requried constructors: @VarT@ and @ConT@+-- other constructors are used for convenience of pretty-printing the type.+data TypeF loc var r+    = VarT loc var      -- ^ Variables+    | ConT loc var [r]  -- ^ type constant with list of arguments+    | ArrowT loc r r    -- ^ Special case of ConT that is rendered as ->+    | TupleT loc [r]    -- ^ Special case of ConT that is rendered as (,,,)+    | ListT loc r       -- ^ Special case of ConT that is rendered as [a]+    deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic, Data)++$(deriveShow1 ''TypeF)+$(deriveEq1   ''TypeF)+$(deriveOrd1  ''TypeF)++-- | Values that are tagged explicitly with their type.+data Typed loc v a = Typed+  { typed'type  :: Type loc v+  , typed'value :: a+  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data)++-- | Monomorphic types.+newtype Type loc var = Type { unType :: Fix (TypeF loc var) }+  deriving (Show, Eq, Ord, Generic, Data)++instance HasLoc (Type loc v) where+  type Loc (Type loc v) = loc+  getLoc (Type (Fix x)) = case x of+    VarT   loc _   -> loc+    ConT   loc _ _ -> loc+    ArrowT loc _ _ -> loc+    TupleT loc _   -> loc+    ListT  loc _   -> loc++instance (NFData loc, NFData var) => NFData (Type loc var) where+  rnf (Type m) = foldFix go m where+    go = \case+      VarT   l v   -> rnf l `seq` rnf v+      ConT   l v x -> rnf l `seq` rnf v `seq` rnf x+      ArrowT l a b -> rnf l `seq` rnf a `seq` rnf b+      TupleT l x   -> rnf l `seq` rnf x+      ListT  l x   -> rnf l `seq` rnf x++-- | 'varT' @loc x@ constructs a type variable named @x@ with source code at @loc@.+varT :: loc -> var -> Type loc var+varT loc var = Type $ Fix $ VarT loc var++-- | 'conT' @loc x@ constructs a type constant named @x@ with source code at @loc@.+conT :: loc -> var -> [Type loc var] -> Type loc var+conT loc name args = Type $ Fix $ ConT loc name $ fmap unType $ args++-- | 'arrowT' @loc t0 t1@ constructs an arrow type from @t0@ to @t1@ with source code at @loc@.+arrowT :: loc -> Type loc v -> Type loc v -> Type loc v+arrowT loc (Type t0) (Type t1) = Type $ Fix $ ArrowT loc t0 t1++-- | 'tupleT' @loc ts@ constructs tuple of types @ts@ with source code at @loc@.+tupleT :: loc -> [Type loc var] -> Type loc var+tupleT loc ts = Type $ Fix $ TupleT loc $ fmap unType ts++-- | 'listT' @loc t@ constructs list of @t@ with source code at @loc@.+listT :: loc -> Type loc var -> Type loc var+listT loc (Type t) = Type $ Fix $ ListT loc t++--------------------------------------------------------------------------------++-- | Functor for signature is a special type that we need for type inference algorithm.+-- We specify which variables in the type are schematic (non-free).+data SignatureF loc var r+    = ForAllT loc var r     -- ^ specify schematic variable+    | MonoT (Type loc var)  -- ^ contains the type+    deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Data)++$(deriveShow1 ''SignatureF)+$(deriveEq1   ''SignatureF)+$(deriveOrd1  ''SignatureF)++-- | Signaure is a special type that we need for type inference algorithm.+-- We specify which variables in the type are schematic (non-free).+newtype Signature loc var = Signature { unSignature :: Fix (SignatureF loc var)+  } deriving (Show, Eq, Ord, Data)++instance Functor (Signature loc) where+  fmap f (Signature x) = Signature $ foldFix go x+    where+      go = \case+        ForAllT loc var a -> Fix $ ForAllT loc (f var) a+        MonoT ty          -> Fix $ MonoT $ fmap f ty++instance Functor (Type a) where+  fmap f (Type x) = Type $ foldFix go x+    where+      go = \case+        VarT loc name      -> Fix $ VarT loc $ f name+        ConT loc name args -> Fix $ ConT loc (f name) args+        ArrowT loc a b     -> Fix $ ArrowT loc a b+        TupleT loc as      -> Fix $ TupleT loc as+        ListT loc a        -> Fix $ ListT loc a++instance HasLoc (Signature loc var) where+  type Loc (Signature loc var) = loc+  getLoc (Signature x) = foldFix go x+    where+      go = \case+        MonoT ty        -> getLoc ty+        ForAllT loc _ _ -> loc++-- | Mapping over source code locations. It's like functor but for source code locations.+class LocFunctor f where+  mapLoc :: (locA -> locB) -> f locA var -> f locB var++-- | Sets the source code location to given value for all expressions in the functor.+setLoc :: LocFunctor f => loc -> f locA v -> f loc v+setLoc loc = mapLoc (const loc)++instance LocFunctor Type where+  mapLoc f (Type x) = Type $ foldFix go x+    where+      go = \case+        VarT loc name      -> Fix $ VarT (f loc) name+        ConT loc name args -> Fix $ ConT (f loc) name args+        ArrowT loc a b     -> Fix $ ArrowT (f loc) a b+        TupleT loc as      -> Fix $ TupleT (f loc) as+        ListT loc a        -> Fix $ ListT (f loc) a++instance LocFunctor Signature where+  mapLoc f (Signature x) = Signature $ foldFix go x+    where+      go = \case+        ForAllT loc var a -> Fix $ ForAllT (f loc) var a+        MonoT ty          -> Fix $ MonoT $ mapLoc f ty++-- | Mapps over all types that are contained in the value+class TypeFunctor f where+  mapType :: (Type loc var -> Type loc var) -> f loc var -> f loc var++instance TypeFunctor Type where+  mapType f = f++-- | 'forAllT' @x t@ universally quantifies @x@ in @t@.+forAllT :: loc -> v -> Signature loc v -> Signature loc v+forAllT loc x (Signature t) = Signature $ Fix $ ForAllT loc x t++-- | 'monoT' @t@ lifts a monomorophic type @t@ to a polymorphic one.+monoT :: Type loc src -> Signature loc src+monoT = Signature . Fix . MonoT++-- | Converts simple type to signature with all free variables set to schematic.+typeToSignature :: (Eq loc, Ord v) => Type loc v -> Signature loc v+typeToSignature ty = foldr (\(v, src) a -> forAllT src v a) (monoT ty) vs+  where+    vs = tyVarsInOrder ty++-- | Reads all type-variables.+getTypeVars :: (Ord var, HasTypeVars f) => f src var -> [(src, var)]+getTypeVars = varSetToList . tyVars++--------------------------------------------------------------------------------++-- | The class of types which have free type variables.+class HasTypeVars f where+    -- | 'tyVars' @t@ calculates the set of free type variables in @t@.+    tyVars :: Ord var => f src var -> VarSet src var++    -- | 'tyVarsInOrder' @t@ is like 'tyVars' @t@, except that the type+    -- variables are returned in the order in which they are encountered.+    tyVarsInOrder :: (Eq src, Ord var) => f src var -> [(var, src)]++instance HasTypeVars Type where+    tyVars = foldFix go . unType+      where+        go = \case+          VarT loc v    -> VarSet $ M.singleton v loc+          ConT _ _ args -> mconcat args+          ArrowT _ a b  -> mappend a b+          TupleT _ as   -> mconcat as+          ListT _ a     -> a++    tyVarsInOrder = nubOrdOn fst . foldFix go . unType+      where+        go = \case+          VarT loc var -> [(var, loc)]+          ConT _ _ as  -> mconcat as+          ArrowT _ a b -> mappend a b+          TupleT _ as  -> mconcat as+          ListT _ a    -> a+++instance HasTypeVars Signature where+    tyVars = foldFix go . unSignature+      where+        go = \case+          MonoT t       -> tyVars t+          ForAllT _ x t -> VarSet $ M.delete x $ unVarSet t++    tyVarsInOrder = nubOrdOn fst . foldFix go . unSignature+      where+        go = \case+          MonoT t         -> tyVarsInOrder t+          ForAllT src x t -> L.deleteBy ((==) `on` fst) (x, src) t++--------------------------------------------------------------------------------++-- | Set with information on source code locations.+-- We use it to keep the source code locations for variables.+newtype VarSet src var = VarSet { unVarSet :: Map var src }+  deriving (Semigroup, Monoid)++-- | 'difference' for @VarSet@'s+differenceVarSet :: Ord var => VarSet src var -> VarSet src var -> VarSet src var+differenceVarSet (VarSet a) (VarSet b) = VarSet $ a `M.difference` b++-- | Converts varset to list.+varSetToList :: VarSet src var -> [(src, var)]+varSetToList (VarSet m) = fmap swap $ M.toList m++-- | Checks membership of the item in the varset.+memberVarSet :: Ord var => var -> VarSet src var -> Bool+memberVarSet k (VarSet m) = M.member k m++--------------------------------------------------------------------------------++-- | Removes all information on variables in the type.+-- it gets the thing that we store in constructor @MonoT@.+stripSignature :: Signature src var -> Type src var+stripSignature = foldFix go . unSignature+  where+    go = \case+      ForAllT _ _ r -> r+      MonoT ty -> ty++-- | Separates type variables from type definition.+splitSignature :: Signature loc var -> ([var], Type loc var)+splitSignature (Signature x) = flip foldFix x $ \case+  ForAllT _ v (vs, t) -> (v:vs, t)+  MonoT t             -> ([], t)++-- | If underlying type is a function with several arguments it extracts its list of arguments and result type.+extractFunType :: Type loc var -> ([Type loc var], Type loc var)+extractFunType ty = case extractArrow ty of+  Just (lhs, rhs) ->+    let (args, rhs') = extractFunType rhs+    in  (lhs : args, rhs')+  Nothing         -> ([], ty)++-- | If underlying type is an arrow it extracts its single argument and result type.+extractArrow :: Type loc var -> Maybe (Type loc var, Type loc var)+extractArrow (Type (Fix x)) = case x of+  ArrowT _ a b -> Just (Type a, Type b)+  _            -> Nothing++------------------------------------++-- | Checks that type is monomorphic.+isMono :: Type loc var -> Bool+isMono (Type t) = getAll $ flip foldFix t $ \case+  VarT _ _  -> All False+  other     -> fold other++-- | Checks that type is polymorphic.+isPoly :: Type loc var -> Bool+isPoly = not . isMono
+ src/Type/Check/HM/TypeError.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE DeriveAnyClass     #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DerivingStrategies #-}+-- | This module contains types for structured type errors.+module Type.Check.HM.TypeError where++import Control.DeepSeq (NFData)+import Data.Data+import Data.Function (on)+import GHC.Generics    (Generic)+import Type.Check.HM.Type+import Type.Check.HM.Subst++import qualified Data.List as L++-- | Type errors.+data TypeError loc var+  = OccursErr  loc (Type loc var)                 -- ^ error of mismatch of polymorphic constructors, infinite type. Like [a] = a+  | UnifyErr   loc (Type loc var) (Type loc var)  -- ^ Unification error+  | SubtypeErr loc (Type loc var) (Type loc var)  -- ^ Subtype error (happens on explicit type assertions)+  | NotInScopeErr loc var                         -- ^ Missing signature in context for free-variable.+  | EmptyCaseExpr loc                             -- ^ no case alternatives in the case expression+  | FreshNameFound                                -- ^ internal error with fresh name substitution+  deriving stock    (Show, Eq, Functor, Generic, Data)+  deriving anyclass (NFData)++instance LocFunctor TypeError where+  mapLoc f = \case+    OccursErr loc ty     -> OccursErr (f loc) (mapLoc f ty)+    UnifyErr loc tA tB   -> UnifyErr (f loc) (mapLoc f tA) (mapLoc f tB)+    SubtypeErr loc tA tB -> SubtypeErr (f loc) (mapLoc f tA) (mapLoc f tB)+    NotInScopeErr loc v  -> NotInScopeErr (f loc) v+    EmptyCaseExpr loc    -> EmptyCaseExpr (f loc)+    FreshNameFound       -> FreshNameFound++instance HasTypeVars TypeError where+  tyVars = \case+    OccursErr _ ty     -> tyVars ty+    UnifyErr _ a b     -> tyVars a <> tyVars b+    SubtypeErr _ a b   -> tyVars a <> tyVars b+    NotInScopeErr _ _  -> mempty+    EmptyCaseExpr _    -> mempty+    FreshNameFound     -> mempty++  tyVarsInOrder err = L.nubBy ((==) `on` fst) $ case err of+    OccursErr _ ty     -> tyVarsInOrder ty+    UnifyErr _ a b     -> tyVarsInOrder a <> tyVarsInOrder b+    SubtypeErr _ a b   -> tyVarsInOrder a <> tyVarsInOrder b+    NotInScopeErr _ _  -> mempty+    EmptyCaseExpr _    -> mempty+    FreshNameFound     -> mempty++instance CanApply TypeError where+  apply f = \case+    OccursErr loc ty   -> OccursErr loc $ apply f ty+    UnifyErr loc a b   -> UnifyErr loc (apply f a) (apply f b)+    SubtypeErr loc a b -> SubtypeErr loc (apply f a) (apply f b)+    other              -> other+
+ test/Main.hs view
@@ -0,0 +1,12 @@+-- |+module Main where++import Test.Tasty+import qualified TM.SKI+import qualified TM.NumLang++main :: IO ()+main = defaultMain $ testGroup "HM"+  [ TM.SKI.tests+  , TM.NumLang.tests+  ]
+ test/TM/NumLang.hs view
@@ -0,0 +1,327 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies #-}+-- | Tests for language with lambda calculus with numbers and booleans.+module TM.NumLang where++import Data.String+import Test.Tasty+import Test.Tasty.HUnit++import Data.Either+import qualified Type.Check.HM as T+import qualified Data.Map.Strict as M++infixr ~>++data CodeLoc = CodeLoc+  { codeLoc'line :: Int+  , codeLoc'col  :: Int+  }+  deriving (Show, Eq)++-- | Primitives of our language.+-- We support integers and booleans+data Prim+  = PInt CodeLoc Int     -- ^ integers+  | PBool CodeLoc Bool   -- ^ booleans+  deriving (Show, Eq)++-- | Type for variables+type Var = String++-- types for the language++type Ty = T.Type CodeLoc Var++(~>) :: Ty -> Ty -> Ty+(~>) a b = T.arrowT defLoc a b++boolT, intT :: Ty+boolT = T.conT defLoc "Bool" []+intT  = T.conT defLoc "Int" []++-- | Language tag (we need it for Lang instance)+data NumLang++-- | Instanciate to provide the right components of the language+instance T.Lang NumLang where+  type Src  NumLang = CodeLoc   -- ^ source code locations+  type Var  NumLang = Var       -- ^ variables+  type Prim NumLang = Prim      -- ^ primitives++  -- what type is assigned to primitive literals of the language+  getPrimType = \case+    PInt  loc _ -> T.conT loc "Int"  []+    PBool loc _ -> T.conT loc "Bool" []++-- | Expressions for our language+newtype Expr = Expr { unExpr :: T.Term Prim CodeLoc Var }++-- | In real case we should get this info from parser.+-- For example we assign same code location to all expressions.+defLoc :: CodeLoc+defLoc = CodeLoc 0 0++-- primitives++-- | constructor for integer literals+int :: Int -> Expr+int = Expr . T.primE defLoc . PInt defLoc++-- | constructor for boolean literals+bool :: Bool -> Expr+bool = Expr . T.primE defLoc . PBool defLoc++-- numeric expressions++instance Num Expr where+  (+) = app2 "+"+  (*) = app2 "*"+  (-) = app2 "-"+  negate = app "negate"+  fromInteger = int . fromInteger+  abs = error "undefined"+  signum = error "undefined"++-- boolean expressions++-- | Boolean &&+andB :: Expr -> Expr -> Expr+andB = app2 "&&"++-- | Boolean ||+orB :: Expr -> Expr -> Expr+orB = app2 "||"++-- | Boolean negation+notB :: Expr -> Expr+notB = app "not"++-- comparisons++eq, neq, gt, lt, gte, lte :: Expr -> Expr -> Expr+eq  = app2 "=="+neq = app2 "/="+lt  = app2 "<"+gt  = app2 ">"+lte = app2 "<="+gte = app2 ">="++-- if then else++-- | If-expressions+if_ :: Expr -> Expr -> Expr -> Expr+if_ = app3 "if"++----------------------------------------------------------+-- lambda calc++-- Variables (construct them from string literals)+instance IsString Expr where+  fromString = Expr . T.varE defLoc++toBind :: Var -> Expr -> T.Bind CodeLoc Var (T.Term Prim CodeLoc Var)+toBind v (Expr e) = T.Bind defLoc v e++-- | Application+app :: Expr -> Expr -> Expr+app (Expr a) (Expr b) = Expr $ T.appE defLoc a b++-- | Binary application+app2 :: Expr -> Expr -> Expr -> Expr+app2 a b c = app (app a b) c++-- | Ternary application+app3 :: Expr -> Expr -> Expr -> Expr -> Expr+app3 a b c d = app (app2 a b c) d++-- | Let-expressions+let_ :: Var -> Expr -> Expr -> Expr+let_ v e (Expr body) = Expr $ T.letE defLoc (toBind v e) body++-- | Let-expressions with recursion+letRec :: [(Var, Expr)] -> Expr -> Expr+letRec es (Expr body) = Expr $ T.letRecE defLoc (fmap (uncurry toBind) es) body++-- | Lambda-expressions+lam :: Var -> Expr -> Expr+lam v (Expr fun) = Expr $ T.lamE defLoc v fun++----------------------------------------------------------+-- custom constructors++-- types for custom types+pointT, circleT, rectT :: Ty+pointT  = T.conT defLoc "Point" []+circleT = T.conT defLoc "Circle" []+rectT = T.conT defLoc "Rect" []++-- | Point constructor+point :: Expr -> Expr -> Expr+point = app2 (Expr $ T.constrE defLoc (intT ~> intT ~> pointT) "Point")++circle :: Expr -> Expr -> Expr+circle = app2 (Expr $ T.constrE defLoc (pointT ~> intT ~> circleT) "Circle")++rect :: Expr -> Expr -> Expr+rect = app2 (Expr $ T.constrE defLoc (pointT ~> pointT ~> rectT) "Rect")++casePoint :: Expr -> (Var, Var) -> Expr -> Expr+casePoint (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e+  [T.CaseAlt defLoc "Point" [tyVar intT x, tyVar intT y] pointT body]++caseCircle :: Expr -> (Var, Var) -> Expr -> Expr+caseCircle (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e+  [T.CaseAlt defLoc "Circle" [tyVar pointT x, tyVar intT y] circleT body]++caseRect :: Expr -> (Var, Var) -> Expr -> Expr+caseRect (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e+  [T.CaseAlt defLoc "Rect" [tyVar pointT x, tyVar pointT y] rectT body]++tyVar :: Ty -> Var -> T.Typed CodeLoc Var (CodeLoc, Var)+tyVar ty v = T.Typed ty (defLoc, v)++----------------------------------------------------------+-- Type inference context+--+-- We define in context type signatures for all known functions+-- or functions that were already derived on previous steps of compilation.++-- | Context contains types for all known definitions+defContext :: T.Context CodeLoc Var+defContext = T.Context $ M.fromList $ mconcat+  [ booleans+  , nums+  , comparisons+  , [("if", forA $ T.monoT $ boolT ~> aT ~> aT ~> aT)]+  ]+  where+    booleans =+      [ "&&"  `is` (boolT ~> boolT ~> boolT)+      , "||"  `is` (boolT ~> boolT ~> boolT)+      , "not" `is` (boolT ~> boolT)+      ]++    nums =+      [ "+"  `is` (intT ~> intT ~> intT)+      , "*"  `is` (intT ~> intT ~> intT)+      , "-"  `is` (intT ~> intT ~> intT)+      , "negate" `is` (intT ~> intT)+      ]++    comparisons = fmap ( `is` (intT ~> intT ~> boolT)) ["==", "/=", "<", ">", "<=", ">="]++    is a b = (a, T.monoT b)++    -- forall a . ...+    forA = T.forAllT defLoc "a"++    -- a type variable "a"+    aT = T.varT defLoc "a"+++----------------------------------------------------------+-- examples++intExpr1 :: Expr+intExpr1 = negate $ ((20::Expr) + 30) * 100++boolExpr1 :: Expr+boolExpr1 = andB (andB (notB ((intExpr1 `lte` 1000) `orB` (2 `gt` 0))) (bool True)) (5 `neq` (2 + 2))++failExpr1 :: Expr+failExpr1 = lam "x" $ 2 + "x" `eq` (bool True)++failExpr2 :: Expr+failExpr2 = 2 + bool True++failExpr3 :: Expr+failExpr3 = 2 + "missingVar"++-- | Simple integer function+intFun1 :: Expr+intFun1 = lam "x" ((1 + "x") * 10)++-- | Square distance of the point to zero+squareDist :: Expr+squareDist = lam "x" $ lam "y" $ "x" * "x" + "y" * "y"++-- | Check that point is inside circle+insideCircle :: Expr+insideCircle = lam "d" $ lam "x" $ lam "y" $+  let_ "squareDist" squareDist+    (app2 "squareDist" "x" "y") `lt` ("d" * "d")++-- | Factorial+fact :: Expr+fact = lam "x" $ letRec+  [ ("fac", lam "n" $ if_ (eq "n" 0) 1 ("n" * app "fac" ("n" - 1)))+  ]+  (app "fac" "x")++-- | Greatest common divisor+gcd' :: Expr+gcd' = lam "x" $ lam "y" $ defAbs $ defMod $+  letRec+    [ ("gcd", lam "a" $ lam "b" $ if_ ("b" `eq` 0) (app "abs" "a") (app2 "gcd" "b" (app2 "mod" "a" "b")))+    ]+  (app2 "gcd" "x" "y")+  where+    defAbs = let_ "abs" (lam "a" $ if_ ("a" `gte` 0) "a" (negate "a"))+    defMod = let_ "mod" (lam "a" $ lam "b" $ letRec [("go", lam "m" $ lam "n" $ if_ ("m" `lt` "n") "m" (app2 "go" ("m" - "n") "n"))] (app2 "go" "a" "b"))++-- geometry examples++addPointLam :: Expr+addPointLam = lam "a" $ lam "b" $+  casePoint "a" ("ax", "ay") $+    casePoint "b" ("bx", "by") $ point ("ax" + "bx") ("ay" + "by")++negatePointLam :: Expr+negatePointLam = lam "p" $ casePoint "p" ("px", "py") $+  point (negate "px") (negate "py")++addPoint :: Expr -> Expr -> Expr+addPoint = app2 addPointLam++negatePoint :: Expr -> Expr+negatePoint = app negatePointLam++rectSquare :: Expr+rectSquare = lam "r" $ defAbs $ caseRect "r" ("p1", "p2") $+  casePoint "p1" ("p1x", "p1y") $ casePoint "p2" ("p2x", "p2y") $+    app "abs" $ ("p1x" - "p2x") * ("p1y" - "p2y")+  where+    defAbs = let_ "abs" (lam "a" $ if_ ("a" `gte` 0) "a" (negate "a"))++insideCircle2 :: Expr+insideCircle2 = lam "c" $ lam "p" $ caseCircle "c" ("center", "rad") $+  casePoint (addPoint "center" (negatePoint "p")) ("ax", "ay") $+    app3 insideCircle "rad" "ax" "ay"++----------------------------------------------------------+-- tests++tests :: TestTree+tests = testGroup "lambda calculus with numbers and booleans"+  [ check "int expr"        intT                            intExpr1+  , check "bool expr"       boolT                           boolExpr1+  , check "int fun"         (intT ~> intT)                  intFun1+  , check "square dist fun" (intT ~> intT ~> intT)          squareDist+  , check "inside circle"   (intT ~> intT ~> intT ~> boolT) insideCircle+  , check "factorial"       (intT ~> intT)                  fact+  , check "gcd"             (intT ~> intT ~> intT)          gcd'+  , fails "Fail mismatch 1" failExpr1+  , fails "Fail mismatch 2" failExpr2+  , fails "Fail missing var" failExpr3+  , check "add points"      (pointT ~> pointT ~> pointT)    addPointLam+  , check "negate point"    (pointT ~> pointT)              negatePointLam+  , check "rect square"     (rectT ~> intT)                 rectSquare+  , check "inside circle 2" (circleT ~> pointT ~> boolT)    insideCircle2+  ]+  where+    infer = T.inferType defContext . unExpr+    check msg ty expr = testCase msg $ Right ty @=? (infer expr)+    fails msg expr = testCase msg $ assertBool "Detected wrong type" $ isLeft (infer expr)+
+ test/TM/SKI.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE EmptyDataDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeFamilies      #-}+-- | Tests with type-inference for SKI-combinators+module TM.SKI (tests) where++import Data.Text (Text)+import Test.Tasty+import Test.Tasty.HUnit++import Type.Check.HM++tests :: TestTree+tests = testGroup "infer"+  [ testCase "SKI:I"+  $ Right (var "a" --> var "a") @=? (inferType mempty termI)+  , testCase "SKI:K"+  $ Right (var "a" --> (var "b" --> var "a")) @=? (inferType mempty termK)+  , testCase "let-chain-case"+  $ Right (var "a" --> var "a") @=? (inferType mempty termLetChain)+  , testCase "let-rec-chain-case"+  $ Right (var "a" --> var "a") @=? (inferType mempty termLetRecChain)+  ]+  where+    a --> b = arrowT () a b+    var     = varT ()++----------------------------------------------------------------+data NoPrim+  deriving (Show)++data TestLang++instance Lang TestLang where+  type Src  TestLang = ()+  type Var  TestLang = Text+  type Prim TestLang = NoPrim+  getPrimType _ = error "No primops"++-- I combinator+termI,termK :: Term NoPrim () Text+termI = lamE () "x" $ varE () "x"+termK = lamE () "x" $ lamE () "y" $ varE () "x"++termLetChain :: Term NoPrim () Text+termLetChain = lamE () "x" $ letE ()+  (Bind () "a" $ varE () "x")+    (letE ()+      (Bind () "b" $ varE () "a")+      (varE () "b"))++termLetRecChain :: Term NoPrim () Text+termLetRecChain = lamE () "x" $ letRecE ()+  [ Bind () "a" $ varE () "x"+  , Bind () "b" $ varE () "a"+  ]+  (varE () "b")+