<div dir="ltr">Hello,<div><br></div><div>I've seen instances of this problem show up over and over again, and I think that there is a more principled solution, based on the idea of `improvement`.</div><div>The idea is to allow programmers to specify custom improvements.  Functional dependencies are one way to do this, but there is no reason why this</div><div>should be the only way.   The details of this idea are explained in this paper: "Simplifying and Improving Qualified Types" (<a href="http://web.cecs.pdx.edu/~mpj/pubs/RR-1040.pdf">http://web.cecs.pdx.edu/~mpj/pubs/RR-1040.pdf</a>).</div><div><br></div><div>In concrete Haskell syntax, this might work like this:</div><div><br></div><div>1. Add a new declaration:</div><div><br></div><div>  improve CS using EQs</div><div><br></div><div>Here the `CS` are a collection of constraints, and the `EQs` are a collection of equations.</div><div><br></div><div>2. Modify the constraint solver, so that when it sees `CS` in the inert set, it will emit the `EQs` as derived constraints.</div><div><br></div><div>This is all.  </div><div><br></div><div>So now you can write things like this:</div><div><br></div><div>    improve PolyMonad a b Identity using (a ~ Identity, b ~ Identity)</div><div><br></div><div>This tells GHC that it is OK to assume that if the final result is `Identity`,</div><div>then the first two arguments will also be in the identity monad.</div><div><br></div><div>This is a fairly conservative extension, in that it is only used to instantiate variables,</div><div>and it never needs to produce new equality proofs.  This is pretty much exactly how FDs work</div><div>in the current implementation of GHC.  For example, the declaration:</div><div><br></div><div>    class C a b | a -> b where ...</div><div><br></div><div>with GHC's current implementation, is exactly equivalent to:</div><div><br></div><div>    class C a b where ...</div><div>    improve (C a b, C a c) using (b ~ c)</div><div><br></div><div>Aside: GHC actually checks that all instances are consistent with the FD declarations,</div><div>so GHC *could* use them to actually generate new evidence, but it does not do so at the moment.</div><div><br></div><div>Anyway, implementing something like this should not be too hard, and it seems that it could be</div><div>used not just for the PolyMonads work, but also for other cases where one wants to write</div><div>specific improvements.</div><div><br></div><div>-Iavor</div><div><br></div><div>PS:  with GHC's current approach to resolving instances, you could also avoid some of the</div><div>ambiguities for the `Identity` instance by writing it like this:</div><div>   </div><div>    instance (a ~ Identity, b ~ Idnetity) => PolyMonad a b Identity where ...</div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><br></div><div><div><br></div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Mar 2, 2015 at 8:38 AM, Jan Bracker <span dir="ltr"><<a href="mailto:jan.bracker@googlemail.com" target="_blank">jan.bracker@googlemail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Adam,<div><br></div><div>again thank you for your extensive and patient answer!</div><div><br></div><div class="gmail_extra"><div class="gmail_quote"><span class=""><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
It's a bit hard to know exactly what is going on without the full code,<br>
but I think what is happening is this: you have an unsolved constraint<br>
`Polymonad Identity n_abpq Identity` and your plugin provides an<br>
evidence term of type `Polymonad Identity Identity Identity`, but of<br>
course this is ill-typed, because `n_abpq` is not `Identity`. Hence Core<br>
Lint quite reasonably complains.<br></blockquote><div><br></div></span><div>I would have thought the constraint solver would derive that 'obviously'</div><div>`n_abpq` needs to be unified with `Identity` and substitutes.</div><span class=""><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">I'm not sure exactly what you are trying to do, but I think the right<br>
way to approach this problem is to simulate a functional dependency on<br>
Polymonad (in fact, can you use an actual functional dependency)?</blockquote><div><br></div></span><div>That is exactly what I _don't_ want to do. I am trying to achieve a more </div><div>general version of monads, called polymonads as it was introduced here [1].</div><span class=""><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"> When confronted with the constraint `Polymonad Identity n_abpq Identity`, do<br>
not try to solve it directly, but instead notice that you must have<br>
`n_abpq ~ Identity`. Your plugin can emit this as an additional derived<br>
constraint, which will allow GHC's built-in solver to instantiate the<br>
unification variable `n_abpq` and then solve the original constraint<br>
using the existing instance. No manual evidence generation needed!<br></blockquote><div><br></div></span><div>Yes, that makes perfect sense! I was so gridlocked, I did not see this as a</div><div>possibility to solve the problem.</div><span class=""><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Out of interest, can you say anything about your aims here? I'm keen to<br>
find out about the range of applications of typechecker plugins.<br></blockquote><div><br></div></span><div>I want to make Polymonads as proposed in [1] usable in Haskell. They generalize</div><div>the bind operator to a more general signature `M a -> (a -> N b) -> P b`. Polymonads</div><div>subsume the standard Monad as well as indexed or parameterized monad, without </div><div>relying on functional dependencies, which can be limiting (there may be different </div><div>requirement depending on the monad being implemented).</div><div>Currently I am providing a type class for this:</div><div><br></div><div><span class=""><div>class Polymonad m n p where</div></span><div>  (>>=) :: m a -> (a -> n b) -> p b</div></div><div><br></div><div>As the paper points out in section 4.2 (Ambiguity), type inference breaks down,</div><div>because the constraint solver is not able to solve the ambiguity. Here a small example:</div><div><br></div><div>-- Return operator for the IO polymonad</div><div>instance Polymonad Identity Identity IO where </div><div>  -- ...</div><div><br></div><div>-- Identity polymonad</div><span class=""><div>instance Polymonad Identity Identity Identity where </div></span><div>  -- ...</div><div><br></div><div>return :: (Polymonad Identity Identity m) => a -> m a</div><div>return x = Identity x >>= Identity</div><div><br></div><div><div>test :: Identity Bool</div><div>test = do</div><div>  x <- return True</div><div>  return x</div></div><div><br></div><div>For this example GHC already gives the following ambiguity errors:</div><div><br></div><div><div>Main.hs:134:3:</div><div>    No instance for (Polymonad m0 n0 Identity)</div><div>      arising from a do statement</div><div>    The type variables ‘m0’, ‘n0’ are ambiguous</div><div>    Note: there is a potential instance available:</div><span class=""><div>      instance Polymonad Identity Identity Identity</div></span><div>        -- Defined in ‘Polymonad’</div><div>    In a stmt of a 'do' block: x <- return True</div><div>    In the expression:</div><div>      do { x <- return True;</div><div>           return x }</div><div>    In an equation for ‘test’:</div><div>        test</div><div>          = do { x <- return True;</div><div>                 return x }</div><div><br></div><div>Main.hs:134:8:</div><div>    No instance for (Polymonad Identity Identity m0)</div><div>      arising from a use of ‘return’</div><div>    The type variable ‘m0’ is ambiguous</div><div>    Note: there are several potential instances:</div><span class=""><div>      instance Polymonad Identity Identity Identity</div></span><div>        -- Defined in ‘Polymonad’</div><div>      instance Polymonad Identity Identity IO -- Defined at Main.hs:85:10</div><div>    In a stmt of a 'do' block: x <- return True</div><div>    In the expression:</div><div>      do { x <- return True;</div><div>           return x }</div><div>    In an equation for ‘test’:</div><div>        test</div><div>          = do { x <- return True;</div><div>                 return x }</div><div><br></div><div>Main.hs:135:3:</div><div>    No instance for (Polymonad Identity Identity n0)</div><div>      arising from a use of ‘return’</div><div>    The type variable ‘n0’ is ambiguous</div><div>    Note: there are several potential instances:</div><span class=""><div>      instance Polymonad Identity Identity Identity</div></span><div>        -- Defined in ‘Polymonad’</div><div>      instance Polymonad Identity Identity IO -- Defined at Main.hs:85:10</div><div>    In a stmt of a 'do' block: return x</div><div>    In the expression:</div><div>      do { x <- return True;</div><div>           return x }</div><div>    In an equation for ‘test’:</div><div>        test</div><div>          = do { x <- return True;</div><div>                 return x }</div></div><div><br></div><div>Of course, in the given example we can fix the ambiguity by adding type annotations.</div><div>But as soon as the examples become bigger that is not possible anymore.</div><div><br></div><div>Using the approach of the paper [1] these constraints are solvable unambiguously.</div><div>That's what I am working on.</div><div><br></div><div>All the best,</div><div>Jan</div><div><br></div><div>[1]: <a href="http://arxiv.org/pdf/1406.2060v1.pdf" target="_blank">http://arxiv.org/pdf/1406.2060v1.pdf</a></div><div><div class="h5"><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div><div>
On 26/02/15 10:07, Jan Bracker wrote:<br>
> Hi Adam,<br>
><br>
> thank you for your quick and detailed answer! I think I understand how<br>
> to construct evidence for typeclass constraints now. But trying to apply<br>
> this, I still have some problems.<br>
><br>
> I have something along the following lines:<br>
><br>
> class Polymonad m n p where<br>
>   -- Functions<br>
><br>
> instance Polymonad Identity Identity Identity where<br>
>   -- Implementation<br>
><br>
> -- Further instances and some small chunk of code involving them:<br>
><br>
> The code implies the following constraint:<br>
> Polymonad Identity n_abpq Identity<br>
><br>
> As the ambiguity error I get says, when trying to compile this: There is<br>
> only one matching instance (the one above, lets call<br>
> it $fPolymonadIdentityIdentityIdentity).<br>
><br>
> So my plugin tries to tell GHC to use that instance. As far as I<br>
> understand it, since the parameters<br>
> of $fPolymonadIdentityIdentityIdentity are no type variables and there<br>
> is no superclass it should be as easy as saying:<br>
> EvDFunApp $fPolymonadIdentityIdentityIdentity [] []<br>
><br>
> But when I run this with -dcore-lint I get the following error message:<br>
><br>
> *** Core Lint errors : in result of Desugar (after optimization) ***<br>
> <no location info>: Warning:<br>
>     In the expression: >><br>
>                          @ Identity<br>
>                          @ Any<br>
>                          @ Identity<br>
>                          $fPolymonadIdentityIdentityIdentity<br>
>                          @ ()<br>
>                          @ ()<br>
>                          (idOp @ Bool True)<br>
>                          (>>=<br>
>                             @ Identity<br>
>                             @ Identity<br>
>                             @ Any<br>
>                             $fPolymonadIdentityIdentityIdentity<br>
>                             @ Char<br>
>                             @ ()<br>
>                             (return<br>
>                                @ Char @ Identity<br>
> $fPolymonadIdentityIdentityIdentity (C# 'a'))<br>
>                             (\ _ [Occ=Dead] -><br>
>                                return @ () @ Identity<br>
> $fPolymonadIdentityIdentityIdentity ()))<br>
>     Argument value doesn't match argument type:<br>
>     Fun type:<br>
>         Polymonad Identity Any Identity =><br>
>         forall a_abdV[sk] b_abdW[sk].<br>
>         Identity a_abdV[sk] -> Any b_abdW[sk] -> Identity b_abdW[sk]<br>
>     Arg type: Polymonad Identity Identity Identity<br>
>     Arg: $fPolymonadIdentityIdentityIdentity<br>
><br>
> What am I missing? Why doesn't the argument type "Polymonad Identity<br>
> Identity Identity" match the first argument of the function type<br>
> "Polymonad Identity Any Identity => forall a_abdV[sk] b_abdW[sk].<br>
> Identity a_abdV[sk] -> Any b_abdW[sk] -> Identity b_abdW[sk]". Why is<br>
> the type variable translated to "Any"?<br>
><br>
> Best,<br>
> Jan<br>
<br>
</div></div><div><div>--<br>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
</div></div></blockquote></div></div></div><br></div></div>
<br>_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
<br></blockquote></div><br></div>