Re: Functions in programming

Re: Functions in programming

[Thorsten Altenkirch]

> There is one problem, of course: Haskell does not think this is
> legal as
> it thinks all datatypes should have at least one constructor.  (BTW do
> any functional languages allow NO constructors? They really should.)

Yes, Agda does.

> But now we have remembered that initial and final datatypes are
> supposed
> to coincide we have a blinding flash of inspiration:  because ()=1 is
> the final type it must also be the initial object.  So constant
> functions ARE the same as initial functions after all ....... so the
> student was not confused at all!
>
> Or was he?

I think it is a common misunderstanding that because you can write non-
terminating function that you should. Non-termination is a bug and it
is not what functional programming is about.

Btw, Agda is total, but you are allowed to ignore the termination
checker.

Thorsten

>
>
> -robin
>
>
> Robin Cockett, Calgary
>
>
>


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

Re: Functions in programming

[Bill Lawvere]

Thanks for the several interesting replies.
I think I am learning what "lazy" means, but
there seems to be embedded in it a presupposition
that the order in which new expressions are
introduced in a computation is something that
one does not carefully plan. It still seems to
me to be possible that the developing languages
are partly the legacy of an epoch when computational
power was qualitatively less than now.

I was especially heartened to see the lack of
support for St. John's position "in the beginning
was the word", especially in view of the recent
attempts by physicists to revive that idealist
position. Many of us have long instinctively
believed that language should fit concepts
and concepts should fit reality.

Bill


************************************************************
F. William Lawvere, Professor emeritus
Mathematics Department, State University of New York
244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA
Tel. 716-645-6284
HOMEPAGE:  http://www.acsu.buffalo.edu/~wlawvere
************************************************************



On Fri, 20 Mar 2009, Robin Cockett wrote:

> Peter Selinger wrote:
>> I hope that these examples help to dispell the view that untyped
>> languages, or lazy languages, are some kind of "practical hack"
>> invented by programmers and implementors that don't really fit any
>> mathematical model. Or, as Robin put it, "whose relation to standard
>> mathematical settings is surprisingly remote". Actually, the contrary
>> is very much true, and category theory is a large part of the reason.
>> [The same cannot, of course, be said for such languages as C, Fortran,
>> Perl, or Visual Basic, which actually *are* practical hacks with no
>> mathematical model. That is precisely why theoreticians study Haskell
>> or ML or Scheme or the lambda calculus or Agda or Charity and so
>> forth.]
>>
> Well I certainly did not intend to imply (or I think say) that lazy
> functional languages (Haskell) or other strict languages (the ML family)
> are hacks!  Absolutely not -- gosh I would loose my job!!!
>
> Clearly I should be clearer on what I did not say!
>
> For example I should be clear that things "whose relation to standard
> mathematical settings is surprisingly remote" can be (in fact usually
> are) extremely mathematical and important to the development of
> mathematical thought!   When I said that producing something from
> nothing  "may be a bit of a shock to a mathematician" this was not
> saying that, therefore it is not mathematical: the fact that Fermat's
> last theorem was proven may also have shocked a good few mathematicians
> who had not expected it.  In this case it is a shock in the sense that
> naively a mathematician may not have considered carefully what setting
> he was actually in ...
>
> I certainly did want to emphasize the sense in which a program language
> can be an exploration of a particular perspective (Mathematics by other
> means).   Furthermore, that there is a creative tension between
> implementation (which, in case anyone thinks otherwise, is -- if done
> well -- /very/ mathematical: for example in the case of the lambda
> calculus rests on the now extensive theory of rewriting) and semantics,
> which I view as prescriptive mathematics (typified by set theory and
> logic of the 1900s) in which one asserts far reaching axioms hoping
> madly that they are "right" -- or at least useful.
>
> Computer Scientists probably understand this best as simply the
> difference between a bottom-up and top-down approach -- played out
> perhaps on a slightly broader canvas -- and would instantly recognize
> the importance of both (as I am sure would mathematicians).
>
> Of course, it is nice if the two approaches meet.  (And if I did not
> know Peter better I might think that he is  saying that the whole
> business is nicely sewn up ...  nothing could be further from the
> truth!  Of course he didn't say this. It only may have sounded like he
> did! ;-) )
>
> If you will now forgive me for being a little colorful to reemphasize a
> point  ... (then that is definitely it from me!)
>
> The prescriptive approach, of course, is extremely arrogant: it says
> "this is what I want" and "this is how the world should be".  It was
> typified by the development of set theory whose the aim was to a pin
> down exactly what God had intended once and for all.   Of course, the
> real danger to this, much more serious than getting it wrong -- you can
> always fix that -- is that God is actually playing with a number of
> settings and hasn't really settled on which one he likes best!   The
> Greeks understood this perfectly 8-)       .
>
> This is where Category Theory slips into the picture: it is clearly
> stupid to study just one setting (unless God makes up his mind suddenly)
> instead lets just study them all!  Now in the process of dredging
> through God's basement (where he keeps his discarded ideas) it would
> definitely be rather disheartening if we found the lambda calculus
> (after all that is where HE keeps his discarded ideas)!  So let us
> suppose that this does not happen ... but  that we do find ("hiding
> under the wreckage of set theory" Paul Taylor quickly adds) a really
> nice implementable category which has a simple axiomatization and
> resembles the sort of naive mathematics that everyone uses.  Wouldn't it
> just be tempting to pull it out and implement it anyway?  ... and,
> strictly as a market ploy of course, put about that God had had an off
> day and had made a mistake?
>
> The point is that even if there is a base computational reality, we are
> in the altogether strange situation that we don't actually have to
> accept it!  Computation, just like mathematics, is open to
> prescription.  We can still choose to work in more restrictive settings
> where getting around (in some ways) may be easier (or safer).  And this
> is a important aspect of programming language and semantics research
> ...  in particular, being Turing complete is /not /an absolute
> requirement of a programming language (it is certainly something which
> one can ask about a language!).
>
> Far from the semantical/prescriptive approach to computation being
> dead,  it is more alive than ever ...  this is not an argument against
> computability, however, it IS an argument for the important role of
> Category Theory in Computer Science for helping us to understand the
> relationship between settings we might want to implement (... on which I
> think Peter agrees!)
>
> -robin

Re: Functions in programming

[Robin Cockett]

Peter Selinger wrote:
> I hope that these examples help to dispell the view that untyped
> languages, or lazy languages, are some kind of "practical hack"
> invented by programmers and implementors that don't really fit any
> mathematical model. Or, as Robin put it, "whose relation to standard
> mathematical settings is surprisingly remote". Actually, the contrary
> is very much true, and category theory is a large part of the reason.
> [The same cannot, of course, be said for such languages as C, Fortran,
> Perl, or Visual Basic, which actually *are* practical hacks with no
> mathematical model. That is precisely why theoreticians study Haskell
> or ML or Scheme or the lambda calculus or Agda or Charity and so
> forth.]
>
Well I certainly did not intend to imply (or I think say) that lazy
functional languages (Haskell) or other strict languages (the ML family)
are hacks!  Absolutely not -- gosh I would loose my job!!!

Clearly I should be clearer on what I did not say!

For example I should be clear that things "whose relation to standard
mathematical settings is surprisingly remote" can be (in fact usually
are) extremely mathematical and important to the development of
mathematical thought!   When I said that producing something from
nothing  "may be a bit of a shock to a mathematician" this was not
saying that, therefore it is not mathematical: the fact that Fermat's
last theorem was proven may also have shocked a good few mathematicians
who had not expected it.  In this case it is a shock in the sense that
naively a mathematician may not have considered carefully what setting
he was actually in ...

