From db932048bab8d46070b6888b5d2427cb8f9309d4 Mon Sep 17 00:00:00 2001 From: sebastianselander Date: Sun, 19 Feb 2023 02:10:57 +0100 Subject: [PATCH] Tried fixing bug. Failed. --- src/TypeChecker/HM.hs | 58 ++++++++++++++++++++++++++--------------- src/TypeChecker/HMIr.hs | 10 ++++++- test_program | 7 ++--- 3 files changed, 50 insertions(+), 25 deletions(-) diff --git a/src/TypeChecker/HM.hs b/src/TypeChecker/HM.hs index 27ed8ba..8671d1b 100644 --- a/src/TypeChecker/HM.hs +++ b/src/TypeChecker/HM.hs @@ -3,11 +3,11 @@ {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# HLINT ignore "Use traverse_" #-} -module TypeChecker.HM (typecheck) where +module TypeChecker.HM where import Control.Monad.Except import Control.Monad.State -import Data.Bifunctor (second) +import Data.Bifunctor (bimap, second) import Data.Functor.Identity (Identity, runIdentity) import Data.Map (Map) import qualified Data.Map as M @@ -25,16 +25,14 @@ data Ctx = Ctx { constr :: Map Type Type , frsh :: Char } deriving Show -run :: Infer a -> Either String a -run = runIdentity . runExceptT . flip evalStateT initC - -int = TMono "Int" +run :: Infer a -> Either String (a, Ctx) +run = runIdentity . runExceptT . flip runStateT initC initC :: Ctx initC = Ctx M.empty M.empty M.empty 'a' typecheck :: Program -> Either Error T.Program -typecheck = run . inferPrg +typecheck = undefined . run . inferPrg inferPrg :: Program -> Infer T.Program inferPrg (Program bs) = do @@ -61,10 +59,8 @@ inferExp = \case EInt i -> return (int, T.EInt int i) EId i -> (\t -> (t, T.EId t i)) <$> lookupVar i EAdd e1 e2 -> do - (t1, e1') <- inferExp e1 - (t2, e2') <- inferExp e2 - unless (isInt t1 && isInt t2) (throwError "Can not add non-ints") - return (int,T.EAdd int e1' e2') + insertSig "+" (TArr int (TArr int int)) + inferExp (EApp (EApp (EId "+") e1) e2) EApp e1 e2 -> do (t1, e1') <- inferExp e1 (t2, e2') <- inferExp e2 @@ -77,13 +73,7 @@ inferExp = \case (ret_t,e') <- inferExp e t <- solveConstraints (TArr fr ret_t) return (t, T.EAbs t name e') - ELet name e1 e2 -> do - fr <- fresh - insertVar name fr - (t1, e1') <- inferExp e1 - (t2, e2') <- inferExp e2 - ret_t <- solveConstraints t1 - return (ret_t, T.ELet ret_t name e1' e2') + ELet name e1 e2 -> error "Let expression not implemented yet" isInt :: Type -> Bool @@ -112,6 +102,8 @@ fresh = do modify (\st -> st { frsh = succ chr }) return $ TPol (Ident [chr]) +-- Constraint solving is wrong. (\x. x) 3 is inferred with the type 'a' + addConstraint :: Type -> Type -> Infer () addConstraint t1 t2 = do when (t2 `contains` t1) (throwError $ "Can't match type " ++ printTree t1 ++ " with " ++ printTree t2) @@ -126,13 +118,16 @@ solveConstraints :: Type -> Infer Type solveConstraints t = do c <- gets constr v <- gets vars - subst t <$> solveAll (M.toList c) + xs <- solveAll (M.toList c) + modify (\st -> st { constr = M.fromList xs }) + return $ subst t xs subst :: Type -> [(Type, Type)] -> Type subst t [] = t subst (TArr t1 t2) (x:xs) = subst (TArr (replace x t1) (replace x t2)) xs subst t (x:xs) = subst (replace x t) xs +-- Annoying fucking bug here solveAll :: [(Type, Type)] -> Infer [(Type, Type)] solveAll [] = return [] solveAll (x:xs) = case x of @@ -140,16 +135,37 @@ solveAll (x:xs) = case x of (TArr t1 t2, b) -> fmap ((b, TArr t1 t2) :) $ solveAll $ solve (b, TArr t1 t2) xs (a, TArr t1 t2) -> fmap ((a, TArr t1 t2) :) $ solveAll $ solve (a, TArr t1 t2) xs (TMono a, TPol b) -> fmap ((TPol b, TMono a) :) $ solveAll $ solve (TPol b, TMono a) xs - (TPol a, TMono b) -> fmap ((TPol a, TMono a) :) $ solveAll $ solve (TPol a, TMono b) xs + (TPol a, TMono b) -> fmap ((TPol a, TMono b) :) $ solveAll $ solve (TPol a, TMono b) xs (TMono a, TMono b) -> if a == b then solveAll xs else throwError "Can't unify types" (TPol a, TPol b) -> fmap ((TPol a, TPol b) :) $ solveAll $ solve (TPol a, TPol b) xs solve :: (Type, Type) -> [(Type, Type)] -> [(Type, Type)] -solve x = map (second (replace x)) +solve x = map (both (replace x)) replace :: (Type, Type) -> Type -> Type replace a (TArr t1 t2) = TArr (replace a t1) (replace a t2) replace (a,b) c = if a==c then b else c +both :: (a -> b) -> (a,a) -> (b,b) +both f = bimap f f + +int = TMono "Int" +a = TPol "a" +b = TPol "b" +c = TPol "c" +d = TPol "d" +e = TPol "e" +arr = TArr + +set = [(a, arr d e), (c, arr int d), (arr int (arr int int), arr b c)] + +prg = EAbs "f" (EAbs "x" (EApp (EId "f") (EAdd (EId "x") (EInt 1)))) + +bug = EApp (EAbs "x" (EAdd (EAnn (EId "x") a) (EInt 3))) (EInt 2) + +-- (\x. \y. x + y + 1) +prg2 = EApp (EAbs "x" (EId "x")) (EInt 1) + +-- -- Known bugs -- (x : a) + 3 type checks diff --git a/src/TypeChecker/HMIr.hs b/src/TypeChecker/HMIr.hs index f0158b6..036fa42 100644 --- a/src/TypeChecker/HMIr.hs +++ b/src/TypeChecker/HMIr.hs @@ -20,7 +20,15 @@ data Exp | EApp Type Exp Exp | EAdd Type Exp Exp | EAbs Type Ident Exp - deriving (C.Eq, C.Ord, C.Show, C.Read) + deriving (C.Eq, C.Ord, C.Read) + +instance Show Exp where + show (EId t (Ident i)) = i ++ " : " ++ show t + show (EInt _ i) = show i + show (ELet t i e1 e2) = error "Show for let not implemented" + show (EApp t e1 e2) = show e1 ++ " " ++ show e2 ++ " : " ++ show t + show (EAdd _ e1 e2) = show e1 ++ " + " ++ show e2 + show (EAbs t (Ident i) e) = "\\ " ++ i ++ ". " ++ show e ++ " : " ++ show t type Id = (Type, Ident) diff --git a/test_program b/test_program index b81c8de..e342096 100644 --- a/test_program +++ b/test_program @@ -1,4 +1,5 @@ -main : Mono Int ; -main = let f = \x. x in f 5 ; - +id : Mono Int -> Mono Int ; +id = \x. x ; +main : Poly a ; +main = id 3 ;