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 <li...@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 <arifords...@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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
