I feel so unbelievably ignorant now. I thought with all the IORefs in the type checking process that zonking did this in these refs. Somehow I started thinking that some of these remained in SDocs, not thinking showSDoc is pure and results in a String, which holds no IORefs.
Does this mean that for the idType to come out correctly I should also zonk (AND BIND) the Id-value I return?
Ph.
Sent from Samsung Mobile
-------- Original message --------
From: Simon Peyton-Jones
Date: 30/08/2013 18:25 (GMT+01:00)
To: "Holzenspies, P.K.F. (EWI)" ,glasgow-haskell-users@haskell.org
Subject: RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
Haskell is a *functional* language. Consider
say $ " pre-zonk: " ++ pp all_expr_ty
zonkTcType all_expr_ty
say $ " post-zonk: " ++ pp all_expr_ty
pp is a pure function; it is given the same input both times, so of course it produces the same output.
If you collect the result of zonkTcType you might have better luck, thus:
say $ " pre-zonk: " ++ pp all_expr_ty
zonked_expr_ty <- zonkTcType all_expr_ty
say $ " post-zonk: " ++ pp zonked_expr_ty
Zonking walks over a type, returning a new type in which unification variables are replaced by the types they unified to.
Hope this helps
Simon
| -----Original Message-----
| From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
| bounces@haskell.org] On Behalf Of p.k.f.holzenspies@utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users@haskell.org
| Subject: Question about correct GHC-API use for type checking (or
| zonking, or tidying)
|
| Dear GHC-ers,
|
| I'm working on building an interactive environment around the
| composition of expressions. Users can type in (i.e. give strings of)
| expressions and can then use these expressions to produce other
| expressions. I'm close to having a working GHC-API binding for this. The
| resulting types, however, still contain some things I don't quite
| understand. Any help would be appreciated.
|
| Below, I've included the function exprFromString which should parse,
| rename and typecheck strings to Id-things and give their type (although,
| ideally, the idType of said Id-thing should be the same as the type
| returned). This function lives in the IA (InterActive) monad; a monad
| that is a GhcMonad and can lift monadic computations in TcM into itself
| using liftTcM (which uses the initTcPrintErrors and
| setInteractiveContext functions similarly to TcRnDriver.tcRnExpr).
|
| Near the end of the function, debugging output is produced. This output
| confuses me slightly. Here is the output for the three inputs "map (+1)
| [1..10]", "5" and "\\x -> x":
|
|
| map (+1) [1..10]
| pre-zonk: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
| post-zonk: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
| idType: [b_c]
| tidied: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
| 5
| pre-zonk: forall a. GHC.Num.Num a_d => t_c
| post-zonk: forall a. GHC.Num.Num a_d => t_c
| idType: a_b
| tidied: forall a. GHC.Num.Num a_d => t_c
| \x -> x
| pre-zonk: forall t. t_e
| post-zonk: forall t. t_e
| idType: forall t. t -> t
| tidied: forall t. t_e
|
|
| The zonking and tidying part of the type-checking process are still a
| bit unclear to me and I suspect the problems arise there. It looks to me
| that the type variables in the quantifications are different ones from
| those in the pi/rho-types. I had expected the types to only contain the
| variables over which they are quantified, so e.g. in the map-example, I
| had expected "forall b . (GHC.Enum.Enum b, GHC.Num.Num b) => [b]"
|
| Can anyone explain what I'm missing?
|
| Regards,
| Philip
|
|
|
|
|
| exprFromString :: String -> IA (Id,Type)
| exprFromString str = do
| dfs <- getDynFlags
| let pp = showSDoc dfs . ppr
| pst <- mkPState dfs buf <$> newRealSrcLoc
|
| {- Parse -}
| (loc,rdr_expr) <- case unP parseStmt pst of
| PFailed span err -> throwOneError (mkPlainErrMsg dfs span err)
| POk pst' (Just (L l (ExprStmt rdr_expr _ _ _))) -> do
| logWarningsReportErrors (getMessages pst')
| return (l,rdr_expr)
| POk pst' thing -> throw $ maybe EmptyParse (const
| NonExpressionParse) thing
| liftTcM $ do
| fresh_it <- freshName loc str
|
| {- Rename -}
| (rn_expr, fvs) <- checkNoErrs $ rnLExpr rdr_expr
|
| {- Typecheck -}
| let binds = mkBinds fresh_it rn_expr fvs
|
| (((_bnds,((_tc_expr,res_ty),id)),untch),lie) <- captureConstraints .
| captureUntouchables $
| tcLocalBinds binds ((,) <$> tcInferRho rn_expr <*> tcLookupId
| fresh_it)
| ((qtvs, dicts, _bool, _evbinds), lie_top) <- captureConstraints $
| simplifyInfer True False [(fresh_it, res_ty)] (untch,lie)
|
| let all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty)
| say str
| say $ " pre-zonk: " ++ pp all_expr_ty
| zonkTcType all_expr_ty
| say $ " post-zonk: " ++ pp all_expr_ty
| say $ " idType: " ++ pp (idType id)
| say $ " tidied: " ++ pp (tidyTopType all_expr_ty)
|
| return (id,all_expr_ty)
| where
| say = liftIO . putStrLn
| buf = stringToStringBuffer str
| freshName loc str = (\u -> mkInternalName u name loc) <$> newUnique
| where
| name = mkOccNameFS varName $ fsLit $ "it" ++ show (lineOf loc)
| isVarChar c = isAlphaNum c || c == '_' || c == '\''
| lineOf (RealSrcSpan s) = srcSpanStartLine s
| lineOf _ = -1
|
| mkBinds :: Name -> LHsExpr Name -> FreeVars -> HsLocalBinds Name
| mkBinds nm e@(L l _) fvs = HsValBinds $ ValBindsOut [(NonRecursive,
| unitBag the_bind)] []
| where
| the_bind = L l (mkTopFunBind (L l nm) [mkMatch [] e
| emptyLocalBinds]) { bind_fvs = fvs }
|
|
|
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
