Learn You a Haskell for Great Good - a few doubts

[Karthick Gururaj]

Hello,

I'm learning Haskell from the extremely well written (and well illustrated as well!) tutorial - http://learnyouahaskell.com/chapters. I have couple of questions from my readings so far.

In "typeclasses - 101" (http://learnyouahaskell.com/types-and-typeclasses#typeclasses-101), there is a paragraph that reads:
Enum members are sequentially ordered types - they can be enumerated. The main advantage of the Enum typeclass is that we can use its types in list ranges. They also have defined successors and predecesors, which you can get with the succ and pred functions. Types in this class: (), Bool, Char, Ordering, Int, Integer, Float and Double.

What is the "()" type? Does it refer to a tuple? How can tuple be ordered, let alone be enum'd? I tried:
Prelude> take 10 [(1,1) ..]
<interactive>:1:8:
    No instance for (Enum (t, t1))
      arising from the arithmetic sequence `(1, 1) .. '
                   at <interactive>:1:8-17
    Possible fix: add an instance declaration for (Enum (t, t1))
    In the second argument of `take', namely `[(1, 1) .. ]'
    In the expression: take 10 [(1, 1) .. ]
    In the definition of `it': it = take 10 [(1, 1) .. ]

This is expected and is logical.

But, surprise:
Prelude> (1,1) > (1,2)
False
Prelude> (2,2) > (1,1)
True
Prelude> (1,2) > (2,1)
False
Prelude> (1,2) < (2,1)
True

So tuples are in "Ord" type class atleast. What is the ordering logic?

Another question, on the curried functions - specifically for infix functions. Suppose I need a function that takes an argument and adds five to it. I can do:
Prelude> let addFive = (+) 5
Prelude> addFive 4
9

The paragraph: "Infix functions can also be partially applied by using sections. To section an infix function, simply surround it with parentheses and only supply a parameter on one side. That creates a function that takes one parameter and then applies it to the side that's missing an operand": describes a different syntax. I tried that as well:

Prelude> let addFive' = (+5)
Prelude> addFive' 3
8

Ok. Works. But on a non-commutative operation like division, we get:
Prelude> let x = (/) 20.0
Prelude> x 10
2.0
Prelude> let y = (/20.0)
Prelude> y 10
0.5

So a curried infix operator fixes the first argument and a "sectioned infix" operator fixes the second argument?

Regards,
Karthick

[Karthick Gururaj]

Hello,

Regards,
Karthick

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

[Chris Smith]

On Thu, 2011-03-03 at 11:39 +0530, Karthick Gururaj wrote:
> What is the "()" type? Does it refer to a tuple? How can tuple be
> ordered, let alone be enum'd? I tried:

The () type is pronounced "unit". It is a type with only 1 value, also
called () and pronounced "unit". Since it only has one possible value,
it conveys no information at all, and is sometimes used in situations
analogous to C's 'void' keyword.

Okay, actually that was a little bit of a lie; () has two "values": ()
and bottom. Bottom is the "value" that corresponds to the program
hanging in an infinite loop or dying with an error message. But if you
have an actual, honest-to-goodness value that's not bottom, it has to be
().

> But, surprise:
> Prelude> (1,1) > (1,2)
> False
> Prelude> (2,2) > (1,1)
> True
> Prelude> (1,2) > (2,1)
> False
> Prelude> (1,2) < (2,1)
> True

Okay, so this is no longer Enum, but just Ord. The ordering defined in
the Ord instance for tuples is the normal lexicographic order: the
comparison between the first elements dominates; but if the first
elements coincide, then the second are compared instead. For larger
tuple types, the same pattern continues.

Think of it like organizing words in alphabetical order, where here you
know the words all have the same number of letters.

> Ok. Works. But on a non-commutative operation like division, we get:
> Prelude> let x = (/) 20.0
> Prelude> x 10
> 2.0
> Prelude> let y = (/20.0)
> Prelude> y 10
> 0.5
>
> So a curried infix operator fixes the first argument and a "sectioned
> infix" operator fixes the second argument?

Sections can be either left sections or right sections, so you can pick
which argument is provided.

Prelude> let y = (/ 20.0)
Prelude> y 10
0.5
Prelude> let y = (20.0 /)
Prelude> y 10
2.0

Hope that helps,

--
Chris Smith

[Karthick Gururaj]

On Thu, Mar 3, 2011 at 11:48 AM, Chris Smith <cds...@gmail.com> wrote:
> On Thu, 2011-03-03 at 11:39 +0530, Karthick Gururaj wrote:
>> What is the "()" type? Does it refer to a tuple? How can tuple be
>> ordered, let alone be enum'd? I tried:
>
> The () type is pronounced "unit".  It is a type with only 1 value, also
> called () and pronounced "unit".  Since it only has one possible value,
> it conveys no information at all, and is sometimes used in situations
> analogous to C's 'void' keyword.
>
> Okay, actually that was a little bit of a lie; () has two "values": ()
> and bottom.  Bottom is the "value" that corresponds to the program
> hanging in an infinite loop or dying with an error message.  But if you
> have an actual, honest-to-goodness value that's not bottom, it has to be
> ().

Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
any case, my question is answered since it is not a tuple.

Thanks, it does!

[Ivan Lazar Miljenovic]

On 3 March 2011 17:59, Karthick Gururaj <karthick...@gmail.com> wrote:
> On Thu, Mar 3, 2011 at 11:48 AM, Chris Smith <cds...@gmail.com> wrote:
>> On Thu, 2011-03-03 at 11:39 +0530, Karthick Gururaj wrote:
>>> What is the "()" type? Does it refer to a tuple? How can tuple be
>>> ordered, let alone be enum'd? I tried:
>>
>> The () type is pronounced "unit".  It is a type with only 1 value, also
>> called () and pronounced "unit".  Since it only has one possible value,
>> it conveys no information at all, and is sometimes used in situations
>> analogous to C's 'void' keyword.
>>
>> Okay, actually that was a little bit of a lie; () has two "values": ()
>> and bottom.  Bottom is the "value" that corresponds to the program
>> hanging in an infinite loop or dying with an error message.  But if you
>> have an actual, honest-to-goodness value that's not bottom, it has to be
>> ().
> Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
> any case, my question is answered since it is not a tuple.

Yes.

--
Ivan Lazar Miljenovic
Ivan.Mi...@gmail.com
IvanMiljenovic.wordpress.com

[Antti-Juhani Kaijanaho]

On Thu, Mar 03, 2011 at 12:29:44PM +0530, Karthick Gururaj wrote:
> Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
> any case, my question is answered since it is not a tuple.

It can be viewed as the trivial 0-tuple.

--
Antti-Juhani Kaijanaho, Jyväskylä, Finland
http://antti-juhani.kaijanaho.fi/newblog/
http://www.flickr.com/photos/antti-juhani/

[Paul Sujkov]

Hi,

you can always check the types using GHCi prompt:

*Prelude> :i (,)

data (,) a b = (,) a b -- Defined in GHC.Tuple

instance (Bounded a, Bounded b) => Bounded (a, b)

  -- Defined in GHC.Enum

instance (Eq a, Eq b) => Eq (a, b) -- Defined in Data.Tuple

instance Functor ((,) a) -- Defined in Control.Monad.Instances

instance (Ord a, Ord b) => Ord (a, b) -- Defined in Data.Tuple

instance (Read a, Read b) => Read (a, b) -- Defined in GHC.Read

instance (Show a, Show b) => Show (a, b) -- Defined in GHC.Show

that's for a tuple. You can see that tuple has an instance for the Ord class.

*Prelude> :i ()

data () = () -- Defined in GHC.Unit

instance Bounded () -- Defined in GHC.Enum

instance Enum () -- Defined in GHC.Enum

instance Eq () -- Defined in Data.Tuple

instance Ord () -- Defined in Data.Tuple

instance Read () -- Defined in GHC.Read

instance Show () -- Defined in GHC.Show

and that's for a unit type.

--
Regards, Paul Sujkov

[Karthick Gururaj]

On Thu, Mar 3, 2011 at 8:00 PM, Paul Sujkov <psu...@gmail.com> wrote:
> Hi,
> you can always check the types using GHCi prompt:
> *Prelude> :i (,)
> data (,) a b = (,) a b -- Defined in GHC.Tuple
> instance (Bounded a, Bounded b) => Bounded (a, b)
>   -- Defined in GHC.Enum
> instance (Eq a, Eq b) => Eq (a, b) -- Defined in Data.Tuple
> instance Functor ((,) a) -- Defined in Control.Monad.Instances
> instance (Ord a, Ord b) => Ord (a, b) -- Defined in Data.Tuple
> instance (Read a, Read b) => Read (a, b) -- Defined in GHC.Read
> instance (Show a, Show b) => Show (a, b) -- Defined in GHC.Show
> that's for a tuple. You can see that tuple has an instance for the Ord
> class.
> *Prelude> :i ()
> data () = () -- Defined in GHC.Unit
> instance Bounded () -- Defined in GHC.Enum
> instance Enum () -- Defined in GHC.Enum
> instance Eq () -- Defined in Data.Tuple
> instance Ord () -- Defined in Data.Tuple
> instance Read () -- Defined in GHC.Read
> instance Show () -- Defined in GHC.Show
> and that's for a unit type.

> [snip]
Ah, thanks! I didn't know about :i, tried only :t () which didn't give
very interesting information.

[Alexander Solla]

On Wed, Mar 2, 2011 at 10:09 PM, Karthick Gururaj <karthick...@gmail.com> wrote:

Hello,

I'm learning Haskell from the extremely well written (and well
illustrated as well!) tutorial - http://learnyouahaskell.com/chapters.
I have couple of questions from my readings so far.

In "typeclasses - 101"
(http://learnyouahaskell.com/types-and-typeclasses#typeclasses-101),
there is a paragraph that reads:
Enum members are sequentially ordered types - they can be enumerated.
The main advantage of the Enum typeclass is that we can use its types
in list ranges. They also have defined successors and predecesors,
which you can get with the succ and pred functions. Types in this
class: (), Bool, Char, Ordering, Int, Integer, Float and Double.

What is the "()" type? Does it refer to a tuple? How can tuple be
ordered, let alone be enum'd?

Any set can be put into an order.  That's the well-ordering principle.  Basically, the most natural order for pairs is the lexicographical order.  There are instances of the form:

instance (Ord a, Ord b) => Ord (a,b)

in GHC.Enum (if you're using GHC).  You can also create Enum instances for pairs, but at least one of the "sides" must be bounded.  Otherwise, the enumeration will have an uncomputable order-type (something like the order type of the rationals). Check out http://en.wikipedia.org/wiki/Order_type if you're interested in what all that "order type" stuff means.

I wrote  an instance for this very purpose the other day:

-- An intuitive way to think about this is in terms of tables. Given datatypes

--

-- @

-- data X = A | B | C | D deriving ('Bounded', 'Enum', 'Eq', 'Ord', 'Show')

-- data Y = E | F | G     deriving ('Bounded', 'Enum', 'Eq', 'Ord', 'Show')

-- @

--

-- we can form the table

--

-- @

-- (A, E)   (A, F)   (A, G)

-- (B, E)   (B, F)   (B, G)

-- (C, E)   (C, F)   (C, G)

-- (D, E)   (D, F)   (D, G)

-- @

--

-- in a natural lexicographical order.  We simply require that there be a finite

-- number of columns, and allow an unbounded number of rows (in so far as the

-- lazy evaluation mechanism allows them).  In even more practical terms, we require

-- a finite number of columns because we use that number to perform arithmetic.

instance ( Bounded b

         , Enum a

         , Enum b

         ) => Enum (a, b) where

              toEnum k = let n = 1 + fromEnum (maxBound :: b) -- Enums are 0 indexed, but we want to

                             a = toEnum ((k `div` n))         -- divide by the number of elements in a row to find the row and

                             b = toEnum ((k `mod` n))         -- get the remainder to find the column.

                          in (a,b) 

              

              fromEnum (a, b) = let n = 1 + fromEnum (maxBound :: b)

                                    i = fromEnum a

                                    j = fromEnum b

                                 in (i*n + j)

-- | This instance of 'Enum' is defined in terms of the previous instance.  We

-- use the natural equivalence of the types @(a,b,c)@ and @(a,(b,c))@ and use

-- the previous definition.  Again, notice that all elements but the first must

-- be bounded.

instance ( Bounded b

         , Bounded c

         , Enum a

         , Enum b

         , Enum c

         ) => Enum (a, b, c) where

                   fromEnum (a, b, c) = fromEnum (a, (b,c))

                   toEnum k = let (a, (b, c)) = toEnum k

                               in (a, b,  c)

                                                       

 

So tuples are in "Ord" type class atleast. What is the ordering logic?

Lexicographical.  Dictionary order. 

Another question, on the curried functions - specifically for infix
functions. Suppose I need a function that takes an argument and adds
five to it. I can do:
Prelude> let addFive = (+) 5
Prelude> addFive 4
9

The paragraph: "Infix functions can also be partially applied by using
sections. To section an infix function, simply surround it with
parentheses and only supply a parameter on one side. That creates a
function that takes one parameter and then applies it to the side
that's missing an operand": describes a different syntax. I tried that
as well:

Prelude> let addFive' = (+5)
Prelude> addFive' 3
8

Ok. Works. But on a non-commutative operation like division, we get:
Prelude> let x = (/) 20.0
Prelude> x 10
2.0
Prelude> let y = (/20.0)
Prelude> y 10
0.5

So a curried infix operator fixes the first argument and a "sectioned
infix" operator fixes the second argument?

I guess, except you can section infix operators the other way:

> let twentyover = (20 /)

> twentyover 5

4.0

[Richard O'Keefe]

By the way, tuples *can* be members of Enum if you make them so.
Try

instance (Enum a, Enum b, Bounded b) => Enum (a,b)
where
toEnum n = (a, b)
where a = toEnum (n `div` s)
b = toEnum (n `mod` s)
p = fromEnum (minBound `asTypeOf` b)
q = fromEnum (maxBound `asTypeOf` b)
s = q - p + 1
fromEnum (a, b) = fromEnum a * s + fromEnum b
where p = fromEnum (minBound `asTypeOf` b)
q = fromEnum (maxBound `asTypeOf` b)
s = q - p + 1

data T1 = A | B | C deriving (Enum, Eq, Bounded, Show)
data T2 = D | E | F deriving (Enum, Eq, Bounded, Show)

t1 = [(A,D) .. (B,F)]

I can't think of an approach that doesn't require all but one of
the tuple elements to have Bounded types. There are of course
all sorts of ways to enumerate tuples; this one is compatible
with the Ord instance.

[Alexander Solla]

On Thu, Mar 3, 2011 at 1:58 PM, Richard O'Keefe <o...@cs.otago.ac.nz> wrote:

I can't think of an approach that doesn't require all but one of
the tuple elements to have Bounded types.  

It's not possible.  Such an enumeration could potentially have an uncomputable order-type, possibly equal to the order-type of the rationals.  (In other words, there could be countably infinitely many elements between any two elements)

It's possible to define a computational system where you can do arithmetic on countable ordinals, but it has the expressive power of Turing machines with oracles (where an oracle is a thing that correctly guesses the "right" answer for a computation that does not halt in finite time (consider a sequence approaching pi as a limit).   We can re-interpret the oracle's guess as passing to a limit ordinal.  In any case, TMs+ oracles are strictly stronger than just TMs.

[Daniel Fischer]

On Thursday 03 March 2011 23:25:48, Alexander Solla wrote:
> On Thu, Mar 3, 2011 at 1:58 PM, Richard O'Keefe <o...@cs.otago.ac.nz>
wrote:
> > I can't think of an approach that doesn't require all but one of
> > the tuple elements to have Bounded types.
>
> It's not possible.

Meaning: It's not possible while respecting the order.
Ignoring the order, it's of course possible (finite products of countable
sets are countable).

[Markus]

What about having the order by diagonals, like:

0 1 3
2 4
5

and have none of the pair be bounded?

--
Markus Läll

On 4 Mar 2011, at 01:10, Daniel Fischer <daniel.i...@googlemail.com

[Daniel Fischer]

On Friday 04 March 2011 03:24:34, Markus wrote:
> What about having the order by diagonals, like:
>
> 0 1 3
> 2 4
> 5
>
> and have none of the pair be bounded?
>

I tacitly assumed product order (lexicographic order).

[Karthick Gururaj]

There are so many responses, that I do not know where to start..

I'm top-posting since that seems best here, let me know if there are
group guidelines against that.

Some clarifications in order on my original post:
a. I ASSUMED that '()' refers to tuples, where we have atleast a pair.
This is from my Haskell ignorance, so let us forget that for now.
b. Also, when I said: tuples can not be ordered, let alone be enum'd -
I meant: there is no reasonable way of ordering tuples, let alone enum
them.

That does not mean we can't define them:
1. (a,b) > (c,d) if a>c
2. (a,b) > (c,d) if b>d
3. (a,b) > (c,d) if a^2 + b^2 > c^2 + d^2
4. (a,b) > (c,d) if a*b > c*d

If we can imagine (a,b) as a point in the xy plane, (1) defines
ordering based on which point is "more to the right of y axis", (2)
based on "which point is more above x axis", (3) on "which point is
farther from origin" and (4) on "which rectangle made of origin and
the point as diagonally opposite vertices has more area". Which of
these is a reasonable definition? The set of complex numbers do not
have a "default" ordering, due to this very issue.

For enumerating them, we *can* go along the diagonal as suggested. But
why that and not something else? By the way - enumerating them along
the diagonal introduces a new ordering between tuples.

When we do not have a "reasonable" way of ordering, I'd argue to not
have anything at all - let the user decide based on his/her
application of the tuple.

As a side note, the cardinality of rational numbers is the same as
those of integers - so both are "equally" infinite.

Regards,
Karthick

[Richard O'Keefe]

On 4/03/2011, at 5:49 PM, Karthick Gururaj wrote:
> I meant: there is no reasonable way of ordering tuples, let alone enum
> them.

There are several reasonable ways to order tuples.

>
> That does not mean we can't define them:
> 1. (a,b) > (c,d) if a>c

Not really reasonable because it isn't compatible with equality.

> 2. (a,b) > (c,d) if b>d
> 3. (a,b) > (c,d) if a^2 + b^2 > c^2 + d^2
> 4. (a,b) > (c,d) if a*b > c*d

Ord has to be compatible with Eq, and none of these are.
Lexicographic ordering is in wide use and fully compatible
with Eq.

> Which of
> these is a reasonable definition?

> The set of complex numbers do not
> have a "default" ordering, due to this very issue.

No, that's for another reason. The complex numbers don't have
a standard ordering because when you have a ring or field and
you add an ordering, you want the two to be compatible, and
there is no total order for the complex numbers that fits in
the way required.

>
> When we do not have a "reasonable" way of ordering, I'd argue to not
> have anything at all

There is nothing unreasonable about lexicographic order.
It makes an excellent default.

>
>
> As a side note, the cardinality of rational numbers is the same as
> those of integers - so both are "equally" infinite.

Ah, here we come across the distinction between cardinals and
ordinals. Two sets can have the same cardinality but not be
the same order type. (Add 1 to the first infinite cardinal
and you get the same cardinal back; add 1 to the first infinite
ordinal and you don't get the same ordinal back.)

[wren ng thornton]

On 3/3/11 2:58 AM, Antti-Juhani Kaijanaho wrote:
> On Thu, Mar 03, 2011 at 12:29:44PM +0530, Karthick Gururaj wrote:
>> Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
>> any case, my question is answered since it is not a tuple.
>
> It can be viewed as the trivial 0-tuple.

Except that this is problematic since Haskell doesn't have 1-tuples
(which would be distinct from plain values in that they have an extra
bottom).

In an idealized world, yes, unit can be thought of as the nullary
product which serves as left- and right-identity for the product
bifunctor. Unfortunately, Haskell's tuples aren't quite products.[1]

[1] To be fair, a lot of thought went into choosing for them to be the
way they are. The way they are generally matches the semantics we
desire, but this is one of the places where they don't. The only way to
"fix" this is to have two different product types, which is problematic
for the obvious reasons.

--
Live well,
~wren

[Karthick Gururaj]

On Fri, Mar 4, 2011 at 10:42 AM, Richard O'Keefe <o...@cs.otago.ac.nz> wrote:
>
> On 4/03/2011, at 5:49 PM, Karthick Gururaj wrote:
>> I meant: there is no reasonable way of ordering tuples, let alone enum
>> them.
>
> There are several reasonable ways to order tuples.
>>
>> That does not mean we can't define them:
>> 1. (a,b) > (c,d) if a>c
>
> Not really reasonable because it isn't compatible with equality.
>> 2. (a,b) > (c,d) if b>d
>> 3. (a,b) > (c,d) if a^2 + b^2 > c^2 + d^2
>> 4. (a,b) > (c,d) if a*b > c*d
>
> Ord has to be compatible with Eq, and none of these are.

Hmm.. not true. Can you explain what do you mean by "compatibility"?

One of the following, and exactly one, must always hold, on a ordered
set (is this what you mean by "compatibility"?), for any arbitrary
legal selection of a, b, c and d.
a. (a, b) EQ (c, d)
b. (a, b) LT (c, d)
c. (a, b) GT (c, d)

All the definitions above are compatible in this sense.

> Lexicographic ordering is in wide use and fully compatible
> with Eq.
>> Which of
>> these is a reasonable definition?
>
>> The set of complex numbers do not
>> have a "default" ordering, due to this very issue.
>
> No, that's for another reason.  The complex numbers don't have
> a standard ordering because when you have a ring or field and
> you add an ordering, you want the two to be compatible, and
> there is no total order for the complex numbers that fits in
> the way required.
>>
>> When we do not have a "reasonable" way of ordering, I'd argue to not
>> have anything at all
>
> There is nothing unreasonable about lexicographic order.
> It makes an excellent default.

Ok - at this stage, I'll just take your word for it. I'm not able to
still appreciate the choice of the default ordering order, but I need
to wait until I get to see/develop some real code.

>>
>>
>> As a side note, the cardinality of rational numbers is the same as
>> those of integers - so both are "equally" infinite.
>
> Ah, here we come across the distinction between cardinals and
> ordinals.  Two sets can have the same cardinality but not be
> the same order type.  (Add 1 to the first infinite cardinal
> and you get the same cardinal back; add 1 to the first infinite
> ordinal and you don't get the same ordinal back.)

:) Ok. The original point was whether there is a reasonable way to
enumerate a tuple, I guess there is none.

[Chris Smith]

On Mar 4, 2011 2:49 AM, "Karthick Gururaj" <karthick...@gmail.com> wrote:
> > Ord has to be compatible with Eq, and none of these are.
> Hmm.. not true. Can you explain what do you mean by "compatibility"?

Compatibility would mean that x == y if and only if compare x y == EQ.  This is not a restricrion enforced by the type system, but it is something that I would think ought to be true (though it is not,for example, for the IEEE floating point types; I personally consider that a bug and believe the IEEE notions of comparison ought to be exposed in a different set of operations rather than instances of Ord and Eq).  In this sense it is much like the monad laws.  So whether it has to be true depends on what you mean by "has to be".

> Ok - at this stage, I'll just take your word for it. I'm not able to
> still appreciate the choice of the default ordering order, but I need
> to wait until I get to see/develop some real code.

The most common use of Ord in real code, to be honest, is to use the value in some data structure like Data.Set.Set or Data.Map.Map, which requires Ord instances.  For this purpose, any Ord instance that is compatible with Eq will do fine.

--
Chris

[Ozgur Akgun]

On 4 March 2011 09:47, Karthick Gururaj <karthick...@gmail.com> wrote:

I'm not able to still appreciate the choice of the default ordering order,

I don't know if this will help you appreciate the default or not, but just to say this default is concordant with the auto-derived Ord instances.

data Tuple3 a b c = Tuple3 a b c

    deriving (Eq,Ord,Show)

ghci> sort [Tuple3 1 2 4, Tuple3 1 2 3, Tuple3 2 1 1, Tuple3 1 3 5]

[Tuple3 1 2 3,Tuple3 1 2 4,Tuple3 1 3 5,Tuple3 2 1 1]

ghci> sort [(1,2,4), (1,2,3), (2,1,1), (1,3,5)]

[(1,2,3),(1,2,4),(1,3,5),(2,1,1)]

No surprises here. Just another place where we have the lexicographic ordering by default.

HTH,

--
Ozgur Akgun

[Max Rabkin]

On Fri, Mar 4, 2011 at 17:37, Chris Smith <cds...@gmail.com> wrote:
> The most common use of Ord in real code, to be honest, is to use the value
> in some data structure like Data.Set.Set or Data.Map.Map, which requires Ord
> instances.  For this purpose, any Ord instance that is compatible with Eq
> will do fine.

It's true that you can build valid Maps and Sets with any valid
instance of Ord that defines a total order that is consistent with Eq,
and lookup, membership testing and insert will work. However, there
are operations on Maps and Sets which make the order visible to the
caller: min, max, splits, folds, etc.

--Max

[Markus Läll]

Sorry, I didn't mean to answer you in particular. I meant to say that for tuples you could (I think) have an enumeration over them without requiring any component be bounded.

An example of type (Integer, Integer) you would have:

[(0,0) ..] = [(0,0) (0,1) (1,0) (0,2) (1,1) (2,0) ... ]

where the order can be visualized by taking diagonals of a table starting from the upper left:

    0      1      2     ..
0 (0,0)  (0,1)  (0,2) 
1 (1,0)  (1,1)  (1,2)
2 (2,0)  (2,1)  (2,2)
..

Would this also have an uncomputable order type? At least for comparing tuples you'd just:

lt :: (Integer,Integer) -> (Integer,Integer) -> Bool
(a,b) `lt` (c,d) = let
      sum1 = (a + b)
      sum2 = (c + d)
   in if sum1 == sum2
         then a < c
         else sum1 < sum2


Implementing fromEnum looks like a bit harder problem..


--
Markus Läll

[Alexander Solla]

On Fri, Mar 4, 2011 at 8:45 AM, Markus Läll <marku...@gmail.com> wrote:

Would this also have an uncomputable order type? At least for comparing tuples you'd just:

You can tell if an enumeration will have an uncomputable order type by whether or not your enumeration has to "count to infinity" before it can continue.  For example, let's use top-left to bottom-right diagonals.  Then you would have to "count infinitely many steps" (0,0), (1,1), (2,2), (3,3) ... before you could go to the next diagonal.  This excludes an enumeration from being computable in the usual sense (or having a computable order type).  As Daniel pointed out, every countable set can be put in some computable order, since it can inherit the order of the naturals through the enumeration. 

lt :: (Integer,Integer) -> (Integer,Integer) -> Bool
(a,b) `lt` (c,d) = let
      sum1 = (a + b)
      sum2 = (c + d)
   in if sum1 == sum2
         then a < c
         else sum1 < sum2

The order you impose is a bit broken, but the principle of using diagonals is sound. (Consider (1,2) and (2,1):  under this order, (1,2) `lt` (2,1) and (2,1) `lt` (1,2), so (1,2) == (2,1))

Indeed, the diagonal construction is how an enumeration of the rationals is demonstrated.

[Alexander Solla]

On Thu, Mar 3, 2011 at 10:14 PM, wren ng thornton <wr...@freegeek.org> wrote:

On 3/3/11 2:58 AM, Antti-Juhani Kaijanaho wrote:

On Thu, Mar 03, 2011 at 12:29:44PM +0530, Karthick Gururaj wrote:

Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
any case, my question is answered since it is not a tuple.

It can be viewed as the trivial 0-tuple.

Except that this is problematic since Haskell doesn't have 1-tuples (which would be distinct from plain values in that they have an extra bottom).

I don't get this line of thought.  I understand what you're saying, but why even bother trying to distinguish between bottoms when they can't be compared by equality, or even computed? The type (forall a . a) doesn't contain any values!   It is empty, and so is a subset of any other type.  If you choose to interpret all bottoms as being the same non-existent, unquantifiable (in the language of Haskell) "proto-value", you get the isomorphism between types a and (a), as types.  Indeed, those are the semantics in use by the language.  A value written (a) is interpreted as a.  A type written (a) is interpreted as a.  

In an idealized world, yes, unit can be thought of as the nullary product which serves as left- and right-identity for the product bifunctor. Unfortunately, Haskell's tuples aren't quite products.[1]

I'm not seeing this either.  (A,B) is certainly the Cartesian product of A and B.  In what sense are you using "product" here? Is your complaint a continuation of your previous (implicit) line of thought regarding distinct bottoms?

[Daniel Fischer]

On Friday 04 March 2011 17:45:13, Markus Läll wrote:
> Sorry, I didn't mean to answer you in particular. I meant to say that
> for tuples you could (I think) have an enumeration over them without
> requiring any component be bounded.

Yes, you can (at least mathematically, it may be different if you consider
actual Enum instances, then Int overflow has to be reckoned with).

The problem is with simultaneous Ord and Enum instances.
Let's call an

instance Ord A where ...

and an

instance Enum A where ...

compatible when toEnum and fromEnum are strictly monotonic, i.e.

x `rel` y <=> fromEnum x `rel` fromEnum y

for rel in { (<), (==), (>) }
and analogously for toEnum (restricted to legitimate arguments).
And let's ignore overflow, so pretend Int were infinite (so Int = Z).

That means, for compatible Ord and Enum instances, it follows that for any
x, y \in A with x <= y, the set { z \in A : x <= z && z <= y } is finite
[it has at most (fromEnum y - fromEnum x + 1) elements].

So when A is a tuple type and the Ord instance is lexicographic ordering,
a compatible Enum instance is only possible if

- at least one component is empty, or
- at most one component is infinite and only single-element types appear as
components before the infinite one.

Otherwise, if x1 < x2 and Y is infinite, the set
S(t) = { (x,y) : (x1,t) <= (x,y) && (x,y) <= (x2,t) }
is infinite because we can embed Y into it [foo y = if y < t then (x2,y)
else (x1,y)].

In fact, for any Enum instance, there is exactly one compatible Ord
instance, namely

x `rel` y <=> fromEnum x `rel` fromEnum y

Conversely, given an Ord instance, if there exists a compatible Enum
instance, fromEnum gives an order-isomorphism between A and a subset of the
integers. Then there are four main possibilities

1. A is finite
(then A has the order type of some natural number n = card(A))
2. A has a smallest element but not a largest
(then A has the order type of the natural numbers N)
3. A has a largest element but no smallest
(then A has the order type of Z-N)
4. A has neither a smallest nor a largest element
(then A has the order type of Z)

Anyway, there exists a compatible Enum instance (and then infinitely many),
if and only if A has the order type of a subset of the integers.

>
> An example of type (Integer, Integer) you would have:
>
> [(0,0) ..] = [(0,0) (0,1) (1,0) (0,2) (1,1) (2,0) ... ]

That's (Nat, Nat) rather than (Integer,Integer), not fundamentally
different, but simpler to handle.

>
> where the order can be visualized by taking diagonals of a table
> starting from the upper left:
>
> 0 1 2 ..
> 0 (0,0) (0,1) (0,2)
> 1 (1,0) (1,1) (1,2)
> 2 (2,0) (2,1) (2,2)
> ..
>
> Would this also have an uncomputable order type?

No, order type is that of N, if order is given by enumeration

> At least for comparing
> tuples you'd just:
>
> lt :: (Integer,Integer) -> (Integer,Integer) -> Bool
> (a,b) `lt` (c,d) = let
> sum1 = (a + b)
> sum2 = (c + d)
> in if sum1 == sum2
> then a < c
> else sum1 < sum2
>
>
> Implementing fromEnum looks like a bit harder problem..

That's pretty easy, in fact.

fromEnum (a,b) = t + a
where
s = a+b
t = (s*(s+1)) `quot` 2 -- triangular number

toEnum is a bit more difficult, you have to take a square root to see on
which diagonal you are

[Daniel Fischer]

On Friday 04 March 2011 22:33:20, Alexander Solla wrote:
> > Unfortunately, Haskell's tuples aren't quite products.[1]
>
> I'm not seeing this either. (A,B) is certainly the Cartesian product of
> A and B.

Not quite in Haskell, there

(A,B) = A×B \union {_|_}

_|_ and (_|_,b) are distinguishable.

(A,()) contains

- (a,()) for a in A
- (a, _|_) for a in A
- _|_

the three classes are distinguishable

case x of
(a,b) -> do
putStrLn "Bona fide tuple"
case b of
() -> putStrLn "With defined second component"

will produce different output for them.

In Haskell, |(A,B)| = |A|×|B| + 1 (and |()| = 2, () = { (), _|_ }),
and |(A,B,C)| = |A|×|B|×|C| + 1 etc.
So one would expect |(A)| = |A| + 1 by consistency for 1-tuples.

> In what sense are you using "product" here?

Set theoretic or more general, category theoretic, I presume.

> Is your complaint
> a continuation of your previous (implicit) line of thought regarding
> distinct bottoms?

I don't think distinguishing bottoms is the issue, but distinuishing bottom
from partially defined values.

[wren ng thornton]

On 3/4/11 4:33 PM, Alexander Solla wrote:
> On Thu, Mar 3, 2011 at 10:14 PM, wren ng thornton<wr...@freegeek.org> wrote:
>> On 3/3/11 2:58 AM, Antti-Juhani Kaijanaho wrote:
>>> On Thu, Mar 03, 2011 at 12:29:44PM +0530, Karthick Gururaj wrote:
>>>
>>>> Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
>>>> any case, my question is answered since it is not a tuple.
>>>>
>>>
>>> It can be viewed as the trivial 0-tuple.
>>>
>>
>> Except that this is problematic since Haskell doesn't have 1-tuples (which
>> would be distinct from plain values in that they have an extra bottom).
>>
>>
> I don't get this line of thought. I understand what you're saying, but why
> even bother trying to distinguish between bottoms when they can't be
> compared by equality, or even computed?

If we have,

data OneTuple a = One a

Then

_|_ /= One _|_

This can be detected by seq: the left-hand side doesn't terminate,
whereas the right-hand side does. And moreover, this can mess up other
things (e.g., monads) by introducing too much laziness. Space leaks are
quite a serious matter and they have nothing to do with trying to
compare uncomputable values. Do you want a seemingly insignificant
refactoring to cause your program to suddenly hang forever? Or to take
up gobs more space than it used to?

This is very similar to the problems that people run into because,

_|_ /= (\x -> _|_)

> The type (forall a . a) doesn't contain any values!

Nope, it contains one. Just ask any proof theorist, or anyone who uses
witnesses to capture information in the type system.

> If you choose to interpret all bottoms as being the same non-existent,
> unquantifiable (in the language of Haskell) "proto-value", you get the
> isomorphism between types a and (a), as types.

Nope, because we have

notBottom :: OneTuple a -> Bool
notBottom x = x `seq` True

whereas

isBottom :: a -> Bool
isBottom x = x `seq` True

> Indeed, those are the
> semantics in use by the language. A value written (a) is interpreted as a.
> A type written (a) is interpreted as a.

That's a syntactic matter. Those are parentheses of grouping, not
parentheses of tuple construction. For example, you can say:

(,) a b

or

(,,) a b c

But you can't say

() a

>> In an idealized world, yes, unit can be thought of as the nullary product
>> which serves as left- and right-identity for the product bifunctor.
>> Unfortunately, Haskell's tuples aren't quite products.[1]
>
> I'm not seeing this either. (A,B) is certainly the Cartesian product of A
> and B. In what sense are you using "product" here? Is your complaint a
> continuation of your previous (implicit) line of thought regarding distinct
> bottoms?

It is not the case that for every pair, ab, we have that:

ab == (fst ab, snd ab)

Why? Well consider ab = undefined:

_|_ /= (_|_,_|_)

I'm using "product" in the category theoretic sense, which is the sense
in which it applies to Compact Closed Categories (i.e., the models of
lambda calculi). Though it also works in the domain theoretic sense
(i.e., how people reason about laziness), since Haskell's tuples are
neither domain products nor smash products.

[Richard O'Keefe]

On 4/03/2011, at 10:47 PM, Karthick Gururaj wrote:

> On Fri, Mar 4, 2011 at 10:42 AM, Richard O'Keefe <o...@cs.otago.ac.nz> wrote:
>>
>> On 4/03/2011, at 5:49 PM, Karthick Gururaj wrote:
>>> I meant: there is no reasonable way of ordering tuples, let alone enum
>>> them.
>>
>> There are several reasonable ways to order tuples.
>>>
>>> That does not mean we can't define them:
>>> 1. (a,b) > (c,d) if a>c
>>
>> Not really reasonable because it isn't compatible with equality.
>>> 2. (a,b) > (c,d) if b>d
>>> 3. (a,b) > (c,d) if a^2 + b^2 > c^2 + d^2
>>> 4. (a,b) > (c,d) if a*b > c*d
>>
>> Ord has to be compatible with Eq, and none of these are.
> Hmm.. not true. Can you explain what do you mean by "compatibility"?

Trichotomy.
Ad definition 1:
(1,2) > (1,3) is false
(1,2) > (1,3) is false
but (1,2) ==(1,3) is also false.

Ad definition 2:
Same as definition 1 only flipped.

Ad definition 3:
(3,4) > (4,3) is false
(3,4) < (4,3) is false
but (3,4) ==(4,3) is also false.

Ad definition 4:

(1,0) > (0,1) is false
(1,0) < (0,1) is false
but (1,0) ==(0,1) is also false.

Ord is a subclass of Eq, after all.

>
> One of the following, and exactly one, must always hold, on a ordered
> set (is this what you mean by "compatibility"?), for any arbitrary
> legal selection of a, b, c and d.
> a. (a, b) EQ (c, d)
> b. (a, b) LT (c, d)
> c. (a, b) GT (c, d)
>
> All the definitions above are compatible in this sense.

As I just showed, none of them is.

>>> As a side note, the cardinality of rational numbers is the same as
>>> those of integers - so both are "equally" infinite.
>>
>> Ah, here we come across the distinction between cardinals and
>> ordinals. Two sets can have the same cardinality but not be
>> the same order type. (Add 1 to the first infinite cardinal
>> and you get the same cardinal back; add 1 to the first infinite
>> ordinal and you don't get the same ordinal back.)
>
> :) Ok. The original point was whether there is a reasonable way to
> enumerate a tuple, I guess there is none.

And the original point was about ordering, which is why it's
relevant that there are more order types than size types.

[Karthick Gururaj]

My definitions were incomplete, they need to be "extended" and not
taken as is. Let me define them completely for the sake of this
argument:
Defn 1. Given four arbitrary a, b, c and d on a set X which is an
instance of Ord (so a = b, a > b and a < b are defined), let:
(a, b) > (c, d) iff a > c (GT)
(a, b) < (c, d) iff a < c (LT)
(a, b) = (c, d) iff a = c. (EQ)
(please note that I'm redefining the EQ for pairs as well).

With this, the following hold:
(1, 2) = (1, 3)
(2, 1) > (1, 10)
(4, 0) < (5, 5)
It should be obvious that only one of GT, LT and EQ will hold, for any
arbitrary a, b, c, d.

Of course, the definition of EQ here is not what would be considered
"reasonable". I also see now, as I'm typing this, if we define EQ to
be the way it is in Haskell (which IS the reasonable way), then none
of my definitions of GT/LT will hold. Also, using the lexical compare
DOES fall in place with the EQ the way it is defined..

The confusion started for me as I thought of n-tuples as vectors in
n-dimensional space, on which one doesn't usually define GT and LT
operators. Now I see some light :)

[Richard O'Keefe]

On 7/03/2011, at 5:38 PM, Karthick Gururaj wrote:
> Defn 1. Given four arbitrary a, b, c and d on a set X which is an
> instance of Ord (so a = b, a > b and a < b are defined), let:
> (a, b) > (c, d) iff a > c (GT)
> (a, b) < (c, d) iff a < c (LT)
> (a, b) = (c, d) iff a = c. (EQ)
> (please note that I'm redefining the EQ for pairs as well).

Yes, I noted that. I'm painfully familiar with that ordering
from Smalltalk. (See LookupKey and Association.)

>
> Of course, the definition of EQ here is not what would be considered
> "reasonable".

Exactly so.

> I also see now, as I'm typing this, if we define EQ to
> be the way it is in Haskell (which IS the reasonable way), then none
> of my definitions of GT/LT will hold.

I may not have made it sufficiently clear when I mentioned Eq that I
meant "the definitions of Eq for tuples that come standard with Haskell".

> The confusion started for me as I thought of n-tuples as vectors in
> n-dimensional space, on which one doesn't usually define GT and LT
> operators. Now I see some light :)

n
Well, in n-dimensional space you are usually dealing with X for some
base set X. With a tuple (T1,...,Tn) the types T1,...,Tn are
often completely different.

For what it's worth, you _can_ define < on n-dimensional spaces,
and lexicographic order is a popular way to do it. You can even
put a total order on polynomials in a finite number of variables,
provided the coefficients come from an ordered set.

[Alexander Solla]

On Sat, Mar 5, 2011 at 5:06 AM, wren ng thornton <wr...@freegeek.org> wrote:

On 3/4/11 4:33 PM, Alexander Solla wrote:

On Thu, Mar 3, 2011 at 10:14 PM, wren ng thornton<wr...@freegeek.org>  wrote:

On 3/3/11 2:58 AM, Antti-Juhani Kaijanaho wrote:

On Thu, Mar 03, 2011 at 12:29:44PM +0530, Karthick Gururaj wrote:

Thanks - is this the same "unit" that accompanies IO in "IO ()" ? In
any case, my question is answered since it is not a tuple.

It can be viewed as the trivial 0-tuple.

Except that this is problematic since Haskell doesn't have 1-tuples (which
would be distinct from plain values in that they have an extra bottom).

I don't get this line of thought.  I understand what you're saying, but why
even bother trying to distinguish between bottoms when they can't be
compared by equality, or even computed?

If we have,

  data OneTuple a = One a

Then

   _|_ /= One _|_

That is vacuously true.  I will demonstrate the source of the contradiction later.  But you also have "_|_ == One _|_", by evaluation:

> Just undefined

Just *** Exception: Prelude.undefined

 

This can be detected by seq: the left-hand side doesn't terminate, whereas the right-hand side does. And moreover, this can mess up other things (e.g., monads) by introducing too much laziness. Space leaks are quite a serious matter and they have nothing to do with trying to compare uncomputable values. Do you want a seemingly insignificant refactoring to cause your program to suddenly hang forever? Or to take up gobs more space than it used to?

'seq' is not a "function", since it breaks referential transparency and possibly extensionality in function composition.  By construction, "seq a b = b", and yet "seq undefined b /= b".  Admittedly, the Haskell report and the GHC implementation, diverge on this issue.  Haskell98 specifically defines seq in terms of a comparison with bottom, whereas GHC "merely" reduces the first argument to WHNF.  In any case, the reduction is a side effect, with which can lead to inconsistent semantics if 'seq' is included in "the language". 

It is nice to know that we can work in a consistent language if we avoid certain constructs, such as 'seq', 'unsafePerformIO', and probably others.  In addition to making the "core language" conceptually simpler, it means that we can be sure we aren't inadvertently destroying the correctness guarantees introduced by the Howard-Curry correspondence theorem.

 

Nope, it contains one. Just ask any proof theorist, or anyone who uses witnesses to capture information in the type system.

I have studied enough proof theory, model theory, and lattice theory to know that there is room for both positions.  Just because you /can/ lift a lattice into one with bottom, it doesn't mean you /should/, if it means losing conceptual clarity.  In particular, I don't see why you want to generate an algebra of special cases that add no expressiveness, and include them in "the language", when you can use a quotient construction to remove them from the language.  As a practical matter, 'seq' is necessary.  But it should be treated as a special case (like unsafePerformIO), because it IS one.

 

Also, there is no need for a set to contain an element for it to be named or quantified over.  The empty set can be a witness just as well as a singleton set.  EmptyDataDecls works just as well whether you interpret (undefined :: Blah) to mean "a Blah that is not defined" or "a Blah that is the value 'undefined'".  Indeed, the latter is paradoxical.  'undefined = undefined' type checks, but it is not well-founded -- which is exactly why it is not defined!  'undefined' is not a value.   It is the name for a thing which cannot be evaluated.  We happen to know that there are a lot of things which cannot be evaluated, but the quotient construction treats them all the same.  (There is the practical issue of GHC handling Prelude.undefined differently than the other bottoms.  But I won't complain about that ;0)

If you choose to interpret all bottoms as being the same non-existent,
unquantifiable (in the language of Haskell) "proto-value", you get the
isomorphism between types a and (a), as types.

Nope, because we have

   notBottom :: OneTuple a -> Bool
   notBottom x = x `seq` True

whereas

   isBottom :: a -> Bool
   isBottom x = x `seq` True

 

seq is not a function, and is removed from consideration by the quotient construction I have mentioned, specifically because of how it behaves on bottom and the fact that the Haskell98 report defines it in terms of comparing values to bottom, an operation which is known to be impossible.  notBottom and isBottom are also not functions, for the same reason.

 

 

Indeed, those are the
semantics in use by the language.  A value written (a) is interpreted as a.
 A type written (a) is interpreted as a.

That's a syntactic matter. Those are parentheses of grouping, not parentheses of tuple construction. For example, you can say:

   (,) a b

or

   (,,) a b c

But you can't say

   () a

Does it matter?  We give syntax its semantics by interpreting it. The only reason we can say [] a  or (,) a is because they were included as special cases, for syntactic sugar.  As a matter of fact, it is entirely unnecessary to be able to introduce the machinery to express the type '(a)', because we can just express the isomorphic type 'a'.

  

In an idealized world, yes, unit can be thought of as the nullary product
which serves as left- and right-identity for the product bifunctor.
Unfortunately, Haskell's tuples aren't quite products.[1]

I'm not seeing this either.  (A,B) is certainly the Cartesian product of A
and B.  In what sense are you using "product" here? Is your complaint a
continuation of your previous (implicit) line of thought regarding distinct
bottoms?

It is not the case that for every pair, ab, we have that:

   ab == (fst ab, snd ab)

Why? Well consider ab = undefined:

   _|_ /= (_|_,_|_)

> (undefined, undefined)

(*** Exception: Prelude.undefined

That is as close to Haskell-equality as you can get for a proto-value that does not have an Eq instance.  As a consequence of referential transparency, evaluation induces an equivalence relation.  This implies that (_|_, _|_) = _|_ = (_|_, _|_).

I value referential transparency, and so reject constructs which violate it.  

Please demonstrate a proof that _|_ /= (_|_, _|_), so that I can exclude the unsound constructs you will undoubtedly have to use from my interpretation of "the language".  I am more interested in finding the consistent fragment of what you call Haskell than defending what I call Haskell.

[Alexander Solla]

On Mon, Mar 7, 2011 at 3:38 PM, Alexander Solla <alex....@gmail.com> wrote:

This can be detected by seq: the left-hand side doesn't terminate, whereas the right-hand side does. And moreover, this can mess up other things (e.g., monads) by introducing too much laziness. Space leaks are quite a serious matter and they have nothing to do with trying to compare uncomputable values. Do you want a seemingly insignificant refactoring to cause your program to suddenly hang forever? Or to take up gobs more space than it used to?

'seq' is not a "function", since it breaks referential transparency and possibly extensionality in function composition.  By construction, "seq a b = b", and yet "seq undefined b /= b".  Admittedly, the Haskell report and the GHC implementation, diverge on this issue.  Haskell98 specifically defines seq in terms of a comparison with bottom, whereas GHC "merely" reduces the first argument to WHNF.  In any case, the reduction is a side effect, with which can lead to inconsistent semantics if 'seq' is included in "the language". 

It is nice to know that we can work in a consistent language if we avoid certain constructs, such as 'seq', 'unsafePerformIO', and probably others.  In addition to making the "core language" conceptually simpler, it means that we can be sure we aren't inadvertently destroying the correctness guarantees introduced by the Howard-Curry correspondence theorem.

As a matter of fact, if you read GHC.Prim, you will see that seq is a bottom!

seq :: a -> b -> b

seq = let x = x in x

The "magic" semantics of evaluating the first argument are done by the compiler/runtime, and are apparently not expressible in Haskell.  This is true of

inline

lazy

unsafeCoerce

and dozens of others, all of which are expressed as specialized types with the same equation:

let x = x in x

[Daniel Fischer]

On Tuesday 08 March 2011 00:58:36, Alexander Solla wrote:
>
> As a matter of fact, if you read GHC.Prim, you will see that seq is a
> bottom!

No, you don't. GHC.Prim is a dummy module whose only purpose is to let
haddock generate documentation. Every function there has the code
let x = x in x, e.g.

plusWord# :: Word# -> Word# -> Word#
plusWord# = let x = x in x

minusWord# :: Word# -> Word# -> Word#
minusWord# = let x = x in x

undefined is not yet available, otherwise probably everything in GHC.Prim
would be pseudo-defined as undefined for haddock.

>
> seq :: a -> b -> b
> seq = let x = x in x
>
> The "magic" semantics of evaluating the first argument are done by the
> compiler/runtime, and are apparently not expressible in Haskell.

Right.
But neither is addition of Word# etc., for the primitives, you have to do
something special.

> This is true of
> inline
> lazy
> unsafeCoerce
>
> and dozens of others, all of which are expressed as specialized types
> with the same equation:
> let x = x in x

_______________________________________________

[wren ng thornton]

On 3/7/11 6:38 PM, Alexander Solla wrote:
> 'seq' is not a "function", since it breaks referential transparency and
> possibly extensionality in function composition. By construction, "seq a b
> = b", and yet "seq undefined b /= b". Admittedly, the Haskell report and
> the GHC implementation, diverge on this issue. Haskell98 specifically
> defines seq in terms of a comparison with bottom, whereas GHC "merely"
> reduces the first argument to WHNF. In any case, the reduction is a side
> effect, with which can lead to inconsistent semantics if 'seq' is included
> in "the language".
>
> It is nice to know that we can work in a consistent language if we avoid
> certain constructs, such as 'seq', 'unsafePerformIO', and probably others.
> In addition to making the "core language" conceptually simpler, it means
> that we can be sure we aren't inadvertently destroying the correctness
> guarantees introduced by the Howard-Curry correspondence theorem.

You are free to reason in whichever language you so desire. But that
does not mean the semantics of the language you desire are the same as
the semantics of Haskell. Fact of the matter is that Haskell has 'seq'
and bottom, even if you choose to call them non-functions or non-values.

>> It is not the case that for every pair, ab, we have that:
>>
>> ab == (fst ab, snd ab)
>>
>> Why? Well consider ab = undefined:
>>
>> _|_ /= (_|_,_|_)
>>
>
> > (undefined, undefined)
> (*** Exception: Prelude.undefined
>
> That is as close to Haskell-equality as you can get for a proto-value that
> does not have an Eq instance. As a consequence of referential transparency,
> evaluation induces an equivalence relation. This implies that (_|_, _|_) =
> _|_ = (_|_, _|_).
>
> I value referential transparency, and so reject constructs which violate it.
>
>
> Please demonstrate a proof that _|_ /= (_|_, _|_), so that I can exclude the
> unsound constructs you will undoubtedly have to use from my interpretation
> of "the language". I am more interested in finding the consistent fragment
> of what you call Haskell than defending what I call Haskell.

The trivial proof is:

seq _|_ () == _|_

/=

seq (_|_,_|_) () == ()

But you refuse to believe that 'seq' exists, so here's another proof:

case _|_ of (_,_) -> () == _|_

/=

case (_|_,_|_) of (_,_) -> () == ()

Do you refuse to believe that case analysis exists too?

[Daniel Fischer]

On Tuesday 08 March 2011 00:38:53, Alexander Solla wrote:
> On Sat, Mar 5, 2011 at 5:06 AM, wren ng thornton <wr...@freegeek.org>
wrote:
> >

> > If we have,
> >
> > data OneTuple a = One a
> >
> > Then
> >
> > _|_ /= One _|_
>
> That is vacuously true. I will demonstrate the source of the
> contradiction
>
> later. But you also have "_|_ == One _|_", by evaluation:
> > Just undefined
>
> Just *** Exception: Prelude.undefined
>

But that shows that _|_ and Just _|_ aren't the same (in Haskell), doesn't
it?

case x of
Just _ -> "Just something"
Nothing -> "Nothing"

produces "Just something" for (Just _|_), but not for _|_.

> > This can be detected by seq: the left-hand side doesn't terminate,
> > whereas the right-hand side does. And moreover, this can mess up
> > other things (e.g., monads) by introducing too much laziness. Space
> > leaks are quite a serious matter and they have nothing to do with
> > trying to compare uncomputable values. Do you want a seemingly
> > insignificant refactoring to cause your program to suddenly hang
> > forever? Or to take up gobs more space than it used to?
>
> 'seq' is not a "function", since it breaks referential transparency

Does it, if one assumes that 'seq a b' is *not* the same as 'b' ?

> and
> possibly extensionality in function composition. By construction, "seq
> a b = b", and yet "seq undefined b /= b". Admittedly, the Haskell
> report and the GHC implementation, diverge on this issue. Haskell98
> specifically defines seq in terms of a comparison with bottom, whereas
> GHC "merely" reduces the first argument to WHNF.

But reducing to WHNF is precisely what is needed to detect bottom.
If a value is a constructor application or a lambda, it's not bottom.

> In any case, the
> reduction is a side effect, with which can lead to inconsistent
> semantics if 'seq' is included in "the language".

But seq is "in the language", as specified by the report. You can argue
that it shouldn't and campaign for its removal, but it's in now and
speaking about Haskell, one can only sometimes ignore it.

> >
> > It is not the case that for every pair, ab, we have that:
> > ab == (fst ab, snd ab)
> >
> > Why? Well consider ab = undefined:
> > _|_ /= (_|_,_|_)
> >
> > (undefined, undefined)
>
> (*** Exception: Prelude.undefined
>
> That is as close to Haskell-equality as you can get for a proto-value
> that does not have an Eq instance. As a consequence of referential
> transparency, evaluation induces an equivalence relation. This implies
> that (_|_, _|_) = _|_ = (_|_, _|_).

But

case x of
(_, _) -> "Okay"

distinguishes _|_ and (_|_, _|_). In Haskell98 and Haskell2010, they are
not the same.

>
> I value referential transparency, and so reject constructs which violate
> it.
>
>
> Please demonstrate a proof that _|_ /= (_|_, _|_), so that I can exclude
> the unsound constructs you will undoubtedly have to use from

Pattern matching

> my interpretation of "the language".
> I am more interested in finding the
> consistent fragment of what you call Haskell than defending what I call
> Haskell.

That can be a source of much confusion. Usually, 'Haskell' is understood as
the language defined in the report. There's some room for interpretation,
but not too much. If you call soemthing too different 'Haskell', people
won't understand you.

[wren ng thornton]

On 3/7/11 6:58 PM, Alexander Solla wrote:
> The "magic" semantics of evaluating the first argument are done by the
> compiler/runtime, and are apparently not expressible in Haskell.

Of course this is true. The only ways of forcing evaluation in Haskell
are (a) to perform pattern matches on a value, (b) use 'seq'--- either
directly or in its disguised forms: strict data constructors and
-XBangPatterns.

In order to use pattern matching you need to know what the constructors
of the type are in order to force a choice between different
constructors; therefore you can't use case analysis to define a function
with the type and semantics of 'seq'.

But 'seq' is still defined in the Haskell report and therefore a part of
Haskell. Many have lamented the problems introduced by a parametric
polymorphic 'seq'; if it were just type-class polymorphic then it
wouldn't be such a problem. But then a type-class polymorphic 'seq'
could lead to maintenance issues similar to those faced by Java's
checked exceptions, which is why it was rejected from Haskell.

[Ben Moseley]

On 7 Mar 2011, at 23:38, Alexander Solla wrote:

   _|_ /= (_|_,_|_)

> (undefined, undefined)

(*** Exception: Prelude.undefined

That is as close to Haskell-equality as you can get for a proto-value that does not have an Eq instance.  As a consequence of referential transparency, evaluation induces an equivalence relation.  This implies that (_|_, _|_) = _|_ = (_|_, _|_).

Surely the key thing is the '(' character which is produced immediately before the exception is encountered.

I'd say that demonstrates that in GHC  _|_ /= (_|_,_|_).

--Ben