Re: [Haskell-cafe] Problems with Type family and Typeable

1 Aug 2017


      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-td58607...


2017-07-31 20:13 GMT+03:00 Kai Zhang :
...
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 
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 :
...
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.