Question about correct GHCAPI use for type checking (or zonking, or tidying)
Simon PeytonJones
simonpj at microsoft.com
Fri Aug 30 18:24:35 CEST 2013
Haskell is a *functional* language. Consider
say $ " prezonk: " ++ pp all_expr_ty
zonkTcType all_expr_ty
say $ " postzonk: " ++ 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 $ " prezonk: " ++ pp all_expr_ty
zonked_expr_ty < zonkTcType all_expr_ty
say $ " postzonk: " ++ 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: Glasgowhaskellusers [mailto:glasgowhaskellusers
 bounces at haskell.org] On Behalf Of p.k.f.holzenspies at utwente.nl
 Sent: 29 August 2013 14:42
 To: glasgowhaskellusers at haskell.org
 Subject: Question about correct GHCAPI use for type checking (or
 zonking, or tidying)

 Dear GHCers,

 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 GHCAPI 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 Idthings and give their type (although,
 ideally, the idType of said Idthing 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]
 prezonk: forall b. (GHC.Enum.Enum b_i, GHC.Num.Num b_i) => [b_i]
 postzonk: 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
 prezonk: forall a. GHC.Num.Num a_d => t_c
 postzonk: forall a. GHC.Num.Num a_d => t_c
 idType: a_b
 tidied: forall a. GHC.Num.Num a_d => t_c
 \x > x
 prezonk: forall t. t_e
 postzonk: forall t. t_e
 idType: forall t. t > t
 tidied: forall t. t_e


 The zonking and tidying part of the typechecking 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/rhotypes. I had expected the types to only contain the
 variables over which they are quantified, so e.g. in the mapexample, 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 $ " prezonk: " ++ pp all_expr_ty
 zonkTcType all_expr_ty
 say $ " postzonk: " ++ 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 }



 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
More information about the Glasgowhaskellusers
mailing list