More type safety in Core?

Callan McGill callan.mcgill at gmail.com
Tue Sep 14 21:43:37 UTC 2021


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

Best,
Callan

On Tue, 14 Sept 2021 at 15:44, Richard Eisenberg <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/
>   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 <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)
> 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
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> 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/20210914/ed5e08ca/attachment.html>


More information about the ghc-devs mailing list