<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"><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><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><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><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><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><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><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><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><div>class Polymonad m n p where</div><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><div>instance Polymonad Identity Identity Identity where </div><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><div> instance Polymonad Identity Identity Identity</div><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><div> instance Polymonad Identity Identity Identity</div><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><div> instance Polymonad Identity Identity Identity</div><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><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><br></div></div>