By tracing how unittyped produced the 'True-s and 'False-s in the error messages, and by Oleg's lecture,<br><br>> 1 meter + 5 second<br><br><interactive>:17:9:<br> Couldn't match type 'False with 'True<br>
When using functional dependencies to combine<br> UnitTyped.And 'False 'False 'False,<br> arising from the dependency `a b -> c'<br> in the instance declaration in `UnitTyped'<br>
UnitTyped.And 'False 'False 'True,<br> arising from a use of `+' at <interactive>:17:9<br> In the expression: 1 meter + 5 second<br> In an equation for `it': it = 1 meter + 5 second<br>
<br><br>I understood how type-level equalities<br><a href="https://github.com/nushio3/dimensional-tf/blob/master/attic/typeeq-01.hs">https://github.com/nushio3/dimensional-tf/blob/master/attic/typeeq-01.hs</a><br>and type-level list lookups<br>
<a href="https://github.com/nushio3/dimensional-tf/blob/master/attic/typeeq-03.hs">https://github.com/nushio3/dimensional-tf/blob/master/attic/typeeq-03.hs</a><br><br>can be implemented using overlapped instances. Thank you for the instructions.<br>
<br>and I'm looking forward to see TYPEREP with ghc7.6.1's promoted integers and TH pretty soon!<br><div class="gmail_extra"><br><br><div class="gmail_quote">2012/11/27 Takayuki Muranushi <span dir="ltr"><<a href="mailto:muranushi@gmail.com" target="_blank">muranushi@gmail.com</a>></span><br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear <span name="Gábor Lehel">Gábor, Erik, and Oleg,<br><br>Thank you for your advices. Also what I have wanted, the extensible dimensional type system, has just been released.<br>
</span><span></span> <br>
<a href="http://hackage.haskell.org/package/unittyped-0.1" target="_blank">http://hackage.haskell.org/package/unittyped-0.1</a><br><br>Now I have homeworks to test these, thank you!<div class="HOEnZb"><div class="h5"><br>
<br><div class="gmail_extra"><br><br><div class="gmail_quote">
2012/11/27 Erik Hesselink <span dir="ltr"><<a href="mailto:hesselink@gmail.com" target="_blank">hesselink@gmail.com</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
If you're up for it, Oleg has a lot of interesting material about this subject [1].<br><br>Regards,<br><br>Erik<br><br>[1] <a href="http://okmij.org/ftp/Haskell/typeEQ.html" target="_blank">http://okmij.org/ftp/Haskell/typeEQ.html</a><br>
<div class="gmail_extra"><br><br><div class="gmail_quote"><div>On Sun, Nov 25, 2012 at 9:36 AM, Takayuki Muranushi <span dir="ltr"><<a href="mailto:muranushi@gmail.com" target="_blank">muranushi@gmail.com</a>></span> wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>Is it possible to write<br>
<br>
type family SameType a b :: Bool<br>
<br>
which returns True if a and b are the same type, and False otherwise?<br>
<br>
I encountered this problem when I was practicing promoted lists and<br>
tuples in ghc-7.6.1. One of my goal for practice is to write more<br>
"modular" version of extensible-dimensional calculations, and to<br>
understand whether ghc-7.6.1 is capable of it.<br>
<br>
<a href="http://hackage.haskell.org/packages/archive/dimensional/0.10.2/doc/html/Numeric-Units-Dimensional-Extensible.html" target="_blank">http://hackage.haskell.org/packages/archive/dimensional/0.10.2/doc/html/Numeric-Units-Dimensional-Extensible.html</a><br>
<br>
Some of my attempts:<br>
<br>
<a href="https://github.com/nushio3/dimensional-tf/blob/master/attic/list-02.hs" target="_blank">https://github.com/nushio3/dimensional-tf/blob/master/attic/list-02.hs</a><br>
This fails because :==: is not an equality test between a and b, but<br>
is a equality test within a (promoted) kind.<br>
<br>
<a href="https://github.com/nushio3/dimensional-tf/blob/master/attic/list-03.hs" target="_blank">https://github.com/nushio3/dimensional-tf/blob/master/attic/list-03.hs</a><br>
This fails because type instance declarations are not read from top to<br>
bottom. (not like function declarations.)<br>
<br>
<a href="https://github.com/nushio3/dimensional-tf/blob/master/attic/map-03.hs" target="_blank">https://github.com/nushio3/dimensional-tf/blob/master/attic/map-03.hs</a><br>
I could define a lookup using class constraints, but when I use it,<br>
results in overlapping instances.<br>
<br>
So, will somebody teach me which of the following is correct?<br>
<br>
* We can write a type family SameType a b :: Bool<br>
* We cannot do that because of theoretical reason (that leads to<br>
non-termination etc.)<br>
* We cannot write SameType, but there are ways to write functions like<br>
'filter' and 'merge' , over type-level lists, without using SameType.<br>
<br>
Always grateful to your help,<br>
--<br>
Takayuki MURANUSHI<br>
The Hakubi Center for Advanced Research, Kyoto University<br>
<a href="http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html" target="_blank">http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html</a><br>
<br></div></div><div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></blockquote></div><br></div>
</blockquote></div><br><br clear="all"><br>-- <br>Takayuki MURANUSHI<br>The Hakubi Center for Advanced Research, Kyoto University<br><a href="http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html" target="_blank">http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html</a><br>
</div>
</div></div></blockquote></div><br><br clear="all"><br>-- <br>Takayuki MURANUSHI<br>The Hakubi Center for Advanced Research, Kyoto University<br><a href="http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html" target="_blank">http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html</a><br>
</div>