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 }
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
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
Does this mean that for the idType to come out correctly I should also zonk (AND BIND) the Id-value I return?
Yes, zonk the type and grab the type that comes back.
S
From: p.k.f.holzenspies@utwente.nl [mailto:p.k.f.holzenspies@utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
Subject: Re: Question about correct GHC-API use for type checking (or zonking, or tidying)
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
Dear Simon, et al,
I had a chance to try it now. The strange thing is that when I use the lines:
zonked_id <- TcMType.zonkId id
say $ "zonked idType: " ++ pp (idType zonked_id)
that is still some unresolved type variable (i.e. prints as "b_i"). Since I already have the intended target-type (considering the code by which it is produced), is it safe to do what TcMType.zonkId does and manually set it? In other words, I now do this:
zonked_ty <- zonkTcType all_expr_ty
return (setIdType id zonked_ty)
Will this bite me later?
Regards,
Philip
From: Simon Peyton-Jones [mailto:simonpj@microsoft.com]
Sent: maandag 2 september 2013 13:34
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)
Does this mean that for the idType to come out correctly I should also zonk (AND BIND) the Id-value I return?
Yes, zonk the type and grab the type that comes back.
S
From: p.k.f.holzenspies@utwente.nlmailto:p.k.f.holzenspies@utwente.nl [mailto:p.k.f.holzenspies@utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org
Subject: Re: Question about correct GHC-API use for type checking (or zonking, or tidying)
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
The id you are getting is a monomorphic id, with a type like a->a, not the polymorphic forall a. a->a. You don't want to go round arbitrarily creating a new Id with the same unique but a different type. I have no idea what would happen then.
It's hard for me to understand just what you code is trying to do. I think you are making bindig
it = <some expr>
and then you want the type of "it". Maybe something like
(binds', gbl_env) <- tcLocalBinds (..your bindin..)
poly_id <- setGblEnv gbl_env (tcLooupId the_id_name)
But I'm not totally sure.
S
From: p.k.f.holzenspies@utwente.nl [mailto:p.k.f.holzenspies@utwente.nl]
Sent: 03 September 2013 14:18
To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
Subject: RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
Dear Simon, et al,
I had a chance to try it now. The strange thing is that when I use the lines:
zonked_id <- TcMType.zonkId id
say $ "zonked idType: " ++ pp (idType zonked_id)
that is still some unresolved type variable (i.e. prints as "b_i"). Since I already have the intended target-type (considering the code by which it is produced), is it safe to do what TcMType.zonkId does and manually set it? In other words, I now do this:
zonked_ty <- zonkTcType all_expr_ty
return (setIdType id zonked_ty)
Will this bite me later?
Regards,
Philip
From: Simon Peyton-Jones [mailto:simonpj@microsoft.com]
Sent: maandag 2 september 2013 13:34
To: Holzenspies, P.K.F. (EWI); glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org
Subject: RE: Question about correct GHC-API use for type checking (or zonking, or tidying)
Does this mean that for the idType to come out correctly I should also zonk (AND BIND) the Id-value I return?
Yes, zonk the type and grab the type that comes back.
S
From: p.k.f.holzenspies@utwente.nlmailto:p.k.f.holzenspies@utwente.nl [mailto:p.k.f.holzenspies@utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users@haskell.orgmailto:glasgow-haskell-users@haskell.org
Subject: Re: Question about correct GHC-API use for type checking (or zonking, or tidying)
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
participants (2)
-
p.k.f.holzenspies＠utwente.nl -
Simon Peyton-Jones