I certainly did want to emphasize the sense in which a program language
can be an exploration of a particular perspective (Mathematics by other
means).   Furthermore, that there is a creative tension between
implementation (which, in case anyone thinks otherwise, is -- if done
well -- /very/ mathematical: for example in the case of the lambda
calculus rests on the now extensive theory of rewriting) and semantics,
which I view as prescriptive mathematics (typified by set theory and
logic of the 1900s) in which one asserts far reaching axioms hoping
madly that they are "right" -- or at least useful.

Computer Scientists probably understand this best as simply the
difference between a bottom-up and top-down approach -- played out
perhaps on a slightly broader canvas -- and would instantly recognize
the importance of both (as I am sure would mathematicians).

Of course, it is nice if the two approaches meet.  (And if I did not
know Peter better I might think that he is  saying that the whole
business is nicely sewn up ...  nothing could be further from the
truth!  Of course he didn't say this. It only may have sounded like he
did! ;-) )

If you will now forgive me for being a little colorful to reemphasize a
point  ... (then that is definitely it from me!)

The prescriptive approach, of course, is extremely arrogant: it says
"this is what I want" and "this is how the world should be".  It was
typified by the development of set theory whose the aim was to a pin
down exactly what God had intended once and for all.   Of course, the
real danger to this, much more serious than getting it wrong -- you can
always fix that -- is that God is actually playing with a number of
settings and hasn't really settled on which one he likes best!   The
Greeks understood this perfectly 8-)       .

This is where Category Theory slips into the picture: it is clearly
stupid to study just one setting (unless God makes up his mind suddenly)
instead lets just study them all!  Now in the process of dredging
through God's basement (where he keeps his discarded ideas) it would
definitely be rather disheartening if we found the lambda calculus
(after all that is where HE keeps his discarded ideas)!  So let us
suppose that this does not happen ... but  that we do find ("hiding
under the wreckage of set theory" Paul Taylor quickly adds) a really
nice implementable category which has a simple axiomatization and
resembles the sort of naive mathematics that everyone uses.  Wouldn't it
just be tempting to pull it out and implement it anyway?  ... and,
strictly as a market ploy of course, put about that God had had an off
day and had made a mistake?

The point is that even if there is a base computational reality, we are
in the altogether strange situation that we don't actually have to
accept it!  Computation, just like mathematics, is open to
prescription.  We can still choose to work in more restrictive settings
where getting around (in some ways) may be easier (or safer).  And this
is a important aspect of programming language and semantics research
...  in particular, being Turing complete is /not /an absolute
requirement of a programming language (it is certainly something which
one can ask about a language!).

Far from the semantical/prescriptive approach to computation being
dead,  it is more alive than ever ...  this is not an argument against
computability, however, it IS an argument for the important role of
Category Theory in Computer Science for helping us to understand the
relationship between settings we might want to implement (... on which I
think Peter agrees!)

-robin

Re: Functions in programming

[Peter Selinger]

Robin Cockett wrote:
>
> SO (you are right) the first problem is that usually maps (as a category
> theorist is thinking of such) are not what is implemented.  Functional
> programming languages, for example, originate from combinatory algebra
> and the \lambda-calculus  ... typing is only really introduced
> retrospectively as useful sugar on this underlying structure ... what is
> implemented is application -- or at least a particular
> rewriting/reduction process of application.  A function A -> B is then a
> just a  term  which can be typed to be of type A -> B which can be
> applied to a term of type A to reduce (maybe) to something of type B
> ... application (as rewriting) is definitely the primitive and typing is
> retrospective  (although very nice and useful).
>
> However, at this stage it does /look/ deceptively categorical as one
> does define f :: A -> B!  And, of course that has led people to look at
> how one might interpret this as actually categorical ... and, of course,
> thereby hangs a lot of excellent work!
>
> However, what emerges is something whose relation to standard
> mathematical settings is surprisingly remote.  Lazy evaluation (mixed
> with non-termination/partiality) is definitely partly to blame for this ...

Hi all,

sorry for writing twice in one day. If I didn't know Robin better, I
would think he suggested that something is not categorical just
because the functions in question are not morphisms in Set, but in
some other category. And that the only "standard mathematical setting"
is the category of sets and functions! Of course he didn't say any of
these things. It only sounded like he did!

Robin's examples:

(1) The untyped lambda calculus. It is wrong to say that, in untyped
languages, functions have no domain or codomain. What is correct is
that there is just a single domain, which serves as the domain and
codomain of all functions. So a model of an untyped language is a
category with only one object U (but typically lots of morphisms).
Now, a non-trivial such category can evidently not be
cartesian-closed, because it cannot have an initial object.  However,
it *can* have binary products, internal function spaces, and even
binary coproducts. In other words, it is possible to find one-object
categories in which U = U x U, and U = U -> U, and possibly even
U = U + U (and a few additional properties). Such categories are
models of the untyped lambda calculus. The search for concrete
examples of such categories has led to lots of interesting
mathematical work, most of which is not category theory per se.
However, clearly category theory is the most appropriate language for
stating what properties a model has to satisfy.

Moreover, the constructions that Robin mentioned, by which one passes
from an untyped language to a typed language, are categorical in
nature.  One such construction is simply to split all idempotents.
Even starting from a one-object category such as the above, one ends
up with a cartesian-closed category with lots of objects, i.e., a
"typed" setting.

(2) Lazy languages. Here, an appropriate model is a category of
pointed DCPO's (for simplicity, take finite posets with a least
element, and monotone functions as the morphisms).  Note that we do
*not* require the morphisms to preserve the least element. The least
element of each poset represents a non-terminating computation in that
codomain. Functions that preserve the least element are called
"strict", and they correspond to "eager" computations (i.e., they are
forced to diverge if one of the inputs diverge). Functions that do not
necessarily preserve the least element are "lazy" computations. For
example, the "lazy booleans" are the three-element poset Bool={T,F,bot},
where T and F are incomparable, and bot is the bottom element. There
are exactly 11 lazy functions from Bool to Bool. 9 of them are eager, and
they correspond to every possible function f(bot)=bot, f(T)=a, f(F)=b,
where a,b in {T,F,bot}. 2 functions are not eager, and they are the
constant T and the constant F function (i.e., f(bot)=f(T)=f(F)=T, and
f(bot)=f(T)=f(F)=F).

Now clearly this category has a terminal object, namely the
one-element poset 1={bot}. It is equally obvious that 1 is not
initial, because there are for example 3 different monotone functions
from 1 to Bool. And of course, the two non-strict functions from 1 to
Bool are exactly the functions that Miles Gould so elegantly expressed
in Haskell. It is equally obvious that this category has no initial
object (and of course, for the same reason, neither does Haskell have
an initial type).

None of this is the least bit mysterious, neither mathematically, nor
from a programming perspective.

Robin mentioned the limit-colimit coincidence, but he forgot that this
only applies to directed limits. It is of course false that initial
objects and terminal objects always coincide, even in models where the
limit-colimit coincidence holds.

One may further object that the description of the particular category
of DCPO's is not really category theory, that it is ad hoc and not
particularly canonical (for example, it is not the free category of
any particular kind). And indeed, the devil is in the details and
there are many open problems regarding the existence of categories of
DCPO's that are suitable for particular purposes. However, there is
no question that category theory gives the correct tools for
specifying what kind of category one must construct, for discussing
alternatives between the different approaches, etc.



