Thoughts on the design of External Core

[Simon Peyton-Jones]

Aaron,

I've digested your msg, and yes on balance I think you are probably right.  Really the only disadvantages of the IfaceSyn route are:

* Need to take more care with errors
* The possiblity that the needs of interface files and the needs of External Core might not be identical.

On the up-side, using IfaceSyn guarantees that it'll stay up to date.


Concerning type checking, the IfaceSyn typechecker does not check that, say, in an application (f x) the type of f is compatible with the type of x.  I urge you *not* to make it check, because that'll make more work even when reading interface files.

Instead,
(1) run the existing tcIfaceExpr stuff (which really amounts to a kind of reader, turning the strings in IfaceSyn into the Ids and TyCons of Core),
(2) run CoreLint to check that the resulting terms are well-typed.

You may need to work on Core Lint's error messages a bit, but it does the right kind of thing.


Let me know how it goes.

Simon

| -----Original Message-----
| From: Aaron Tomb [mailto:atomb at soe.ucsc.edu]
| Sent: 15 February 2007 00:50
| To: GHC Users Mailing List
| Cc: Simon Peyton-Jones
| Subject: Thoughts on the design of External Core
|
| Over the last few days, I've put some more thought into the overall
| design of External Core. I looked through some of the GHC code some
| more, and I'm leaning toward a preference for using IfaceSyn
| throughout the whole External Core processing path.
|
| Simon, feel free to digest this at your leisure when you return.
|
| I also welcome feedback from anyone else. I don't assume that either
| of the following lists is complete or fully correct, and would like
| to hear any comments or criticism.
|
| Now, on to what I see as the pros and cons of using the Iface
| infrastructure for all aspects of External Core.
|
| Pros:
|
| * The input segment of this path is largely complete already. It
| needs a little fixing up (some of which I've already done), but the
| general design seems sound.
|
| * The code in HscMain that calls emitExternalCore is in the middle of
| the Iface processing pipeline. So, full Iface information is already
| available. If I understand things correctly, this means that all of
| the code of the current module is already in scope in IfaceSyn
| format. Maybe I'm wrong, though, and only type signatures are fully
| present?
|
| * Though I hear that the Iface typechecker generally assumes the
| absence of errors, the best long-term design decision might be to
| beef it up to the point where it can really tell you what's wrong
| when given ill-typed input. It is an external representation, after
| all. Currently, it's only likely to have come from GHC itself.
| Perhaps in the future other tools will also manipulate .hi files,
| however. Using IfaceSyn for External Core would encourage us to
| improve the typechecker, which would make interfacing with such tools
| more viable.
|
| * It looks like it would be straightforward to pretty-print IfaceSyn
| in ExternalCore format directly. It has almost exactly the same set
| of data constructors as (the old) ExternalCore does. The conversion
| from Core -> Abstract ExternalCore -> Concrete ExternalCore seems
| unnecessary. We could just do IfaceSyn -> Concrete ExternalCore.
|
| Cons:
|
| * If the Iface typechecker is indeed less than helpful in the face of
| errors, it will need to be improved.
|
| * I may be missing complications that would make the picture less
| rosy than I've implied.
|
| * One approach to the architecture of GHC (which I had in mind
| originally) is that all "source code", in whatever format, should
| somehow go through the HsSyn portion of the compiler. Thus, this part
| of the compiler does all of the real error checking, whereas the rest
| can assume certain correctness properties. Using IfaceSyn for
| External Core would violate this architectural assumption.
|
| Aaron