2010/9/8 Miguel Mitrofanov <[email protected]>: > > On 8 Sep 2010, at 20:01, Gábor Lehel wrote: > >> I'm bad at expositions so I'll just lead with the code: >> >> {-# LANGUAGE EmptyDataDecls, TypeFamilies #-} >> >> data True :: * >> data False :: * >> >> class TypeValue a where >> type ValueTypeOf a :: * >> value :: ValueTypeOf a >> >> instance TypeValue True where >> type ValueTypeOf True = Bool >> value = True >> >> instance TypeValue False where >> type ValueTypeOf False = Bool >> value = False >> >> main = print (value :: ValueTypeOf True) >> >> (In case this is initially confusing, there are entirely distinct >> type-level and value-level True and False involved which merely share >> a name. The idea is to take type-level 'values' and reflect them down >> to the corresponding value-level, er, values.) >> >> Which results in the following error message: >> >> Couldn't match expected type `Bool' >> against inferred type `ValueTypeOf a' >> NB: `ValueTypeOf' is a type function, and may not be injective >> In the first argument of `print', namely >> `(value :: ValueTypeOf True)' >> In the expression: print (value :: ValueTypeOf True) >> In the definition of `main': >> main = print (value :: ValueTypeOf True) >> >> >> This is strange and vaguely amusing to me. I get that type functions >> are not injective, but I can't figure out how it applies to this >> situation. Obviously if I had written `print (value :: Bool)` it would >> rightly complain that there could be any number of instances which map >> to Bool, and how in the world should it know which one I meant. > > Well, it's the same thing, actually. Since "ValueTypeOf True" is "Bool", > "value :: ValueTypeOf True" is exactly the same as "value :: Bool".
Oh. Hmm. That makes sense. So I gather there's absolutely no way to specify which instance you mean, and hence to use `value` as any concrete type? > >> But it >> seems like in this case the compiler knows everything it needs to >> know. And it even manages to deduce, from the exact same expression >> (`print` isn't giving it any extra information), that it's >> simultaneously a Bool and not necessarily a Bool. >> >> Is this "supposed" to work? If not, why not? >> >> >> -- >> Work is punishment for failing to procrastinate effectively. >> _______________________________________________ >> Haskell-Cafe mailing list >> [email protected] >> http://www.haskell.org/mailman/listinfo/haskell-cafe > > -- Work is punishment for failing to procrastinate effectively. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
