<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Sep 14, 2021, at 5:43 PM, Callan McGill <<a href="mailto:callan.mcgill@gmail.com" class="">callan.mcgill@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div dir="ltr" class="">Following on from Richard mentioning this paper and video there was an extremely nice version of this done recently by Sam Derbyshire using type checker plugins that is well worth a look to see what is involved: <a href="https://github.com/sheaf/ghc-tcplugin-api/tree/main/examples/SystemF" class="">https://github.com/sheaf/ghc-tcplugin-api/tree/main/examples/SystemF</a><br class=""></div></div></div></blockquote><div><br class=""></div><div>I just want to amplify that Callan above in promoting Sam's work -- an unfortunate oversight on my part. Very cool how it works with the new plugins architecture!</div><div><br class=""></div><div>Richard</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div dir="ltr" class=""><br class=""></div><div class="">Best,<br class=""></div><div class="">Callan<br class=""></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 14 Sept 2021 at 15:44, Richard Eisenberg <<a href="mailto:lists@richarde.dev" class="">lists@richarde.dev</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;" class="">Hi Ari,<div class=""><br class=""></div><div class="">This is a fine idea in theory, but (at present) a poor one in practice, for at least the following reasons:</div><div class=""><br class=""></div><div class="">* 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: <a href="https://iohk.io/en/research/library/papers/system-f-in-agdafor-fun-and-profit/" target="_blank" class="">https://iohk.io/en/research/library/papers/system-f-in-agdafor-fun-and-profit/</a> There is some work on encoding System F in this way in Haskell, but it's rough: <a href="https://www.cis.upenn.edu/~plclub/blog/2020-06-26-Strongly-typed-System-F/" target="_blank" class="">https://www.cis.upenn.edu/~plclub/blog/2020-06-26-Strongly-typed-System-F/</a> Note that GHC Core is significantly more complex than either of these more modest languages.</div><div class=""><br class=""></div><div class="">* 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.</div><div class=""><br class=""></div><div class="">* 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.</div><div class=""><br class=""></div><div class="">* 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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Richard</div><div class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Sep 14, 2021, at 8:38 AM, Ari Fordsham <<a href="mailto:arifordsham@gmail.com" target="_blank" class="">arifordsham@gmail.com</a>> wrote:</div><br class=""><div class=""><div dir="ltr" class="">I don't know if this is the right forum for this, I apologise if I'm intruding...<div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Conal Eliottt has done something similar in a blog post (<a href="http://conal.net/blog/posts/overloading-lambda#:~:text=Haskell%20source%20language.-,I,-originally%20intended%20to" target="_blank" class="">http://conal.net/blog/posts/overloading-lambda#:~:text=Haskell%20source%20language.-,I,-originally%20intended%20to</a>) and it seems relatively straightforward.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Ari Fordsham</div></div>
_______________________________________________<br class="">ghc-devs mailing list<br class=""><a href="mailto:ghc-devs@haskell.org" target="_blank" class="">ghc-devs@haskell.org</a><br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" target="_blank" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br class=""></div></blockquote></div><br class=""></div></div>_______________________________________________<br class="">
ghc-devs mailing list<br class="">
<a href="mailto:ghc-devs@haskell.org" target="_blank" class="">ghc-devs@haskell.org</a><br class="">
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br class="">
</blockquote></div></div>
</div></blockquote></div><br class=""></body></html>