hindley-milner (empty) → 0.1.0.0

raw patch · 12 files changed

+737/−0 lines, 12 filesdep +basedep +containersdep +data-fixsetup-changed

Dependencies added: base, containers, data-fix, hindley-milner, hspec, mtl, transformers

Files

• Setup.hs +2/−0
• hindley-milner.cabal +108/−0
• src/Language/HM.hs +17/−0
• src/Language/HM/AlgorithmW.hs +209/−0
• src/Language/HM/Alpha.hs +17/−0
• src/Language/HM/Term.hs +82/−0
• src/Language/HM/Theta.hs +54/−0
• src/Language/HM/Type.hs +122/−0
• src/Language/HM/TypeError.hs +19/−0
• test/Language/HM/AlgorithmWSpec.hs +56/−0
• test/Language/HM/TypeSpec.hs +50/−0
• test/Spec.hs +1/−0

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain

@@ -0,0 +1,108 @@+-- Initial hindley-milner.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+-- The name of the package.
+name:                   hindley-milner
+
+-- The package version.  See the Haskell package versioning policy (PVP)
+-- for standards guiding when and how versions should be incremented.
+-- http://www.haskell.org/haskellwiki/Package_versioning_policy
+-- PVP summary:         +-+------- breaking API changes
+--                      | | +----- non-breaking API additions
+--                      | | | +--- code changes with no API change
+version:                0.1.0.0
+
+-- A short (one-line) description of the package.
+synopsis:               Template for Hindley-Milner based languages
+
+-- A longer description of the package.
+description:
+    This package contains an implemention of Hindley-Milner and Algorithm W as
+    a starting point for derived languages.
+
+-- The license under which the package is released.
+license: MIT
+
+-- The file containing the license text.
+-- license-file:           LICENSE
+
+-- The package author(s).
+author:                 Michael B. Gale
+
+-- An email address to which users can send suggestions, bug reports, and
+-- patches.
+maintainer:             michael.gale@cl.cam.ac.uk
+
+-- A copyright notice.
+-- copyright:
+
+category:               Language
+
+build-type:             Simple
+
+-- Extra files to be distributed with the package, such as examples or a
+-- README.
+-- extra-source-files:
+
+-- Constraint on the version of Cabal needed to build this package.
+cabal-version:          >=1.10
+
+source-repository head
+  type:                 git
+  location:             https://github.com/mbg/hindley-milner
+
+library
+  exposed-modules:
+    Language.HM,
+    Language.HM.AlgorithmW,
+    Language.HM.Alpha,
+    Language.HM.Term,
+    Language.HM.Theta,
+    Language.HM.Type,
+    Language.HM.TypeError
+
+  other-modules:
+
+
+  -- LANGUAGE extensions used by modules in this package.
+  -- other-extensions:
+
+  -- Other library packages from which modules are imported.
+  build-depends:
+    base >=4.8 && <4.9,
+    containers >=0.5,
+    data-fix,
+    mtl,
+    transformers
+
+  -- Directories containing source files.
+  hs-source-dirs:       src
+
+  -- Base language which the package is written in.
+  default-language:     Haskell2010
+
+  default-extensions:
+    DeriveFunctor,
+    DeriveFoldable,
+    DeriveTraversable,
+    TypeSynonymInstances,
+    FlexibleInstances
+
+test-suite spec
+  type:                 exitcode-stdio-1.0
+
+  main-is:              Spec.hs
+
+  other-modules:
+    Language.HM.AlgorithmWSpec,
+    Language.HM.TypeSpec
+
+  build-depends:
+    base >=4.8 && <4.9,
+    hindley-milner,
+    hspec,
+    containers >= 0.5
+
+  hs-source-dirs:       test
+
+  default-language:     Haskell2010

