2010/9/8 Miguel Mitrofanov
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Work is punishment for failing to procrastinate effectively.