[Haskell-cafe] interesting type families problem
Miguel Mitrofanov
miguelimo38 at yandex.ru
Wed Sep 8 12:48:45 EDT 2010
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".
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list