more work on Hindley-Milner

diff --git a/fp.cabal b/fp.cabal
index 018b0d6..9d650ec 100644 (file)
--- a/fp.cabal
+++ b/fp.cabal
@@ -19,7 +19,10 @@ library
   exposed-modules: Lambda
                    Lambda.Parser.Fancy
                    Lambda.Parser.Simple
   exposed-modules: Lambda
                    Lambda.Parser.Fancy
                    Lambda.Parser.Simple

+                   HM
+                   HM.Parser

   other-modules:   Lambda.Term
   other-modules:   Lambda.Term

+                   HM.Term

   build-depends:       base >=4.7 && <4.8
                      , text >=1.2 && <1.3
                      , attoparsec >=0.12 && <0.13
   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 (file)
--- 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
 --
 -- 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(..)
   ( -- * Types
     Type(..)

+  , Term

     -- * Type inference
   , algW
   ) where
 
     -- * 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
 
 
 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 :: 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)
 
 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
   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 (file)
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 (file)
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 (file)
--- a/src/Lambda/Parser/Fancy.hs
+++ b/src/Lambda/Parser/Fancy.hs
@@ -14,8 +14,12 @@
 -- TODO: proper documentation
 
 module Lambda.Parser.Fancy 
 -- TODO: proper documentation
 
 module Lambda.Parser.Fancy 

-  ( tRead
+  (
+  -- * Main parser
+    tRead

   , parseTerm
   , parseTerm

+  -- * Auxiliary parsers
+  , parseVar

   )  where
 
 import Data.Text as T hiding (map)
   )  where
 
 import Data.Text as T hiding (map)