[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    Re: [Haskell-cafe] Equality test between types that returns type-level Bool ?
From:       Gábor_Lehel <illissius () gmail ! com>
Date:       2012-11-25 15:51:43
Message-ID: CAPNUp0-uQbt4W3AVUa7DNocPPfi=mw7k_y1OwY2WyVHpVuKjOw () mail ! gmail ! com
[Download RAW message or body]

On Sun, Nov 25, 2012 at 9:36 AM, Takayuki Muranushi <muranushi@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.)

This is correct. It's not currently possible to have overlapping type
family instances without breaking the soundness of the type system.
There's some work on changing it:
http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

> * We cannot write SameType, but there are ways to write functions like
> 'filter' and 'merge' , over type-level lists, without using SameType.

Not easily that I know of. There's no way to write a general "else",
"otherwise", "if not", etc. case. You have to explicitly enumerate
every type you want to use it with. It _is_ possible with type classes
and OverlappingInstances, but beyond the trivial cases it tends to
make my head hurt (and there's no way to get a result "out" of a type
class "computation" and into a type family).

> 
> 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@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe



-- 
Your ship was destroyed in a monadic eruption.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


[prev in list] [next in list] [prev in thread] [next in thread]