A type checker plugin for row types

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
17 messages Options
Reply | Threaded
Open this post in threaded view
|

A type checker plugin for row types

Nicolas Frisby
Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Ara Adkins
Just given this a read! 

It looks like you’ve put a fantastic amount of effort into this so far, and I can certainly see how it’s finding its legs! I’m very much looking forward to seeing this develop further. I can definitely foresee some uses for polykinded column types, and the possibility for named arguments is certainly interesting (though I have some concerns about performance — though none are relevant at such an early stage). 

Unfortunately I don’t think I can answer any of the questions that I spotted on my read-through. 

Again, I’m looking forward to seeing this develop, and the naming of `coxswain` and `sculls` gave me a giggle. 

_ara

On 10 Sep 2017, at 23:24, Nicolas Frisby <[hidden email]> wrote:

Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Nicolas Frisby
Whoops! I forgot about that section of my draft. I added a little blurb ("Performance?") Thanks Ara!



On Sun, Sep 10, 2017 at 3:41 PM Ara Adkins <[hidden email]> wrote:
Just given this a read! 

It looks like you’ve put a fantastic amount of effort into this so far, and I can certainly see how it’s finding its legs! I’m very much looking forward to seeing this develop further. I can definitely foresee some uses for polykinded column types, and the possibility for named arguments is certainly interesting (though I have some concerns about performance — though none are relevant at such an early stage). 

Unfortunately I don’t think I can answer any of the questions that I spotted on my read-through. 

Again, I’m looking forward to seeing this develop, and the naming of `coxswain` and `sculls` gave me a giggle. 

_ara

On 10 Sep 2017, at 23:24, Nicolas Frisby <[hidden email]> wrote:

Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Ara Adkins
Glad I could be of help! I just gave it a read and that generated core is much better than I expected. I’d still have some concerns regarding certain uses (e.g. named arguments) having more performance overhead than hoped, but at this stage it’s far better than I would’ve initially thought! 

Definitely a useful addition to the wiki page. 

_ara

On 10 Sep 2017, at 23:58, Nicolas Frisby <[hidden email]> wrote:

Whoops! I forgot about that section of my draft. I added a little blurb ("Performance?") Thanks Ara!



On Sun, Sep 10, 2017 at 3:41 PM Ara Adkins <[hidden email]> wrote:
Just given this a read! 

It looks like you’ve put a fantastic amount of effort into this so far, and I can certainly see how it’s finding its legs! I’m very much looking forward to seeing this develop further. I can definitely foresee some uses for polykinded column types, and the possibility for named arguments is certainly interesting (though I have some concerns about performance — though none are relevant at such an early stage). 

Unfortunately I don’t think I can answer any of the questions that I spotted on my read-through. 

Again, I’m looking forward to seeing this develop, and the naming of `coxswain` and `sculls` gave me a giggle. 

_ara

On 10 Sep 2017, at 23:24, Nicolas Frisby <[hidden email]> wrote:

Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Iavor Diatchki
Hello Nick,

very nice!  Do you have any thoughts on how to use rows in class/type family declarations (i.e. how do we match on them)?  For example, if I was to use the rows to make up some sort of record, system (i.e. declare `Rec :: Row -> Type`), how might I define the `Show` instance for `Rec`?

-Iavor



On Mon, Sep 11, 2017 at 12:10 AM Ara Adkins <[hidden email]> wrote:
Glad I could be of help! I just gave it a read and that generated core is much better than I expected. I’d still have some concerns regarding certain uses (e.g. named arguments) having more performance overhead than hoped, but at this stage it’s far better than I would’ve initially thought! 

Definitely a useful addition to the wiki page. 


_ara

On 10 Sep 2017, at 23:58, Nicolas Frisby <[hidden email]> wrote:

Whoops! I forgot about that section of my draft. I added a little blurb ("Performance?") Thanks Ara!



On Sun, Sep 10, 2017 at 3:41 PM Ara Adkins <[hidden email]> wrote:
Just given this a read! 

It looks like you’ve put a fantastic amount of effort into this so far, and I can certainly see how it’s finding its legs! I’m very much looking forward to seeing this develop further. I can definitely foresee some uses for polykinded column types, and the possibility for named arguments is certainly interesting (though I have some concerns about performance — though none are relevant at such an early stage). 

Unfortunately I don’t think I can answer any of the questions that I spotted on my read-through. 

Again, I’m looking forward to seeing this develop, and the naming of `coxswain` and `sculls` gave me a giggle. 

_ara

On 10 Sep 2017, at 23:24, Nicolas Frisby <[hidden email]> wrote:

Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Adam Gundry-2
In reply to this post by Nicolas Frisby
Hi Nick,

This is great work, and I look forward to seeing the code once it is
ready. I've had a quick glance over your wiki page, and thought I should
send you some initial comments, though it deserves deeper attention
which I will try to find time to give it. :-)

I don't see a reference to Iavor's paper "Improving Haskell Types with
SMT" (http://yav.github.io/publications/improving-smt-types.pdf). If
you've not come across it, it might give a useful alternative
perspective on how plugins work, especially with regard to derived
constraints.

The following is based on my faulty memory, so apologies if it is out of
date or misleading...

> When/where exactly do Derived constraints arise?

