> On Sep 14, 2021, at 5:43 PM, Callan McGill <callan.mcg...@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 <li...@richarde.dev > <mailto: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/ > > <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 <arifords...@gmail.com >> <mailto: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 >> >> <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 <mailto:ghc-devs@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@haskell.org <mailto:ghc-devs@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
