New-to-Haskell, i.e. elementary, Haskell questions; extended discussions

Takayuki Muranushi | 25 Nov 2012 09:36

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

(Continue reading)

headers

Gábor Lehel | 25 Nov 2012 16:51

Re: Equality test between types that returns type-level Bool ?

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?
>

(Continue reading)

headers

Erik Hesselink | 26 Nov 2012 22:18

Re: 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 <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

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

headers

Takayuki Muranushi | 27 Nov 2012 00:42

Re: 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 <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

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

headers

Takayuki Muranushi | 28 Nov 2012 16:47

Re: 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

<interactive>: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 <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
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 <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.

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

--
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