p.k.f.holzenspies | 29 Aug 15:42 2013
Picon
Picon

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
(Continue reading)

Simon Peyton-Jones | 30 Aug 18:24 2013
Picon

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 <at> haskell.org] On Behalf Of p.k.f.holzenspies <at> utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users <at> haskell.org
| Subject: Question about correct GHC-API use for type checking (or
| zonking, or tidying)
| 
| Dear GHC-ers,
(Continue reading)

p.k.f.holzenspies | 30 Aug 18:49 2013
Picon
Picon

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 <simonpj <at> microsoft.com>
Date: 30/08/2013 18:25 (GMT+01:00)
To: "Holzenspies, P.K.F. (EWI)" <p.k.f.holzenspies <at> utwente.nl>,glasgow-haskell-users <at> 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 <at> haskell.org] On Behalf Of p.k.f.holzenspies <at> utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users <at> 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 <at> (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 <at> haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 2 Sep 13:34 2013
Picon

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 <at> utwente.nl [mailto:p.k.f.holzenspies <at> utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users <at> 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 <simonpj <at> microsoft.com>
Date: 30/08/2013 18:25 (GMT+01:00)
To: "Holzenspies, P.K.F. (EWI)" <p.k.f.holzenspies <at> utwente.nl>,glasgow-haskell-users <at> 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 <at> haskell.org] On Behalf Of p.k.f.holzenspies <at> utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users <at> 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 <at> (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 <at> haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
p.k.f.holzenspies | 3 Sep 15:18 2013
Picon
Picon

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 <at> microsoft.com]
Sent: maandag 2 september 2013 13:34
To: Holzenspies, P.K.F. (EWI); glasgow-haskell-users <at> 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 <at> utwente.nl [mailto:p.k.f.holzenspies <at> utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users <at> 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 <simonpj <at> microsoft.com>
Date: 30/08/2013 18:25 (GMT+01:00)
To: "Holzenspies, P.K.F. (EWI)" <p.k.f.holzenspies <at> utwente.nl>,glasgow-haskell-users <at> 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 <at> haskell.org] On Behalf Of p.k.f.holzenspies <at> utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users <at> 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 <at> (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 <at> haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 4 Sep 18:00 2013
Picon

RE: Question about correct GHC-API use for type checking (or zonking, or tidying)

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 <at> utwente.nl [mailto:p.k.f.holzenspies <at> utwente.nl]
Sent: 03 September 2013 14:18
To: Simon Peyton-Jones; glasgow-haskell-users <at> 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 <at> microsoft.com]
Sent: maandag 2 september 2013 13:34
To: Holzenspies, P.K.F. (EWI); glasgow-haskell-users <at> 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 <at> utwente.nl [mailto:p.k.f.holzenspies <at> utwente.nl]
Sent: 30 August 2013 17:49
To: Simon Peyton-Jones; glasgow-haskell-users <at> 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 <simonpj <at> microsoft.com>
Date: 30/08/2013 18:25 (GMT+01:00)
To: "Holzenspies, P.K.F. (EWI)" <p.k.f.holzenspies <at> utwente.nl>,glasgow-haskell-users <at> 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 <at> haskell.org] On Behalf Of p.k.f.holzenspies <at> utwente.nl
| Sent: 29 August 2013 14:42
| To: glasgow-haskell-users <at> 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 <at> (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 <at> haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane