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

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

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

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

On September 11, 2017 9:34:15 AM GMT+01:00, Adam Gundry 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 ghc-devs@haskell.org 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 ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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

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 < matthewtpickering@gmail.com> 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 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#...

...

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

...

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

bit 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

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 < nicolas.frisby@gmail.com> 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 ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs