A type checker plugin for row types

[Adam Gundry]

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/