Suppose I have a class with an equality superclass

    class a ~ b => C a b

and a wanted constraint `C alpha Int`, for some touchable variable
`alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the
superclass (derived means we don't actually need evidence for it in
order to build the core term, but solving it might help fill in some
touchable variables).  Sorry if this is obvious and not exact enough!

> When do touchables "naturally" arise in Given constraints?

Do you mean "touchable" or "unification variable" here (and elsewhere?).
A skolem is always untouchable, but the converse is not true.

I think that unification variables can arise in Given constraints, but
that they will always be untouchable. Suppose we have defined

    f :: forall a b . ((a ~ b) => a -> b) -> Int

(never mind that it is ambiguous) and consider type-checking the call `f
id`. We end up checking `id` against type `a -> b` with given `a ~ b`
where `a` and `b` are unification variables. They must be untouchable,
however, otherwise we might unify them, which would be wrong.

Hope this helps,

Adam


On 10/09/17 23:24, Nicolas Frisby wrote:

> Hi all. I've been spending my free time for the last couple months on a
> type checker plugin for row types. The free time waxes and wanes;
> sending an email like this one was my primary goal for the past couple
> weeks.
>
> At the very least, I hoped this project would let me finally get some
> hands on experience with OutsideIn. And I definitely have. But I've also
> made more progress than I anticipated, and I think the plugin is
> starting to have legs!
>
> I haven't uploaded the code yet to github -- it's not quite ready to
> share. But I did do a write up on the dev wiki.
>
>  
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>
> I would really appreciate and questions, comments, and --- boy, oh boy
> --- answers.
>
> I hope to upload within a week or so, and I'll update that wiki page and
> reply to this email when I do.
>
> Thanks very much. -Nick
>
> P.S. -- I've CC'd and BCC'd people who I anticipate would be
> specifically interested in this (e.g. plugins, row types, etc). Please
> feel free to forward to others that come to mind; I know some inboxes
> abjectly can't afford default list traffic.
>
> P.P.S. -- One hold up for the upload is: which license? I intend to
> release under BSD3, mainly to match GHC since one ideal scenario would
> involve being packaged with/integrated into GHC. But my brief recent
> research suggests that the Apache license might be more conducive to
> eventual widespread adoption. If you'd be willing to advise or even just
> refer me to other write ups, please feel free to email me directly or to
> start a separate thread on a more appropriate distribution list (CC'ing
> me, please). Thanks again.


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Iavor Diatchki

Ah, yes, derived constraints.  The mapping to logic I have in my mind is as follows:

Given = assumption, used in proofs
Wanted = goal, needs proof
Derived = implied by assumptions and goals

A derived constraint may be used to instantiate touchable unification variables, and guarantees that in doing so we are not loosing any generally.

Consider, for example, a wanted: `(x + 5) ~ 8`.  From this we can generate a new derived constraint `x ~ 3`, which would allow GHC to instantiate `x` to 3. 

A derived constraint could also be used to detect that the current set of goals is inconsistent, for example if we got a derived constraint equivalent to False, we would immediately know that the current set of goals has no solution.

-Iavor


On Mon, Sep 11, 2017, 9:35 AM Adam Gundry <[hidden email]> wrote:
Hi Nick,

This is great work, and I look forward to seeing the code once it is
ready. I've had a quick glance over your wiki page, and thought I should
send you some initial comments, though it deserves deeper attention
which I will try to find time to give it. :-)

I don't see a reference to Iavor's paper "Improving Haskell Types with
SMT" (http://yav.github.io/publications/improving-smt-types.pdf). If
you've not come across it, it might give a useful alternative
perspective on how plugins work, especially with regard to derived
constraints.

The following is based on my faulty memory, so apologies if it is out of
date or misleading...

> When/where exactly do Derived constraints arise?

Suppose I have a class with an equality superclass

    class a ~ b => C a b

and a wanted constraint `C alpha Int`, for some touchable variable
`alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the
superclass (derived means we don't actually need evidence for it in
order to build the core term, but solving it might help fill in some
touchable variables).  Sorry if this is obvious and not exact enough!

> When do touchables "naturally" arise in Given constraints?

Do you mean "touchable" or "unification variable" here (and elsewhere?).
A skolem is always untouchable, but the converse is not true.

I think that unification variables can arise in Given constraints, but
that they will always be untouchable. Suppose we have defined

    f :: forall a b . ((a ~ b) => a -> b) -> Int

(never mind that it is ambiguous) and consider type-checking the call `f
id`. We end up checking `id` against type `a -> b` with given `a ~ b`
where `a` and `b` are unification variables. They must be untouchable,
however, otherwise we might unify them, which would be wrong.

Hope this helps,

Adam


