From: Tomáš Musil Date: Tue, 30 Dec 2014 22:29:21 +0000 (+0100) Subject: more work on Hindley-Milner X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/f9d54d61f2feba3f37c9e7c5f4ab87bf7b3e6166?ds=sidebyside more work on Hindley-Milner --- diff --git a/fp.cabal b/fp.cabal index 018b0d6..9d650ec 100644 --- a/fp.cabal +++ b/fp.cabal @@ -19,7 +19,10 @@ library exposed-modules: Lambda Lambda.Parser.Fancy Lambda.Parser.Simple + HM + HM.Parser other-modules: Lambda.Term + HM.Term build-depends: base >=4.7 && <4.8 , text >=1.2 && <1.3 , attoparsec >=0.12 && <0.13 diff --git a/src/Lambda/Type.hs b/src/HM.hs similarity index 66% rename from src/Lambda/Type.hs rename to src/HM.hs index e54dbe5..83bbe04 100644 --- a/src/Lambda/Type.hs +++ b/src/HM.hs @@ -1,30 +1,23 @@ -- | --- Module : Lambda.Type +-- Module : HM -- Copyright : Tomáš Musil 2014 -- License : BSD-3 -- -- Maintainer : tomik.musil@gmail.com -- Stability : experimental -- --- Data types for Hindley-Milner types. +-- This is a toy implementation of λ-calculus with Hindley-Milner type system. - -module Lambda.Type +module HM ( -- * Types Type(..) + , Term -- * Type inference , algW ) where -import Lambda.Term - -type TypeVarName = String -type TypeName = String - -data Type = Primitive TypeName | TypeVar TypeVarName | TypeFunction Type Type deriving (Show) -data TypeScheme = TScheme Type | TSForAll TypeVarName TypeScheme deriving (Show) - -data HMTerm = HMTerm Term TypeScheme | HMLet VarName HMTerm HMTerm TypeScheme +import HM.Term +import HM.Parser type Substitution = TypeScheme -> TypeScheme @@ -37,13 +30,13 @@ substitute = undefined unify :: TypeScheme -> TypeScheme -> Either String Substitution unify (TScheme (Primitive a)) (TScheme (Primitive b)) | a == b = Right id unify (TScheme (TypeVar a)) (TScheme (TypeVar b)) | a == b = Right id -unify a b = Left "cannot unify " ++ show a ++ " with " ++ show b +unify a b = Left $ "cannot unify " ++ show a ++ " with " ++ show b algW :: HMTerm -> Either String TypeScheme algW (HMTerm (Var _) t) = Right t algW (HMTerm (Lambda x t) (TScheme p)) = do let v = TScheme (TypeVar fresh) - np <- substitute v x t + np = substitute v x t unify p np algW (HMTerm (App u v) t) = do tu <- algW u diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs new file mode 100644 index 0000000..556cbdb --- /dev/null +++ b/src/HM/Parser.hs @@ -0,0 +1,83 @@ +{-# OPTIONS_GHC -fno-warn-unused-do-bind -fno-warn-orphans #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | +-- Module : HM.Parser +-- Copyright : Tomáš Musil 2014 +-- License : BSD-3 +-- +-- Maintainer : tomik.musil@gmail.com +-- Stability : experimental +-- +-- Parser for Hindley-Milner terms and types. + +module HM.Parser + ( tRead + , parseTerm + ) where + +import Data.Text as T hiding (map) +import Data.Attoparsec.Text +import Control.Applicative + +import HM.Term +import qualified Lambda.Parser.Fancy as Lambda +import qualified Lambda.Term as Lambda + +braced :: String -> String +braced t = "(" ++ t ++ ")" + +instance Show Term where + show (Var x) = x + show (Lam x (NTTerm (Lam y t))) = show (Lam (x ++ " " ++ y) t) + show (Lam x t) = braced $ "λ" ++ x ++ "." ++ show t + show (App a (NTTerm (App b c))) = show a ++ " " ++ (braced $ show (App b c)) + show (App t r) = show t ++ " " ++ show r + show (Let x e1 e2) = braced $ "let " ++ x ++ " = " ++ show e1 ++ " in " ++ show e2 + +instance Show TypedTerm where + show (NTTerm t) = show t + show (TTerm t tp) = braced $ show t ++ " :: " ++ show tp + +instance Show Type where + show (Primitive t) = t + show (TypeVar t) = t + show (TypeFunction a b) = braced $ show a ++ " -> " ++ show b + +instance Show TypeScheme where + show (TScheme t) = show t + show (TSForAll x t) = braced $ "∀" ++ x ++ ": " ++ show t + +tRead :: String -> Term +tRead = undefined + +parseTerm :: Parser TypedTerm +parseTerm = parseLet <|> + (lambdaToHM <$> Lambda.parseTerm) + +parseLet :: Parser TypedTerm +parseLet = do + char '(' + string "let " + (Lambda.Var x) <- Lambda.parseVar + string " = " + e1 <- lambdaToHM <$> Lambda.parseTerm + string " in " + e2 <- lambdaToHM <$> Lambda.parseTerm + char ')' + return . NTTerm $ Let x e1 e2 + +lambdaToHM :: Lambda.Term -> TypedTerm +lambdaToHM (Lambda.Var x) = NTTerm $ Var x +lambdaToHM (Lambda.App t u) = NTTerm $ App (lambdaToHM t) (lambdaToHM u) +lambdaToHM (Lambda.Lambda x t) = NTTerm $ Lam x (lambdaToHM t) + +-- | +-- TODO prop> t == tRead (show (t :: Term)) + +{- +tRead :: String -> Term +tRead s = case parseOnly (parseTerm <* endOfInput) (T.pack s) of + (Right t) -> t + (Left e) -> error e +-} diff --git a/src/HM/Term.hs b/src/HM/Term.hs new file mode 100644 index 0000000..0a686f9 --- /dev/null +++ b/src/HM/Term.hs @@ -0,0 +1,30 @@ +-- | +-- Module : HM.Term +-- Copyright : Tomáš Musil 2014 +-- License : BSD-3 +-- +-- Maintainer : tomik.musil@gmail.com +-- Stability : experimental +-- +-- Data types for Hindley-Milner terms. + +module HM.Term + ( -- * Types + VarName + , TypeVarName + , TypeName + , Term(..) + , TypedTerm(..) + , Type(..) + , TypeScheme(..) + ) where + +type VarName = String +type TypeVarName = String +type TypeName = String + +data Type = Primitive TypeName | TypeVar TypeVarName | TypeFunction Type Type +data TypeScheme = TScheme Type | TSForAll TypeVarName TypeScheme + +data Term = Var VarName | Lam VarName TypedTerm | App TypedTerm TypedTerm | Let VarName TypedTerm TypedTerm +data TypedTerm = NTTerm Term | TTerm Term TypeScheme diff --git a/src/Lambda/Parser/Fancy.hs b/src/Lambda/Parser/Fancy.hs index 79c1ca9..9a1deb3 100644 --- a/src/Lambda/Parser/Fancy.hs +++ b/src/Lambda/Parser/Fancy.hs @@ -14,8 +14,12 @@ -- TODO: proper documentation module Lambda.Parser.Fancy - ( tRead + ( + -- * Main parser + tRead , parseTerm + -- * Auxiliary parsers + , parseVar ) where import Data.Text as T hiding (map)