More type safety in Core?

[Callan McGill]

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>