I hope that these examples help to dispell the view that untyped
languages, or lazy languages, are some kind of "practical hack"
invented by programmers and implementors that don't really fit any
mathematical model. Or, as Robin put it, "whose relation to standard
mathematical settings is surprisingly remote". Actually, the contrary
is very much true, and category theory is a large part of the reason.
[The same cannot, of course, be said for such languages as C, Fortran,
Perl, or Visual Basic, which actually *are* practical hacks with no
mathematical model. That is precisely why theoreticians study Haskell
or ML or Scheme or the lambda calculus or Agda or Charity and so
forth.]

-- Peter

Re: Functions in programming

[Peter Selinger]

Robin Cockett wrote:
>
> SO (you are right) the first problem is that usually maps (as a category
> theorist is thinking of such) are not what is implemented.  Functional
> programming languages, for example, originate from combinatory algebra
> and the \lambda-calculus  ... typing is only really introduced
> retrospectively as useful sugar on this underlying structure ... what is
> implemented is application -- or at least a particular
> rewriting/reduction process of application.  A function A -> B is then a
> just a  term  which can be typed to be of type A -> B which can be
> applied to a term of type A to reduce (maybe) to something of type B
> ... application (as rewriting) is definitely the primitive and typing is
> retrospective  (although very nice and useful).
>
> However, at this stage it does /look/ deceptively categorical as one
> does define f :: A -> B!  And, of course that has led people to look at
> how one might interpret this as actually categorical ... and, of course,
> thereby hangs a lot of excellent work!
>
> However, what emerges is something whose relation to standard
> mathematical settings is surprisingly remote.  Lazy evaluation (mixed
> with non-termination/partiality) is definitely partly to blame for this ...

Hi all,

sorry for writing twice in one day. If I didn't know Robin better, I
would think he suggested that something is not categorical just
because the functions in question are not morphisms in Set, but in
some other category. And that the only "standard mathematical setting"
is the category of sets and functions! Of course he didn't say any of
these things. It only sounded like he did!

Robin's examples:

(1) The untyped lambda calculus. It is wrong to say that, in untyped
languages, functions have no domain or codomain. What is correct is
that there is just a single domain, which serves as the domain and
codomain of all functions. So a model of an untyped language is a
category with only one object U (but typically lots of morphisms).
Now, a non-trivial such category can evidently not be
cartesian-closed, because it cannot have an initial object.  However,
it *can* have binary products, internal function spaces, and even
binary coproducts. In other words, it is possible to find one-object
categories in which U = U x U, and U = U -> U, and possibly even
U = U + U (and a few additional properties). Such categories are
models of the untyped lambda calculus. The search for concrete
examples of such categories has led to lots of interesting
mathematical work, most of which is not category theory per se.
However, clearly category theory is the most appropriate language for
stating what properties a model has to satisfy.

Moreover, the constructions that Robin mentioned, by which one passes
from an untyped language to a typed language, are categorical in
nature.  One such construction is simply to split all idempotents.
Even starting from a one-object category such as the above, one ends
up with a cartesian-closed category with lots of objects, i.e., a
"typed" setting.

(2) Lazy languages. Here, an appropriate model is a category of
pointed DCPO's (for simplicity, take finite posets with a least
element, and monotone functions as the morphisms).  Note that we do
*not* require the morphisms to preserve the least element. The least
element of each poset represents a non-terminating computation in that
codomain. Functions that preserve the least element are called
"strict", and they correspond to "eager" computations (i.e., they are
forced to diverge if one of the inputs diverge). Functions that do not
necessarily preserve the least element are "lazy" computations. For
example, the "lazy booleans" are the three-element poset Bool={T,F,bot},
where T and F are incomparable, and bot is the bottom element. There
are exactly 11 lazy functions from Bool to Bool. 9 of them are eager, and
they correspond to every possible function f(bot)=bot, f(T)=a, f(F)=b,
where a,b in {T,F,bot}. 2 functions are not eager, and they are the
constant T and the constant F function (i.e., f(bot)=f(T)=f(F)=T, and
f(bot)=f(T)=f(F)=F).

Now clearly this category has a terminal object, namely the
one-element poset 1={bot}. It is equally obvious that 1 is not
initial, because there are for example 3 different monotone functions
from 1 to Bool. And of course, the two non-strict functions from 1 to
Bool are exactly the functions that Miles Gould so elegantly expressed
in Haskell. It is equally obvious that this category has no initial
object (and of course, for the same reason, neither does Haskell have
an initial type).

None of this is the least bit mysterious, neither mathematically, nor
from a programming perspective.

Robin mentioned the limit-colimit coincidence, but he forgot that this
only applies to directed limits. It is of course false that initial
objects and terminal objects always coincide, even in models where the
limit-colimit coincidence holds.

One may further object that the description of the particular category
of DCPO's is not really category theory, that it is ad hoc and not
particularly canonical (for example, it is not the free category of
any particular kind). And indeed, the devil is in the details and
there are many open problems regarding the existence of categories of
DCPO's that are suitable for particular purposes. However, there is
no question that category theory gives the correct tools for
specifying what kind of category one must construct, for discussing
alternatives between the different approaches, etc.



I hope that these examples help to dispell the view that untyped
languages, or lazy languages, are some kind of "practical hack"
invented by programmers and implementors that don't really fit any
mathematical model. Or, as Robin put it, "whose relation to standard
mathematical settings is surprisingly remote". Actually, the contrary
is very much true, and category theory is a large part of the reason.
[The same cannot, of course, be said for such languages as C, Fortran,
Perl, or Visual Basic, which actually *are* practical hacks with no
mathematical model. That is precisely why theoreticians study Haskell
or ML or Scheme or the lambda calculus or Agda or Charity and so
forth.]

-- Peter

Re: Functions in programming

[Peter Selinger]

Hi all,

I am surprised that, in answer to one of Andrew Stacey's original
questions (i.e., how are mathematical functions related to functions
in computer programming), nobody has mentioned Moggi's work. I
originally replied to Andrew privately, thinking that surely my reply
would be one of dozens of more or less identical ones.

Here is what I wrote:

> Your wider question, on how functions in mathematics relate to
> functions in computing, is an interesting and well-studied question.
> In its simplest form, computer functions are the same as math
> functions, i.e., they input an argument from a set, and compute an
> output from another set. However, computer functions can have
> additional behaviors known as "side effects". Here are some examples
> of possible side-effects:
>
> (a) non-termination (loops forever)
> (b) non-determinism (can output several possible values on the same input)
> (c) probability (can call a random number generator)
> (d) input/output (can write stuff to the screen or to a file)
> (e) state (can "remember" some information from the last time it was called)
> (f) exceptions (can indicate an error condition, to be handled elsewhere)
> ...
>
> Interestingly, all of the above can be dealt with by using category
> theory. Each of these notions of side-effect corresponds to a
> particular strong monad on the category of sets. Each notion of
> function corresponds to a morphism in the corresponding Kleisli
> category.  This was discovered by Moggi in the 1980's, see the
> following paper, and particularly Example 1.1:
>
> Eugenio Moggi, "Notions of computation and monads". Information And
> Computation, 93(1), 1991.
> http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf

And I may further elaborate, in case it is not obvious, what the monad
is in each of the 6 examples of side-effects mentioned above:

(a) TX = X+1
(b) TX = powerset(X)
(c) TX = probability distributions on X
(d) For output: TX = X x Sigma^*
    For input: TX = X + Sigma->X + Sigma^2->X + ...
    (Here, Sigma is an alphabet, and Sigma^* the free monoid generated
    by it).
(e) TX = S -> (X x S), where S is a fixed set of states.
(f) TX = X + E, where E is a fixed set of exceptions.

It is straightforward to equip each of these operations with the
structure of a strong monad, and to convince yourself that the Kleisli
category in each case is the desired category of side-effecting
functions.

