[Haskell-cafe] interesting type families problem
Gábor Lehel
illissius at gmail.com
Wed Sep 8 13:04:39 EDT 2010
2010/9/8 Miguel Mitrofanov <miguelimo38 at yandex.ru>:
>
> 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
--
Work is punishment for failing to procrastinate effectively.
More information about the Haskell-Cafe
mailing list