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

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

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.

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.

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

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

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

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

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

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

Dear Bill, It's not primarily a matter of efficiency, but rather of expressiveness. In a lazy language one can define an infinite list, pass it around as a value, and access particular elements of it "on demand". This demand-driven computation can be conceptually much cleaner than trying to carefully plan, in advance, which values should be computed in what order. See, for example: http://www.haskell.org/haskellwiki/Performance/Laziness http://lua-users.org/wiki/HammingNumbersVariant Best, Michael On 21 Mar 2009, at 16:06, Bill Lawvere wrote:

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

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