Of course this is not the end of the story: much further work has been
devoted to the question of how to combine several such monads (for
example, probability and state, or probability and non-determinism).
Also, in the presence of higher-order functions, Set is not always
good enough as a base category, and one typically considers other base
categories such as a suitable category of DCPOs.

So the question is not, as some have put it, whether non-termination
(or other side effects) are "good" or "bad" to have in a programming
language, but rather, what monad you would like to work with.

In response to Bill Lawvere's question: laziness refers to an
evaluation strategy where subterms are evaluated only if they are
actually needed. For example, an "eager" evaluation of the arithmetic
expression 0*(2+3) would first compute 2+3=5, then multiply the result
by 0. A "lazy" evaluation would recognize that computing 2+3 is
unnecessary. The question is not only one of efficiency, but also one
of termination: if instead of 2+3, we use a non-terminating
expression, then the lazy evaluation will terminate, whereas the eager
one will not. In a lazy language such as Haskell, you can implement a
function that computes the first 5 prime numbers as follows: (1)
compute the list L of all prime numbers, in increasing order, and (2)
take the first 5 elements of L. Since Haskell is lazy, it will
automatically only do as much work in step (1) as is actually needed
in step (2), i.e., it will not attempt to compute an infinite list.
This leads to a quite natural programming style, often reminiscent of
mathematical notation.

-- Peter

Andrew Stacey wrote:
>
> Here's a question for those who know about translating between
> category theory for mathematicians and category theory for computer
> programmers.
>
> In class today I was discussing functions with domain the empty set.
> The students don't have much background in formal set theory (and
> none in category theory though I'm doing my best to sneak it in
> where I can) so they were trying to get to grips with the idea that
> the _are_ functions from the empty set, but just not very many of
> them.
>
> Afterwards, one student asked about how this related to functions as
> used in computer programming.  It seemed from what he said that he
> had some understanding of the formal relationship between functions
> in mathematics and functions in computer programs - beyond them
> having the same name.  He said that a function that takes no input
> is known as a "constant function" and so wasn't sure how to fit the
> two notions together.
>
> I, on the other hand, am at the level of "Ooo, look!  Mathematicians
> and computer programmers both use the word 'function'.  So do
> biologists and event organisers.  Maybe we should organise a
> function whose function would be to investigate all these different
> uses.' so I didn't know what answer to give.
>
> The best that I could think of was that program functions have a
> 'hidden' input: the fact that they have been called.  So a function
> defined on the empty set corresponds to a function that can never be
> called.
>
> Can anyone help me straighten this out?
>
> Extra kudos for answers that I can just pass on to the student!
>
> Thanks,
>
> Andrew Stacey
>
>

Re: Functions in programming

[MigMit]

> However, what emerges is something whose relation to standard
> mathematical settings is surprisingly remote.  Lazy evaluation (mixed
> with non-termination/partiality) is definitely partly to blame for this ...

Can you elaborate a bit?

> Of course, this really will not seem at all mysterious to a Haskell
> programmer who will mutter about strictness and bottoms.  But it may be
> a bit of a shock to a mathematician!

Hm-m-m, aren't Haskell (or, in fact, all) programmers just a special
sort of mathematicians?

Re: Functions in programming

[Robin Cockett]

I am not sure whether you got a response to this ...  here is my attempt.

Bill Lawvere wrote:
>
> Question: Do the various programming languages explicitly
> implement the indispensible ingredient of categorical
> semantics, that every map has a unique codomain?
SO (you are right) the first problem is that usually maps (as a category
theorist is thinking of such) are not what is implemented.  Functional
programming languages, for example, originate from combinatory algebra
and the \lambda-calculus  ... typing is only really introduced
retrospectively as useful sugar on this underlying structure ... what is
implemented is application -- or at least a particular
rewriting/reduction process of application.  A function A -> B is then a
just a  term  which can be typed to be of type A -> B which can be
applied to a term of type A to reduce (maybe) to something of type B
... application (as rewriting) is definitely the primitive and typing is
retrospective  (although very nice and useful).

However, at this stage it does /look/ deceptively categorical as one
does define f :: A -> B!  And, of course that has led people to look at
how one might interpret this as actually categorical ... and, of course,
thereby hangs a lot of excellent work!

However, what emerges is something whose relation to standard
mathematical settings is surprisingly remote.  Lazy evaluation (mixed
with non-termination/partiality) is definitely partly to blame for this ...
>
> I don't know the technical meaning of "lazy"; was it an
> attempt to avoid the processing speed and ram needed to
> take account of the composition with inclusion maps,
> etcetera?
Lazy evaluation is basically a reduction strategy for the lambda
calculus.  It is a graph reduction strategy (you need a machine model
with pointers) which does a "by-name"/"by need" evaluation with sharing
of subexpressions which are duplicated in the rewriting process.

Sharing arises as in the reduction
                  S x y z => x z (y z)
if z is a big structure you don't want to duplicate it so you "share" it
... and this means also you can share any rewriting you do on that
structure.

In terms of the rewriting steps required on the lambda calculus this
reduction strategy is optimal  ... however, in storage requirements it
is often not optimal (so sometimes a "by-value" reduction will do better
under this criterion).

One feature of this rewriting technique is that it never looks at
subterms which will be eliminated. E.g. in
                      K x y => x
the contents of y will never be inspected (as there is apparently no
need).

Of course, this is all well and good, except, when y had happened to be
a term which did not terminate (i.e. had no support) , suddenly now one
can produce something very definite from nothing!

Of course this is what Miles Gould pointed out with a really simple
Haskell program (lovely!).  Even if you define the initial type
"correctly" you can still write

five :: Initial -> Int
five _ = 5

and actually get 5 from nowhere!

Of course, this really will not seem at all mysterious to a Haskell
programmer who will mutter about strictness and bottoms.  But it may be
a bit of a shock to a mathematician!

-robin

P.S.   Steve Vickers and Stevenson pointed out Chairman Mao plagiarized
O:-) :

According to the Penguin Dictionary of quotations:

Karl von Clausewitz (1780-1831): "War is nothing more than the
continuation of politics by other means".

Re: Functions in programming

[Bill Lawvere]

Question: Do the various programming languages explicitly
implement the indispensible ingredient of categorical
semantics, that every map has a unique codomain?

I don't know the technical meaning of "lazy"; was it an
attempt to avoid the processing speed and ram needed to
take account of the composition with inclusion maps,
etcetera?

Bill

************************************************************
F. William Lawvere, Professor emeritus
Mathematics Department, State University of New York
244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA
Tel. 716-645-6284
HOMEPAGE:  http://www.acsu.buffalo.edu/~wlawvere
************************************************************



On Tue, 17 Mar 2009, Robin Cockett wrote:

