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