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 simo...@microsoft.com
Date: 30/08/2013 18:25 (GMT+01:00)
To: Holzenspies, P.K.F. (EWI)
p.k.f.holzensp...@utwente.nl,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-
| boun...@haskell.org] On Behalf Of p.k.f.holzensp...@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:
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-
| boun...@haskell.org] On Behalf Of p.k.f.holzensp...@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
