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 <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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170911/c9a0dad5/attachment.html>