Ari Fordsham 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

Hi Ari, This is a fine idea in theory, but (at present) a poor one in practice, for at least the following reasons: * GHC's internal language is based on System F, allowing polymorphism. Modeling polymorphism in the way you describe is hard, even for a language that supports full dependent types -- so much so that successfully doing it (in Agda) is the subject of a recent peer-reviewed publication: https://iohk.io/en/research/library/papers/system-f-in-agdafor-fun-and-profi... There is some work on encoding System F in this way in Haskell, but it's rough: https://www.cis.upenn.edu/~plclub/blog/2020-06-26-Strongly-typed-System-F/ Note that GHC Core is significantly more complex than either of these more modest languages. * Core is manipulated a *lot*. Having intrinsic typing means, essentially, that every optimization would have to be proved sound, in the compiler. This is another thing that would be wonderful in theory, but we're just very far away from being able to achieve this in practice. * I don't think we'd save very much at all: any information used to make runtime decisions must be present at runtime, and types are erased. So if we did this, we'd still need to carry (likely via class constraints) lots of information around to runtime. The difference would be that it would be passed implicitly instead of explicitly, but doing this won't speed GHC up. * I actually tried something like this while on holiday a few years ago: I wanted to label Coercions with their role. This is a tempting subset of the challenge you describe, because roles are very first-order (there are only 3 of them!) and yet hard to get right. My work ran into no dead ends, exactly, but it quickly required lots and lots of fancy support structures. (For example, we would need a finite map where both keys and values are indexed by some role. And we'd need existentials. Lots of them.) If I had more time, I might have finished this, but there are bigger fish to fry. So: I'd be very happy with being able to do this as a long-term goal, but I'd say we are years away from it -- and the best way toward it is simply adding support for dependent types. Richard

On Sep 14, 2021, at 8:38 AM, Ari Fordsham wrote:

I don't know if this is the right forum for this, I apologise if I'm intruding...

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.

Conal Eliottt has done something similar in a blog post (http://conal.net/blog/posts/overloading-lambda#:~:text=Haskell%20source%20la... http://conal.net/blog/posts/overloading-lambda#:~:text=Haskell%20source%20la...) and it seems relatively straightforward.

This would be especially beneficial to those working at the cutting edge of GHC features, statically ensuring their Core manipulations are correct. I would be surprised if existing compiler bugs wouldn't be found while implementing this.

What would the performance impact be? would using GADTs incur extra overhead? I'd assume you'd save something by lugging around less type information in Core.

Ari Fordsham _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs