diff --git a/previous-approaches/hml/.gitignore b/previous-approaches/hml/.gitignore deleted file mode 100644 index c368d453..00000000 --- a/previous-approaches/hml/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -.stack-work/ -*~ \ No newline at end of file diff --git a/previous-approaches/hml/CHANGELOG.md b/previous-approaches/hml/CHANGELOG.md deleted file mode 100644 index 90030a52..00000000 --- a/previous-approaches/hml/CHANGELOG.md +++ /dev/null @@ -1,11 +0,0 @@ -# Changelog for `hml` - -All notable changes to this project will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), -and this project adheres to the -[Haskell Package Versioning Policy](https://pvp.haskell.org/). - -## Unreleased - -## 0.1.0.0 - YYYY-MM-DD diff --git a/previous-approaches/hml/LICENSE b/previous-approaches/hml/LICENSE deleted file mode 100644 index c5b6c166..00000000 --- a/previous-approaches/hml/LICENSE +++ /dev/null @@ -1,30 +0,0 @@ -Copyright Author name here (c) 2023 - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials provided - with the distribution. - - * Neither the name of Author name here nor the names of other - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/previous-approaches/hml/README.md b/previous-approaches/hml/README.md deleted file mode 100644 index 79ae1a27..00000000 --- a/previous-approaches/hml/README.md +++ /dev/null @@ -1 +0,0 @@ -# hml diff --git a/previous-approaches/hml/Setup.hs b/previous-approaches/hml/Setup.hs deleted file mode 100644 index 9a994af6..00000000 --- a/previous-approaches/hml/Setup.hs +++ /dev/null @@ -1,2 +0,0 @@ -import Distribution.Simple -main = defaultMain diff --git a/previous-approaches/hml/app/Gamma.hs b/previous-approaches/hml/app/Gamma.hs deleted file mode 100644 index 02de5e0f..00000000 --- a/previous-approaches/hml/app/Gamma.hs +++ /dev/null @@ -1,106 +0,0 @@ --------------------------------------------------------------------------- --- The type environment Gamma --------------------------------------------------------------------------- -module Gamma( Gamma - , gamma0 -- the initial gamma - , gammaFind - , gammaExtend - , gammaCoDomain - ) where - -import qualified Data.Map as Map -import Types -import Parser( readType ) - - --------------------------------------------------------------------------- --- initial gamma --------------------------------------------------------------------------- -gamma0 :: Gamma -gamma0 - = gammaCreate - -- builtin functions - [("(,)", "forall a b. a -> b -> (a,b)") - ,("[]", "forall a. [a]") - ,(":", "forall a. a -> [a] -> [a]") - ,("$", "forall a b. (a -> b) -> a -> b") - ,("if", "forall a. Bool -> a -> a -> a") - - -- standard functions - ,("id", "forall a. a -> a") - ,("apply", "forall a b. (a -> b) -> a -> b") - ,("const", "forall a b. a -> b -> a") - ,("choose", "forall a. a -> a -> a") - ,("revapp", "forall a b. a -> (a -> b) -> b") - ,("undefined", "forall a. a") - - -- booleans - ,("True", "Bool") - ,("False", "Bool") - - -- integers - ,("plus", "Int -> Int -> Int") - ,("lt", "Int -> Int -> Bool") - ,("gt", "Int -> Int -> Bool") - ,("inc", "Int -> Int") - - -- polymorphic functions - ,("ids", "[forall a. a -> a]") - ,("auto", "(forall a. a -> a) -> (forall a. a -> a)") - ,("xauto", "forall a. (forall b. b -> b) -> a -> a") - - ,("takeAuto", "((forall a. a -> a) -> (forall a. a -> a)) -> (forall a. a -> a)") - - -- lists - ,("single", "forall a. a -> [a]") - ,("head", "forall a. [a] -> a") - ,("tail", "forall a. [a] -> [a]") - ,("map", "forall a b. (a -> b) -> [a] -> [b]") - ,("length", "forall a. [a] -> Int") - ,("null", "forall a. [a]-> Bool") - ,("append", "forall a. [a] -> [a] -> [a]") - - -- tuples - ,("fst", "forall a b. (a,b) -> a") - ,("snd", "forall a b. (a,b) -> b") - - -- ST monad - ,("runST", "forall a. (forall s. ST s a) -> a") - ,("newRef", "forall a s. a -> ST s (Ref s a)") - ,("returnST", "forall a s. a -> ST s a") - ] - - --------------------------------------------------------------------------- --- Gamma is a mapping from (term) variables to types --------------------------------------------------------------------------- - --- | Gamma maps term variables to types -data Gamma = Gamma (Map.Map Name Type) - - -gammaCreate :: [(String,String)] -> Gamma -gammaCreate bindings - = gammaFromList $ [(name,readType tp) | (name,tp) <- bindings] - -gammaEmpty - = Gamma Map.empty - -gammaFromList xs - = Gamma (Map.fromList xs) - -gammaFind (Gamma g) name - = case Map.lookup name g of - Nothing -> error ("unbound variable: " ++ name) - Just tp -> tp - -gammaExtend (Gamma g) name tp - = Gamma (Map.insert name tp g) - -instance Show Gamma where - show (Gamma g) = show g - - -gammaCoDomain :: Gamma -> [Type] -gammaCoDomain (Gamma g) - = Map.elems g diff --git a/previous-approaches/hml/app/InferBasic.hs b/previous-approaches/hml/app/InferBasic.hs deleted file mode 100644 index ac1c1731..00000000 --- a/previous-approaches/hml/app/InferBasic.hs +++ /dev/null @@ -1,85 +0,0 @@ --------------------------------------------------------------------------- --- Type inference --- --- Basic type inference algorithm for HML as described in the paper. --------------------------------------------------------------------------- -module InferBasic( inferType, features ) where - -import PPrint -import Types -import Operations -import Unify -import Gamma - -features :: [Feature] -features = [] --------------------------------------------------------------------------- --- Infer the type of a term --------------------------------------------------------------------------- -inferType :: Term -> IO Type -inferType term - = runInfer $ - do uniqueReset - infer gamma0 term - - -infer :: Gamma -> Term -> Infer Type -infer gamma (Var name) - = return (gammaFind gamma name) - -infer gamma (Lit i) - = return (TCon "Int") - -infer gamma (Let name expr body) - = do tp <- infer gamma expr - infer (gammaExtend gamma name tp) body - -infer gamma (Lam name expr) - = do -- we can treat this as an annotated lambda expression: (\x -> e) => (\(x::some a. a) -> e) - infer gamma (ALam name annotAny expr) - -infer gamma (ALam name ann expr) - = do (tp1,tp2) <- withRankIncrease $ -- we are going inside a lambda - do (some,tp1) <- instantiateAnnot ann -- instantiate the "some" quantifiers - tp2 <- infer (gammaExtend gamma name tp1) expr - -- check that we don't infer polytypes for arguments - taus <- mapM isFlexTau some - check (and taus) ("Using unannoted parameter(s) polymorphically with type(s): " ++ show some) - return (tp1,tp2) - -- generalize the result - generalize gamma $ - do res <- freshInstanceVar tp2 - return (mkFun tp1 res) - -infer gamma (App e1 e2) - = do tp1 <- infer gamma e1 - tp2 <- infer gamma e2 - generalize gamma $ - do rho1 <- instantiate tp1 - res <- freshInstanceVar Bottom - arg <- freshInstanceVar tp2 - -- message $ "function unify: " ++ show rho1 ++ " and " ++ show tp2 - unify rho1 (mkFun arg res) - return res - -infer gamma (Ann expr ann) - = do -- we can treat annotations just as applications to an annotated identity function: (e::s) => ((\(x::s).x) e) - infer gamma (App (ALam "x" ann (Var "x")) expr) - -infer gamma (Rigid expr) - = infer gamma expr - - - - - - - - - - - - - - - diff --git a/previous-approaches/hml/app/Main.hs b/previous-approaches/hml/app/Main.hs deleted file mode 100644 index 21ae3bf0..00000000 --- a/previous-approaches/hml/app/Main.hs +++ /dev/null @@ -1,292 +0,0 @@ --------------------------------------------------------------------------- --- Main module: --------------------------------------------------------------------------- -module Main where - -import qualified Control.Exception as Exn ( catch ) -import PPrint -import Types ( Type, Feature(..) ) -import Parser( readType, readTerm ) - - -import InferBasic -- import basic HML type inference as described in the paper - --------------------------------------------------------------------------- --- Main functions --------------------------------------------------------------------------- -check :: String -> IO () -check input - = do inference input - putStrLn "" - -testAll :: IO () -testAll - = test testsAll - -inference :: String -> IO Type -inference input - = do term <- readTerm input - putPretty (text "expr:" <+> align (pretty term) <> linebreak) - - tp <- inferType term - putPretty (text "type:" <+> align (pretty tp) <> linebreak) - return tp - --------------------------------------------------------------------------- --- Tests --------------------------------------------------------------------------- -testsAll :: [Test] -testsAll - = concat - [ testsHM -- Hindley Milner - , testsHR -- Higher rank & impredicative - , testsNary -- N-ary applications, order of arguments - , testsFlexible -- Flexible bounds - , testsExists -- Encoding of existentials - , testsRigidAnn -- Rigid annotations - , if (SupportPropagation `elem` features) then testsProp else [] - , if (SupportPropagateToArg `elem` features) then testsPropArg else [] - -- , testsRigid -- Experimental "rigid" keyword - ] - -testsHM - = -- standard Hindley-Milner tests - [("\\x -> x", ok "forall a. a -> a") - ,("\\f x -> f x", ok "forall a b. (a -> b) -> a -> b") - ,("inc True", Wrong) - ,("let i = \\x -> x in i i", ok "forall a. a -> a") - ,("\\i -> i i", Wrong) -- infinite type - ,("\\i -> (i 1, i True)", Wrong) -- polymorphic use of parameter - ,("single id", ok "forall (a >= forall b. b -> b). [a]") - ,("choose (\\x y -> x) (\\x y -> y)", ok "forall a. a -> a -> a") - ,("choose id", ok "forall (a >= forall b. b -> b). a -> a") - ] - -testsHR - = -- impredicative application and higher rank arguments are fully supported - [("xauto",ok "forall a. (forall a. a -> a) -> a -> a") -- just to show the types of xauto and auto - ,("auto", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("\\(i :: forall a. a -> a) -> i i", ok "forall (a >= forall b. b -> b). (forall b. b -> b) -> a") -- ok "forall a. (forall a. a -> a) -> a -> a") - ,("auto id", ok "forall a. a -> a") - ,("apply auto id", ok "forall a. a -> a") - ,("(single :: (forall a. a -> a) -> [forall a. a->a]) id", ok "[forall a. a-> a]") - ,("runST (returnST 1)", ok "Int") - ,("runST (newRef 1)", Wrong) - ,("apply runST (returnST 1)", ok "Int") - ,("map xauto ids", ok "forall a. [a -> a]") - ,("map xauto (map xauto ids)", Wrong) - ,("map auto ids", ok "[forall a. a -> a]") - ,("map auto (map auto ids)", ok "[forall a. a -> a]") - ,("head ids", ok "forall a. a -> a") - ,("tail ids", ok "[forall a. a -> a]") - ,("apply tail ids", ok "[forall a. a -> a]") - ,("map head (single ids)", ok "[forall a. a -> a]") - ,("apply (map head) (single ids)", ok "[forall a. a -> a]") - - -- check infinite poly types - ,("(undefined :: some a. [a -> a] -> Int) (undefined :: some c. [(forall d. d -> c) -> c])", Wrong) - ,("(undefined :: some a. [a -> a] -> Int) (undefined :: [(forall d. d -> d) -> (Int -> Int)])", Wrong) - ,("(undefined :: some a. [a -> (forall b. b -> b)] -> Int) (undefined :: some c. [(forall d. d -> d) -> c])", ok "Int") - - -- these fail horribly in ghc: (choose auto id) is rejected while ((choose auto) id) is accepted -- so much for parenthesis :-) - ,("choose id auto", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("choose auto id", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("choose xauto xauto", ok "forall a. (forall b. b -> b) -> a -> a") - ,("choose id xauto", Wrong) - ,("choose xauto id", Wrong) - - -- these fail too in ghc: (choose ids []) is accepted while (choose [] ids) is rejected - ,("choose [] ids", ok "[forall a. a -> a]") - ,("choose ids []", ok "[forall a. a -> a]") - - -- check escaping skolems - ,("\\x -> auto x", Wrong) -- escape in match - ,("let poly (xs :: [forall a. a -> a]) = 1 in (\\x -> poly x)", Wrong) -- escape in apply - ,("\\x -> (x :: [forall a. a -> a])", Wrong) -- escape in apply - ,("\\x -> let polys (xs :: [forall a . a -> a]) = 1; f y = x in polys [f::some a. forall b. b -> a]",Wrong) -- escape in unify (with rigid annotations, otherwise we get a skolem mismatch) - ,("ids :: forall b. [forall a. a -> b]", Wrong) -- unify different skolems - - -- co/contra variance - ,("let g (x::(forall a. a -> a) -> Int) = x id; f (x :: Int -> Int) = x 1 in g f", Wrong) -- HMF is invariant - ,("let g (x::(forall a. a -> a) -> Int) = x id; f (x :: Int -> Int) = x 1 in g (\\(x :: forall a. a -> a) -> f x)", ok "Int") -- but we can always use explicit annotations to type such examples - - -- shared polymorphism - ,("let f (x :: [forall a.a -> a]) = x in let g (x :: [Int -> Int]) = x in let ids = [id] in (f ids, g ids)", ok "([forall a. a -> a],[Int -> Int])") - ] - -testsExists - = [-- simulating existential types - ("let pack x f = \\(open :: some b. forall a. (a,a -> Int) -> b) -> open (x,f); \ - \unpack ex f = ex f; \ - \existsB = pack True (\\b -> if b then 1 else 0); \ - \existsI = pack 1 id; \ - \exs = [existsB,existsI]\ - \in unpack (head exs) (\\ex -> (snd ex) (fst ex))" - ,ok "Int") - ] - -testsRigidAnn - = -- test 'rigid' annotations, i.e. annotations are taken literally and do not instantiate or generalize - [("single (id :: forall a. a -> a)", ok "forall (a >= forall b. b -> b). [a]") - ,("(id :: forall a. a -> a) 1", ok "Int") -- not all annotations are rigid - ,("(id :: some a. a -> a) 1", ok "Int") - ,("\\x -> ((\\y -> x) :: some a. forall b. b -> a)", ok "forall a. forall (b >= forall c. c -> a). a -> b") - ,("\\(f :: forall a. a -> a) -> ((f f) :: forall a. a -> a)", ok "forall (a >= forall b. b -> b). (forall b. b -> b) -> a") - ,("revapp (id :: forall a. a -> a) auto", ok "forall a. a -> a") - ,("choose inc id", ok "Int -> Int") - ,("choose inc (id :: forall a. a -> a)", if SupportRigidAnnotations `elem` features then Wrong else ok "Int -> Int") - ,("choose inc (id :: some a. a -> a)", ok "Int -> Int") - ] - -testsNary - = -- tests n-ary applications - [("revapp id auto", ok "forall a. a -> a") - ,("let f = revapp id in f auto", ok "forall a. a -> a") - ,("let f = revapp (id :: forall a. a -> a) in f auto", ok "forall a. a -> a") - -- check functions that return polymorphic values - ,("head ids 1", ok "Int") - ,("auto id 1", ok "Int") - ] - -testsFlexible - = -- test sharing of polymorphic types - [("let ids = single id in (map auto ids, append (single inc) ids)", ok "([forall a. a -> a],[Int -> Int])") - ,("single id",ok "forall (a >= forall b. b -> b). [a]") - ,("choose id",ok "forall (a >= forall b. b -> b). a -> a") - ,("choose id inc", ok "Int -> Int") - ,("choose id auto", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("\\x y -> x", ok "forall a. forall (b >= forall c. c -> a). a -> b") - ] - -testsRigid - = [-- Experimental: the "rigid" keyword prevents instantiation or generalization of the principal type of an expression - -- this is perhaps more convenient than writing an annotation (but not more expressive) - ("single (rigid id)", ok "[forall a. a -> a]") - ,("let pauto (f :: forall a. a -> a) = rigid f in map pauto ids", ok "[forall a. a -> a]") - ,("let pauto (f :: forall a. a -> a) = rigid f in map pauto (map pauto ids)", ok "[forall a. a -> a]") - ,("\\x -> rigid (\\y -> x)", ok "forall a. a -> (forall b. b -> a)") - ,("\\x -> rigid (\\y -> const x y)", ok "forall a. a -> (forall b. b -> a)") - ,("let c x = rigid (\\y -> x) in \\x y -> c x y", ok "forall a b. a -> b -> a") - ,("choose plus (\\x -> id)", ok "Int -> Int -> Int") - ,("choose plus (\\x -> rigid id)", Wrong) - ,("choose inc (rigid id)", Wrong) - ,("choose id", ok "forall a. (a -> a) -> (a -> a)") - ,("choose (rigid id)", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("revapp (rigid id) auto", ok "forall a. a -> a") - -- manipulate instantiation of each quantifier: - ,("[const]", ok "forall a b. [a -> b -> a]") - ,("[rigid const]", ok "[forall a b. a -> b -> a]") - ,("[const :: some a. forall b. a -> b -> a]", ok "forall a. [forall b. a -> b -> a]") - ,("[const :: some b. forall a. a -> b -> a]", ok "forall b. [forall a. a -> b -> a]") - ] - --- Type propagation tests -testsProp - = [ -- test type propagation (SupportPropagation `elem` features) - ("(\\f -> f f) :: (forall a. a -> a) -> (forall a. a -> a)", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("(let x = 1 in (\\f -> (f x, f True))) :: (forall a. a -> a) -> (Int,Bool)", ok "(forall a. a -> a) -> (Int,Bool)") - ] - ++ - [-- test type propagation through applications (SupportAppPropagation `elem` features) - ("single id :: [forall a. a -> a]", ok "[forall a. a -> a]") - ,("returnST 1 :: forall s. ST s Int", ok "forall s. ST s Int") - ,("auto id :: Int -> Int", ok "Int -> Int") - ,("head ids 1 :: Int", ok "Int") - ,("head ids :: Int -> Int", ok "Int -> Int") - ] - -testsPropArg - = [-- test type propagation to arguments (SupportPropagateToArg `elem` features) - ("takeAuto (\\f -> f f)", ok "forall a. a -> a") - ,("[id]: [ids]", ok "[[forall a. a -> a]]") - ,("([id] :: [forall a. a -> a]) : [[\\x -> x]]", ok "[[forall a. a -> a]]") - ,("apply takeAuto (\\f -> f f)", ok "forall a. a -> a") - ,("revapp (\\f -> f f) takeAuto", ok "forall a. a -> a") - ,("apply (\\f -> choose auto f) (auto :: (forall a. a -> a) -> (forall a. a -> a))", ok "(forall a. a -> a) -> (forall a. a -> a)") - ,("revapp (auto :: (forall a. a -> a) -> (forall a. a -> a)) (\\f -> choose auto f)", ok "(forall a. a -> a) -> (forall a. a -> a)") - ] - --- this is *not* supported by HML: inference of polymorphic types for arguments that are just passed around.. -testsEtaPoly - = -- in MLF arguments can have an inferred polymorphic type as long as it is not used (or revealed explicitly) - [("\\x -> auto x", ok "forall a. (forall a. a -> a) -> a -> a") - ,("\\x -> (auto x, x 1)", Wrong) - ,("\\x -> (auto x, (x :: forall a. a -> a) 1)", ok "forall a. (forall a. a -> a) -> (a -> a, Int)") - ,("\\x -> (auto x, (x :: Int -> Int) 1)", Wrong) - ] - --------------------------------------------------------------------------- --- Test framework --------------------------------------------------------------------------- -type Test = (String,TestResult) -data TestResult = Ok Type - | Wrong - -ok :: String -> TestResult -ok stringType - = Ok (readType stringType) - - -test :: [Test] -> IO () -test ts - = do xs <- mapM test1 ts - putStrLn ("\ntested: " ++ show (length ts)) - putStrLn ("failed: " ++ show (sum xs) ++ "\n") - -test1 :: Test -> IO Int -test1 (input,Ok resultTp) - = do tp <- inference input - if (show tp == show resultTp) - then testOk "" - else testFailed (": test was expected to have type: " ++ show resultTp) - `Exn.catch` \err -> - do putStrLn (show err) - testFailed (": test should be accepted with type: " ++ show resultTp) - -test1 (input, Wrong) - = do inference input - testFailed ": a type error was expected" - `Exn.catch` \err -> - do putStrLn (show err) - testOk " (the input was justly rejected)" - -testFailed msg - = do putStrLn (header ++ "\ntest failed" ++ msg ++ "\n" ++ header ++ "\n") - return 1 - where - header = replicate 40 '*' - -testOk msg - = do putStrLn ("ok " ++ msg) - putStrLn "" - return 0 - --------------------------------------------------------------------------- --- Help ----------------------------------------------------------------------------- - -help - = putStrLn $ unlines - [ "Usage:" - , " check \"\\\\x -> x\" : type check an expression" - , " testAll : run all tests" - , " test testsHM : run the Hindley-Milner tests" - , " test testsHR : run the Higer-rank tests" - , " test testsRigidAnn : run the rigid annotations tests" - , " test testsExists : run the existential types tests" - , " test testsPoly : run the 'poly' keyword tests" - ] - - - - - - - - - - - - -main :: IO () -main = return () diff --git a/previous-approaches/hml/app/Operations.hs b/previous-approaches/hml/app/Operations.hs deleted file mode 100644 index 0fe8140b..00000000 --- a/previous-approaches/hml/app/Operations.hs +++ /dev/null @@ -1,554 +0,0 @@ --------------------------------------------------------------------------- --- Common operations on types --------------------------------------------------------------------------- -module Operations( - -- * Generalization, skolemization and instantiation - generalize - , skolemize - , instantiate - , instantiateAnnot - , quantify - , xgeneralize - , normalize, constructedForm - - -- * Creat fresh type variables - , freshSkolems, freshInstanceVar - , uniqueReset - - -- * Inference - , Infer, runInfer - , HasTypeVar - , freeTvs, freeSkolems, (|->), subst - - -- * Helpers - , message - , check, failure - , onlyIf - , isTau, isFlexTau, isScheme, isUniVar, ground - - , readRef, writeRef, newRef - , withRankInf, withRankIncrease, getRank - ) where - -import Debug.Trace( trace ) -import Data.IORef( IORef, newIORef, modifyIORef, readIORef, writeIORef ) -import System.IO.Unsafe( unsafePerformIO ) -import Data.List( sort ) -import PPrint -import Types -import Subst -import Gamma - - --------------------------------------------------------------------------- --- Generalize --- Uses efficient generalization by lambda-ranking unifiable variables. See: --- See: George Kuan and David McQueen, "Efficient ML type inference with ranked type variables" --------------------------------------------------------------------------- -generalize :: Gamma -> Infer Type -> Infer Type -generalize gamma inf - = do tp <- withRankInf inf - tvsTp <- freeTvs tp - (gtp,gtvs) <- xgeneralize tp - -- message $ "generalize over: " ++ show tp ++ ": " ++ show tvs - assertGen tvsTp gtvs -- assert that we generalize correctly - normalize gtp - where - assertGen tvsTp tvs - = do -- assert that we generalize correctly - tvsG <- freeTvs (gammaCoDomain gamma) - let tvsX = (tvsTp `diff` tvsG) - if (sort tvs /= sort tvsX) - then message ("warning: different generalization:\n tvs: " ++ show (sort tvs) ++ "\ntvsX: " ++ show (show tvsX)) - else return () - --- | "quantify" is used when type schemes are unified -quantify :: Type -> Infer Type -quantify tp - = do (gtp,_) <- xgeneralize tp - return gtp - -xgeneralize :: Type -> Infer (Type,[TypeVar]) -xgeneralize tp - = do tvsTp <- freeTvs tp - depth <- getRank - tvs <- genTvs depth tvsTp - qs <- freshQuantifiers tvs - stp <- subQuantifiers qs tvs tp - -- gtp <- mkForallQ qs stp - return (mkForallQ qs stp,tvs) - where - genTvs depth [] - = return [] - genTvs depth (tv@(TypeVar _ (Uni ref)):tvs) - = do bound <- readRef ref - case bound of - Instance tp rank | rank > depth - -> do tvsTp <- freeTvs tp - gtvs <- genTvs depth (tvsTp `union` tvs) - return ([tv] `union` gtvs) - _ -> genTvs depth tvs - -subQuantifiers qs tvs tp - = -- subNew (tvIds tvs) (map (\q -> TVar (TypeVar (quantId q) Quantified)) qs) |-> tp - do mapM_ (\(quant,TypeVar _ (Uni ref)) -> writeRef ref (Equal (TVar (TypeVar (quantId quant) Quantified)))) - (zip qs tvs) - subst tp - -filterM pred [] - = return [] -filterM pred (x : xs) - = do keep <- pred x - xs' <- filterM pred xs - if keep then return (x:xs') else return xs' - - --------------------------------------------------------------------------- --- Instantiation --------------------------------------------------------------------------- - --- | Instantiate a type -instantiate :: Type -> Infer Rho -instantiate tp - = do t <- ground tp - case t of - Forall q tp - -> do tv <- freshTVar q - stp <- subNew [quantId q] [tv] |-> tp - -- message $ "instantiate: " ++ show tp ++ ": " ++ show stp - instantiate stp - rho -> return rho - --- | Instantiate the the "some" quantifiers of an annotation to fresh type variables -instantiateAnnot :: Annot -> Infer ([Type],Type) -instantiateAnnot (Annot [] tp) - = do ntp <- normalize tp - return ([],ntp) -instantiateAnnot (Annot qs tp) - = do tvs <- freshTVars qs - stp <- subNew (quantIds qs) tvs |-> tp - ntp <- normalize stp - return (tvs,ntp) - - --------------------------------------------------------------------------- --- Skolemization --------------------------------------------------------------------------- --- | Skolemize a quantified type and return the newly introduced skolem variables -skolemize :: Type -> Infer ([TypeVar],Rho) -skolemize tp - = do t <- ground tp - case splitQuants t of - (qs,rho) | not (null qs) - -> do sks <- freshSkolems (length qs) - srho <- subNew (quantIds qs) (map TVar sks) |-> rho - -- message ("skolemize: " ++ show tp ++ " to " ++ show srho) - return (sks, srho) - _ -> return ([],tp) - - ---------------------------------------------------------------------------- --- constructed form ---------------------------------------------------------------------------- -constructedForm tp - = case tp of - Forall (Quant id bound) rho - -> do eq <- checkTVar id rho - if eq then constructedForm rho - else return tp - _ -> return tp - where - checkTVar id rho - = case rho of - TVar (TypeVar id2 (Uni ref)) - -> do bound <- readRef ref - case bound of - Equal t -> checkTVar id t - _ -> return False - TVar (TypeVar id2 Quantified) | id == id2 - -> return True - _ -> return False - - --------------------------------------------------------------------------- --- normalization --------------------------------------------------------------------------- -normalize :: Type -> Infer Type -normalize tp - = do stp <- subst tp -- apply all substitutions - (tvs,ntp) <- normalizeSchemeFtv stp - return ntp - -normalizeSchemeFtv :: Type -> Infer ([TypeVar],Type) -normalizeSchemeFtv tp - = case tp of - Forall (Quant id bound) rho - -> do (tvs,nrho) <- normalizeSchemeFtv rho - if (not (tvFromId id `elem` tvs)) - then return (tvs,nrho) - else do (btvs,nbound) <- normalizeSchemeFtv bound - case nrho of - (TVar (TypeVar id2 Quantified)) | id == id2 - -> return (btvs,nbound) - _ -> do tp <- if (isRho nbound) - then (subNew [id] [nbound]) |-> nrho - else return (Forall (Quant id nbound) nrho) - return (btvs `union` (remove (tvFromId id) tvs), tp) - _ -> do tvs <- ftv tp - return (tvs,tp) - - -isRho :: Type -> Bool -isRho tp - = case tp of - Forall _ _ -> False - Bottom -> False - _ -> True - --------------------------------------------------------------------------- --- Free type variables --------------------------------------------------------------------------- -freeSkolems :: HasTypeVar a => a -> Infer [TypeVar] -freeSkolems tp - = do tvs <- ftv tp - return [tv | tv <- tvs, isSkolem (tvFlavour tv)] - - --- | return the free unifiable variables of a type -freeTvs :: HasTypeVar a => a -> Infer [TypeVar] -freeTvs tp - = do tvs <- ftv tp - return [tv | tv <- tvs, isUni (tvFlavour tv)] - - --------------------------------------------------------------------------- --- Type variables --------------------------------------------------------------------------- - --- | Things that have type variables -class HasTypeVar a where - -- | Return the free type variables - ftv :: a -> Infer [TypeVar] - - -- | Apply a substitution - (|->) :: Sub -> a -> Infer a - - -- | substitute the free reference type variables - subst :: a -> Infer a - - - -instance HasTypeVar a => HasTypeVar [a] where - ftv xs - = do tvss <- mapM ftv xs - return (foldl union [] tvss) - - sub |-> xs - = mapM (sub |->) xs - - subst xs - = mapM subst xs - -instance HasTypeVar Type where - ftv tp - = case tp of - Forall (Quant id bound) rho - -> do tvs <- ftv rho - if (tvFromId id `elem` tvs) - then do btvs <- ftv bound - return (btvs `union` (remove (tvFromId id) tvs)) - else return tvs - TApp t1 t2 -> do tvs1 <- ftv t1 - tvs2 <- ftv t2 - return (tvs1 `union` tvs2) - TVar tv -> case tv of - TypeVar id (Uni ref) - -> do bound <- readRef ref - case bound of - Instance _ _ -> return [tv] - Equal t -> ftv t - _ -> return [tv] - TCon _ -> return [] - Bottom -> return [] - - - sub |-> tp - = case tp of - Forall (Quant id bound) rho - -> do srho <- (subRemove sub [id]) |-> rho - sbnd <- sub |-> bound - return (Forall (Quant id sbnd) srho) - TApp t1 t2 -> do st1 <- sub |-> t1 - st2 <- sub |-> t2 - return (TApp st1 st2) - TCon name -> return tp - TVar tv -> case tv of - TypeVar id (Uni ref) - -> do bound <- readRef ref - case bound of - Equal t -> sub |-> t - Instance _ _ -> case subLookup sub tv of - Just newtp -> return newtp - Nothing -> return tp - _ -> case subLookup sub tv of -- replace even bound ones, useful for instantiation - Just newtp -> return newtp - Nothing -> return tp - Bottom -> return tp - - subst tp - = case tp of - Forall (Quant id bound) rho - -> do srho <- subst rho - sbnd <- subst bound - return (Forall (Quant id sbnd) srho) - TApp tp1 tp2 -> do stp1 <- subst tp1 - stp2 <- subst tp2 - return (TApp stp1 stp2) - TVar (TypeVar _ (Uni ref)) - -> do bound <- readRef ref - case bound of - Equal t -> do ft <- subst t - writeRef ref (Equal ft) - return ft - Instance _ _ -> return tp - _ -> return tp - - -instance HasTypeVar Bound where - ftv bound - = case bound of - Equal tp -> error "Operations.ftv: equality quantifier?" - Instance tp _ -> ftv tp - - sub |-> bound - = case bound of - Equal tp -> error "Operations.|->: equality quantifier?" - Instance tp r -> do stp <- sub |-> tp - return (Instance stp r) - - subst bound - = case bound of - Instance tp r -> do stp <- subst tp - return (Instance stp r) - Equal tp -> error "Operations.subst: equality quantifier?" - - - --------------------------------------------------------------------------- --- Helpers --------------------------------------------------------------------------- -check :: Bool -> String -> Infer () -check pred msg - = if pred then return () - else failure msg - -failure :: String -> a -failure msg - = error ("error: " ++ msg) - -onlyIf :: Bool -> Infer () -> Infer () -onlyIf pred inf - = if pred then inf else return () - --------------------------------------------------------------------------- --- Fresh type variables --------------------------------------------------------------------------- --- | return fresh skolem variables -freshSkolems :: Int -> Infer [TypeVar] -freshSkolems - = freshTypeVars Skolem - --- | return fresh bound variables -freshQuantifiers :: [TypeVar] -> Infer [Quant] -freshQuantifiers tvs - = mapM freshQuantifier tvs - -freshQuantifier (TypeVar _ (Uni ref)) - = do bound <- readRef ref - id <- freshId - case bound of - Equal tp -> error "Operations.freshQuantifier: do subst?" - Instance tp rank -> return (Quant id tp) - --- | return fresh unifiable types -freshTVars :: [Quant] -> Infer [Type] -freshTVars qs - = mapM freshTVar qs - --- | return a fresh unifiable type -freshTVar :: Quant -> Infer Type -freshTVar (Quant id tp) - = freshInstanceVar tp - - -freshInstanceVar :: Type -> Infer Type -freshInstanceVar tp - = do rank <- getRank -- instantiate under the current rank - scheme <- isScheme tp - ref <- newRef (if scheme then Instance tp rank else Equal tp) - tv <- freshTypeVar (Uni ref) - return (TVar tv) - - --- | return fresh type variables of a certain |Flavour| -freshTypeVars :: Flavour -> Int -> Infer [TypeVar] -freshTypeVars fl n - = mapM (\_ -> freshTypeVar fl) [1..n] - --- | return a fresh type variable -freshTypeVar :: Flavour -> Infer TypeVar -freshTypeVar fl - = do id <- freshId - return (TypeVar id fl) - --- | return a fresh identifier -freshId :: Infer Id -freshId - = do id <- unique - return id - - --------------------------------------------------------------------------- --- --------------------------------------------------------------------------- - --- | Is this a monotype? -isTau tp - = case tp of - Forall _ _ -> return False - TApp t1 t2 -> do b1 <- isTau t1 - b2 <- isTau t2 - return (b1 && b2) - TVar (TypeVar _ (Uni ref)) - -> do bound <- readRef ref - case bound of - Equal t -> isTau t - Instance Bottom _ -> return True - Instance _ _ -> return False - Bottom -> return False - TCon _ -> return True - - --- | Is this a monotype with flexible bounds only? -isFlexTau tp - = case tp of - Forall _ _ -> return False - TApp t1 t2 -> do b1 <- isFlexTau t1 - b2 <- isFlexTau t2 - return (b1 && b2) - TVar (TypeVar _ (Uni ref)) - -> do bound <- readRef ref - case bound of - Equal t -> isFlexTau t - -- Instance Bottom _ -> return True - Instance _ _ -> return True - Bottom -> return False - TCon _ -> return True - --- | Is this a type scheme? -isScheme tp - = case tp of - Forall q rho -> return True - TVar (TypeVar _ (Uni ref)) - -> do bound <- readRef ref - case bound of - Equal t -> isScheme t - Instance _ _ -> return False - Bottom -> return True - _ -> return False - -ground :: Type -> Infer Type -ground tp@(TVar (TypeVar _ (Uni ref))) - = do bound <- readRef ref - case bound of - Equal t -> ground t - Instance _ _ -> return tp -ground tp - = return tp - - -isUniVar :: Type -> Infer Bool -isUniVar tp - = do t <- ground tp - case t of - TVar (TypeVar _ (Uni _)) - -> return True - _ -> return False - --------------------------------------------------------------------------- --- Infer --------------------------------------------------------------------------- --- | The type inference monad, just IO for convenience -newtype Infer a = Infer (Env -> IO a) - -type Env = Rank - -runInfer :: Infer a -> IO a -runInfer (Infer inf) - = inf 0 - -instance Functor Infer where - fmap f (Infer inf) = Infer (\env -> fmap f (inf env)) - -instance Monad Infer where - return x = Infer (\env -> return x) - (Infer inf) >>= f = Infer (\env -> do x <- inf env - case f x of - Infer inf2 -> inf2 env) - -message :: String -> Infer () -message msg - = liftIO $ putStrLn msg - - --- Ranks -withRank :: Rank -> Infer a -> Infer a -withRank r (Infer inf) - = Infer (\rank -> inf r) - -getRank :: Infer Rank -getRank - = Infer (\rank -> return rank) - -withRankIncrease :: Infer a -> Infer a -withRankIncrease inf - = do r <- getRank - withRank (r+1) inf - -withRankInf :: Infer a -> Infer a -withRankInf inf - = withRank rankInf inf - --- Refs -liftIO :: IO a -> Infer a -liftIO io - = Infer (\env -> io) - -readRef :: IORef a -> Infer a -readRef ref - = liftIO (readIORef ref) - -writeRef :: IORef a -> a -> Infer () -writeRef ref x - = liftIO (writeIORef ref x) - -newRef :: a -> Infer (IORef a) -newRef x - = liftIO (newIORef x) - - -{-# NOINLINE uniqueInt #-} -uniqueInt :: IORef Int -uniqueInt = unsafePerformIO (newIORef 0) - --- | Quick and dirty unique numbers :-) -unique :: Infer Int -unique = do u <- readRef uniqueInt - writeRef uniqueInt (u+1) - return u - -uniqueReset :: Infer () -uniqueReset - = writeRef uniqueInt 0 - - diff --git a/previous-approaches/hml/app/PPrint.hs b/previous-approaches/hml/app/PPrint.hs deleted file mode 100644 index c81260e7..00000000 --- a/previous-approaches/hml/app/PPrint.hs +++ /dev/null @@ -1,475 +0,0 @@ ------------------------------------------------------------------------------ -{- Copyright (C) 2004 Daan Leijen. - - This is free software; you can redistribute it and/or modify it under the - terms described in the file "license.txt" at the root of the distribution. --} ------------------------------------------------------------------------------ -{- | - Maintainer : daan@equational.org - Stability : provisional - Portability : haskell98 - - Pretty print module based on Philip Wadlers /prettier printer/ - - * Philip Wadler, /A prettier printer/ Draft paper, - April 1997, revised March 1998. - --} ------------------------------------------------------------------------------ -module PPrint - ( Doc, Docs - , Pretty(pretty,prettyList), putPretty - - , show, putDoc, hPutDoc - - , (<>) - , (<+>) - , (), () - , (<$>), (<$$>) - - , sep, fillSep, hsep, vsep - , cat, fillCat, hcat, vcat - , punctuate - - , align, hang, indent - , fill, fillBreak - - , list, tupled, semiBraces, encloseSep - , angles, langle, rangle - , parens, lparen, rparen - , braces, lbrace, rbrace - , brackets, lbracket, rbracket - , dquotes, dquote, squotes, squote - - , comma, space, dot, backslash - , semi, colon, equals - - , string, bool, int, integer, float, double, rational - - , softline, softbreak - , empty, char, text, line, linebreak, nest, group - , column, nesting, width - - , SimpleDoc(..) - , renderPretty, renderCompact - , displayS, displayIO - -- * Colors - , Color(..) - , color, bcolor - , writeDoc - ) where - -import IO -- (Handle,hPutStr,hPutChar,stdout,openFile,hClose) - - -infixr 5 ,,<$>,<$$> -infixr 6 <>,<+> - - ------------------------------------------------------------ --- list, tupled and semiBraces pretty print a list of --- documents either horizontally or vertically aligned. ------------------------------------------------------------ -list = encloseSep lbracket rbracket comma -tupled = encloseSep lparen rparen comma -semiBraces = encloseSep lbrace rbrace semi - -encloseSep left right sep ds - = case ds of - [] -> left <> right - [d] -> left <> d <> right - _ -> align (cat (zipWith (<>) (left : repeat sep) ds) <> right) - - ------------------------------------------------------------ --- punctuate p [d1,d2,...,dn] => [d1 <> p,d2 <> p, ... ,dn] ------------------------------------------------------------ -punctuate p [] = [] -punctuate p [d] = [d] -punctuate p (d:ds) = (d <> p) : punctuate p ds - - ------------------------------------------------------------ --- high-level combinators ------------------------------------------------------------ -sep = group . vsep -fillSep = fold () -hsep = fold (<+>) -vsep = fold (<$>) - -cat = group . vcat -fillCat = fold () -hcat = fold (<>) -vcat = fold (<$$>) - -fold f [] = empty -fold f ds = foldr1 f ds - -x <> y = x `beside` y -x <+> y = x <> space <> y -x y = x <> softline <> y -x y = x <> softbreak <> y -x <$> y = x <> line <> y -x <$$> y = x <> linebreak <> y - -softline = group line -softbreak = group linebreak - -squotes = enclose squote squote -dquotes = enclose dquote dquote -braces = enclose lbrace rbrace -parens = enclose lparen rparen -angles = enclose langle rangle -brackets = enclose lbracket rbracket -enclose l r x = l <> x <> r - -lparen = char '(' -rparen = char ')' -langle = char '<' -rangle = char '>' -lbrace = char '{' -rbrace = char '}' -lbracket = char '[' -rbracket = char ']' - -squote = char '\'' -dquote = char '"' -semi = char ';' -colon = char ':' -comma = char ',' -space = char ' ' -dot = char '.' -backslash = char '\\' -equals = char '=' - - ------------------------------------------------------------ --- Combinators for prelude types ------------------------------------------------------------ - --- string is like "text" but replaces '\n' by "line" -string "" = empty -string ('\n':s) = line <> string s -string s = case (span (/='\n') s) of - (xs,ys) -> text xs <> string ys - -bool :: Bool -> Doc -bool b = text (show b) - -int :: Int -> Doc -int i = text (show i) - -integer :: Integer -> Doc -integer i = text (show i) - -float :: Float -> Doc -float f = text (show f) - -double :: Double -> Doc -double d = text (show d) - -rational :: Rational -> Doc -rational r = text (show r) - - ------------------------------------------------------------ --- overloading "pretty" ------------------------------------------------------------ -putPretty :: Pretty a => a -> IO () -putPretty p - = putDoc (pretty p) - -class Pretty a where - pretty :: a -> Doc - prettyList :: [a] -> Doc - prettyList = list . map pretty - -instance Pretty a => Pretty [a] where - pretty = prettyList - -instance Pretty Doc where - pretty = id - -instance Pretty () where - pretty () = text "()" - -instance Pretty Bool where - pretty b = bool b - -instance Pretty Char where - pretty c = char c - prettyList s = string s - -instance Pretty Int where - pretty i = int i - -instance Pretty Integer where - pretty i = integer i - -instance Pretty Float where - pretty f = float f - -instance Pretty Double where - pretty d = double d - - ---instance Pretty Rational where --- pretty r = rational r - -instance (Pretty a,Pretty b) => Pretty (a,b) where - pretty (x,y) = tupled [pretty x, pretty y] - -instance (Pretty a,Pretty b,Pretty c) => Pretty (a,b,c) where - pretty (x,y,z)= tupled [pretty x, pretty y, pretty z] - -instance Pretty a => Pretty (Maybe a) where - pretty Nothing = empty - pretty (Just x) = pretty x - - - ------------------------------------------------------------ --- semi primitive: fill and fillBreak ------------------------------------------------------------ -fillBreak f x = width x (\w -> - if (w > f) then nest f linebreak - else text (spaces (f - w))) - -fill f d = width d (\w -> - if (w >= f) then empty - else text (spaces (f - w))) - -width d f = column (\k1 -> d <> column (\k2 -> f (k2 - k1))) - - ------------------------------------------------------------ --- semi primitive: Alignment and indentation ------------------------------------------------------------ -indent i d = hang i (text (spaces i) <> d) - -hang i d = align (nest i d) - -align d = column (\k -> - nesting (\i -> nest (k - i) d)) --nesting might be negative :-) - - - ------------------------------------------------------------ --- Primitives ------------------------------------------------------------ -type Docs = [Doc] - -data Doc = Empty - | Char Char -- invariant: char is not '\n' - | Text !Int String -- invariant: text doesn't contain '\n' - | Line !Bool -- True <=> when undone by group, do not insert a space - | Cat Doc Doc - | Nest !Int Doc - | Union Doc Doc -- invariant: first lines of first doc longer than the first lines of the second doc - | Column (Int -> Doc) - | Nesting (Int -> Doc) - | Colored Bool Color Doc - | ColoredEnd - -data SimpleDoc = SEmpty - | SChar !Int Char SimpleDoc - | SText !Int !Int String SimpleDoc - | SLine !Int SimpleDoc - | SColorOpen Bool Color SimpleDoc - | SColorClose SimpleDoc - - -empty = Empty - -char '\n' = line -char c = Char c - -text "" = Empty -text s = Text (length s) s - -line = Line False -linebreak = Line True - -beside x y = Cat x y -nest i x = Nest i x -column f = Column f -nesting f = Nesting f -group x = Union (flatten x) x - -color c doc = Colored True c doc -bcolor c doc = Colored False c doc - - -flatten :: Doc -> Doc -flatten (Cat x y) = Cat (flatten x) (flatten y) -flatten (Nest i x) = Nest i (flatten x) -flatten (Line break) = if break then Empty else Text 1 " " -flatten (Union x y) = flatten x -flatten (Column f) = Column (flatten . f) -flatten (Nesting f) = Nesting (flatten . f) -flatten (Colored f c d) = Colored f c (flatten d) -flatten other = other --Empty,Char,Text - - - ------------------------------------------------------------ --- Renderers ------------------------------------------------------------ - ------------------------------------------------------------ --- renderPretty: the default pretty printing algorithm ------------------------------------------------------------ - --- list of indentation/document pairs; saves an indirection over [(Int,Doc)] -data DocList = Nil - | Cons !Int Doc DocList - -renderPretty :: Float -> Int -> Doc -> SimpleDoc -renderPretty rfrac w x - = best 0 0 0 (Cons 0 x Nil) - where - -- r :: the ribbon width in characters - r = max 0 (min w (round (fromIntegral w * rfrac))) - - -- best :: b = base nesting - -- n = indentation of current line - -- k = current column - -- (ie. (k >= n) && (k - n == count of inserted characters) - best b n k Nil = SEmpty - best b n k (Cons i d ds) - = case d of - Empty -> best b n k ds - Char c -> let k' = k+1 in seq k' (SChar b c (best b n k' ds)) - Text l s -> let k' = k+l in seq k' (SText b l s (best b n k' ds)) - Line _ -> SLine i (best b i i ds) - Cat x y -> best b n k (Cons i x (Cons i y ds)) - Nest j x -> let i' = i+j in seq i' (best (if b==0 then i' else b) n k (Cons i' x ds)) - Union x y -> nicest n k (best b n k (Cons i x ds)) - (best b n k (Cons i y ds)) - - Column f -> best b n k (Cons i (f k) ds) - Nesting f -> best b n k (Cons i (f i) ds) - Colored f c x -> SColorOpen f c (best b n k (Cons i x (Cons i ColoredEnd ds))) - ColoredEnd -> SColorClose (best b n k ds) - - --nicest :: r = ribbon width, w = page width, - -- n = indentation of current line, k = current column - -- x and y, the (simple) documents to chose from. - -- precondition: first lines of x are longer than the first lines of y. - nicest n k x y | fits width x = x - | otherwise = y - where - width = min (w - k) (r - k + n) - - -fits w x | w < 0 = False -fits w SEmpty = True -fits w (SChar i c x) = fits (w - 1) x -fits w (SText i l s x) = fits (w - l) x -fits w (SLine i x) = True -fits w (SColorOpen f c x) = fits w x -fits w (SColorClose x) = fits w x - ------------------------------------------------------------ --- renderCompact: renders documents without indentation --- fast and fewer characters output, good for machines ------------------------------------------------------------ -renderCompact :: Doc -> SimpleDoc -renderCompact x - = scan 0 [x] - where - scan k [] = SEmpty - scan k (d:ds) = case d of - Empty -> scan k ds - Char c -> let k' = k+1 in seq k' (SChar 0 c (scan k' ds)) - Text l s -> let k' = k+l in seq k' (SText 0 l s (scan k' ds)) - Line _ -> SLine 0 (scan 0 ds) - Cat x y -> scan k (x:y:ds) - Nest j x -> scan k (x:ds) - Union x y -> scan k (y:ds) - Column f -> scan k (f k:ds) - Nesting f -> scan k (f 0:ds) - Colored f c x-> SColorOpen f c (scan k (x : ColoredEnd : ds)) - ColoredEnd -> SColorClose (scan k ds) - ------------------------------------------------------------ --- Displayers: displayS and displayIO ------------------------------------------------------------ -displayS :: SimpleDoc -> ShowS -displayS SEmpty = id -displayS (SChar i c x) = showChar c . displayS x -displayS (SText i l s x) = showString s . displayS x -displayS (SLine i x) = showString ('\n':indentation i) . displayS x -displayS (SColorOpen f c x) = displayS x -displayS (SColorClose x) = displayS x - -displayIO :: Handle -> SimpleDoc -> IO () -displayIO handle simpleDoc - = display simpleDoc - where - display SEmpty = return () - display (SChar i c x) = do{ hPutChar handle c; display x} - display (SText i l s x) = do{ hPutStr handle s; display x} - display (SLine i x) = do{ hPutStr handle ('\n':indentation i); display x} - display (SColorOpen f c x)= display x - display (SColorClose x) = display x - - -{-------------------------------------------------------------------------- - Interface ---------------------------------------------------------------------------} --- | Available colors on a console. Normally, background colors are --- converted to their /dark/ variant. -data Color = Black - | DarkRed - | DarkGreen - | DarkYellow - | DarkBlue - | DarkMagenta - | DarkCyan - | Gray - | DarkGray - | Red - | Green - | Yellow - | Blue - | Magenta - | Cyan - | White - | ColorDefault - deriving (Show,Eq,Ord,Enum) - ------------------------------------------------------------ --- default pretty printers: show, putDoc and hPutDoc ------------------------------------------------------------ -instance Show Doc where - showsPrec d doc = displayS (renderPretty 0.8 80 doc) - -putDoc :: Doc -> IO () -putDoc doc = hPutDoc stdout doc - - -hPutDoc :: Handle -> Doc -> IO () -hPutDoc handle doc = displayIO handle (renderPretty 0.8 80 doc) - - -writeDoc :: FilePath -> Doc -> IO () -writeDoc fpath doc - = do h <- openFile fpath WriteMode - hPutDoc h doc - hClose h - - ------------------------------------------------------------ --- insert spaces --- "indentation" used to insert tabs but tabs seem to cause --- more trouble than they solve :-) ------------------------------------------------------------ -spaces n | n <= 0 = "" - | otherwise = replicate n ' ' - -indentation n = spaces n - ---indentation n | n >= 8 = '\t' : indentation (n-8) --- | otherwise = spaces n diff --git a/previous-approaches/hml/app/Parser.hs b/previous-approaches/hml/app/Parser.hs deleted file mode 100644 index 6e7a1e1d..00000000 --- a/previous-approaches/hml/app/Parser.hs +++ /dev/null @@ -1,323 +0,0 @@ --------------------------------------------------------------------------- --- Parse a simple functional programs --- -{- expr ::= let binder1; ..; binderN in expr -- let binding, N >= 1 - | \arg1 .. argN -> expr -- lambda expression, N >= 1 - | if expr then expr else expr - | expr :: annot - | expr1 expr2 - | id -- identifier - | integer -- integers: [-]{0-9}+ - | True -- booleans - | False - | [expr1,..,exprN] -- list (N >= 0) - | (expr1,expr2) -- tuple - | (expr) -- parenthesis - | expr1 $ expr2 -- application operator - | expr1 : expr2 -- list constructor operator - | rigid expr -- experimental rigid keyword - - binder::= id arg1 .. argN = expr -- let binding: N >= 0 - - arg ::= id -- identifier - | (id :: annot) -- annotated binder - - annot ::= some ids . type - | type - - type ::= forall ids . type -- quantification - | type -> type -- function type - | [type] -- list type - | (type,type) -- tuple type - | (type) -- parenthesis - | id -- type variable - | Con -- type constructor (Int, Bool, etc) --} --------------------------------------------------------------------------- -module Parser( readTerm, readType ) where - -import Char -import Text.ParserCombinators.Parsec -import qualified Text.ParserCombinators.Parsec.Token as P -import Text.ParserCombinators.Parsec.Language( haskellDef ) - -import Types - - --------------------------------------------------------------------------- --- To parse types, we translate bound type variables to identifiers --- using a state in the parser --------------------------------------------------------------------------- -type Parse a = CharParser St a -data St = St { uniq :: Int, idMap :: [(Name,Id)] } - - -readTerm :: String -> IO Term -readTerm input - = case runParser (wrap term) (St 0 []) "" input of - Left err -> fail (show err) - Right x -> return x - -readType :: String -> Type -readType input - = case runParser (wrap ptype) (St 0 []) "" input of - Left err -> error (show err) - Right x -> x - - - -wrap :: Parse a -> Parse a -wrap p - = do whiteSpace - x <- p - eof - return x - --------------------------------------------------------------------------- --- Parse terms --------------------------------------------------------------------------- - - - -term :: Parse Term -term - = letTerm <|> lambdaTerm <|> ifTerm <|> annotation - "term" - -letTerm - = do reserved "let" - binders <- semiSep letBinder - reserved "in" - t <- term - return (foldr ($) t binders) - -letBinder :: Parse (Term -> Term) -letBinder - = do x <- identifier - args <- many lambdaBinder - reservedOp "=" - t <- term - return (Let x (foldr ($) t args)) - -lambdaTerm - = do reservedOp "\\" - bs <- many1 lambdaBinder - reservedOp "->" - t <- term - return (foldr ($) t bs) - -lambdaBinder :: Parse (Term -> Term) -lambdaBinder - = do n <- identifier - return (Lam n) - <|> - parens (do n <- identifier - reservedOp "::" - ann <- pannot - return (ALam n ann) - ) - - -ifTerm - = do reserved "if" - t1 <- application - reserved "then" - t2 <- application - reserved "else" - t3 <- application - return (App (App (App (Var "if") t1) t2) t3) - - - -annotation :: Parse Term -annotation - = do t <- longapply - (do reservedOp "::" - ann <- pannot - return (Ann t ann) - <|> - return t - ) - "annotation" - - -longapply - = do t1 <- rigidTerm - (do reservedOp "$" - t2 <- term - return (App (App (Var "$") t1) t2) - <|> - do reservedOp ":" - t2 <- term - return (App (App (Var ":") t1) t2) - <|> - return t1) - -rigidTerm - = do reserved "rigid" - t <- atom - return (Rigid t) - <|> - application - -application :: Parse Term -application - = do ts <- many1 atom - return (foldl1 App ts) - -atom :: Parse Term -atom - = do symbol "(" - t1 <- term - (do symbol "," - t2 <- term - symbol ")" - return (App (App (Var "(,)") t1) t2) - <|> - do symbol ")" - return t1 - ) - <|> - do symbol "[" - ts <- commaSep term - symbol "]" - return (foldr (\x xs -> App (App (Var ":") x) xs) (Var "[]") ts) - <|> - do x <- identifier - return (Var x) - <|> - do i <- integer - return (Lit (fromInteger i)) - "expression" - - - - --------------------------------------------------------------------------- --- Parse types --------------------------------------------------------------------------- -pannot :: Parse Annot -pannot - = do reserved "some" - names <- many1 identifier - withIds names $ \ids -> - do reservedOp "." - tp <- ptype - return (mkAnnot ids tp) - <|> - do tp <- ptype - return (mkAnnot [] tp) - - -ptype - = do ptypeEx - - -ptypeEx - = do reserved "forall" - quants <- many1 quantifier - let (names,mkQuants) = unzip quants - withIds names $ \ids -> - do reservedOp "." - tp <- ptype - let qs = zipWith (\f id -> f id) mkQuants ids - return (mkForallQ qs tp) - <|> - tpfun - "type" - -quantifier - = do name <- identifier - return (name, \id -> Quant id Bottom) - <|> - do symbol "(" - name <- identifier - symbol ">=" - tp <- ptype - symbol ")" - return (name,\id -> Quant id tp) - -tpfun - = do t1 <- tpapp - (do reservedOp "->" - t2 <- tpfun - return (mkFun t1 t2) - <|> - return t1 - ) - -tpapp - = do tps <- many1 tpatom - return (foldl1 TApp tps) - -tpatom - = do symbol "(" - tp1 <- ptype - (do symbol "," - tp2 <- ptype - symbol ")" - return (mkTuple tp1 tp2) - <|> - do symbol ")" - return tp1 - ) - <|> - do tp <- squares ptype - return (mkList tp) - <|> - do name <- identifier - if (isUpper (head name)) - then return (TCon name) - else do id <- lookupId name - return (TVar (TypeVar id Quantified)) - "simple type" - - --------------------------------------------------------------------------- --- Unique id's for type variables --------------------------------------------------------------------------- - -lookupId :: Name -> Parse Id -lookupId name - = do st <- getState - case lookup name (idMap st) of - Nothing -> fail ("unbound type variable: " ++ name) - Just id -> return id - -withIds :: [Name] -> ([Id] -> Parse a) -> Parse a -withIds names f - = do st0 <- getState - ids <- mapM createId names - x <- f ids - updateState (\st -> st{ idMap = idMap st0 }) -- restore the old idmap - return x - -createId :: Name -> Parse Id -createId name - = do st <- getState - let id = uniq st -1 - setState (st{ uniq = id, idMap = (name,id) : idMap st}) - return id - - --------------------------------------------------------------------------- --- lexer like Haskell --------------------------------------------------------------------------- - -langDef :: P.LanguageDef st -langDef = haskellDef { P.reservedNames = ["let", "in", "forall", "some", "if", "then", "else", "rigid" ], - P.reservedOpNames = ["::", "\\", ".", "->", "$", ":"] } - -lexer = P.makeTokenParser langDef -parens = P.parens lexer -squares = P.squares lexer -integer = P.integer lexer -reservedOp = P.reservedOp lexer -reserved = P.reserved lexer -identifier = P.identifier lexer -dot = P.dot lexer -whiteSpace = P.whiteSpace lexer -lexeme = P.whiteSpace lexer -symbol = P.symbol lexer -commaSep = P.commaSep lexer -semiSep = P.semiSep lexer \ No newline at end of file diff --git a/previous-approaches/hml/app/Subst.hs b/previous-approaches/hml/app/Subst.hs deleted file mode 100644 index 356ed514..00000000 --- a/previous-approaches/hml/app/Subst.hs +++ /dev/null @@ -1,52 +0,0 @@ --------------------------------------------------------------------------- --- Operations on type variables --- --- HasTypeVar, ftv, substitution (|->) --- Subititutions (Sub), Type variables (Tvs), --------------------------------------------------------------------------- - -module Subst( - -- * Substitution - Sub - , subNew, subEmpty, subIsEmpty - , subRemove, subLookup - ) where - -import Types -import qualified Data.IntMap as M - - - --------------------------------------------------------------------------- --- A substitution is an idempotent mapping from type variables to types --------------------------------------------------------------------------- - --- | A substitution from type variables to types -newtype Sub = Sub (M.IntMap Type) - -subEmpty - = Sub (M.empty) - -subIsEmpty (Sub s) - = M.null s - -subSingle :: Id -> Type -> Sub -subSingle id tp - = Sub (M.singleton id tp) - -subNew ids tps - = Sub (M.fromList (zip ids tps)) - -subLookup :: Sub -> TypeVar -> Maybe Type -subLookup (Sub s) tv - = M.lookup (tvId tv) s - -subRemove :: Sub -> [Id] -> Sub -subRemove (Sub s) ids - = Sub (foldr M.delete s ids) - - -instance Show Sub where - show (Sub s) = show s - - diff --git a/previous-approaches/hml/app/Types.hs b/previous-approaches/hml/app/Types.hs deleted file mode 100644 index b0db3ed8..00000000 --- a/previous-approaches/hml/app/Types.hs +++ /dev/null @@ -1,438 +0,0 @@ --------------------------------------------------------------------------- --- Basic definition of types and terms --------------------------------------------------------------------------- -module Types( - -- * Definitions - Name, Id - , Term(..) - , Annot(..) - , Type(..), Rho, Tau, Scheme, FType - , Bound(..), Quant(..) - - -- * Terms - , isAnnot - - -- * Type variables - , TypeVar(..), Flavour(..) - , tvId, tvIds, tvFlavour, tvFromId - , quantId, quantIds - , isUni, isQuantified, isSkolem - , Rank, rankInf - , splitQuants - - - -- * Type operations - - , mkForall, mkForallQ, mkAnnot, mkFun, mkTuple, mkList - , annotAny - , splitFun - - -- * misc - , union, disjoint, intersect, diff, subseteq, remove - , assert, assertM - - -- * Features - , Feature(..) - - ) where - -import List( partition ) -import PPrint -import Data.IORef( IORef, readIORef ) -import System.IO.Unsafe( unsafePerformIO ) --------------------------------------------------------------------------- --- Type inference features --------------------------------------------------------------------------- -data Feature = SupportRigidAnnotations -- do not instantiate or generalize type annotations - | SupportPropagation -- propagate types through lambda expressions and let-bindings - | SupportPropagateToArg -- propagate parameter types to argument expressions - deriving Eq - - --------------------------------------------------------------------------- --- Terms --------------------------------------------------------------------------- -type Name = String - -data Term = Var Name -- x - | Lit Int -- 3 - | App Term Term -- f x - | Lam Name Term -- \x -> x - | ALam Name Annot Term -- \(x::Int) -> x - | Let Name Term Term -- let x = f y in x+1 - | Ann Term Annot -- (f x) :: Int - | Rigid Term -- experimental: rigid x (do not instantiate/generalize the type of "x") - - --- | is an expression annotated? -isAnnot :: Term -> Bool -isAnnot (Rigid expr) = True -isAnnot (Ann expr ann) = True -isAnnot (Let name expr body) = isAnnot body -isAnnot _ = False - - --------------------------------------------------------------------------- --- Types --------------------------------------------------------------------------- - -type Id = Int -- Identifiers - -type Scheme = Type -- type schemes with flexible quantifiers -type FType = Type -- system-F types -type Rho = Type -- Unquantified F-type -type Tau = Type -- No ForAlls anywhere - --- | Type annotations: "some a. type". A type annotation is closed under "some" type variables -data Annot = Annot [Quant] Type - --- | Types -data Type = Forall Quant Type -- ^ "forall (a >= tp). tp" - | TVar TypeVar -- ^ "a" - | TCon Name -- ^ "Int" - | TApp Type Type -- ^ "Maybe a" - | Bottom -- ^ Most polymorphic type, i.e. "forall a. a" - - --- | A quantifier. The type gives the bound which is 'Bottom' for normal quantifiers. -data Quant = Quant Id Type - - --- | Type variables represent substitutable parts of a type, only |Free| variables can be unified -data TypeVar = TypeVar Id Flavour - --- | A type variable comes in three flavours: bound, as a skolem constant, and unifiable variables -data Flavour = Quantified - | Skolem - | Uni (IORef Bound) -- the updateable reference implements substitution - --- | The bound of unified variable. -data Bound = Equal Type -- ^ it is equal to a certain type - | Instance Scheme Rank -- ^ it can be an instance of some type - --- | The type variable rank is used for efficient generalization --- | The rank corresponds with the depth of the earliest lamda binding that refers to --- | this type variable. The depth of the outermost lambda binding in the environment is 0. --- | We use an infinite rank (rankInf) for type variables that do not occur in the environment. --- See: George Kuan and David McQueen, "Efficient ML type inference with ranked type variables" -type Rank = Int - --- | The 'infinite' rank is used for variables that do not occur in the environment. --- | When unifying schemes, variables with a rank bigger than rankInf can be created, and the rank --- | is then used to count the depth of the quantifiers. -rankInf :: Rank -rankInf = maxBound `div` 2 - --- Accessors -tvFlavour (TypeVar _ fl) = fl -tvId (TypeVar id _) = id -tvIds typeVars = map tvId typeVars - -tvFromId id = TypeVar id (error "Types.tvFromId") - -quantId (Quant id _) = id -quantBound (Quant _ bound) = bound -quantIds qs = map quantId qs - -isQuantified Quantified = True -isQuantified _ = False - -isUni (Uni _) = True -isUni _ = False - -isSkolem Skolem = True -isSkolem _ = False - -boundNone - = Instance Bottom rankInf - -splitFun :: Type -> Maybe (Type,Type) -splitFun tp - = case tp of - TApp (TApp (TCon "->") arg) res - -> Just (arg,res) - _ -> Nothing - - - - --------------------------------------------------------------------------- --- Helper functions --------------------------------------------------------------------------- - -normalize :: Type -> Type -normalize tp - = tp - -mkForall :: [Id] -> Type -> Type -mkForall ids tp - = mkForallQ (mkQuants ids) tp - -mkForallQ [] tp - = tp -mkForallQ qs1 tp - = case (splitQuants tp) of - (qs2,tp2) | not (null qs2) -> mkForallQ (qs1 ++ qs2) tp2 - ([],TVar (TypeVar id Quantified)) - -> case [qtp | Quant qid qtp <- reverse qs1, qid == id] of - (qtp:_) -> qtp - _ -> tp - _ -> foldr Forall tp qs1 - -mkQuants ids - = [Quant id Bottom | id <- ids] - -splitQuants :: Type -> ([Quant],Type) -splitQuants tp - = split [] tp - where - split qs tp - = case tp of - Forall q t -> split (q:qs) t - _ -> (reverse qs,tp) - - -mkAnnot :: [Id] -> Type -> Annot -mkAnnot ids tp - = Annot (mkQuants ids) tp - -mkFun :: Type -> Type -> Type -mkFun t1 t2 - = TApp (TApp (TCon "->") t1) t2 - -mkTuple :: Type -> Type -> Type -mkTuple t1 t2 - = TApp (TApp (TCon "(,)") t1) t2 - -mkList :: Type -> Type -mkList tp - = TApp (TCon "[]") tp - --- | the "any type" annotation: (some a. a) -annotAny :: Annot -annotAny - = let id = 0 in Annot [Quant id Bottom] (TVar (TypeVar id Quantified)) - - --------------------------------------------------------------------------- --- Order preservering set operations on lists --------------------------------------------------------------------------- -union :: Eq a => [a] -> [a] -> [a] -union xs ys - = xs ++ (ys `diff` xs) - -diff :: Eq a => [a] -> [a] -> [a] -diff xs ys - = [x | x <- xs, not (x `elem` ys)] - -intersect :: Eq a => [a] -> [a] -> [a] -intersect xs ys - = [x | x <- xs, x `elem` ys] - -disjoint :: Eq a => [a] -> [a] -> Bool -disjoint xs ys - = all (\x -> not (x `elem` ys)) xs - -subseteq :: Eq a => [a] -> [a] -> Bool -subseteq xs ys - = all (`elem` ys) xs - -remove :: Eq a => a -> [a] -> [a] -remove y xs - = [x | x <- xs, x /= y] - --------------------------------------------------------------------------- --- Assertions --------------------------------------------------------------------------- -assert :: String -> Bool -> a -> a -assert msg test x - = if test then x else error ("assertion failed: " ++ msg) - - -assertM :: Monad m => String -> Bool -> m () -assertM msg test - = assert msg test (return ()) - --------------------------------------------------------------------------- --- Equality for type variables is based solely on the identifier --------------------------------------------------------------------------- -instance Eq TypeVar where - (TypeVar id1 fl1) == (TypeVar id2 fl2) = (id1 == id2) - -instance Ord TypeVar where - compare (TypeVar id1 fl1) (TypeVar id2 fl2) = compare id1 id2 - - - --------------------------------------------------------------------------- --- Pretty printing --------------------------------------------------------------------------- - -instance Pretty Term where - pretty term = ppTerm PrecTop term - -instance Pretty Type where - pretty tp = ppTypeEx [] PrecTop tp - -instance Pretty Annot where - pretty ann = ppAnnot ann - -instance Pretty TypeVar where - pretty (TypeVar id Quantified) = text "@" <> pretty id - pretty (TypeVar id Skolem) = text "_" <> pretty id - pretty (TypeVar id (Uni _)) = text "$" <> pretty id - -instance Show Term where - show t = show (pretty t) - -instance Show Type where - show t = show (pretty t) - -instance Show TypeVar where - show t = show (pretty t) - -instance Show Annot where - show ann = show (pretty ann) - - --------------------------------------------------------------------------- --- Precedence --------------------------------------------------------------------------- -data Prec = PrecTop | PrecAnn | PrecFun | PrecOp | PrecApp | PrecAtom - deriving (Eq,Ord,Enum) - -precType :: Type -> Prec -precType tp - = case tp of - Forall _ _ -> PrecTop - TApp (TApp (TCon "->") arg) res -> PrecFun - TApp (TCon "[]") arg -> PrecAtom - TApp _ _ -> PrecApp - _ -> PrecAtom - -precTerm :: Term -> Prec -precTerm term - = case term of - App (Var "[]") _ -> PrecAtom - App (App (Var "(,)") e1) e2 -> PrecAtom - App (App (Var "$") e1) e2 -> PrecOp - App (App (Var ":") e1) e2 -> case elements [e1] e2 of - Nothing -> PrecOp - Just _ -> PrecAtom - - Let _ _ _ -> PrecTop - Ann _ _ -> PrecAnn - Lam _ _ -> PrecFun - ALam _ _ _ -> PrecFun - App _ _ -> PrecApp - Rigid _ -> PrecFun - _ -> PrecAtom - - --------------------------------------------------------------------------- --- pretty term --------------------------------------------------------------------------- -ppTerm :: Prec -> Term -> Doc -ppTerm prec term - = (if (prec > precTerm term) then parens else id) - (ppTermEx prec term) - -ppTermEx :: Prec -> Term -> Doc -ppTermEx prec term - = case term of - App (App (App (Var "if") t1) t2) t3 -> hang 2 $ text "if" <+> ppTerm PrecApp t1 text "then" <+> ppTerm PrecApp t2 text "else" <+> ppTerm PrecApp t3 - App (App (Var "(,)") e1) e2 -> parens (ppTerm PrecTop e1 <> comma <> ppTerm PrecTop e2) - App (App (Var "$") e1) e2 -> ppTerm PrecApp e1 <+> text "$" <+> ppTerm PrecTop e2 - App (App (Var ":") e1) e2 -> case elements [e1] e2 of - Nothing -> ppTerm PrecApp e1 <> text ":" <> ppTerm PrecOp e2 - Just es -> list (map (ppTerm PrecTop) es) - - App e1 e2 -> ppTerm PrecApp e1 <+> ppTerm PrecAtom e2 - Lam v e -> char '\\' <> ppLam "->" term - ALam v ann e -> char '\\' <> ppLam "->" term - Let v rhs e -> let (bs,body) = binders [(v,rhs)] e - in align $ text "let" <+> align (vcat (punctuate semi [text v <+> ppLam "=" rhs | (v,rhs) <- bs])) - <> (if (length bs > 1) then line else softline) - <> text "in" <+> ppTerm PrecTop body - Ann e ann -> ppTerm PrecAtom e <+> text "::" <+> pretty ann - Rigid e -> text "rigid" <+> ppTerm PrecTop e - Var n -> text n - Lit i -> pretty i - where - binders acc (Let v rhs e) = binders ((v,rhs):acc) e - binders acc e = (reverse acc, e) - - ppLam arrow (Lam v e) = text v <+> ppLam arrow e - ppLam arrow (ALam v ann e) = parens (text v <> text "::" <> pretty ann) <+> ppLam arrow e - ppLam arrow e = text arrow <+> ppTerm PrecFun e - -elements acc (Var "[]") = Just (reverse acc) -elements acc (App (App (Var ":") e) es) = elements (e:acc) es -elements acc _ = Nothing - --------------------------------------------------------------------------- --- Pretty type --------------------------------------------------------------------------- -ppAnnot (Annot qs tp) - = let nice = niceExtend [] (quantIds qs) - in (if null qs then empty else (text "some" <+> hsep (map (ppQuant nice) qs) <> text ". ")) <> - ppType nice PrecTop tp - - - -ppType :: [(Id,String)] -> Prec -> Type -> Doc -ppType nice prec tp - = (if (prec > precType tp) then parens else id) (ppTypeEx nice prec tp) - -ppTypeEx nice prec tp - = case tp of - Forall _ _ - -> let (qs,rho) = splitQuants tp - nice' = niceExtend nice (map quantId qs) - in text "forall" <+> hsep (map (ppQuant nice') qs) <> dot <+> - ppType nice' PrecTop rho - - TApp (TApp (TCon "->") arg) res -> ppType nice PrecApp arg <+> text "->" <+> ppType nice PrecFun res - TApp (TCon "[]") arg -> brackets (ppType nice PrecTop arg) - TApp (TApp (TCon "(,)") t1) t2 -> parens (ppType nice PrecTop t1 <> text "," <> ppType nice PrecTop t2) - TApp tp arg -> ppType nice PrecApp tp <+> ppType nice PrecAtom arg - - TVar (TypeVar id Quantified) -> ppNice nice id - TVar (TypeVar id (Uni ref)) -> text "$" <> ppNice nice id <> ppBound nice ref - TVar (TypeVar id Skolem) -> text "_" <> pretty id - - TCon name -> text name - Bottom -> text "_|_" - -ppRank :: Rank -> Doc -ppRank r - = if r == maxBound then text "inf" else pretty r - -ppQuant nice (Quant id tp) - = case tp of - Bottom -> ppNice nice id - _ -> parens (ppNice nice id <+> text ">=" <+> ppType nice PrecTop tp) - -ppBound nice ref - = case unsafePerformIO (readIORef ref) of - Equal tp -> text "=" <> ppType nice PrecAtom tp - Instance Bottom rank -> text "_" <> ppRank rank - Instance tp rank -> text "_" <> ppRank rank <> text ">=" <> parens (ppType nice PrecTop tp) - --------------------------------------------------------------------------- --- Pretty print bound identifiers nicely --------------------------------------------------------------------------- -ppNice nice id - = case lookup id nice of - Nothing -> text (show id) -- this can happen due to updateable references :-( - Just name -> text name - -niceExtend :: [(Id,Name)] -> [Id] -> [(Id,Name)] -niceExtend nice ids - = zip ids (drop (length nice) niceNames) ++ nice - - -niceNames :: [String] -niceNames - = [[c] | c <- ['a'..'z']] ++ [[c]++show i | i <- [1::Int ..], c <- ['a'..'z']] - diff --git a/previous-approaches/hml/app/Unify.hs b/previous-approaches/hml/app/Unify.hs deleted file mode 100644 index 083d886c..00000000 --- a/previous-approaches/hml/app/Unify.hs +++ /dev/null @@ -1,145 +0,0 @@ --------------------------------------------------------------------------- --- Unification and matching --------------------------------------------------------------------------- -module Unify ( unify ) where - -import Data.IORef -import PPrint -import Types -import Subst -import Operations - - --------------------------------------------------------------------------- --- unification --------------------------------------------------------------------------- - -unify :: Type -> Type -> Infer () -unify (TCon n1) (TCon n2) | n1 == n2 - = return () - -unify (TVar v1) (TVar v2) | v1 == v2 - = return () - -unify (TApp t1 t2) (TApp u1 u2) - = do unify t1 u1 - unify t2 u2 - -unify (TVar v1) t2 | isUni (tvFlavour v1) - = unifyVar v1 t2 - -unify t1 (TVar v2) | isUni (tvFlavour v2) - = unifyVar v2 t1 - --- this case assumes that types are in normal form -unify t1@(Forall _ _) t2@(Forall _ _) - = case (splitQuants t1, splitQuants t2) of - ((qs1,r1), (qs2,r2)) | length qs1 == length qs2 - -> assert "Unify.Forall" (all isBottom (qs1++qs2)) $ - do let ids1 = quantIds qs1 - ids2 = quantIds qs2 - sks <- freshSkolems (length ids1) - rho1 <- subNew ids1 (map TVar sks) |-> r1 - rho2 <- subNew ids2 (map TVar sks) |-> r2 - unify rho1 rho2 - -- check for escaping skolems - sk1 <- freeSkolems t1 - sk2 <- freeSkolems t2 - check (sks `disjoint` (sk1 `union` sk2)) - ("type is not polymorphic enough in unify:\n type1: " ++ show (pretty t1) ++ "\n type2: " ++ show (pretty t2)) - _ -> failure ("cannot unify types:\n type1: " ++ show (pretty t1) ++ "\n type2: " ++ show (pretty t2)) - -unify t1 t2 - = failure ("cannot unify types:\n type1: " ++ show (pretty t1) ++ "\n type2: " ++ show (pretty t2)) - - -isBottom (Quant _ Bottom) = True -isBottom _ = False - ---------------------------------------------------------------------------- --- Unify variables ---------------------------------------------------------------------------- - --- | Unify a variable -unifyVar tv@(TypeVar id1 (Uni ref1)) tp2 - = do bound1 <- readRef ref1 - case bound1 of - Equal tp1 -> unify tp1 tp2 - Instance t1 rank1 - -> case tp2 of - TVar (TypeVar id2 (Uni ref2)) - -> do bound2 <- readRef ref2 - case bound2 of - Equal t2 - -> unify (TVar tv) t2 -- note: we can't shorten here since tv could be an element of t2 - Instance t2 rank2 - -> do t <- unifyScheme t1 t2 - writeRef ref1 (Equal tp2) - writeInstance ref2 t (min rank1 rank2) - _ -> do tvs <- freeTvs tp2 - check (not (tv `elem` tvs)) ("infinite type: " ++ show tv ++ " and " ++ show tp2) -- occurs check - subsume tp2 t1 - writeRef ref1 (Equal tp2) - -- adjust the lambda-rank of the unifiable variables in tp2 - adjustRank rank1 tp2 - -writeInstance ref tp rank - = do scheme <- isScheme tp - if scheme then writeRef ref (Instance tp rank) - else writeRef ref (Equal tp) - - --- | adjust the lambda-rank of the unifiable variables in a type (note: this can be combined with the occurrence check) -adjustRank :: Rank -> Type -> Infer () -adjustRank rank tp - = case tp of - TVar (TypeVar id2 (Uni ref2)) - -> do bound <- readRef ref2 - case bound of - Equal t -> adjustRank rank t - Instance t rank2 -> onlyIf (rank2 > rank) (writeRef ref2 (Instance t rank)) - -- Instance _ rank2 -> error "Unify.adjustRank: adjusting a type scheme" - Forall q rho -> assert "Unify.adjustRank.Forall: adjusting type scheme" (isBottom q) $ - adjustRank rank rho - TApp t1 t2 -> do adjustRank rank t1 - adjustRank rank t2 - _ -> return () - - ---------------------------------------------------------------------------- --- Subsume ---------------------------------------------------------------------------- -subsume :: Type -> Scheme -> Infer () -subsume tp1 scheme - = do tp2 <- constructedForm scheme - case tp2 of - Bottom - -> return () - _ -> do (sks,rho1) <- skolemize tp1 - rho2 <- instantiate tp2 - unify rho1 rho2 - -- check for escaping skolems - sk1 <- freeSkolems tp1 - sk2 <- freeSkolems tp2 - check (sks `disjoint` (sk1 `union` sk2)) - ("type is not polymorphic enough in subsume:\n type1: " ++ show tp1 ++ "\n type2: " ++ show tp2) - - ---------------------------------------------------------------------------- --- Unify two type schemes (ie. find their join) ---------------------------------------------------------------------------- -unifyScheme :: Scheme -> Scheme -> Infer Scheme -unifyScheme s1 s2 - = do tp1 <- constructedForm s1 - tp2 <- constructedForm s2 - case (tp1,tp2) of - (Bottom,_) -> return tp2 - (_,Bottom) -> return tp1 - _ -> do rho <- withRankIncrease $ -- Instantiate under an increased rank so we can quantify afterwards - do rho1 <- instantiate tp1 - rho2 <- instantiate tp2 - unify rho1 rho2 - return rho1 - quantify rho - - diff --git a/previous-approaches/hml/app/readme.txt b/previous-approaches/hml/app/readme.txt deleted file mode 100644 index df65236f..00000000 --- a/previous-approaches/hml/app/readme.txt +++ /dev/null @@ -1,66 +0,0 @@ - -This is a small but optimized reference implementation of the HML type system -described in the paper "Flexible types: Robust type inference for first-class polymorphism", -available at "http://research.microsoft.com/users/daan/pubs.html" - -This implementation uses IO references to implement substitution instead of using -explicit substitutions. Also, it uses ranked unification type variables to implement -efficient generalization. - -Just load the prototype in GHCi as: - - > ghci Main.hs - -and from the GHCi prompt, run the tests: - - *Main> testAll - ... - -or check some expressions yourself: - - *Main> check "\\x -> x" - expr: \x -> x - type: forall a. a -> a - - *Main> check "auto" - expr: auto - type: forall a. (forall b. b -> b) -> a -> a - - *Main> check "apply auto id" - expr: apply auto id - type: forall a. a -> a - - *Main> check "map auto ids" - expr: map auto ids - type: forall a. [a -> a] - -or get some more help: - - *Main> help - ... - -See the test-cases in "Main.hs" for many more examples, -and "Gamma.hs" for the standard available functions. - -Have fun, --- Daan Leijen. - - -Note: At the moment, it does not yet use canonical forms and some programs are incorrectly -rejected depending on the order of quantifiers. - - - -Modules: --------------------------------------------------------------------------------------------- -PPrint.hs Pretty printer library -Types.hs Basic definitions of terms and types -Parser.hs Basic parser for terms and types -Subst.hs Explicit substitutions -Gamma.hs Type environment: also contains standard functions like "const", or "id" -Operations.hs Basic type operations: instantiate, skolemize etc. -Unify.hs Unification, subsumption, and unifyScheme algorithms - -InferBasic.hs Basic HML type inference -Main.hs Main module - diff --git a/previous-approaches/hml/hml.cabal b/previous-approaches/hml/hml.cabal deleted file mode 100644 index c01b0191..00000000 --- a/previous-approaches/hml/hml.cabal +++ /dev/null @@ -1,75 +0,0 @@ -cabal-version: 2.2 - --- This file has been generated from package.yaml by hpack version 0.36.0. --- --- see: https://github.com/sol/hpack - -name: hml -version: 0.1.0.0 -description: Please see the README on GitHub at -homepage: https://github.com/githubuser/hml#readme -bug-reports: https://github.com/githubuser/hml/issues -author: Author name here -maintainer: example@example.com -copyright: 2023 Author name here -license: BSD-3-Clause -license-file: LICENSE -build-type: Simple -extra-source-files: - README.md - CHANGELOG.md - -source-repository head - type: git - location: https://github.com/githubuser/hml - -library - exposed-modules: - Lib - other-modules: - Paths_hml - autogen-modules: - Paths_hml - hs-source-dirs: - src - ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints - build-depends: - base >=4.7 && <5 - default-language: Haskell2010 - -executable hml-exe - main-is: Main.hs - other-modules: - Gamma - InferBasic - Operations - Parser - PPrint - Subst - Types - Unify - Paths_hml - autogen-modules: - Paths_hml - hs-source-dirs: - app - ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N - build-depends: - base >=4.7 && <5 - , hml - default-language: Haskell2010 - -test-suite hml-test - type: exitcode-stdio-1.0 - main-is: Spec.hs - other-modules: - Paths_hml - autogen-modules: - Paths_hml - hs-source-dirs: - test - ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N - build-depends: - base >=4.7 && <5 - , hml - default-language: Haskell2010 diff --git a/previous-approaches/hml/package.yaml b/previous-approaches/hml/package.yaml deleted file mode 100644 index 34eddf66..00000000 --- a/previous-approaches/hml/package.yaml +++ /dev/null @@ -1,59 +0,0 @@ -name: hml -version: 0.1.0.0 -github: "githubuser/hml" -license: BSD-3-Clause -author: "Author name here" -maintainer: "example@example.com" -copyright: "2023 Author name here" - -extra-source-files: -- README.md -- CHANGELOG.md - -# Metadata used when publishing your package -# synopsis: Short description of your package -# category: Web - -# To avoid duplicated efforts in documentation and dealing with the -# complications of embedding Haddock markup inside cabal files, it is -# common to point users to the README.md file. -description: Please see the README on GitHub at - -dependencies: -- base >= 4.7 && < 5 - -ghc-options: -- -Wall -- -Wcompat -- -Widentities -- -Wincomplete-record-updates -- -Wincomplete-uni-patterns -- -Wmissing-export-lists -- -Wmissing-home-modules -- -Wpartial-fields -- -Wredundant-constraints - -library: - source-dirs: src - -executables: - hml-exe: - main: Main.hs - source-dirs: app - ghc-options: - - -threaded - - -rtsopts - - -with-rtsopts=-N - dependencies: - - hml - -tests: - hml-test: - main: Spec.hs - source-dirs: test - ghc-options: - - -threaded - - -rtsopts - - -with-rtsopts=-N - dependencies: - - hml diff --git a/previous-approaches/hml/src/Lib.hs b/previous-approaches/hml/src/Lib.hs deleted file mode 100644 index d36ff271..00000000 --- a/previous-approaches/hml/src/Lib.hs +++ /dev/null @@ -1,6 +0,0 @@ -module Lib - ( someFunc - ) where - -someFunc :: IO () -someFunc = putStrLn "someFunc" diff --git a/previous-approaches/hml/stack.yaml b/previous-approaches/hml/stack.yaml deleted file mode 100644 index 3e1e783a..00000000 --- a/previous-approaches/hml/stack.yaml +++ /dev/null @@ -1,67 +0,0 @@ -# This file was automatically generated by 'stack init' -# -# Some commonly used options have been documented as comments in this file. -# For advanced use and comprehensive documentation of the format, please see: -# https://docs.haskellstack.org/en/stable/yaml_configuration/ - -# Resolver to choose a 'specific' stackage snapshot or a compiler version. -# A snapshot resolver dictates the compiler version and the set of packages -# to be used for project dependencies. For example: -# -# resolver: lts-21.13 -# resolver: nightly-2023-09-24 -# resolver: ghc-9.6.2 -# -# The location of a snapshot can be provided as a file or url. Stack assumes -# a snapshot provided as a file might change, whereas a url resource does not. -# -# resolver: ./custom-snapshot.yaml -# resolver: https://example.com/snapshots/2023-01-01.yaml -resolver: - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/21/24.yaml - -# User packages to be built. -# Various formats can be used as shown in the example below. -# -# packages: -# - some-directory -# - https://example.com/foo/bar/baz-0.0.2.tar.gz -# subdirs: -# - auto-update -# - wai -packages: -- . -# Dependency packages to be pulled from upstream that are not in the resolver. -# These entries can reference officially published versions as well as -# forks / in-progress versions pinned to a git hash. For example: -# -# extra-deps: -# - acme-missiles-0.3 -# - git: https://github.com/commercialhaskell/stack.git -# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a -# -# extra-deps: [] - -# Override default flag values for local packages and extra-deps -# flags: {} - -# Extra package databases containing global packages -# extra-package-dbs: [] - -# Control whether we use the GHC we find on the path -# system-ghc: true -# -# Require a specific version of Stack, using version ranges -# require-stack-version: -any # Default -# require-stack-version: ">=2.13" -# -# Override the architecture used by Stack, especially useful on Windows -# arch: i386 -# arch: x86_64 -# -# Extra directories used by Stack for building -# extra-include-dirs: [/path/to/dir] -# extra-lib-dirs: [/path/to/dir] -# -# Allow a newer minor version of GHC than the snapshot specifies -# compiler-check: newer-minor diff --git a/previous-approaches/hml/stack.yaml.lock b/previous-approaches/hml/stack.yaml.lock deleted file mode 100644 index 16308d5d..00000000 --- a/previous-approaches/hml/stack.yaml.lock +++ /dev/null @@ -1,13 +0,0 @@ -# This file was autogenerated by Stack. -# You should not edit this file by hand. -# For more information, please see the documentation at: -# https://docs.haskellstack.org/en/stable/lock_files - -packages: [] -snapshots: -- completed: - sha256: abcc4a65c15c7c2313f1a87f01bfd4d910516e1930b99653eef1d2d006515916 - size: 640074 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/21/24.yaml - original: - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/21/24.yaml diff --git a/previous-approaches/hml/test/Spec.hs b/previous-approaches/hml/test/Spec.hs deleted file mode 100644 index cd4753fc..00000000 --- a/previous-approaches/hml/test/Spec.hs +++ /dev/null @@ -1,2 +0,0 @@ -main :: IO () -main = putStrLn "Test suite not yet implemented"