src/Lambda/Type.hs

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