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