[Haskell-cafe] Reachable variables exercise
Carlos Camarao
carlos.camarao at gmail.com
Thu Sep 16 23:56:05 EDT 2010
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-cafe/attachments/20100916/9221f365/attachment.html
More information about the Haskell-Cafe
mailing list