<div class="gmail_quote">---------- Forwarded message ----------<br>From: <b class="gmail_sendername">Carlos Camarao</b> <span dir="ltr"><<a href="mailto:carlos.camarao@gmail.com">carlos.camarao@gmail.com</a>></span><br>
Date: Fri, Sep 17, 2010 at 12:01 AM<br>Subject: Re: [Haskell-cafe] Reachable variables exercise<br>To: Luke Palmer <<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>><br><br><br><br>boolify o has type Boolable a => Bool under the proposal, then<br>
we have ambiguity, type error, right?<br><br>In general, consider 'e' as (g:: K=>a -> t) (o:: O a=>a); then the<br>type of 'e' has constraint (O a) iff 'a' occurs in t.<br>
<br>Let's think about how could 'a' not occur in t. That happens if 'o' is<br>not needed for computing the result; well, or, as in your example, 'g'<br>is overloaded and requires the argument to resolve the overloading<br>
('a' occurs in K and does not occur in t), in which case K=>t is<br>ambiguous.<br><br>Cheers,<br><font color="#888888"><br>Carlos</font><div><div></div><div class="h5"><br><br><br><div class="gmail_quote">On Thu, Sep 16, 2010 at 6:56 PM, Luke Palmer <span dir="ltr"><<a href="mailto:lrpalmer@gmail.com" target="_blank">lrpalmer@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">I am not totally sure if I understand your proposal correctly, but if<br>
I do, then it has a flaw. Consider:<br>
<br>
class Boolable a where<br>
boolify :: a -> Bool<br>
<div><br>
class O a where<br>
o :: a<br>
<br>
</div> main = print $ boolify o<br>
<br>
It seems like under your proposal this should not be a type error.<br>
But if that is so, then what is its output?<br>
<br>
Luke<br>
<div><div></div><div><br>
On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao<br>
<<a href="mailto:carlos.camarao@gmail.com" target="_blank">carlos.camarao@gmail.com</a>> wrote:<br>
> Hi. Consider for example an expression e0 like:<br>
><br>
> fst (True,e)<br>
><br>
> where e is any expression.<br>
><br>
> e0 should have type Bool IMHO irrespectively of the type of e. In Haskell<br>
> this is the case if e's type is monomorphic, or polymorphic, or<br>
> constrained and there is a default in the current module that removes<br>
> the constraints. However, e0 is not type-correct if e has a<br>
> constrained type and the constraints are not subject to<br>
> defaulting. For example:<br>
><br>
> class O a where o::a<br>
> main = print $ fst(True,o)<br>
><br>
> generates a type error; in GHC:<br>
><br>
> Ambiguous type variable `a' in the constraint:<br>
> `O a' arising from a use of `o' at ...<br>
> Probable fix: add a type signature that fixes these type variable(s)<br>
><br>
> A solution (that avoids type signatures) can be given as follows.<br>
><br>
> The type of f e, for f of type, say, K=>t'->t and e of type K'=> t'<br>
> should be:<br>
><br>
> K +_t K' => t (not K U K' => t)<br>
><br>
> where K +_t K' denotes the constraint-set obtained by adding from K'<br>
> only constraints with type variables reachable from t.<br>
><br>
> (A type variable is reachable if it appears in the same constraint as<br>
> either a type variable free in the type, or another reachable type<br>
> variable.)<br>
><br>
> Comments? Does that need and deserve a proposal?<br>
><br>
> Cheers,<br>
><br>
> Carlos<br>
><br>
</div></div>> _______________________________________________<br>
> Haskell-Cafe mailing list<br>
> <a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
><br>
><br>
</blockquote></div><br>
</div></div></div><br>