More type safety in Core?

[Richard Eisenberg]

> On Sep 14, 2021, at 5:43 PM, Callan McGill <callan.mcgill at gmail.com> wrote:
> 
> 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: https://github.com/sheaf/ghc-tcplugin-api/tree/main/examples/SystemF <https://github.com/sheaf/ghc-tcplugin-api/tree/main/examples/SystemF>

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!

Richard

> 
> Best,
> Callan
> 
> On Tue, 14 Sept 2021 at 15:44, Richard Eisenberg <lists at richarde.dev <mailto:lists at richarde.dev>> wrote:
> 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-profit/ <https://iohk.io/en/research/library/papers/system-f-in-agdafor-fun-and-profit/>   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/ <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 <arifordsham at gmail.com <mailto:arifordsham at gmail.com>> 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%20language.-,I,-originally%20intended%20to <http://conal.net/blog/posts/overloading-lambda#:~:text=Haskell%20source%20language.-,I,-originally%20intended%20to>) 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 at haskell.org <mailto:ghc-devs at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs <http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs>
> 
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org <mailto:ghc-devs at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs <http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210915/38b4fd0f/attachment.html>