[Haskell-cafe] Problems with Type family and Typeable

[Dmitry Olshansky]

I didn't see any blog post or something else about it. But I had such
experience:
non-lazy type level if
<https://ghc.haskell.org/trac/ghc/ticket/11113#ticket>
type-level Fib
<http://haskell.1045720.n5.nabble.com/Memoization-in-Type-Calculation-td5860792.html>



2017-07-31 20:13 GMT+03:00 Kai Zhang <zk65900931 at gmail.com>:

> 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/20170801/d8af0360/attachment.html>