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   , TypeScheme(..)
  15   , Term(..)
  16   , TypedTerm(..)
  17     -- * Type inference
  18   , algW
  19   ) where
  20
  21 import Control.Monad.State
  22
  23 import HM.Term
  24 import HM.Parser
  25
  26 type Substitution = TypeScheme -> TypeScheme
  27 type VarS a = State Int a
  28
  29 fresh :: TypeVarName
  30 fresh = undefined
  31 --fresh = do
  32 --  n <- get
  33 --  "a" ++ show n
  34
  35
  36 substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
  37 substitute = undefined
  38
  39 unify :: TypeScheme -> TypeScheme -> Either String Substitution
  40 unify (TScheme (Primitive a)) (TScheme (Primitive b)) | a == b = Right id
  41 unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id
  42 unify a b = Left $ "cannot unify " ++ show a ++ " with " ++ show b
  43
  44 algW :: TypedTerm -> Either String TypeScheme
  45 algW (TTerm (Var _) t) = Right t
  46 --algW (TTerm (Lam x t) (TScheme p)) = do
  47 --  let v = TScheme (TypeVar fresh)
  48 --      np = substitute v x t
  49 --  unify p np
  50 --algW (TTerm (App u v) t) = do
  51 --  tu <- algW u
  52 --  tv <- algW v
  53 --  case tu of
  54 --    (TScheme (TypeFunction a b)) -> do
  55 --      unify a tv
  56 --      return b
  57 --    _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv