[Haskell-cafe] Equality test between types that returns type-level Bool ?
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality test between types that returns type-level Bool ?
On Sun, Nov 25, 2012 at 9:36 AM, Takayuki Muranushi 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
Re: [Haskell-cafe] Equality test between types that returns type-level Bool ?
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 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality test between types that returns type-level Bool ?
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 > 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 > 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@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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Equality test between types that returns type-level Bool ?
By tracing how unittyped produced the 'True-s and 'False-s in the error messages, and by Oleg's lecture, > 1 meter + 5 second :17:9: 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 :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 https://github.com/nushio3/dimensional-tf/blob/master/attic/typeeq-01.hs and type-level list lookups https://github.com/nushio3/dimensional-tf/blob/master/attic/typeeq-03.hs can be implemented using overlapped instances. Thank you for the instructions. and I'm looking forward to see TYPEREP with ghc7.6.1's promoted integers and TH pretty soon! 2012/11/27 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 > >> 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 >> 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@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 > -- 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
