More type safety in Core?

[Ben Gamari]

Ari Fordsham <arifordsham at gmail.com> writes:

> I don't know if this is the right forum for this, I apologise if I'm
> intruding...
>
Indeed it is! No reason to apologise.

> Are there any plans to use the type system to enforce safety in Core, via
> e.g. GADTs? This would replace much of core-lint with static checking.
>
I am unaware of any plans currently. In general changing GHC's Core
language (or even just its Haskell representation) is something that
doesn't happen very often and for good reason.

To me, giving the Core AST more precise types would be a very
significant undertaking (touching a good fraction of the compiler) and
it is not clear to me that it wouldn't have compiler performance
implications. Afterall, expression types are still runtime-relevant to
the compiler and therefore can't be dropped. Moreover, the lifted
equality constraints that your GADTs constructors would no doubt carry
do have a runtime representation.

It's also not clear that catching ill-formed Core statically would pay
its way given the inevitable bookkeeping that the more elaborate types
would involve; this is especially true given that typing expressions
won't eliminate the need for dynamic Core Linting, which would still be
necessary to check things like well-scoped-ness.

These are my high-level thoughts; to say anything more concrete we would
need to consider a concrete proposal. It is certainly an interesting
area to explore and while I may be skeptical I would love to be proven
wrong.

Cheers,

- Ben
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210914/066463a5/attachment.sig>