RE: Instances That Ignore Type Constraints? (HList-related)

Yeah, I was also thinking of impredicative types and that they would make this problem go away. First of all, we may need to wait a while for such types to become available in Haskell, but Daan has good stuff at avail. Also, for clarity, let me just point out that this is really about an *interaction* of impredicativeness *and* type classes. Hence, I really think that an argument in favor of impredicative types is slightly overrated unless a Haskell approach to impredicativeness is fully conclusive for the type-class story. The following queries make it clear: Prelude> null [fromEnum] <interactive>:1:6: Ambiguous type variable `a' in the constraint: `Enum a' arising from use of `fromEnum' at <interactive>:1:6-13 Probable fix: add a type signature that fixes these type variable(s) Prelude> null [id] False More importantly, I need more input to fully endorse the appropriateness of impredicative types in this sort of context. That is, the question is ... what does it *mean* to wrap (or to box or to cartoon) an expression with non-escaping type variables that locally occur in type-class constraints? GHC/Haskell, as of today: - it means nothing; type error. Some sort of impredicative type: - it means universal quantification Potentially elsewhere: - it means existential quantification In Ghc with incoherent instances: - see above; except that the instance is actually selected. In addition to this scary diversity, all the three last choices are bogus in some sense because the quantified variables are totally inaccessible; so why would a type system honor such potentially accidental opaqueness. In summary, this makes me conclude that null [fromEnum] is just a really loose question to ask, which is perhaps just better rejected by a strong type system, no? Please, prove that I am wrong. :-) Ralf Oleg wrote:
When GHC does implement MLF and start explicitly supporting impredicative types, the problem would be fixed indeed... Currently, the only way to achieve the same effect is to do this manually:
newtype W = W (forall a. (Enum a) => a -> Int)
*Main> null [W fromEnum] False
Perhaps indeed we should move to Cafe...
participants (1)
-
Ralf Lammel