> Vaughan Pratt wrote:
>> The categories mailing list is a good one for this sort of discussion ...
> So here is some (gentle) push-back for Vaughan ...
>
> BTW thank you everyone for pointing out that /everything/ I said was
> wrong/right!   There really are underlying serious pedagogical and
> practical issue behind this ... typified by the comment.
>
>> Thorsten Altenkirch wrote:
>> > There really shouldn't be a difference between the functions in
>> > Mathematics and in Computer Science, especially functional programming.
>>
> The fact that nothing is quite what it "should be" in what has become
> the/a leading functional language is  bothersome on the one hand for
> students struggling to develop a (unified) mathematical view and,
> simultaneously  exciting for researchers who now have to find out which
> (!?!@!) category one is actually working in ... the fact that the answer
> is not an entirely simple (I do like Vaughan's "nuanced"!) is cause
> simultaneously for (pedagogical) concern and (researcher) delight.
>
> This reflects a general tension between semantics and implementation and
> the tussle over which is to be the cart and which is to be the horse.
> As it happens (I recall) one of the motivations behind Haskell was to
> produce a /lazy/ functional language and so a significant focus was
> actually on the implementation side ... perhaps at some semantical cost?
>
> Vaughan comments:
>> There should be differences within Mathematics and within Computer
>> Science, and therefore between them.
> I confess -- in this context -- what springs (uncalled) to mind is the
> (modified) comment of Chairman Mao: Computer Science is the continuation
> of Mathematics by other means!   ... and sometimes the balance between
> what /should/ be done and what /can/ be done is pushed too far.  At what
> stage this becomes a "bug" -- as Thorsten bluntly puts it -- definitely
> should be up for debate.  And there is no doubt in my mind that in
> making this judgment the clarity of the underlying (categorical)
> semantics adds an important perspective .... and even should be
> prescriptive.
>
> Semantics does have some "real" effects: the semantics that a programmer
> has in mind and what is actually implemented by a language/API can be
> rather different ... and this can become particularly subtle as
> languages become more abstract (and peculiar) and are built on top of
> each other.  Through these gaps can lie some very unexpected behaviors!
>
> Vaughan comments:
>> 2.  One should not assume that mathematics has the answer to every
>> practical problem.
> Oft quoted John Arbuthnot commented (some time ago!):
> "There are very few things which we know, which are not capable of being
> reduced to a Mathematical Reasoning; and when they cannot it's a sign
> our knowledge of them is very small and confused; and when a
> Mathematical Reasoning can be had it's as great a folly to make use of
> any other, as to grope for a thing in the dark, when you have a Candle
> standing by you."
>
> It really is hard to say more :-)  ... but maybe "candle" should be
> replaced "compact florescent light bulb"?
>
> -robin
>
>
>
>

Re: Functions in programming

[Robin Cockett]

Vaughan Pratt wrote:
> The categories mailing list is a good one for this sort of discussion ...
So here is some (gentle) push-back for Vaughan ...

BTW thank you everyone for pointing out that /everything/ I said was
wrong/right!   There really are underlying serious pedagogical and
practical issue behind this ... typified by the comment.

> Thorsten Altenkirch wrote:
> > There really shouldn't be a difference between the functions in
> > Mathematics and in Computer Science, especially functional programming.
>
The fact that nothing is quite what it "should be" in what has become
the/a leading functional language is  bothersome on the one hand for
students struggling to develop a (unified) mathematical view and,
simultaneously  exciting for researchers who now have to find out which
(!?!@!) category one is actually working in ... the fact that the answer
is not an entirely simple (I do like Vaughan's "nuanced"!) is cause
simultaneously for (pedagogical) concern and (researcher) delight.

This reflects a general tension between semantics and implementation and
the tussle over which is to be the cart and which is to be the horse.
As it happens (I recall) one of the motivations behind Haskell was to
produce a /lazy/ functional language and so a significant focus was
actually on the implementation side ... perhaps at some semantical cost?

Vaughan comments:
> There should be differences within Mathematics and within Computer
> Science, and therefore between them.
I confess -- in this context -- what springs (uncalled) to mind is the
(modified) comment of Chairman Mao: Computer Science is the continuation
of Mathematics by other means!   ... and sometimes the balance between
what /should/ be done and what /can/ be done is pushed too far.  At what
stage this becomes a "bug" -- as Thorsten bluntly puts it -- definitely
should be up for debate.  And there is no doubt in my mind that in
making this judgment the clarity of the underlying (categorical)
semantics adds an important perspective .... and even should be
prescriptive.

Semantics does have some "real" effects: the semantics that a programmer
has in mind and what is actually implemented by a language/API can be
rather different ... and this can become particularly subtle as
languages become more abstract (and peculiar) and are built on top of
each other.  Through these gaps can lie some very unexpected behaviors!

Vaughan comments:
> 2.  One should not assume that mathematics has the answer to every
> practical problem.
Oft quoted John Arbuthnot commented (some time ago!):
"There are very few things which we know, which are not capable of being
reduced to a Mathematical Reasoning; and when they cannot it's a sign
our knowledge of them is very small and confused; and when a
Mathematical Reasoning can be had it's as great a folly to make use of
any other, as to grope for a thing in the dark, when you have a Candle
standing by you."

It really is hard to say more :-)  ... but maybe "candle" should be
replaced "compact florescent light bulb"?

-robin

Re: Functions in programming

[Nathan Bloomfield]

> There is one problem, of course: Haskell does not think this is legal as
> it thinks all datatypes should have at least one constructor.

This works for me in Hugs:

data Void

foo :: Void -> ()
foo _ = ()

foo undefined = ()

Although it uses laziness and the fact that undefined is a member of every
type.

(Apologies Robin; I forgot to reply to the list!)

-Nathan Bloomfield, Arkansas

Re: Functions in programming

[Andrew Stacey]

Wow!  Thanks for _all_ the replies.  I certainly learnt a lot very quickly
just then.  The students seemed to get the basic idea - assuming that I didn't
mangle it.  One or two seemed to know a bit of category theory and so were
able to see a bit further than the others.

So thanks again.  Particularly, I'm very pleased that I was able to have an
answer for the next class.  I guess that the time zone helped there but even
so it was great to have so many answers so fast.

Andrew

Re: Functions in programming

[Miles Gould]

On Sun, Mar 15, 2009 at 04:18:41PM -0600, Robin Cockett wrote:
> If you want to define the initial object in a functional language you
> should write (say in Haskell):
>
> data Initial =
>      deriving (Show)   -- so we can display the elements

Unfortunately, this wouldn't be initial in Hask, because of two Haskell
features:

1) Every Haskell datatype contains at least one element, namely
"undefined", which represents (among other things) non-terminating
computations.
2) Haskell is a lazy language, and thus functions are not required to
preserve undefinedness.

So we can write as many functions Initial -> Int as we please:

one :: Initial -> Int
one _ = 1               -- The _ means "ignore this input"

five :: Initial -> Int
five _ = 5

seventeen :: Initial -> Int
seventeen _ = -17        -- XXX must get round to renaming this function
                         -- to reflect changed functionality

Calling these functions is as easy as

Hugs> one undefined
1
Hugs> five undefined
5
Hugs> seventeen undefined
-17
[D'oh!]

Hope that helps,

Miles

-- 
Men occasionally stumble over the truth, but most of them pick
themselves up and hurry on as if nothing had happened.
  -- Winston Churchill

Re: Functions in programming

[Tom Hirschowitz]

Dear all,

Before asking what the morphisms 0 -> A are, one should probably fix a
category.
This involves choosing a programming language and a notion of
equivalence for programs, and both choices impact on the existence of
an initial object.



1) A first possibility consists of choosing a programming language and
considering the category where:

  - objects are types (possibly a single one for untyped languages
such as Scheme),

  - morphisms A -> B are programs of type B with one variable of type
A (or variants such as the one proposed by Mike Schulman), considered
equivalent up to observational equivalence.

Observational equivalence might mean a lot of different things. Let us
here put

   M ~ N : A -> B

when for all P : B -> Bool and Q : 1 -> A, PMQ evaluates to true iff
PNQ evaluates to true.

(If your programming language allows infinite loops, you may replace
Bool with 1 and observe termination.)

Then, if your programming language has an empty type A, i.e., one
without any program 1 -> A, it is initial because M ~ N vacuously holds.
An example such programming language is Agda (using an inductive type
with no constructor).