@@ -0,0 +1,17 @@+--------------------------------------------------------------------------------
+
+module Language.HM (
+    module Language.HM.Alpha,
+    module Language.HM.Term,
+    module Language.HM.Type,
+    module Language.HM.TypeError
+) where
+
+--------------------------------------------------------------------------------
+
+import Language.HM.Alpha
+import Language.HM.Term
+import Language.HM.Type
+import Language.HM.TypeError
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,209 @@+--------------------------------------------------------------------------------
+
+module Language.HM.AlgorithmW (
+    -- * Typing contexts
+    Context,
+    empty,
+
+    -- * External interface
+    runW,
+    inferW,
+
+    -- * Misc
+    genInOrder
+) where
+
+--------------------------------------------------------------------------------
+
+import Data.Fix
+import qualified Data.List as L
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Language.HM.Term
+import Language.HM.Theta
+import Language.HM.Type
+import Language.HM.TypeError
+
+--------------------------------------------------------------------------------
+
+-- | Typing contexts.
+type Context = M.Map Var Sigma
+
+-- | 'empty' is the empty typing context.
+empty :: Context
+empty = M.empty
+
+instance CanApply Context where
+    apply s = M.map (apply s)
+
+--------------------------------------------------------------------------------
+
+-- | The type of Algorithm W computations.
+newtype W a = W { unW :: Context -> Int -> Either TypeError (a, Int) }
+
+instance Functor W where
+    f `fmap` (W m) = W $ \ctx n -> do
+        (r,n') <- m ctx n
+        return (f r, n')
+
+instance Applicative W where
+    pure x = W $ \_ n -> return (x, n)
+
+    (W m) <*> (W m') = W $ \ctx n -> do
+        (f, n')  <- m ctx n
+        (x, n'') <- m' ctx n'
+        return (f x, n'')
+
+instance Monad W where
+    W m >>= f = W $ \ctx n -> do
+        (r, n') <- m ctx n
+        let W m' = f r in m' ctx n'
+
+--------------------------------------------------------------------------------
+
+-- | 'fresh' returns a fresh type variable.
+fresh :: W Tau
+fresh = W $ \ctx n -> return (varT ('$' : show n), n + 1)
+
+typeError :: TypeError -> W a
+typeError err = W $ \_ _ -> Left err
+
+--------------------------------------------------------------------------------
+
+-- | 'gen' @t@ generalises a monomorphic type @t@ to a polymorphic type.
+gen :: Tau -> W Sigma
+gen t = W $ \ctx n -> return (gen' ctx t, n)
+
+gen' :: Context -> Tau -> Sigma
+gen' ctx t = S.foldr forAllT (monoT t) vs
+    where
+        cs = S.unions $ map tyVars $ M.elems ctx
+        vs = tyVars t `S.difference` cs
+
+-- | 'genInOrder' @ctx t@ generalises a monomorphic type @t@ to a polymorphic
+-- type in a context @ctx@. This variant of 'gen' ensures that the order of
+-- quantifiers matches that in which type variables occur in @t@.
+genInOrder :: Context -> Tau -> Sigma
+genInOrder ctx t = foldr forAllT (monoT t) vs
+    where
+        cs = S.unions $ map tyVars $ M.elems ctx
+        vs = tyVarsInOrder t L.\\ S.toList cs
+
+-- | 'inst' @t@ instantiates a polymorphic type @t@ with fresh type variables.
+inst :: Sigma -> W Tau
+inst = cataM go
+    where
+        go (MonoT t) = return t
+        go (ForAllT x t) = do
+            i <- fresh
+
+            let s = M.singleton x i
+
+            return (apply s t)
+
+-- | 'withContext' @f m@ runs applies @f@ to the typing context in which @m@ is
+-- run. The context of the overall computation is not affected.
+withContext :: (Context -> Context) -> W a -> W a
+withContext f (W m) = W $ \ctx n -> m (f ctx) n
+
+-- | 'lookupType' @x@ looks up the type of @x@ in the context.
+lookupType :: Var -> W (Maybe Sigma)
+lookupType x = W $ \ctx n -> return (M.lookup x ctx, n)
+
+-- | 'requireType' @x@ looks up the type of @x@ in the context. A type error
+-- is raised if @x@ is not typed in the context.
+requireType :: Var -> W Sigma
+requireType x = lookupType x >>= \r -> case r of
+    Nothing -> typeError $ NotInScopeErr x
+    Just t  -> return t
+
+--------------------------------------------------------------------------------
+
+-- | 'bind' @x t@ binds a type @t@ to a type variable named @x@.
+bind :: String -> TauF (Fix TauF) -> W Theta
+bind x (VarT y) | x == y = return M.empty
+bind x t
+    | x `S.member` tyVars (Fix t) = typeError $ OccursErr x (Fix t)
+    | otherwise = return $ M.singleton x (Fix t)
+
+-- | 'unify' @t0 t1@ unifies two types @t0@ and @t1@. If the two types can be
+-- unified, a substitution is returned which unifies them.
+unify :: Tau -> Tau -> W Theta
+unify t0 t1 = go (unFix t0) (unFix t1)
+    where
+        go (VarT x) t = bind x t
+        go t (VarT x) = bind x t
+        go (ArrowT f x) (ArrowT g y) = do
+            s0 <- go (unFix f) (unFix g)
+            s1 <- go (unFix $ apply s0 x) (unFix $ apply s0 y)
+            return (s1 <@> s0)
+        -- without base types etc., all types are unifiable
+        --  go t0 t1 = typeError $ UnifyErr (Fix t0) (Fix t1)
+
+--------------------------------------------------------------------------------
+
+-- | 'infer' @term@ reconstructs types in @term@.
+infer :: Term -> W TyTerm
+infer term = (\(s,_,e) -> apply s e) `fmap` cata go term
+    where
+        go :: TermF Var (W (Theta, Tau, TyTerm)) -> W (Theta, Tau, TyTerm)
+        go (Var x) = do
+            -- @x@ must be typed in the context
+            pt <- requireType x
+
+            -- instantiate the type of @x@
+            mt <- inst pt
+
+            -- return an annotated variable along with an empty substituion
+            return (M.empty, mt, tyVarE (Typed x (monoT mt)) mt)
+        go (App f x) = do
+            (s0, t0, tf) <- f
+            (s1, t1, tx) <- withContext (apply s0) x
+
+            -- generate a fresh type variable to represent the return type
+            -- of the function
+            mt <- fresh
+
+            -- unify the types
+            s2 <- unify t0 (t1 `arrowT` mt)
+
+            -- return the annotated application
+            return (s2 <@> s1 <@> s0, apply s2 mt, tyAppE tf tx mt)
+        go (Abs x e) = do
+            -- we need a fresh type variable for @x@
+            mt <- fresh
+
+            --
+            (s0, t0, te) <- withContext (M.insert x (monoT mt)) e
+
+            let rt = arrowT mt t0
+
+            -- return the annotated abstraction
+            return (s0, apply s0 rt, tyAbsE (Typed x (monoT mt)) te rt)
+        go (Let x e0 e1) = do
+            -- infer the type of the expression that is being bound
+            (s0, t0, te0) <- e0
+
+            -- generalise the type of the expression that is being bound
+            pt <- withContext (apply s0) (gen t0)
+
+            -- infer the type of the other expression
+            (s1, t1, te1) <- withContext (apply s0 . M.insert x pt) e1
+
+            -- return the annotated let binding
+            return (s1 <@> s0, t1, tyLetE (Typed x pt) te0 te1 t1)
+
+--------------------------------------------------------------------------------
+
+-- | 'runW' @gamma term@ runs Algorithm W on @term@ with an initial context
+-- @gamma@ and returns an updated @term@ with explicit type annotations.
+runW :: Context -> Term -> Either TypeError TyTerm
+runW ctx term = fst `fmap` unW (infer term) ctx 0
+
+-- | 'inferW' @gamma term@ runs Algorithm W on @term@ with an initial context
+-- @gamma@ and returns the polymorphic type of the whole term.
+inferW :: Context -> Term -> Either TypeError Tau
+inferW ctx term = (tyAnn . unTypedF . unFix) `fmap` runW ctx term
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,17 @@+--------------------------------------------------------------------------------
+
+-- | Alpha equivalence.
+module Language.HM.Alpha where
+
+--------------------------------------------------------------------------------
+
+import qualified Data.Map as M
+
+--------------------------------------------------------------------------------
+
+-- | Class of types which have a notion of alpha equivalence.
+class AlphaEq a where
+    -- | 'alphaEq' @x y@ determines whether @x@ and @y@ are alpha-equivalent.
+    alphaEq :: a -> a -> Bool
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,82 @@+--------------------------------------------------------------------------------
+
+-- | This module contains the abstract syntax tree of the term language.
+module Language.HM.Term where
+
+--------------------------------------------------------------------------------
+
+import Data.Fix
+
+import Language.HM.Type
+
+--------------------------------------------------------------------------------
+
+-- | The type of variable names.
+type Var = String
+
+data TermF v r
+    = Var v                 -- ^ Variables.
+    | App r r               -- ^ Applications.
+    | Abs v r               -- ^ Abstractions.
+    | Let v r r             -- ^ Let bindings.
+    deriving (Show, Functor, Foldable, Traversable)
+
+-- | The type of terms.
+type Term = Fix (TermF Var)
+
+-- | 'varE' @x@ constructs a variable whose name is @x@.
+varE :: Var -> Term
+varE = Fix . Var
+
+-- | 'appE' @l r@ constructs an application of @l@ to @r@.
+appE :: Term -> Term -> Term
+appE l r = Fix $ App l r
+
+-- | 'absE' @x e@ constructs an abstraction of @x@ over @e@.
+absE :: Var -> Term -> Term
+absE x e = Fix $ Abs x e
+
+-- | 'letE' @x e0 e1@ constructs a binding of @e0@ to @x@ in @e1@.
+letE :: Var -> Term -> Term -> Term
+letE x e0 e1 = Fix $ Let x e0 e1
+
+--------------------------------------------------------------------------------
+
+-- | Things with type annotations.
+data Typed t a
+    = Typed { untype :: a, tyAnn :: t }
+    deriving (Show, Functor)
+
+-- | Typed term variables.
+type TyVar = Typed Sigma Var
+
+newtype TypedF t f r = TypedF { unTypedF :: Typed t (f r) }
+    deriving Show
+
+instance Functor f => Functor (TypedF t f) where
+    fmap f (TypedF t) = TypedF (fmap (fmap f) t)
+
+-- | Typed terms.
+type TyTerm = Fix (TypedF Tau (TermF TyVar))
+
+-- | 'tyVarE' @x t@ constructs a variable whose name is @x@ and whose type is
+-- @t@.
+tyVarE :: TyVar -> Tau -> TyTerm
+tyVarE x t = Fix $ TypedF $ Typed (Var x) t
+
+-- | 'tyAppE' @l r t@ constructs an application of @l@ to @r@ whose resulting
+-- type is @t@.
+tyAppE :: TyTerm -> TyTerm -> Tau -> TyTerm
+tyAppE l r t = Fix $ TypedF $ Typed (App l r) t
+
+-- | 'tyAbsE' @x e t@ constructs an abstraction of @x@ over @t@ whose type
+-- is @t@.
+tyAbsE :: TyVar -> TyTerm -> Tau -> TyTerm
+tyAbsE x e t = Fix $ TypedF $ Typed (Abs x e) t
+
+-- | 'tyLetE' @x e0 e1 t@ constructs a binding of @e0@ to @x@ in @e1@ whose
+-- resulting type is @t@.
+tyLetE :: TyVar -> TyTerm -> TyTerm -> Tau -> TyTerm
+tyLetE x e0 e1 t = Fix $ TypedF $ Typed (Let x e0 e1) t
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,54 @@+--------------------------------------------------------------------------------
+
+-- | Capture-avoiding substitutions.
+module Language.HM.Theta where
+
+--------------------------------------------------------------------------------
+
+import Data.Fix
+import qualified Data.Map as M
+
+import Language.HM.Type
+import Language.HM.Term
+
+--------------------------------------------------------------------------------
+
+-- | Substitutions of type variables for monomorphic types.
+type Theta = M.Map String Tau
+
+--------------------------------------------------------------------------------
+
+-- | Class of types to which type substitutions can be applied.
+class CanApply a where
+    -- | 'apply' @s t@ applies @s@ to some type @t@.
+    apply :: Theta -> a -> a
+
+instance CanApply Tau where
+    apply s = cata g
+        where
+            g :: TauF Tau -> Tau
+            g (VarT x) = case M.lookup x s of
+                Nothing -> varT x
+                Just t  -> apply s t
+            g (ArrowT t0 t1) = arrowT t0 t1
+
+instance CanApply Sigma where
+    apply s = cata g
+        where
+            g :: SigmaF Sigma -> Sigma
+            g (MonoT t) = monoT (apply s t)
+            g (ForAllT x t) = forAllT x (apply (M.delete x s) t)
+
+instance CanApply t => CanApply (Typed t a) where
+    apply s (Typed x t) = Typed x (apply s t)
+
+instance CanApply TyTerm where
+    apply s = cata g
+        where
+            g (TypedF t) = Fix $ TypedF (apply s t)
+
+-- | @s1@ '<@>' @s2@ applies @s1@ to @s2@.
+(<@>) :: Theta -> Theta -> Theta
+s1 <@> s2 = M.map (apply s1) s2 `M.union` s1
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,122 @@+--------------------------------------------------------------------------------
+
+-- | This module contains the abstract syntax of Hindley-Milner types.
+module Language.HM.Type (
+    module Language.HM.Alpha,
+
+    -- * Monomorphic types.
+    TauF(..),
+    Tau(..),
+    varT,
+    arrowT,
+
+    -- * Polymorphic types.
+    SigmaF(..),
+    Sigma(..),
+    forAllT,
+    monoT,
+
+    HasTypeVars(..)
+) where
+
+--------------------------------------------------------------------------------
+
+import Data.Fix
+import qualified Data.List as L
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Language.HM.Alpha
+
+--------------------------------------------------------------------------------
+
+data TauF r
+    = VarT String
+    | ArrowT r r
+    deriving (Eq, Show, Functor)
+
+-- | Monomorphic types.
+type Tau = Fix TauF
+
+-- | 'varT' @x@ constructs a type variable named @x@.
+varT :: String -> Tau
+varT = Fix . VarT
+
+-- | 'arrowT' @t0 t1@ constructs an arrow type from @t0@ to @t1@.
+arrowT :: Tau -> Tau -> Tau
+arrowT t0 t1 = Fix $ ArrowT t0 t1
+
+--------------------------------------------------------------------------------
+
+data SigmaF r
+    = ForAllT String r
+    | MonoT Tau
+    deriving (Eq, Show, Functor, Foldable, Traversable)
+
+-- | Polymorphic types.
+type Sigma = Fix SigmaF
+
+-- | 'forAllT' @x t@ universally quantifies @x@ in @t@.
+forAllT :: String -> Sigma -> Sigma
+forAllT x t = Fix $ ForAllT x t
+
+-- | 'monoT' @t@ lifts a monomorophic type @t@ to a polymorphic one.
+monoT :: Tau -> Sigma
+monoT = Fix . MonoT
+
+instance AlphaEq Sigma where
+    alphaEq t0 t1 = sigmaEq M.empty (unFix t0) (unFix t1)
+        where
+            tauEq env (VarT x) (VarT y) = case M.lookup x env of
+                -- the variable is bound in the left expression: check that
+                -- it matches the name of the variable in the right expression
+                -- that was bound at the same point
+                Just y' -> y == y'
+                -- the variable is free in the left expression: it should have
+                -- the same name as the variable in the right expression
+                Nothing -> x == y
+            tauEq env (ArrowT t0 t1) (ArrowT t0' t1') =
+                tauEq env (unFix t0) (unFix t0') &&
+                tauEq env (unFix t1) (unFix t1')
+            tauEq _ _ _ = False
+
+            sigmaEq env (MonoT t0) (MonoT t1) =
+                tauEq env (unFix t0) (unFix t1)
+            sigmaEq env (ForAllT x t0) (ForAllT y t1) =
+                sigmaEq (M.insert x y env) (unFix t0) (unFix t1)
+            sigmaEq _ _ _ = False
+
+--------------------------------------------------------------------------------
+
+-- | The class of types which have free type variables.
+class HasTypeVars a where
+    -- | 'tyVars' @t@ calculates the set of free type variables in @t@.
+    tyVars :: a -> S.Set String
+
+    -- | 'tyVarsInOrder' @t@ is like 'tyVars' @t@, except that the type
+    -- variables are returned in the order in which they are encountered.
+    tyVarsInOrder :: a -> [String]
+
+instance HasTypeVars Tau where
+    tyVars = cata go
+        where
+            go (VarT x) = S.singleton x
+            go (ArrowT l r) = l `S.union` r
+
+    tyVarsInOrder = L.nub . cata go
+        where
+            go (VarT x) = [x]
+            go (ArrowT l r) = l ++ r
+
+instance HasTypeVars Sigma where
+    tyVars = cata go
+        where
+            go (MonoT t) = tyVars t
+            go (ForAllT x t) = S.delete x t
+
+    tyVarsInOrder = L.nub . cata go
+        where
+            go (MonoT t) = tyVarsInOrder t
+            go (ForAllT x t) = L.delete x t
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,19 @@+--------------------------------------------------------------------------------
+
+-- | This module contains types for structured type errors.
+module Language.HM.TypeError where
+
+--------------------------------------------------------------------------------
+
+import Language.HM.Type
+
+--------------------------------------------------------------------------------
+
+-- | Type errors.
+data TypeError
+    = OccursErr String Tau
+    | UnifyErr Tau Tau
+    | NotInScopeErr String
+    deriving (Eq, Show)
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,56 @@+--------------------------------------------------------------------------------
+
+module Language.HM.AlgorithmWSpec where
+
+--------------------------------------------------------------------------------
+
+import Test.Hspec
+
+import Language.HM
+import Language.HM.AlgorithmW
+
+--------------------------------------------------------------------------------
+
+e0 :: Term
+e0 = varE "x"
+
+e1 :: Term
+e1 = letE "id" (absE "x" (varE "x")) (varE "id")
+
+t1 :: Tau
+t1 = varT "a" `arrowT` varT "a"
+
+e2 :: Term
+e2 = letE "id"
+        (absE "x" (varE "x"))
+        (appE (varE "id") (varE "id"))
+
+e3 :: Term
+e3 = letE "id"
+        (absE "x" (letE "y" (varE "x") (varE "y")))
+        (appE (varE "id") (varE "id"))
+
+e4 :: Term
+e4 = letE "id"
+        (absE "x" (appE (varE "x") (varE "x")))
+        (varE "id")
+
+-- | 'alphaEqOf' @t r@ is a predicate which tests that the result of some
+-- type inference process @r@ is successful and alpha-equivalent to @t@.
+alphaEqOf :: Tau -> Either TypeError Tau -> Bool
+alphaEqOf _ (Left _)   = False
+alphaEqOf t (Right t') = alphaEq (genInOrder empty t) (genInOrder empty t')
+
+occursFailure :: Either TypeError Tau -> Bool
+occursFailure (Left (OccursErr _ _)) = True
+occursFailure _ = False
+
+spec :: Spec
+spec = do
+    it "not in scope" $ inferW empty e0 `shouldBe` Left (NotInScopeErr "x")
+    it "identity function 1" $ inferW empty e1 `shouldSatisfy` alphaEqOf t1
+    it "identity function 2" $ inferW empty e2 `shouldSatisfy` alphaEqOf t1
+    it "identity function 3" $ inferW empty e3 `shouldSatisfy` alphaEqOf t1
+    it "identity function 4" $ inferW empty e4 `shouldSatisfy` occursFailure
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,50 @@+--------------------------------------------------------------------------------
+
+module Language.HM.TypeSpec where
+
+--------------------------------------------------------------------------------
+
+import Test.Hspec
+
+import qualified Data.Set as S
+
+import Language.HM
+
+--------------------------------------------------------------------------------
+
+
+t0 :: Sigma
+t0 = forAllT "a" (monoT $ (varT "a") `arrowT` (varT "a"))
+
+t1 :: Sigma
+t1 = forAllT "b" (monoT $ (varT "b") `arrowT` (varT "b"))
+
+t2 :: Sigma
+t2 = forAllT "b" (monoT $ (varT "b") `arrowT` (varT "a"))
+
+t3 :: Sigma
+t3 = monoT $ varT "a"
+
+t4 :: Sigma
+t4 = monoT $ varT "b"
+
+spec :: Spec
+spec = do
+    describe "alpha equivalence" $ do
+        context "are alpha equivalent" $ do
+            it "same type" $ alphaEq t0 t0 `shouldBe` True
+            it "alpha-equivalent type" $ alphaEq t0 t1 `shouldBe` True
+
+        context "are not alpha equivalent" $ do
+            it "free variable 1" $ alphaEq t0 t2 `shouldBe` False
+            it "free variable 2" $ alphaEq t3 t4 `shouldBe` False
+
+    describe "type variables" $ do
+        it "t0" $ tyVars t0 `shouldBe` S.fromList []
+        it "t1" $ tyVars t1 `shouldBe` S.fromList []
+        it "t2" $ tyVars t2 `shouldBe` S.fromList ["a"]
+        it "t3" $ tyVars t3 `shouldBe` S.fromList ["a"]
+        it "t4" $ tyVars t4 `shouldBe` S.fromList ["b"]
+
+
+--------------------------------------------------------------------------------

@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}