On 10/09/17 23:24, Nicolas Frisby wrote:
> Hi all. I've been spending my free time for the last couple months on a
> type checker plugin for row types. The free time waxes and wanes;
> sending an email like this one was my primary goal for the past couple
> weeks.
>
> At the very least, I hoped this project would let me finally get some
> hands on experience with OutsideIn. And I definitely have. But I've also
> made more progress than I anticipated, and I think the plugin is
> starting to have legs!
>
> I haven't uploaded the code yet to github -- it's not quite ready to
> share. But I did do a write up on the dev wiki.
>
>
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>
> I would really appreciate and questions, comments, and --- boy, oh boy
> --- answers.
>
> I hope to upload within a week or so, and I'll update that wiki page and
> reply to this email when I do.
>
> Thanks very much. -Nick
>
> P.S. -- I've CC'd and BCC'd people who I anticipate would be
> specifically interested in this (e.g. plugins, row types, etc). Please
> feel free to forward to others that come to mind; I know some inboxes
> abjectly can't afford default list traffic.
>
> P.P.S. -- One hold up for the upload is: which license? I intend to
> release under BSD3, mainly to match GHC since one ideal scenario would
> involve being packaged with/integrated into GHC. But my brief recent
> research suggests that the Apache license might be more conducive to
> eventual widespread adoption. If you'd be willing to advise or even just
> refer me to other write ups, please feel free to email me directly or to
> start a separate thread on a more appropriate distribution list (CC'ing
> me, please). Thanks again.


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Ben Gamari-2
In reply to this post by Adam Gundry-2
On September 11, 2017 9:34:15 AM GMT+01:00, Adam Gundry <[hidden email]> wrote:

>Hi Nick,
>
>This is great work, and I look forward to seeing the code once it is
>ready. I've had a quick glance over your wiki page, and thought I
>should
>send you some initial comments, though it deserves deeper attention
>which I will try to find time to give it. :-)
>
>I don't see a reference to Iavor's paper "Improving Haskell Types with
>SMT" (http://yav.github.io/publications/improving-smt-types.pdf). If
>you've not come across it, it might give a useful alternative
>perspective on how plugins work, especially with regard to derived
>constraints.
>
>The following is based on my faulty memory, so apologies if it is out
>of
>date or misleading...
>
>> When/where exactly do Derived constraints arise?
>
>Suppose I have a class with an equality superclass
>
>    class a ~ b => C a b
>
>and a wanted constraint `C alpha Int`, for some touchable variable
>`alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the
>superclass (derived means we don't actually need evidence for it in
>order to build the core term, but solving it might help fill in some
>touchable variables).  Sorry if this is obvious and not exact enough!
>
>> When do touchables "naturally" arise in Given constraints?
>
>Do you mean "touchable" or "unification variable" here (and
>elsewhere?).
>A skolem is always untouchable, but the converse is not true.
>
>I think that unification variables can arise in Given constraints, but
>that they will always be untouchable. Suppose we have defined
>
>    f :: forall a b . ((a ~ b) => a -> b) -> Int
>
>(never mind that it is ambiguous) and consider type-checking the call
>`f
>id`. We end up checking `id` against type `a -> b` with given `a ~ b`
>where `a` and `b` are unification variables. They must be untouchable,
>however, otherwise we might unify them, which would be wrong.
>
>Hope this helps,
>
>Adam
>
>
>On 10/09/17 23:24, Nicolas Frisby wrote:
>> Hi all. I've been spending my free time for the last couple months on
>a
>> type checker plugin for row types. The free time waxes and wanes;
>> sending an email like this one was my primary goal for the past
>couple
>> weeks.
>>
>> At the very least, I hoped this project would let me finally get some
>> hands on experience with OutsideIn. And I definitely have. But I've
>also
>> made more progress than I anticipated, and I think the plugin is
>> starting to have legs!
>>
>> I haven't uploaded the code yet to github -- it's not quite ready to
>> share. But I did do a write up on the dev wiki.
>>
>>  
>>
>https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>>
>> I would really appreciate and questions, comments, and --- boy, oh
>boy
>> --- answers.
>>
>> I hope to upload within a week or so, and I'll update that wiki page
>and
>> reply to this email when I do.
>>
>> Thanks very much. -Nick
>>
>> P.S. -- I've CC'd and BCC'd people who I anticipate would be
>> specifically interested in this (e.g. plugins, row types, etc).
>Please
>> feel free to forward to others that come to mind; I know some inboxes
>> abjectly can't afford default list traffic.
>>
>> P.P.S. -- One hold up for the upload is: which license? I intend to
>> release under BSD3, mainly to match GHC since one ideal scenario
>would
>> involve being packaged with/integrated into GHC. But my brief recent
>> research suggests that the Apache license might be more conducive to
>> eventual widespread adoption. If you'd be willing to advise or even
>just
>> refer me to other write ups, please feel free to email me directly or
>to
>> start a separate thread on a more appropriate distribution list
>(CC'ing
>> me, please). Thanks again.
>
>
>--
>Adam Gundry, Haskell Consultant
>Well-Typed LLP, http://www.well-typed.com/
>_______________________________________________
>ghc-devs mailing list
>[hidden email]
>http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

It would be great if someone could extract the conclusion of this thread into a Note. Clearly there is a hole in the current state of our source documentation.

Cheers,

- Ben
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Nicolas Frisby
In reply to this post by Adam Gundry-2
Adam, thanks for:

1) The reference to Iavor's paper --- it is a nice more-detailed description of the plugin API/semantics, and the Nelson-Oppen parallel is very illuminating!

2) Asking "Do you mean "touchable" or "unification variable" here and elsewhere?"

That prompted me to finally dig deeper into something, and I've updated/simplified the wiki page accordingly. Basically, I was just using newFlexiTyVar (since it's pretty much the only option in the "official" TcPluginsM interface) without understanding if it's the touchability or the skolem-vs-unification status that was enabling the Given-Given interactions. I'm happy to report that touchability apparently has nothing to do with any of my test cases (including the record and variant library, etc). I'm relieved about that: touchability is a restriction on unification, and my general goal with my plugin architecture is to leave as many of the unification details to GHC's type equality solver as possible.

Thanks. -Nick

On Mon, Sep 11, 2017 at 1:34 AM Adam Gundry <[hidden email]> wrote:
Hi Nick,

This is great work, and I look forward to seeing the code once it is
ready. I've had a quick glance over your wiki page, and thought I should
send you some initial comments, though it deserves deeper attention
which I will try to find time to give it. :-)

I don't see a reference to Iavor's paper "Improving Haskell Types with
SMT" (http://yav.github.io/publications/improving-smt-types.pdf). If
you've not come across it, it might give a useful alternative
perspective on how plugins work, especially with regard to derived
constraints.

The following is based on my faulty memory, so apologies if it is out of
date or misleading...

> When/where exactly do Derived constraints arise?

Suppose I have a class with an equality superclass

    class a ~ b => C a b

and a wanted constraint `C alpha Int`, for some touchable variable
`alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the
superclass (derived means we don't actually need evidence for it in
order to build the core term, but solving it might help fill in some
touchable variables).  Sorry if this is obvious and not exact enough!

