[Haskell-cafe] Reachable variables exercise

[Carlos Camarao]

Ah... now I understand your concern; I should have written
something like:

where K  +_t  K'  denotes the set of constraints from K plus
those from K' that have type variables reachable from t.

instead of:

where K  +_t  K'  denotes the constraint-set obtained by adding from K'
only constraints with type variables reachable from t.

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/9221f365/attachment.html