2) However, in Haskell, you may define an inhabitant of all types by
typing the recursive definition

    bot = bot .

You may also define functions:

f x = True

and

g x = False

having all types A -> Bool, which are not equivalent because

f bot evaluates to True

while

g bot evaluates to False.



3) But there are other possible notions of equivalence! For example,
one may consider only beta, eta, ... equivalence. Then, even with an
empty type A, the functions

f x = True

and

g x = False

are different, hence A is not initial.



4) As a final remark, even in a consistent setting like Agda,
functions from the empty type are frequently applied (in an open
context), typically the canonical function (A * not A) -> B, which
looks like

f (x, y) = !(y(x)),

where !M = match M with {} -- case analysis on zero constructors.



  Pierre Hyvernat and Tom Hirschowitz

-- 

Re: Functions in programming

[Vaughan Pratt]

The categories mailing list is a good one for this sort of discussion:
it's hard to make sense of these issues without the abstract framework
of categories to interpret statements about the difference if any
between a function with no arguments and a function on the empty domain,
as the following examples make clear.

Steve Stevenson wrote:
 > All us Fortran II survivors know this issue well ... This is the
 > "function" versus "routine" argument: (1) a routine can have no
 > arguments but (2) can't return a value. This where CALL comes from.

In both Set and (bottomless) CPO a function (or routine) on the empty
domain is typed as 0 --> X, one with no arguments as 1 --> X (1 being
the empty product).  Andrew, in discussing 0 --> X with your students in
the context of ordinary sets and functions (the category Set) you might
also want to clarify how it differs from 1 --> X.  (Need 1 be identified
with Y^0 for any particular Y?  I would guess that a specific Y^0 should
be different from the empty dependent product but is that the case?  Any
dependent product experts?)

Robin Cockett wrote:
 > But now we have remembered that initial and final datatypes are supposed
 > to coincide we have a blinding flash of inspiration:  because ()=1 is
 > the final type it must also be the initial object.  So constant
 > functions ARE the same as initial functions after all ....... so the
 > student was not confused at all!
 >
 > Or was he?

Haskell datatypes naively are pointed CPOs (CPPO), in which case one
might expect the initial and final CPOs with bottom to coincide as the
zero object (0 = 1).  In that case the distinction between 0 --> X and 1
--> X would then vanish, in accordance with your story.

Without (ultimately) contradicting this, Makoto Hamana's slides at
http://www.cs.gunma-u.ac.jp/~hamana/Papers/cpo.pdf paint a more nuanced
picture comparing (bottomless) CPO, CPPO (which *lacks* an initial
object), and strict CPPO (all functions preserve bottom, unlike CPPO).
Hamana argues for the order-enriched version of the last as the
appropriate semantics for Haskell, where 0 = 1 remains the case, in
agreement with the intuitions and prior semantics of Haskell.  Other
languages may vary.

Thorsten Altenkirch wrote:
 > There really shouldn't be a difference between the functions in
 > Mathematics and in Computer Science, especially functional programming.

1.  There should be differences within Mathematics and within Computer
Science, and therefore between them.  Only in the narrow technical
definition of "function" as a morphism of Set should everyone be in
agreement as to what a function is.  But perhaps what you meant is that
mathematics and CS should recognize the same latitude in the conception
of function, which is reasonable given the difficulty of defining the
boundary between mathematics and CS.

2.  One should not assume that mathematics has the answer to every
practical problem.  Scientists and engineers indeed benefit enormously
from the tools of mathematics, in rough proportion to how many of them
they have at their fingertips, but when mathematics comes up short the
fault does not necessarily lie with the practitioners, who may from time
to time be in need of genuinely new mathematical methods.

 > However, there may be some historic differences. Many Mathematicians
 > still use classical set theory, where the set of functions is a
 > derived concept (i.e. a relation which has certain properties) while
 > in constructive theories (such as Type Theory) as in functional
 > programming, functions are a primitive concepts and they are always
 > computable (I like to say that a function which isn't computable
 > doesn't really function :-).

You constructivists can be so judgmental at times.  :)

 > Another potential confusion is that functional programming languages
 > allow the definition of partial functions which may not be
 > terminating. However, I think this is an unnecessary complication
 > because non-termination is just a bug and we are really only
 > interested in the total functions anyway.

Jimmy Treybig made a fortune from his company Tandem's line of NonStop
servers, see http://en.wikipedia.org/wiki/NonStop .

Computer scientists are confronted with Hobson's Choice of a programming
language that includes some partial recursive functions that diverge on
some inputs, and one that excludes some (total) recursive functions.  No
effectively compilable language can capture all and only the recursive
functions.  If you accept the former in order to avoid the latter, it is
unkind to call all the partial ones buggy, especially when the language
provides some means of getting useful work out of them.  If those
programs can't be analyzed as functions then how is functional
programming relevant to systems programming?  If they can, in what sense
do they terminate?

 > A constant function in functional programming as in set theory is a
 > function which always returns the same value. And clearly there is
 > only one function from the empty set into any set, because any two
 > functions are equal if they agree on all inputs and hence this
 > statement is vaccously true here. The problem in understanding this is
 > the usual trouble in understanding "ex falso quod libet".

I took Andrew's question to be more about existence of f: 0 --> X than
its uniqueness.  We could argue against its existence by noting that the
empty function diverges on every input and also converges on every
input.  Hence it is clearly inconsistent and therefore cannot exist.

It might seem like a bad joke, but some algebraists actually reason that
way to argue that the empty algebra does not exist.  We saw at UACT at
MSRI in 1993 that the authors of "Algebras, Lattices, Varieties: Volume
I" (Volume II still pending) forbid empty algebras because they were
unable to come up with a consistent way of quantifying over the empty
set.  For signatures with no constants, this creates the difficulty that
the subalgebras need not be closed under intersection because of the
possibility of disjoint nonempty subalgebras.  In order to make the set
Sub A of subalgebras of an algebra A a lattice under inclusion, the
authors of ALV created the notion of a subuniverse as a subalgebra that
is allowed to be empty, and define Sub A to be the set of *subuniverses*
of A.  They spell out this arrangement with admirable clarity in
Definition 1.3, and at least one of them insists to this day that
maintaining separate notions of subalgebra and subuniverse in order to
work around the paradoxes of the empty universe is just fine, with no
explanation as to why the inconsistencies supposedly created by empty
algebras do not arise for empty subuniverses.  One side effect of this
algebraic apartheid is that the initial lattice doesn't exist; more
generally varieties without constants don't have initial algebras, only
free algebras on nonempty sets.

Vaughan Pratt

Re: Functions in programming

[Daniel Schüssler]

Hello,

On Sunday 15 March 2009 23:18:41 Robin Cockett wrote:
> There is one problem, of course: Haskell does not think this is legal as
> it thinks all datatypes should have at least one constructor.

With GHC you can have empty types if you include the {-#
OPTIONS -XEmptyDataDecls #-} pragma :)


Greetings,
Daniel

Re: Functions in programming

[Robin Cockett]

The simple questions ARE the good ones ...  and one should certainly not
stop the confusing there!

If you want to define the initial object in a functional language you
should write (say in Haskell):

data Initial =
     deriving (Show)   -- so we can display the elements

After all clearly the initial object is the (inductive) datatype with
zero constructors.  Clearly you then should be able to write perfectly
good programs such as the identity function and the case on this datatype.

idinit:: Initial -> Initial
idinit x = x

init:: Initial -> a
init x = case x of           -- well there are no cases!

There is one problem, of course: Haskell does not think this is legal as
it thinks all datatypes should have at least one constructor.  (BTW do
any functional languages allow NO constructors? They really should.)  No
matter we can try to be a little cleverer and cheat the system by having
a constructor which we cannot construct anyway ...

data Initial = ZZ initial
     deriving (Show)   -- so we can display the elements

This has no elements ... just try to inductively construct them.   So
this works fine as the  initial datatype ... or does it?  At this stage
we belatedly remember we are not quite in the world we expect as initial
and final datatypes coincide so we do actually have a perfectly good
element in this datatype.

forever:: Initial
forever = ZZ forever

You do have to be patient as it does takes a bit of time to display it
... :-)

OK so that did not work!!

But now we have remembered that initial and final datatypes are supposed
to coincide we have a blinding flash of inspiration:  because ()=1 is
the final type it must also be the initial object.  So constant
functions ARE the same as initial functions after all ....... so the
student was not confused at all!

Or was he?

-robin


Robin Cockett, Calgary

Re: Functions in programming

[Ellis D. Cooper]

To Andrew Stacey -

My take on your question is that in programming, functions correspond
in mathematics to partially defined functions. A properly coded
programming function must either return the result of a computation
for given inputs, or return a signal that the programming function is
not defined on the inputs provided. The empty mathematical function
would correspond to the programming function that returns that
"undefined" signal for all inputs whatsoever.

Ellis D. Cooper

Re: Functions in programming

[Thorsten Altenkirch]

There really shouldn't be a difference between the functions in
Mathematics and in Computer Science, especially functional programming.

However, there may be some historic differences. Many Mathematicians
still use classical set theory, where the set of functions is a
derived concept (i.e. a relation which has certain properties) while
in constructive theories (such as Type Theory) as in functional
programming, functions are a primitive concepts and they are always
computable (I like to say that a function which isn't computable
doesn't really function :-).

Another potential confusion is that functional programming languages
allow the definition of partial functions which may not be
terminating. However, I think this is an unnecessary complication
because non-termination is just a bug and we are really only
interested in the total functions anyway.

A constant function in functional programming as in set theory is a
function which always returns the same value. And clearly there is
only one function from the empty set into any set, because any two
functions are equal if they agree on all inputs and hence this
statement is vaccously true here. The problem in understanding this is
the usual trouble in understanding "ex falso quod libet".

Cheers,
Thorsten


On 13 Mar 2009, at 11:29, Andrew Stacey wrote:

> Here's a question for those who know about translating between
> category theory
> for mathematicians and category theory for computer programmers.
>
> In class today I was discussing functions with domain the empty
> set.  The
> students don't have much background in formal set theory (and none
> in category
> theory though I'm doing my best to sneak it in where I can) so they
> were
> trying to get to grips with the idea that the _are_ functions from
> the empty
> set, but just not very many of them.
>
> Afterwards, one student asked about how this related to functions as
> used in
> computer programming.  It seemed from what he said that he had some
> understanding of the formal relationship between functions in
> mathematics and
> functions in computer programs - beyond them having the same name.
> He said
> that a function that takes no input is known as a "constant
> function" and so
> wasn't sure how to fit the two notions together.
>
> I, on the other hand, am at the level of "Ooo, look!  Mathematicians
> and
> computer programmers both use the word 'function'.  So do biologists
> and event
> organisers.  Maybe we should organise a function whose function
> would be to
> investigate all these different uses.' so I didn't know what answer
> to give.
>
> The best that I could think of was that program functions have a
> 'hidden'
> input: the fact that they have been called.  So a function defined
> on the
> empty set corresponds to a function that can never be called.
>
> Can anyone help me straighten this out?
>
> Extra kudos for answers that I can just pass on to the student!
>
> Thanks,
>
> Andrew Stacey
>
>


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

Re: Functions in programming

[Steve Stevenson]

All us Fortran II survivors know this issue well ... This is the
"function" versus "routine" argument: (1) a routine can have no
arguments but (2) can't return a value. This where CALL comes from.

Sent from my iPhone

Steve Stevenson


On Mar 13, 2009, at 7:29, Andrew Stacey <andrew.stacey@math.ntnu.no>
wrote:
> (a lot snipped)
> In class today I was discussing functions with domain the empty
> set.  The
> students don't have much background in formal set theory (and none
> in category
> theory though I'm doing my best to sneak it in where I can) so they
> were
> trying to get to grips with the idea that the _are_ functions from
> the empty
> set, but just not very many of them.
>
>

Re: Functions in programming

[Miguel Mitrofanov]

On 14 Mar 2009, at 06:22, Michael Shulman wrote:
> Normal programming languages do not generally come
> with predefined types that admit no values, since such types are
> evidently not very useful!

That's not exactly true. There is a huge area of type-level
programming (or metaprogramming, as it's called sometimes), and empty
types are useful as some sort of "flags" in this type of programming.
Of course, you can allow some values of this types, but this is what
makes no sense in this case.

Re: Functions in programming

[Luis Barbosa]

On 2009/03/13, at 11:29, Andrew Stacey wrote:

>
> Afterwards, one student asked about how this related to functions
> as used in
> computer programming.  It seemed from what he said that he had some
> understanding of the formal relationship between functions in
> mathematics and
> functions in computer programs - beyond them having the same name.
> He said
> that a function that takes no input is known as a "constant
> function" and so
> wasn't sure how to fit the two notions together.

A constant function in Haskell, as in Maths, has 1 as a domain. The
(isomorphism class of the)
singleton set is written as (); so, for example, the function always
returning integer 5 is declared as

five :: () -> Int

and defined by five () = 5 (notice notation () is used to denote both
set 1 and its (unique) element)

Your student is probably confusing notation () with the empty set.
The notation may be a bit unfortunate
as () may suggest "no input" ... but, of course functions, in
functional programming are just
functions.

Luis
---------------------------------------
Luis S. Barbosa
www.di.uminho.pt/~lsb

Re: Functions in programming

[Vaughan Pratt]

> I, on the other hand, am at the level of "Ooo, look!  Mathematicians and
> computer programmers both use the word 'function'.  So do biologists and event
> organisers.  Maybe we should organise a function whose function would be to
> investigate all these different uses.'

Even a perfunctory analysis should indicate that the attendees would be
likely to come away disfunctional.  :)

> The best that I could think of was that program functions have a 'hidden'
> input: the fact that they have been called.  So a function defined on the
> empty set corresponds to a function that can never be called.
>
> Can anyone help me straighten this out?

That's easy: just have them visualize a function as a list of its values
at the points in its domain enumerated in some fixed order.  Programmers
can easily see how many lists of length n there are for any given size
of codomain of the function (e.g. lists of bits as functions to {0,1}).
  The empty list should hold no terrors for programmers: in particular
they should know it exists, and they should know why there aren't two
empty lists.

Vaughan Pratt

Re: Functions in programming

[Fred E.J. Linton]

Andrew asked (I snip heavily):

> Here's a question for those who know about translating between category
theory
> for mathematicians and category theory for computer programmers.
> 
> In class today I was discussing functions with domain the empty set. ...
> ... [One student reported]
> that a function that takes no input is known as a "constant function" and
so
> wasn't sure how to fit the two notions together.

I think "constant function" should be reserved for functions
that *do* take input, but care not a whit what that input is,
always providing the same output regardless what the input.

A function with empty domain, on the other hand, never even has
a chance of getting called (as you so correctly observe below), 
hence has *no* output whatsoever (and is certainly not a 
constant function).

> The best that I could think of was that program functions have a 'hidden'
> input: the fact that they have been called.  So a function defined on the
> empty set corresponds to a function that can never be called.

Think your student would be able to digest that? If suitably
premasticated, perhaps?

Cheers, -- Fred 

Re: Functions in programming

[Michael Shulman]

Hi Andrew,

(Caveat: I'm not an expert in this field, although I find it fascinating,
so I hope that the experts who are listening will forgive and correct any
misstatements.)

I think your answer ("a function defined on the empty set corresponds
to a function that can never be called") is almost right.  A
programming function having n arguments x_1,...,x_n can be represented
by a set-theoretic function whose domain is an n-ary cartesian product:

A_1 \times ... \times A_n  -->  B

where A_i is the set of values in the type of the variable x_i, and B
is the output type of the function.  Thus, for instance, a function
of two variables with type Int whose output is type Real would be
represented by

Z \times Z --> R

where Z is the set of integers and R the set of real numbers (or
maybe the set of floating-point values, depending on what "Real"
means to your compiler).  Of course, the set-theoretic function is
"extensional," meaning it only knows what output results from each
list of inputs rather than how that output is computed; thus many
different pieces of code will denote the same function.  The fancy
word for this is "denotational semantics."

Now setting n=0, we see that a programming function of no arguments is
represented by a morphism

1 --> B

where 1, a one-element set, is a zero-ary cartesian product.  In other
words, it is just a constant (global) element of B.

The way to represent a function with empty domain in programming is as
a function whose input is of a -type- that admits no values.  Thus,
this function "can never be called" because there is no argument that
you can give it.  Normal programming languages do not generally come
with predefined types that admit no values, since such types are
evidently not very useful!

You can define a good approximation to such a type in an OO language
by writing a class whose only constructor throws a fatal error; thus
there will be no possible "values" having that type.  Of course, there
will then be many different "functions" in the programming sense that
you could write whose domain is such a type, but they will all have
the same denotation, namely the unique function from the empty set to
the set of values of their output type.


By the way, this all assumes that your programming functions are
"strict" in the "call-by-value" sense that all their arguments must be
completely computed before the function is allowed to execute.
However, if you allow "lazy" functions which can ignore some of their
input, which exist in some programming languages, then there can be
plenty of different functions defined on an "empty" type.  For
instance, in a lazily evaluated language the function with one input
of an empty type and defined by "return 3" can still be evaluated and
will promptly return 3.  Since it never -uses- its input, the lazy
language won't even bother trying to figure out what that input is,
and hence won't encounter the fatal error that the input doesn't exist.

In denotational semantics, this is modeled by working, not in a
category of sets, but in a category of a special sort of -posets-.
Among other properties, these posets always have bottom elements,
which represent the "undefined" value, but the functions between them
are not required to preserve the bottom elements.  Such a category
generally has no initial object; the "empty" type corresponds to the
one-element poset, but there are in general many functions out of this
object.

Best,
Mike

On Fri, Mar 13, 2009 at 6:29 AM, Andrew Stacey
<andrew.stacey@math.ntnu.no> wrote:
> Here's a question for those who know about translating between category theory
> for mathematicians and category theory for computer programmers.
>
> In class today I was discussing functions with domain the empty set.  The
> students don't have much background in formal set theory (and none in category
> theory though I'm doing my best to sneak it in where I can) so they were
> trying to get to grips with the idea that the _are_ functions from the empty
> set, but just not very many of them.
>
> Afterwards, one student asked about how this related to functions as used in
> computer programming.  It seemed from what he said that he had some
> understanding of the formal relationship between functions in mathematics and
> functions in computer programs - beyond them having the same name.  He said
> that a function that takes no input is known as a "constant function" and so
> wasn't sure how to fit the two notions together.
>
> I, on the other hand, am at the level of "Ooo, look!  Mathematicians and
> computer programmers both use the word 'function'.  So do biologists and event
> organisers.  Maybe we should organise a function whose function would be to
> investigate all these different uses.' so I didn't know what answer to give.
>
> The best that I could think of was that program functions have a 'hidden'
> input: the fact that they have been called.  So a function defined on the
> empty set corresponds to a function that can never be called.
>
> Can anyone help me straighten this out?
>
> Extra kudos for answers that I can just pass on to the student!
>
> Thanks,
>
> Andrew Stacey
>
>
>

Re: Functions in programming

[Charles Wells]

In terms of common mathematical usage, the student was wrong to say
that a constant function is a function with no input.  A constant
function can be defined on any domain; its defining characteristic is
that it has the same value for every input.

In categorical terms, a constant function is a function that factors
through the terminal object.  The empty function to an object should
be defined as the unique function from the initial object to that
object, but I am not claiming that is common usage.

Some computer languages do indeed have functions with no inputs.
Their output can still vary since the definition may contain global
variables.   No doubt objects (in the sense of OOP) with global
variables can be modeled as objects in a slice category but now I am
out of my depth, so I will stop.

Charles Wells

On Fri, Mar 13, 2009 at 6:29 AM, Andrew Stacey
<andrew.stacey@math.ntnu.no> wrote:
> Here's a question for those who know about translating between category theory
> for mathematicians and category theory for computer programmers.
>
> In class today I was discussing functions with domain the empty set.  The
> students don't have much background in formal set theory (and none in category
> theory though I'm doing my best to sneak it in where I can) so they were
> trying to get to grips with the idea that the _are_ functions from the empty
> set, but just not very many of them.
>
> Afterwards, one student asked about how this related to functions as used in
> computer programming.  It seemed from what he said that he had some
> understanding of the formal relationship between functions in mathematics and
> functions in computer programs - beyond them having the same name.  He said
> that a function that takes no input is known as a "constant function" and so
> wasn't sure how to fit the two notions together.
>
> I, on the other hand, am at the level of "Ooo, look!  Mathematicians and
> computer programmers both use the word 'function'.  So do biologists and event
> organisers.  Maybe we should organise a function whose function would be to
> investigate all these different uses.' so I didn't know what answer to give.
>
> The best that I could think of was that program functions have a 'hidden'
> input: the fact that they have been called.  So a function defined on the
> empty set corresponds to a function that can never be called.
>
> Can anyone help me straighten this out?
>
> Extra kudos for answers that I can just pass on to the student!
>
> Thanks,
>
> Andrew Stacey
>
>
>



-- 
professional website: http://www.cwru.edu/artsci/math/wells/home.html
blog: http://sixwingedseraph.wordpress.com/
abstract math website: http://www.abstractmath.org/MM//MMIntro.htm
astounding math stories: http://www.abstractmath.org/MM//MMAstoundingMath.htm
personal website:  http://www.abstractmath.org/Personal/index.html

Functions in programming

[Andrew Stacey]

Here's a question for those who know about translating between category theory
for mathematicians and category theory for computer programmers.

In class today I was discussing functions with domain the empty set.  The
students don't have much background in formal set theory (and none in category
theory though I'm doing my best to sneak it in where I can) so they were
trying to get to grips with the idea that the _are_ functions from the empty
set, but just not very many of them.

Afterwards, one student asked about how this related to functions as used in
computer programming.  It seemed from what he said that he had some
understanding of the formal relationship between functions in mathematics and
functions in computer programs - beyond them having the same name.  He said
that a function that takes no input is known as a "constant function" and so
wasn't sure how to fit the two notions together.

I, on the other hand, am at the level of "Ooo, look!  Mathematicians and
computer programmers both use the word 'function'.  So do biologists and event
organisers.  Maybe we should organise a function whose function would be to
investigate all these different uses.' so I didn't know what answer to give.

The best that I could think of was that program functions have a 'hidden'
input: the fact that they have been called.  So a function defined on the
empty set corresponds to a function that can never be called.

Can anyone help me straighten this out?

Extra kudos for answers that I can just pass on to the student!

Thanks,

Andrew Stacey