> When do touchables "naturally" arise in Given constraints?

Do you mean "touchable" or "unification variable" here (and elsewhere?).
A skolem is always untouchable, but the converse is not true.

I think that unification variables can arise in Given constraints, but
that they will always be untouchable. Suppose we have defined

    f :: forall a b . ((a ~ b) => a -> b) -> Int

(never mind that it is ambiguous) and consider type-checking the call `f
id`. We end up checking `id` against type `a -> b` with given `a ~ b`
where `a` and `b` are unification variables. They must be untouchable,
however, otherwise we might unify them, which would be wrong.

Hope this helps,

Adam


On 10/09/17 23:24, Nicolas Frisby wrote:
> Hi all. I've been spending my free time for the last couple months on a
> type checker plugin for row types. The free time waxes and wanes;
> sending an email like this one was my primary goal for the past couple
> weeks.
>
> At the very least, I hoped this project would let me finally get some
> hands on experience with OutsideIn. And I definitely have. But I've also
> made more progress than I anticipated, and I think the plugin is
> starting to have legs!
>
> I haven't uploaded the code yet to github -- it's not quite ready to
> share. But I did do a write up on the dev wiki.
>
>
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>
> I would really appreciate and questions, comments, and --- boy, oh boy
> --- answers.
>
> I hope to upload within a week or so, and I'll update that wiki page and
> reply to this email when I do.
>
> Thanks very much. -Nick
>
> P.S. -- I've CC'd and BCC'd people who I anticipate would be
> specifically interested in this (e.g. plugins, row types, etc). Please
> feel free to forward to others that come to mind; I know some inboxes
> abjectly can't afford default list traffic.
>
> P.P.S. -- One hold up for the upload is: which license? I intend to
> release under BSD3, mainly to match GHC since one ideal scenario would
> involve being packaged with/integrated into GHC. But my brief recent
> research suggests that the Apache license might be more conducive to
> eventual widespread adoption. If you'd be willing to advise or even just
> refer me to other write ups, please feel free to email me directly or to
> start a separate thread on a more appropriate distribution list (CC'ing
> me, please). Thanks again.


--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Richard Eisenberg-4
In reply to this post by Ben Gamari-2
Here are my stabs at answers to two of your questions.

> • When/where exactly do Derived constraints arise? I'm not recognizing them in the OutsideIn paper.

I agree with others' comments on this point, but perhaps I can expand. A Derived constraint is essentially a Wanted constraint, but one where there is no need for evidence. They arise for several reasons:

- If we have Ord a as a Wanted, then we'll get Eq a (a superclass constraint) as a Derived. While GHC has no need for an Eq a dictionary, perhaps solving the Eq a constraint will help us solve the Ord a constraint. So the Eq a is Derived.

- Functional dependencies and type family dependencies give rise to Derived constraints. That is, if we have class C a b | a -> b, instance C Int Bool, and [W] C Int a, then we'll get [D] a ~ Bool.

