src/HM.hs

   1 -- |
   2 -- Module      :  HM
   3 -- Copyright   :  Tomáš Musil 2014
   4 -- License     :  BSD-3
   5 --
   6 -- Maintainer  :  tomik.musil@gmail.com
   7 -- Stability   :  experimental
   8 --
   9 -- This is a toy implementation of λ-calculus with Hindley-Milner type system.
  10
  11 module HM
  12   ( -- * Types
  13     Type(..)
  14   , Term
  15     -- * Type inference
  16   , algW
  17   ) where
  18
  19 import HM.Term
  20 import HM.Parser
  21
  22 type Substitution = TypeScheme -> TypeScheme
  23
  24 fresh :: TypeVarName
  25 fresh = undefined
  26
  27 substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
  28 substitute = undefined
  29
  30 unify :: TypeScheme -> TypeScheme -> Either String Substitution
  31 unify (TScheme (Primitive a)) (TScheme (Primitive b)) | a == b = Right id
  32 unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id
  33 unify a b = Left $ "cannot unify " ++ show a ++ " with " ++ show b
  34
  35 algW :: HMTerm -> Either String TypeScheme
  36 algW (HMTerm (Var _) t) = Right t
  37 algW (HMTerm (Lambda x t) (TScheme p)) = do
  38   let v = TScheme (TypeVar fresh)
  39       np = substitute v x t
  40   unify p np
  41 algW (HMTerm (App u v) t) = do
  42   tu <- algW u
  43   tv <- algW v
  44   case tu of
  45     (TScheme (TypeFunction a b)) -> do
  46       unify a tv
  47       return b
  48     _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv