On September 11, 2017 9:34:15 AM GMT+01:00, Adam Gundry <a...@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@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
