Fwd: [Haskell-cafe] Reachable variables exercise

[Carlos Camarao]

---------- Forwarded message ----------
From: Carlos Camarao <carlos.camarao at gmail.com>
Date: Fri, Sep 17, 2010 at 12:01 AM
Subject: Re: [Haskell-cafe] Reachable variables exercise
To: Luke Palmer <lrpalmer at gmail.com>



boolify o has type Boolable a => Bool under the proposal, then
we have ambiguity, type error, right?

In general, consider 'e' as (g:: K=>a -> t) (o:: O a=>a); then the
type of 'e' has constraint (O a) iff 'a' occurs in t.

Let's think about how could 'a' not occur in t. That happens if 'o' is
not needed for computing the result; well, or, as in your example, 'g'
is overloaded and requires the argument to resolve the overloading
('a' occurs in K and does not occur in t), in which case K=>t is
ambiguous.

Cheers,

Carlos



On Thu, Sep 16, 2010 at 6:56 PM, Luke Palmer <lrpalmer at gmail.com> wrote:

> I am not totally sure if I understand your proposal correctly, but if
> I do, then it has a flaw.  Consider:
>
>    class Boolable a where
>        boolify :: a -> Bool
>
>    class O a where
>        o :: a
>
>     main = print $ boolify o
>
> It seems like under your proposal this should not be a type error.
> But if that is so, then what is its output?
>
> Luke
>
> On Thu, Sep 16, 2010 at 7:31 AM, Carlos Camarao
> <carlos.camarao at gmail.com> wrote:
> > Hi. Consider for example an expression e0 like:
> >
> >   fst (True,e)
> >
> > where e is any expression.
> >
> > e0 should have type Bool IMHO irrespectively of the type of e. In Haskell
> > this is the case if e's type is monomorphic, or polymorphic, or
> > constrained and there is a default in the current module that removes
> > the constraints. However, e0 is not type-correct if e has a
> > constrained type and the constraints are not subject to
> > defaulting. For example:
> >
> >   class O a where o::a
> >   main = print $ fst(True,o)
> >
> > generates a type error; in GHC:
> >
> >   Ambiguous type variable `a' in the constraint:
> >      `O a' arising from a use of `o' at ...
> >     Probable fix: add a type signature that fixes these type variable(s)
> >
> > A solution (that avoids type signatures) can be given as follows.
> >
> > The type of f e, for f of type, say, K=>t'->t and e of type K'=> t'
> > should be:
> >
> >       K  +_t   K' => t      (not K U K' => t)
> >
> > where K  +_t  K'  denotes the constraint-set obtained by adding from K'
> > only constraints with type variables reachable from t.
> >
> > (A type variable is reachable if it appears in the same constraint as
> > either a type variable free in the type, or another reachable type
> > variable.)
> >
> > Comments? Does that need and deserve a proposal?
> >
> > Cheers,
> >
> > Carlos
> >
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20100916/f5b2562d/attachment.html