- GHC says that Wanteds cannot rewrite Wanteds. That is, if we have [W] a ~ Bool and [W] a ~ Int, we *don't* want GHC to simplify to [W] Int ~ Bool and then report that. It's very confusing to users! However, sometimes, (I don't have an example) we need Wanteds to rewrite Wanteds in order to make progress. So GHC clones Wanteds into Deriveds, and says that Deriveds *can* rewrite Deriveds. Perhaps after a lot of rewriting, some variables will unify, and then GHC can make progress on the Wanteds. Of course, all this cloning would be non-performant, so GHC essentially does a copy-on-write implementation, where many constraints are [WD], both Wanted and Derived.

While Deriveds *arise* for several reasons, they contribute back to the world in only one: unification. That is, the whole point of Deriveds is so that GHC will discover [D] a ~ Int and then set a := Int.

> • GHC has various kinds of variable and skolem (e.g. signature skolem) that I'm not recognizing in the OutsideIn paper. Is there a comprehensive discussion of them all?

I'm unaware of one, but here are some pointers.

- A skolem tends to be a user-written type variable, unifiable with no other. If you have a declaration (id :: a -> b; id x = x), GHC will reject because it won't unify a with b. a and b are skolems.

- GHC also has "super-skolems", which have a slightly different behavior w.r.t. instances. See Note [Binding when looking up instances] in InstEnv. I've never had to care about this distinction.

- GHC has several different types of unification variables (= metavars).

  * A TauTv is your regular, run-of-the-mill unification variable. It can unify only with monotypes.

  * A SigTv is a metavar that can unify only with another variable. See Note [Signature skolems] in TcType for examples of why this is useful. (Editorial comment: I think the design around SigTvs is wrong, because generally there is a set of variables a given SigTv should not unify with. But GHC doesn't track this info.)

  * FlatMetaTvs and FlatSkolTvs are an implementation detail of how GHC deals with type families. They are documented in Note [The flattening story] in TcFlatten.

I think that's it, but feel free to ask if you run into more.

(In case you're wondering, I didn't really look over the design you're proposing. I leave that to others.)

Good luck!
Richard

> On Sep 11, 2017, at 9:48 AM, Ben Gamari <[hidden email]> wrote:
>
> On September 11, 2017 9:34:15 AM GMT+01:00, Adam Gundry <[hidden email]> wrote:
>> Hi Nick,
>>
>> This is great work, and I look forward to seeing the code once it is
>> ready. I've had a quick glance over your wiki page, and thought I
>> should
>> send you some initial comments, though it deserves deeper attention
>> which I will try to find time to give it. :-)
>>
>> I don't see a reference to Iavor's paper "Improving Haskell Types with
>> SMT" (http://yav.github.io/publications/improving-smt-types.pdf). If
>> you've not come across it, it might give a useful alternative
>> perspective on how plugins work, especially with regard to derived
>> constraints.
>>
>> The following is based on my faulty memory, so apologies if it is out
>> of
>> date or misleading...
>>
>>> When/where exactly do Derived constraints arise?
>>
>> Suppose I have a class with an equality superclass
>>
>>   class a ~ b => C a b
>>
>> and a wanted constraint `C alpha Int`, for some touchable variable
>> `alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the
>> superclass (derived means we don't actually need evidence for it in
>> order to build the core term, but solving it might help fill in some
>> touchable variables).  Sorry if this is obvious and not exact enough!
>>
>>> When do touchables "naturally" arise in Given constraints?
>>
>> Do you mean "touchable" or "unification variable" here (and
>> elsewhere?).
>> A skolem is always untouchable, but the converse is not true.
>>
>> I think that unification variables can arise in Given constraints, but
>> that they will always be untouchable. Suppose we have defined
>>
>>   f :: forall a b . ((a ~ b) => a -> b) -> Int
>>
>> (never mind that it is ambiguous) and consider type-checking the call
>> `f
>> id`. We end up checking `id` against type `a -> b` with given `a ~ b`
>> where `a` and `b` are unification variables. They must be untouchable,
>> however, otherwise we might unify them, which would be wrong.
>>
>> Hope this helps,
>>
>> Adam
>>
>>
>> On 10/09/17 23:24, Nicolas Frisby wrote:
>>> Hi all. I've been spending my free time for the last couple months on
>> a
>>> type checker plugin for row types. The free time waxes and wanes;
>>> sending an email like this one was my primary goal for the past
>> couple
>>> weeks.
>>>
>>> At the very least, I hoped this project would let me finally get some
>>> hands on experience with OutsideIn. And I definitely have. But I've
>> also
>>> made more progress than I anticipated, and I think the plugin is
>>> starting to have legs!
>>>
>>> I haven't uploaded the code yet to github -- it's not quite ready to
>>> share. But I did do a write up on the dev wiki.
>>>
>>>
>>>
>> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>>>
>>> I would really appreciate and questions, comments, and --- boy, oh
>> boy
>>> --- answers.
>>>
>>> I hope to upload within a week or so, and I'll update that wiki page
>> and
>>> reply to this email when I do.
>>>
>>> Thanks very much. -Nick
>>>
>>> P.S. -- I've CC'd and BCC'd people who I anticipate would be
>>> specifically interested in this (e.g. plugins, row types, etc).
>> Please
>>> feel free to forward to others that come to mind; I know some inboxes
>>> abjectly can't afford default list traffic.
>>>
>>> P.P.S. -- One hold up for the upload is: which license? I intend to
>>> release under BSD3, mainly to match GHC since one ideal scenario
>> would
>>> involve being packaged with/integrated into GHC. But my brief recent
>>> research suggests that the Apache license might be more conducive to
>>> eventual widespread adoption. If you'd be willing to advise or even
>> just
>>> refer me to other write ups, please feel free to email me directly or
>> to
>>> start a separate thread on a more appropriate distribution list
>> (CC'ing
>>> me, please). Thanks again.
>>
>>
>> --
>> Adam Gundry, Haskell Consultant
>> Well-Typed LLP, http://www.well-typed.com/
>> _______________________________________________
>> ghc-devs mailing list
>> [hidden email]
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> It would be great if someone could extract the conclusion of this thread into a Note. Clearly there is a hole in the current state of our source documentation.
>
> Cheers,
>
> - Ben
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: A type checker plugin for row types

GHC - devs mailing list
In reply to this post by Nicolas Frisby

Nick

 

Good work! 

 

You ask some questions about the constraint solver – I hope that the answer from others have helped. If not, do re-ask.

 

My main comment is: what does Core look like?  I think your answer is “No change to Core, but there are lots of unsafe coerces littered around”.   But even then I’m not sure.  Even

 

f :: Lacks r “f” => V (Row (r .& (“f” .= Int))) -> V (Row (r .& (“f” .= Int)))

f n x = ???

 

Somehow in the ??? I have to update field n of a tuple x.  How do I do that?

 

And I’m also very uncomfortable having Core littered with unsafeCoerces.   I like Core being statically typed.  What is the simplest primitive(s) we could add to Core to make it possible to express this stuff type-safely?

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Nicolas Frisby
Sent: 10 September 2017 23:25
To: [hidden email]
Cc: Andres Löh <[hidden email]>; Adam Gundry <[hidden email]>; Richard Eisenberg <[hidden email]>
Subject: A type checker plugin for row types

 

Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

 

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

 

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

 

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

 

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

 

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

 

Thanks very much. -Nick

 

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

 

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Nicolas Frisby
Hello Simon! Thanks for taking a look.

I've attempted to address your Core question by adding a new section to the wiki page: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain#SomeLightCoreSnorkeling

Regarding the necessary EvTerms, I haven't thought through that enough to answer. I'll add it to the wiki page.

Thanks. -Nick

On Fri, Sep 15, 2017 at 7:55 AM Simon Peyton Jones <[hidden email]> wrote:

Nick

 

Good work! 

 

You ask some questions about the constraint solver – I hope that the answer from others have helped. If not, do re-ask.

 

My main comment is: what does Core look like?  I think your answer is “No change to Core, but there are lots of unsafe coerces littered around”.   But even then I’m not sure.  Even

 

f :: Lacks r “f” => V (Row (r .& (“f” .= Int))) -> V (Row (r .& (“f” .= Int)))

f n x = ???

 

Somehow in the ??? I have to update field n of a tuple x.  How do I do that?

 

And I’m also very uncomfortable having Core littered with unsafeCoerces.   I like Core being statically typed.  What is the simplest primitive(s) we could add to Core to make it possible to express this stuff type-safely?

 

Simon

 

From: ghc-devs [mailto:[hidden email]] On Behalf Of Nicolas Frisby
Sent: 10 September 2017 23:25
To: [hidden email]
Cc: Andres Löh <[hidden email]>; Adam Gundry <[hidden email]>; Richard Eisenberg <[hidden email]>
Subject: A type checker plugin for row types

 

Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

 

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

 

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

 

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

 

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

 

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

 

Thanks very much. -Nick

 

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

 

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.


_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Nicolas Frisby
In reply to this post by Nicolas Frisby
I've uploaded the code to GitHub.


I went with a BSD3 licence.

It's still very much a work in progress, so I only recommend using it for experimentation for now.

Thanks. -Nick

On Sun, Sep 10, 2017 at 3:24 PM Nicolas Frisby <[hidden email]> wrote:
Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Ara Adkins
Excellent! I've very much been looking forward to having a look at the code for this!

On Sat, Sep 16, 2017 at 10:27 PM, Nicolas Frisby <[hidden email]> wrote:
I've uploaded the code to GitHub.


I went with a BSD3 licence.

It's still very much a work in progress, so I only recommend using it for experimentation for now.

Thanks. -Nick


On Sun, Sep 10, 2017 at 3:24 PM Nicolas Frisby <[hidden email]> wrote:
Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Nicolas Frisby
In reply to this post by Nicolas Frisby
If you'd like to see how exactly the plugin manipulates constraints, I suggest using the `summarize` and `trace` options that are discussed here:


Also, the `sculls/Examples.hs` and `sculls/Elm.hs` files contain my only test cases involving records and variants. Also see `coxswain/test/README`.

I'm kind of spent from rushing towards this "release", so I might be a bit less productive for a while. But I'll be generally responsive about it if others are spending time on it.

In particular: any advice for how to share the generated Haddock documentation without uploading to Hackage/Stackage?

And thanks to all for responding to my questions. I'll have to think harder about the answers given. At least for Derived constraints, in particular, I still don't think we have all of the relevant information in one place. For example, I recalling thinking that I was seeing some Derived constraints that seemed to arise from the unifier "giving up" on a complicated equality and emitting a Given equality instead, and nobody mentioned that in their answers here. I'll try to suss out a repro of that exactly.

Thanks. -Nick

On Sat, Sep 16, 2017 at 2:27 PM Nicolas Frisby <[hidden email]> wrote:
I've uploaded the code to GitHub.


I went with a BSD3 licence.

It's still very much a work in progress, so I only recommend using it for experimentation for now.

Thanks. -Nick


On Sun, Sep 10, 2017 at 3:24 PM Nicolas Frisby <[hidden email]> wrote:
Hi all. I've been spending my free time for the last couple months on a type checker plugin for row types. The free time waxes and wanes; sending an email like this one was my primary goal for the past couple weeks.

At the very least, I hoped this project would let me finally get some hands on experience with OutsideIn. And I definitely have. But I've also made more progress than I anticipated, and I think the plugin is starting to have legs!

I haven't uploaded the code yet to github -- it's not quite ready to share. But I did do a write up on the dev wiki.

  https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain

I would really appreciate and questions, comments, and --- boy, oh boy --- answers.

I hope to upload within a week or so, and I'll update that wiki page and reply to this email when I do.

Thanks very much. -Nick

P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically interested in this (e.g. plugins, row types, etc). Please feel free to forward to others that come to mind; I know some inboxes abjectly can't afford default list traffic.

P.P.S. -- One hold up for the upload is: which license? I intend to release under BSD3, mainly to match GHC since one ideal scenario would involve being packaged with/integrated into GHC. But my brief recent research suggests that the Apache license might be more conducive to eventual widespread adoption. If you'd be willing to advise or even just refer me to other write ups, please feel free to email me directly or to start a separate thread on a more appropriate distribution list (CC'ing me, please). Thanks again.

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Matthew Pickering
Hi Nicolas, I briefly tried out the plugin this morning and have a few comments.

1. The example file on the wiki page fails to compile. I needed to
modify two of the constraints on `getName` and `getPos` to get it to
work.

2. I was inspecting how well the compiler optimises your
representation and came across from very strange core that I didn't
understand.

https://gist.github.com/mpickering/6ec5501400e103d64284701d7537f223

Notice how there is a case on a lambda which binds an unused kind
variable. But I can't understand how this works at all as I can't see
where the lambda is applied.

3. Running -dcore-lint on the example file quickly complains.  I think
making sure that core-lint passes can be quite an important sanity
check, is a fundamental reason which makes core lint work poorly with
type checker plugins? If there is then we should perhaps fix this.

I also packaged up the project for nix if that is useful to anyone else.

https://gist.github.com/2a4b2fa25351bd900052d955a00ace6a

Matt

On Sat, Sep 16, 2017 at 11:00 PM, Nicolas Frisby
<[hidden email]> wrote:

> If you'd like to see how exactly the plugin manipulates constraints, I
> suggest using the `summarize` and `trace` options that are discussed here:
>
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain#PluginDebugOptions
>
> Also, the `sculls/Examples.hs` and `sculls/Elm.hs` files contain my only
> test cases involving records and variants. Also see `coxswain/test/README`.
>
> I'm kind of spent from rushing towards this "release", so I might be a bit
> less productive for a while. But I'll be generally responsive about it if
> others are spending time on it.
>
> In particular: any advice for how to share the generated Haddock
> documentation without uploading to Hackage/Stackage?
>
> And thanks to all for responding to my questions. I'll have to think harder
> about the answers given. At least for Derived constraints, in particular, I
> still don't think we have all of the relevant information in one place. For
> example, I recalling thinking that I was seeing some Derived constraints
> that seemed to arise from the unifier "giving up" on a complicated equality
> and emitting a Given equality instead, and nobody mentioned that in their
> answers here. I'll try to suss out a repro of that exactly.
>
> Thanks. -Nick
>
> On Sat, Sep 16, 2017 at 2:27 PM Nicolas Frisby <[hidden email]>
> wrote:
>>
>> I've uploaded the code to GitHub.
>>
>> https://github.com/nfrisby/coxswain
>>
>> I went with a BSD3 licence.
>>
>> It's still very much a work in progress, so I only recommend using it for
>> experimentation for now.
>>
>> Thanks. -Nick
>>
>>
>> On Sun, Sep 10, 2017 at 3:24 PM Nicolas Frisby <[hidden email]>
>> wrote:
>>>
>>> Hi all. I've been spending my free time for the last couple months on a
>>> type checker plugin for row types. The free time waxes and wanes; sending an
>>> email like this one was my primary goal for the past couple weeks.
>>>
>>> At the very least, I hoped this project would let me finally get some
>>> hands on experience with OutsideIn. And I definitely have. But I've also
>>> made more progress than I anticipated, and I think the plugin is starting to
>>> have legs!
>>>
>>> I haven't uploaded the code yet to github -- it's not quite ready to
>>> share. But I did do a write up on the dev wiki.
>>>
>>>
>>> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>>>
>>> I would really appreciate and questions, comments, and --- boy, oh boy
>>> --- answers.
>>>
>>> I hope to upload within a week or so, and I'll update that wiki page and
>>> reply to this email when I do.
>>>
>>> Thanks very much. -Nick
>>>
>>> P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically
>>> interested in this (e.g. plugins, row types, etc). Please feel free to
>>> forward to others that come to mind; I know some inboxes abjectly can't
>>> afford default list traffic.
>>>
>>> P.P.S. -- One hold up for the upload is: which license? I intend to
>>> release under BSD3, mainly to match GHC since one ideal scenario would
>>> involve being packaged with/integrated into GHC. But my brief recent
>>> research suggests that the Apache license might be more conducive to
>>> eventual widespread adoption. If you'd be willing to advise or even just
>>> refer me to other write ups, please feel free to email me directly or to
>>> start a separate thread on a more appropriate distribution list (CC'ing me,
>>> please). Thanks again.
>
>
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: A type checker plugin for row types

Nicolas Frisby
Thank you Matthew! I very much appreciate this kind of feedback.

1) I've updated the (bulk of the) wiki page to match the github repo just now. In particular, the "Elm" example lives here https://github.com/nfrisby/coxswain/blob/master/sculls/Elm.hs, so I just copied its most recent version onto the wiki. (The delta was the "off-by-one" `Short` constraints, right?)

2) I absolutely agree about -dcore-lint. I wrongly had it in my head that I needed a DEBUG build. See https://github.com/nfrisby/coxswain/issues/3#issuecomment-330266479

3) Awesome! I'll add a link to the README.

Thanks again. -Nick

On Mon, Sep 18, 2017 at 4:11 AM Matthew Pickering <[hidden email]> wrote:
Hi Nicolas, I briefly tried out the plugin this morning and have a few comments.

1. The example file on the wiki page fails to compile. I needed to
modify two of the constraints on `getName` and `getPos` to get it to
work.

2. I was inspecting how well the compiler optimises your
representation and came across from very strange core that I didn't
understand.

https://gist.github.com/mpickering/6ec5501400e103d64284701d7537f223

Notice how there is a case on a lambda which binds an unused kind
variable. But I can't understand how this works at all as I can't see
where the lambda is applied.

3. Running -dcore-lint on the example file quickly complains.  I think
making sure that core-lint passes can be quite an important sanity
check, is a fundamental reason which makes core lint work poorly with
type checker plugins? If there is then we should perhaps fix this.

I also packaged up the project for nix if that is useful to anyone else.

https://gist.github.com/2a4b2fa25351bd900052d955a00ace6a

Matt

On Sat, Sep 16, 2017 at 11:00 PM, Nicolas Frisby
<[hidden email]> wrote:
> If you'd like to see how exactly the plugin manipulates constraints, I
> suggest using the `summarize` and `trace` options that are discussed here:
>
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain#PluginDebugOptions
>
> Also, the `sculls/Examples.hs` and `sculls/Elm.hs` files contain my only
> test cases involving records and variants. Also see `coxswain/test/README`.
>
> I'm kind of spent from rushing towards this "release", so I might be a bit
> less productive for a while. But I'll be generally responsive about it if
> others are spending time on it.
>
> In particular: any advice for how to share the generated Haddock
> documentation without uploading to Hackage/Stackage?
>
> And thanks to all for responding to my questions. I'll have to think harder
> about the answers given. At least for Derived constraints, in particular, I
> still don't think we have all of the relevant information in one place. For
> example, I recalling thinking that I was seeing some Derived constraints
> that seemed to arise from the unifier "giving up" on a complicated equality
> and emitting a Given equality instead, and nobody mentioned that in their
> answers here. I'll try to suss out a repro of that exactly.
>
> Thanks. -Nick
>
> On Sat, Sep 16, 2017 at 2:27 PM Nicolas Frisby <[hidden email]>
> wrote:
>>
>> I've uploaded the code to GitHub.
>>
>> https://github.com/nfrisby/coxswain
>>
>> I went with a BSD3 licence.
>>
>> It's still very much a work in progress, so I only recommend using it for
>> experimentation for now.
>>
>> Thanks. -Nick
>>
>>
>> On Sun, Sep 10, 2017 at 3:24 PM Nicolas Frisby <[hidden email]>
>> wrote:
>>>
>>> Hi all. I've been spending my free time for the last couple months on a
>>> type checker plugin for row types. The free time waxes and wanes; sending an
>>> email like this one was my primary goal for the past couple weeks.
>>>
>>> At the very least, I hoped this project would let me finally get some
>>> hands on experience with OutsideIn. And I definitely have. But I've also
>>> made more progress than I anticipated, and I think the plugin is starting to
>>> have legs!
>>>
>>> I haven't uploaded the code yet to github -- it's not quite ready to
>>> share. But I did do a write up on the dev wiki.
>>>
>>>
>>> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>>>
>>> I would really appreciate and questions, comments, and --- boy, oh boy
>>> --- answers.
>>>
>>> I hope to upload within a week or so, and I'll update that wiki page and
>>> reply to this email when I do.
>>>
>>> Thanks very much. -Nick
>>>
>>> P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically
>>> interested in this (e.g. plugins, row types, etc). Please feel free to
>>> forward to others that come to mind; I know some inboxes abjectly can't
>>> afford default list traffic.
>>>
>>> P.P.S. -- One hold up for the upload is: which license? I intend to
>>> release under BSD3, mainly to match GHC since one ideal scenario would
>>> involve being packaged with/integrated into GHC. But my brief recent
>>> research suggests that the Apache license might be more conducive to
>>> eventual widespread adoption. If you'd be willing to advise or even just
>>> refer me to other write ups, please feel free to email me directly or to
>>> start a separate thread on a more appropriate distribution list (CC'ing me,
>>> please). Thanks again.
>
>
> _______________________________________________
> ghc-devs mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs