A question about tuples

[Chad]

I read somewhere that fst() doesn't necessary give back the first
element; it only means that it gives back something with the same type
of the first element. Can someone give me an example of this?

Chad

[Mark T. B. Carroll]

Chad <cda...@gmail.com> writes:

Hmm, I can't. I look forward to learning more!

Mark

[Dirk Thierbach]

So do I. The definition of "fst" according to the Haskell 98 Standard is

fst :: (a,b) -> a
fst (x,_) = x

and compilers should implement something equivalent to that, even if
their library source code differs. It's hard to imagine a situation where
this doesn't return the first element of a tuple.

- Dirk

[Albert Y. C. Lai]

There is no example. There are only two choices: non-terminate or give
back the first element.

There is a "free theorems" theorem about functions using parametric
polymorphism, like SML's and Haskell's (as opposed to ad-hoc
polymorphism, like base class and subclasses). Vaguely speaking,
precisely because you are not allowed subclassing or "instance of", you
cannot play tricks like "if the type is Int, I do one thing; if the type
is Char, I do an entirely different thing...", and therefore polymorphic
functions must behave very uniformly across types.

Specifically, for a terminating function of type (a,b)->a such as fst,
the free theorem states:

for all f, g, x, y of the right types: (assume they all terminate)
f (fst (x,y)) = fst (f x, g y)

Now I use it to prove:
e1 = fst (e1,e2)

Plug f = const e1, g = const e2 into the free theorem, get:
const e1 (fst (x,y)) = fst (const e1 x, const e2 y)
e1 = fst (e1,e2)

So if fst terminates it must give back the first element.

A paper on "free theorems" is Phil Wadler's "Theorems for Free!":
http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps

[jon.gallagher.04]

On Apr 8, 4:27 pm, "Albert Y. C. Lai" <tre...@vex.net> wrote:
> Vaguely speaking, precisely [...]
Awesome!

> for all f, g, x, y of the right types: (assume they all terminate)
> f (fst (x,y)) = fst (f x, g y)

Which is close to saying that projection is a natural transformation;
however, not quite, because f and g may be partial maps.
This is why restriction categories are important; they "axiomatize"
partiality. With respect to this question, they allow the
"correct" definition of partial product; the pairing of maps <f,g> is
as defined as both f and g are, and <f,g> fst if defined
is equal to f and <f,g> snd if defined is equal to g. The point is
this makes fst a lax natural transformation in a certain sense
that is exactly captured by "assuming they all terminate," but the
laxness condition removes the need to assume things terminate.

Restriction categories
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.126.3753&rep=rep1&type=pdf
Partial products with respect to restriction categories
http://arxiv.org/abs/math/0610500

[jon.gallagher.04]

However, the interesting thing here is that normal order reduction
never evaluates the second argument, so <f,g> fst is in a sense
defined everywhere that f is! This is very interesting, or at least
odd! This says that fst actually increases the "totalness" of a
function (namely <f,g>). Which means in the presence of normal order/
lazy reduction, totalness can be increased. Indeed, take the nowhere
defined function
undefined :: a
and the identity
id :: b -> b
And do
(fst(id,undefined)) x
And you will get x.

This discussion convinces me that normal order/lazy evaluation has an
odd effect on the partiality of functions with respect to
composition. I admit, I really don't understand what is going on!