Re: More type safety in Core?

[Richard Eisenberg]

> On Sep 14, 2021, at 5:43 PM, Callan McGill  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 
> 

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  > 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 > > 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

Re: 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  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  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

Re: More type safety in Core?

[Richard Eisenberg]

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  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

RE: More type safety in Core?

[Simon Peyton Jones via ghc-devs]

One difficulty is that I think that writing Core-to-Core passes might become a 
lot more challenging.   It gets gnarly writing code that satisfies the type 
checker, depending of course on how strong the invariants are.

I think Typesafe runtime code 
generation<https://www.researchgate.net/publication/292674440_Type-safe_Runtime_Code_Generation_Accelerate_to_LLVM>
 has some material on this.

TL;DR: by all means give it a try.  I'm not terribly optimistic... but progress 
is made when we find that things we thought weren't possible are possible after 
all.  So I'd be happy to be proved wrong.

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point 
simo...@microsoft.com<mailto:simo...@microsoft.com> will cease to work.  Use 
simon.peytonjo...@gmail.com<mailto:simon.peytonjo...@gmail.com> instead.  (For 
now, it just forwards to simo...@microsoft.com.)

From: ghc-devs  On Behalf Of Ari Fordsham
Sent: 14 September 2021 13:39
To: ghc-devs@haskell.org
Subject: More type safety in Core?

You don't often get email from 
arifords...@gmail.com<mailto:arifords...@gmail.com>. Learn why this is 
important<http://aka.ms/LearnAboutSenderIdentification>
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<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fconal.net%2Fblog%2Fposts%2Foverloading-lambda%23%3A~%3Atext%3DHaskell%2520source%2520language.-%2CI%2C-originally%2520intended%2520to=04%7C01%7Csimonpj%40microsoft.com%7C3f5f8d3d0bc141e5a78408d9777ca375%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637672217369668112%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C2000=6IB9AcOy%2BzMmbVU51i9IenjPVA6usmeQE87j4Z1tXlk%3D=0>)
 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

Re: More type safety in Core?

[Ben Gamari]

Ari Fordsham  writes:

> I don't know if this is the right forum for this, I apologise if I'm
> intruding...
>
Indeed it is! No reason to apologise.

> 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.
>
I am unaware of any plans currently. In general changing GHC's Core
language (or even just its Haskell representation) is something that
doesn't happen very often and for good reason.

To me, giving the Core AST more precise types would be a very
significant undertaking (touching a good fraction of the compiler) and
it is not clear to me that it wouldn't have compiler performance
implications. Afterall, expression types are still runtime-relevant to
the compiler and therefore can't be dropped. Moreover, the lifted
equality constraints that your GADTs constructors would no doubt carry
do have a runtime representation.

It's also not clear that catching ill-formed Core statically would pay
its way given the inevitable bookkeeping that the more elaborate types
would involve; this is especially true given that typing expressions
won't eliminate the need for dynamic Core Linting, which would still be
necessary to check things like well-scoped-ness.

These are my high-level thoughts; to say anything more concrete we would
need to consider a concrete proposal. It is certainly an interesting
area to explore and while I may be skeptical I would love to be proven
wrong.

Cheers,

- Ben


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: More type safety in Core?

[Ari Fordsham]

Source for Eliott:
https://github.com/conal/lambda-ccc/blob/master/src/LambdaCCC/Lambda.hs

AF


On Tue, 14 Sept 2021 at 13:38, Ari Fordsham  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

More type safety in Core?

[Ari Fordsham]

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