[Haskell-cafe] Reachable variables exercise
lrpalmer at gmail.com
Thu Sep 16 17:56:41 EDT 2010
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?
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
> Comments? Does that need and deserve a proposal?
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe