[Haskell-cafe] Equality test between types that returns type-level Bool ?

[Takayuki Muranushi]

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.

http://hackage.haskell.org/package/unittyped-0.1

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 [1].
>
> Regards,
>
> Erik
>
> [1] 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.
>>
>>
>> http://hackage.haskell.org/packages/archive/dimensional/0.10.2/doc/html/Numeric-Units-Dimensional-Extensible.html
>>
>> Some of my attempts:
>>
>> https://github.com/nushio3/dimensional-tf/blob/master/attic/list-02.hs
>> This fails because :==: is not an equality test between a and b, but
>> is a equality test within a (promoted) kind.
>>
>> https://github.com/nushio3/dimensional-tf/blob/master/attic/list-03.hs
>> This fails because type instance declarations are not read from top to
>> bottom. (not like function declarations.)
>>
>> https://github.com/nushio3/dimensional-tf/blob/master/attic/map-03.hs
>> 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
>> http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>


-- 
Takayuki MURANUSHI
The Hakubi Center for Advanced Research, Kyoto University
http://www.hakubi.kyoto-u.ac.jp/02_mem/h22/muranushi.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121127/e1db9429/attachment.htm>