A type checker plugin for row types

[Ben Gamari]

On September 11, 2017 9:34:15 AM GMT+01:00, Adam Gundry <adam at well-typed.com> 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 at 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