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   ) where
  16
  17 import Lambda.Term
  18
  19 type TypeVarName = String
  20 type TypeName = String
  21
  22 data Type = Primitive TypeName | TypeVar TypeVarName | TypeFunction Type Type deriving (Show)
  23 data TypeScheme = TScheme Type | TSForAll TypeVarName TypeScheme deriving (Show)
  24
  25 data HMTerm = HMTerm Term TypeScheme | HMLet VarName HMTerm HMTerm TypeScheme
  26
  27 fresh :: TypeVarName
  28 fresh = undefined
  29
  30 substitute :: TypeScheme -> TypeVarName -> TypeScheme -> TypeScheme
  31 substitute = undefined
  32
  33 unify :: TypeScheme -> TypeScheme -> Either String TypeScheme
  34 unify = undefined
  35
  36 algW :: HMTerm -> Either String TypeScheme
  37 algW (HMTerm (Var _) t) = Right t
  38 algW (HMTerm (Lambda x t) (TScheme p)) = do
  39   let v = TScheme (TypeVar fresh)
  40   np <- substitute v x t
  41   return $ unify p np
  42 algW (HMTerm (App u v) t) = do
  43   tu <- algW u
  44   tv <- algW v
  45   case tu of
  46     (TScheme (TypeFunction a b)) -> do
  47       unify a tv
  48       return b
  49     _ -> Left $ "cannot apply " ++ show tu ++ " to " ++ show tv
  50
  51
  52