[Haskell-cafe] Equality test between types that returns type-level Bool ?
muranushi at gmail.com
Wed Nov 28 16:47:46 CET 2012
By tracing how unittyped produced the 'True-s and 'False-s in the error
messages, and by Oleg's lecture,
> 1 meter + 5 second
Couldn't match type 'False with 'True
When using functional dependencies to combine
UnitTyped.And 'False 'False 'False,
arising from the dependency `a b -> c'
in the instance declaration in `UnitTyped'
UnitTyped.And 'False 'False 'True,
arising from a use of `+' at <interactive>:17:9
In the expression: 1 meter + 5 second
In an equation for `it': it = 1 meter + 5 second
I understood how type-level equalities
and type-level list lookups
can be implemented using overlapped instances. Thank you for the
and I'm looking forward to see TYPEREP with ghc7.6.1's promoted integers
and TH pretty soon!
2012/11/27 Takayuki Muranushi <muranushi at gmail.com>
> Dear Gábor, Erik, and Oleg,
> Thank you for your advices. Also what I have wanted, the extensible
> dimensional type system, has just been released.
> Now I have homeworks to test these, thank you!
> 2012/11/27 Erik Hesselink <hesselink at gmail.com>
>> If you're up for it, Oleg has a lot of interesting material about this
>> subject .
>>  http://okmij.org/ftp/Haskell/typeEQ.html
>> On Sun, Nov 25, 2012 at 9:36 AM, Takayuki Muranushi <muranushi at gmail.com>wrote:
>>> Is it possible to write
>>> type family SameType a b :: Bool
>>> which returns True if a and b are the same type, and False otherwise?
>>> I encountered this problem when I was practicing promoted lists and
>>> tuples in ghc-7.6.1. One of my goal for practice is to write more
>>> "modular" version of extensible-dimensional calculations, and to
>>> understand whether ghc-7.6.1 is capable of it.
>>> Some of my attempts:
>>> This fails because :==: is not an equality test between a and b, but
>>> is a equality test within a (promoted) kind.
>>> This fails because type instance declarations are not read from top to
>>> bottom. (not like function declarations.)
>>> I could define a lookup using class constraints, but when I use it,
>>> results in overlapping instances.
>>> So, will somebody teach me which of the following is correct?
>>> * We can write a type family SameType a b :: Bool
>>> * We cannot do that because of theoretical reason (that leads to
>>> non-termination etc.)
>>> * We cannot write SameType, but there are ways to write functions like
>>> 'filter' and 'merge' , over type-level lists, without using SameType.
>>> Always grateful to your help,
>>> Takayuki MURANUSHI
>>> The Hakubi Center for Advanced Research, Kyoto University
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
> Takayuki MURANUSHI
> The Hakubi Center for Advanced Research, Kyoto University
The Hakubi Center for Advanced Research, Kyoto University
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe