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.

2010/9/8 Anthony Cowley :

2010/9/8 Gábor Lehel :

...

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?

Here's one way to indicate which value you are referring to.

Anthony

{-# LANGUAGE EmptyDataDecls, TypeFamilies #-} data True data False

class TypeValue a where    type ValueTypeOf a    value :: a -> 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 (undefined::True))

Right. You can also use Tagged :) but I meant specifically with the formulation I presented originally. {-# LANGUAGE EmptyDataDecls, TypeFamilies #-} import Data.Tagged import Control.Applicative data True :: * data False :: * class TypeValue a where type ValueTypeOf a :: * value :: Tagged a (ValueTypeOf a) instance TypeValue True where type ValueTypeOf True = Bool value = Tagged True instance TypeValue False where type ValueTypeOf False = Bool value = Tagged False main = untag $ print <$> (value :: Tagged True (ValueTypeOf True)) -- Work is punishment for failing to procrastinate effectively.