[Haskell-cafe] Problems with Type family and Typeable
Kai Zhang
zk65900931 at gmail.com
Mon Jul 31 17:13:43 UTC 2017
Dmitry, where did you learn this? Is there a blog post that I can read?
Thanks!
On Mon, Jul 31, 2017 at 6:15 AM Dmitry Olshansky <olshanskydr at gmail.com>
wrote:
> Additionally, as I understand now, you will have better compile-time
> performance if write
>
> type Elem x xs = Elem' 'False x xs
>
> type family Elem' (b::Bool) x xs :: Bool where
> Elem' 'True _ _ = 'True
> Elem' 'False a (x ': xs) = Elem' (a == x) a xs
> Elem' 'False _ '[] = 'False
>
> All type calculation is not enough lazy!
>
> 2017-07-31 15:41 GMT+03:00 Li-yao Xia <lysxia at gmail.com>:
>
>> Hello,
>>
>>
>> "Data.Type.Equality.EqStar s t || Elem s ts" resolves to True or False,
>> which are values of type Bool.
>> To understand why that constraint can't be solved, think about how such a
>> function is compiled. At run time, types are erased.
>> A "Proxy p" value carries no more information than unit "()", and a
>> "Tagged _ a" value is in fact just an "a" value.
>> So elemTag is compiled to something equivalent to a function of this
>> type, which has no way of performing the comparison you requested since the
>> type-level boolean was erased:
>>
>> -- Original function
>> elemTag :: Proxy s -> Tagged (t ': ts) a -> Bool
>>
>> -- After type erasure
>> elemTag :: () -> a -> Bool
>>
>> As suggested by the type error, you can reify the boolean "Elem s (t ':
>> ts)" by adding a Typeable constraint, which gets compiled to an additional
>> run time argument.
>>
>> elemTag :: forall a s t ts
>> . Typeable (Elem s (t ': ts))
>> => Proxy s
>> -> Tagged (t ': ts) a
>> -> Bool
>>
>>
>> Li-yao
>>
>>
>>
>>
>> On 07/31/2017 07:15 AM, Kai Zhang wrote:
>>
>>> I got an error when compiling the following codes:
>>>
>>> {-# LANGUAGE TypeOperators #-}
>>> {-# LANGUAGE DataKinds #-}
>>> {-# LANGUAGE TypeFamilies #-}
>>> {-# LANGUAGE ScopedTypeVariables #-}
>>> {-# LANGUAGE UndecidableInstances #-}
>>>
>>> import Data.Type.Bool
>>> import Data.Type.Equality
>>> import Data.Tagged (Tagged(..))
>>> import Data.Typeable
>>>
>>> type family Elem x xs :: Bool where
>>> Elem _ '[] = 'False
>>> Elem a (x ': xs) = a == x || Elem a xs
>>>
>>> elemTag :: forall a s t ts . Proxy s
>>> -> Tagged (t ': ts) a -> Bool
>>> elemTag _ _ = if typeOf (Proxy :: Proxy (Elem s (t ': ts))) == typeOf
>>> (Proxy :: Proxy 'True)
>>> then True
>>> else False
>>>
>>> GHC says:
>>>
>>> • No instance for (Typeable
>>> (Data.Type.Equality.EqStar s t || Elem s ts))
>>> arising from a use of ‘typeOf’
>>> • In the first argument of ‘(==)’, namely
>>> ‘typeOf (Proxy :: Proxy (Elem s (t : ts)))’
>>> In the expression:
>>> typeOf (Proxy :: Proxy (Elem s (t : ts)))
>>> == typeOf (Proxy :: Proxy True)
>>> In the expression:
>>> if typeOf (Proxy :: Proxy (Elem s (t : ts)))
>>> == typeOf (Proxy :: Proxy True) then
>>> True
>>> else
>>> False
>>>
>>> My question: why is ghc unable to deduce that "Data.Type.Equality.EqStar
>>> s
>>> t || Elem s ts" resolves to "Bool" which should be an instance of
>>> Typeable?
>>> How to fix this?
>>>
>>>
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>>
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170731/10a541fc/attachment.html>
More information about the Haskell-Cafe
mailing list