ref: 5b20756d9f95c060641686c2026350086cef5e00
parent: b58a207da4576b658dee36c7dd6dcbfa12c7539f
author: Lennart Augustsson <lennart.augustsson@epicgames.com>
date: Wed Sep 20 10:56:13 EDT 2023
Implement rank-N polymorphism (probably incorrectly).
--- a/TODO
+++ b/TODO
@@ -3,8 +3,7 @@
* Have compile return a Stats record of timing etc
* Add overloading
* Implement deriving
-* Add forall to the syntax of types so it can be nested
- - Rank-N requires small changes in the type checker
+* Make sure rank-N works correctly
* Add the possibility to save a compiler cache in a file
- Add SHA checksumming to the C code
- Use filename as the cache lookup key and SHA for validation
--- a/src/MicroHs/Parse.hs
+++ b/src/MicroHs/Parse.hs
@@ -279,11 +279,15 @@
pKind :: P EKind
pKind = pType
+{-pTypeScheme :: P ETypeScheme
pTypeScheme = P.do
vs <- (pKeyword "forall" *> esome pIdKind <* pSymbol ".") <|< pure []
t <- pType
pure $ if null vs then t else EForall vs t
+-}
+pTypeScheme :: P ETypeScheme
+pTypeScheme = pType
--
-- Partial copy of pExpr, but that includes '->'.
@@ -290,7 +294,10 @@
-- Including '->' in pExprOp interacts poorly with '->'
-- in lambda and 'case'.
pType :: P EType
-pType = pTypeOp
+pType = P.do
+ vs <- (pKeyword "forall" *> esome pIdKind <* pSymbol ".") <|< pure []
+ t <- pTypeOp
+ pure $ if null vs then t else EForall vs t
pTypeOp :: P EType
pTypeOp = pOperators pTypeOper pTypeArg
--- a/src/MicroHs/TypeCheck.hs
+++ b/src/MicroHs/TypeCheck.hs
@@ -440,7 +440,9 @@
EVar _ -> bad
EApp fb xb -> T.do { unify loc fa fb; unify loc xa xb }EUVar i -> addUVar i a
- _ -> impossible
+ _ ->
+ --trace ("impossible unify " ++ showExpr a ++ " = " ++ showExpr b) $+ impossible
EUVar i -> addUVar i b
_ -> impossible
@@ -738,14 +740,26 @@
(ae,) <$> newUVar
else T.do
(e, t) <- tLookupInst "variable" i
--- traceM $ "*** " ++ i ++ " :: " ++ showExpr t ++ " = " ++ showMaybe showExpr mt
- munify (getSLocIdent i) mt t
- T.return (e, t)
+ case mt of
+ Just tu@(EForall _ tt) -> T.do
+ unify (getSLocExpr ae) tt t
+ T.return (e, tu)
+ _ -> T.do
+ munify (getSLocIdent i) mt t
+ T.return (e, t)
EApp f a -> T.do
+ let loc = getSLocExpr ae
+ (ef, tf) <- tcExpr Nothing f
+ (ta, tr) <- unArrow loc tf
+ (ea, _) <- tcExpr (Just ta) a
+ munify loc mt tr
+ T.return (EApp ef ea, tr)
+{- slower and uses more memory(ea, ta) <- tcExpr Nothing a
tr <- unMType mt
(ef, _) <- tcExpr (Just (tArrow ta tr)) f
T.return (EApp ef ea, tr)
+-}
EOper e ies -> tcOper mt e ies
ELam is e -> tcExprLam mt is e
ELit loc l -> tcLit mt loc l
@@ -872,8 +886,8 @@
let
appOp (f, ft) (e1, t1) (e2, t2) = T.do
let l = getSLocExpr f
- (fta1, ftr1) <- unArrow l (Just ft)
- (fta2, ftr2) <- unArrow l (Just ftr1)
+ (fta1, ftr1) <- unArrow l ft
+ (fta2, ftr2) <- unArrow l ftr1
unify l fta1 t1
unify l fta2 t2
-- traceM (showExpr (EApp (EApp f e1) e2))
@@ -914,9 +928,8 @@
munify (getSLocExpr ae) mt t
T.return et
-unArrow :: SLoc -> Maybe EType -> T (EType, EType)
-unArrow _ Nothing = T.do { a <- newUVar; r <- newUVar; T.return (a, r) }-unArrow loc (Just t) =
+unArrow :: SLoc -> EType -> T (EType, EType)
+unArrow loc t =
case getArrow t of
Just ar -> T.return ar
Nothing -> T.do
@@ -931,7 +944,7 @@
tcPats :: forall a . EType -> [EPat] -> (EType -> [Typed EPat] -> T a) -> T a
tcPats t [] ta = ta t []
tcPats t (p:ps) ta = T.do
- (tp, tr) <- unArrow (getSLocExpr p) (Just t)
+ (tp, tr) <- unArrow (getSLocExpr p) t
tcPat tp p $ \ pp -> tcPats tr ps $ \ tt pps -> ta tt ((pp, tp) : pps)
tcExprLam :: Maybe EType -> [EPat] -> Expr -> T (Typed Expr)
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -18,6 +18,7 @@
$(MHS) Foreign && $(EVAL) > Foreign.out && diff Foreign.ref Foreign.out
$(MHS) MutRec && $(EVAL) > MutRec.out && diff MutRec.ref MutRec.out
$(MHS) LocalPoly && $(EVAL) > LocalPoly.out && diff LocalPoly.ref LocalPoly.out
+ $(MHS) Rank2 && $(EVAL) > Rank2.out && diff Rank2.ref Rank2.out
time:
@echo Expect about 10s runtime
@@ -25,3 +26,4 @@
clean:
rm -f *.out *.tmp
+
--
⑨