More type safety in Core?

[Simon Peyton Jones]

One difficulty is that I think that writing Core-to-Core passes might become a lot more challenging.   It gets gnarly writing code that satisfies the type checker, depending of course on how strong the invariants are.

I think Typesafe runtime code generation<https://www.researchgate.net/publication/292674440_Type-safe_Runtime_Code_Generation_Accelerate_to_LLVM> has some material on this.

TL;DR: by all means give it a try.  I'm not terribly optimistic... but progress is made when we find that things we thought weren't possible are possible after all.  So I'd be happy to be proved wrong.

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point simonpj at microsoft.com<mailto:simonpj at microsoft.com> will cease to work.  Use simon.peytonjones at gmail.com<mailto:simon.peytonjones at gmail.com> instead.  (For now, it just forwards to simonpj at microsoft.com.)

From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Ari Fordsham
Sent: 14 September 2021 13:39
To: ghc-devs at haskell.org
Subject: More type safety in Core?

You don't often get email from arifordsham at gmail.com<mailto:arifordsham at gmail.com>. Learn why this is important<http://aka.ms/LearnAboutSenderIdentification>
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%20language.-,I,-originally%20intended%20to<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fconal.net%2Fblog%2Fposts%2Foverloading-lambda%23%3A~%3Atext%3DHaskell%2520source%2520language.-%2CI%2C-originally%2520intended%2520to&data=04%7C01%7Csimonpj%40microsoft.com%7C3f5f8d3d0bc141e5a78408d9777ca375%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637672217369668112%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000&sdata=6IB9AcOy%2BzMmbVU51i9IenjPVA6usmeQE87j4Z1tXlk%3D&reserved=0>) 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210914/eee7e0b0/attachment-0001.html>