<div dir="ltr">I didn't see any blog post or something else about it. But I had such experience:<div><a href="https://ghc.haskell.org/trac/ghc/ticket/11113#ticket" target="_blank">non-lazy type level if</a><br></div><div><a href="http://haskell.1045720.n5.nabble.com/Memoization-in-Type-Calculation-td5860792.html">type-level Fib</a><br></div><div><br></div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-07-31 20:13 GMT+03:00 Kai Zhang <span dir="ltr"><<a href="mailto:zk65900931@gmail.com" target="_blank">zk65900931@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Dmitry, where did you learn this? Is there a blog post that I can read? Thanks!<div><div class="h5"><br><br><div class="gmail_quote"><div dir="ltr">On Mon, Jul 31, 2017 at 6:15 AM Dmitry Olshansky <<a href="mailto:olshanskydr@gmail.com" target="_blank">olshanskydr@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Additionally, as I understand now, you will have better compile-time performance if write<div><br></div><div>type Elem x xs = Elem' 'False x xs</div><div><br></div><div><div style="font-size:12.8px">type family Elem' (b::Bool) x xs :: Bool where</div><div style="font-size:12.8px"> Elem' 'True _ _ = 'True</div><div style="font-size:12.8px"> Elem' 'False a (x ': xs) = Elem' (a == x) a xs</div></div><div style="font-size:12.8px"> Elem' 'False _ '[] = 'False</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">All type calculation is not enough <span style="font-size:12.8px">lazy</span><span style="font-size:12.8px">!</span></div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-07-31 15:41 GMT+03:00 Li-yao Xia <span dir="ltr"><<a href="mailto:lysxia@gmail.com" target="_blank">lysxia@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello,<br>
<br>
<br>
"Data.Type.Equality.EqStar s t || Elem s ts" resolves to True or False, which are values of type Bool.<br>
To understand why that constraint can't be solved, think about how such a function is compiled. At run time, types are erased.<br>
A "Proxy p" value carries no more information than unit "()", and a "Tagged _ a" value is in fact just an "a" value.<br>
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:<br>
<br>
-- Original function<br>
elemTag :: Proxy s -> Tagged (t ': ts) a -> Bool<br>
<br>
-- After type erasure<br>
elemTag :: () -> a -> Bool<br>
<br>
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.<span><br>
<br>
elemTag :: forall a s t ts<br></span>
. Typeable (Elem s (t ': ts))<br>
=> Proxy s<span><br>
-> Tagged (t ': ts) a<br>
-> Bool<br>
<br>
<br></span>
Li-yao<div><div class="m_-6508178601224399146m_8533899565273635219h5"><br>
<br>
<br>
<br>
On 07/31/2017 07:15 AM, Kai Zhang wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="m_-6508178601224399146m_8533899565273635219h5">
I got an error when compiling the following codes:<br>
<br>
{-# LANGUAGE TypeOperators #-}<br>
{-# LANGUAGE DataKinds #-}<br>
{-# LANGUAGE TypeFamilies #-}<br>
{-# LANGUAGE ScopedTypeVariables #-}<br>
{-# LANGUAGE UndecidableInstances #-}<br>
<br>
import Data.Type.Bool<br>
import Data.Type.Equality<br>
import Data.Tagged (Tagged(..))<br>
import Data.Typeable<br>
<br>
type family Elem x xs :: Bool where<br>
Elem _ '[] = 'False<br>
Elem a (x ': xs) = a == x || Elem a xs<br>
<br>
elemTag :: forall a s t ts . Proxy s<br>
-> Tagged (t ': ts) a -> Bool<br>
elemTag _ _ = if typeOf (Proxy :: Proxy (Elem s (t ': ts))) == typeOf<br>
(Proxy :: Proxy 'True)<br>
then True<br>
else False<br>
<br>
GHC says:<br>
<br>
• No instance for (Typeable<br>
(Data.Type.Equality.EqStar s t || Elem s ts))<br>
arising from a use of ‘typeOf’<br>
• In the first argument of ‘(==)’, namely<br>
‘typeOf (Proxy :: Proxy (Elem s (t : ts)))’<br>
In the expression:<br>
typeOf (Proxy :: Proxy (Elem s (t : ts)))<br>
== typeOf (Proxy :: Proxy True)<br>
In the expression:<br>
if typeOf (Proxy :: Proxy (Elem s (t : ts)))<br>
== typeOf (Proxy :: Proxy True) then<br>
True<br>
else<br>
False<br>
<br>
My question: why is ghc unable to deduce that "Data.Type.Equality.EqStar s<br>
t || Elem s ts" resolves to "Bool" which should be an instance of Typeable?<br>
How to fix this?<br>
<br>
<br>
<br></div></div>
______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br>
</blockquote>
<br>
______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div><br></div>
</blockquote></div></div></div></div>
</blockquote></div><br></div>