- Haskell-Cafe - Haskell.org

Re: [Haskell-cafe] Category theory as a design tool
by wren ng thornton 23 Jun '11

23 Jun '11

On 6/22/11 3:59 PM, Arnaud Bailly wrote: > Hello Greg and Alexander, > Thanks for your replies. Funnily, I happen to own the 3 books you mentionned > :-) My interest in category theory is a long standing affair... > > Note that owning a book, having read (most of) it and knowing a theory (or > at least its principles and main concepts) is really quite a different thing > from being able to apply it. One of the big benefits I see to using category theory for dealing with programming languages comes from using CT as a generalized logic for equational reasoning. In particular, making use of the ideas of (co)limits and adjunctions in order to prove that something must behave in a particular way. This requires a bit of work to contort your thinking into the patterns of CT, but it means that once you can prove that something is a foo, then all the theorems about foos will apply. Just having a diagram and knowing it commutes doesn't tell you a whole lot, it just says that one particular equation holds. The real power comes from looking at diagrams that are parametric (since then proving it holds will mean it holds for all parameter valuations), or looking at diagrams where one of the arrows is (essentially) unique (since then you can show things that look like foos actually are foos). That is, the real power of diagrams comes from the quantifiers, which are explained in the text rather than shown in the diagram itself. As an example of this approach, see my comments in the thread about anonymous sum types. For something to be a product means that a particular diagram commutes: namely, a product is the limit of the two point category (and coproducts are the colimit). One of the many things this tells us is that if we posit that A*A ~ A in a category that "has products", we must infer that the category is a meet-(pre)semilattice[1]. [1] Or a really goofy structure where for every A and B there are at most two A->B, with a canonical way of distinguishing them. Of course, for this to be a category we need to define a composition operator, which will take the four compositions into the two possible arrows, which is where it gets strange. -- Live well, ~wren

3 2

Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?
by wren ng thornton 23 Jun '11

23 Jun '11

On 6/22/11 6:00 PM, Casey McCann wrote: > On Wed, Jun 22, 2011 at 2:19 PM, wren ng thornton<wren(a)freegeek.org> wrote: >>>> [1] modulo the A:+:A ~ A issue. >> >> Oops, I should've said A:*:A there. >> >>> That issue is exactly my concern, though, and it seems a bit too >>> thorny to handwave aside. >> >> Indeed. If we have A:*:A ~ A, then A:*:A is not a categorical product. > (...) > > Thank you, that clarified my intuitive sense of why it didn't seem to > work. The same argument, with arrows flipped appropriately, would > apply to a hypothetical coproduct where A :+: A ~ A, wouldn't it? It should. But let's make sure... A coproduct of A and B is an object A+B along with morphisms inl :: A -> A+B and inr :: B -> A+B, such that for any object C and morphisms c1 :: A -> C and c2 :: B -> C, there exists a unique c1|||c2 :: A+B -> C such that c1|||c2 . inl = c1 and c1|||c2 . inr = c2. All of this is the straightforward dualizing of products. So, lets assume A ~ A+A. And lets assume we have some functions inl and inr. Now, for every pair of functions f, g :: A -> C we must come up with a unique function h :: A+A -> C such that h . inl = f and h . inr = g. By isomorphism this is the same as coming up with a unique function h' :: A -> C such that h' . iso . inl = f and h' . iso . inr = g. If inl = inr, then it follows that f = g. Consequently there can only be one morphism between any two objects, so the category is a preorder. If the category has all coproducts then it's a join-semilattice--- exactly dual to the meet-semilattice case for products. If we want a category more interesting than a preorder, then we must have that inl and inr are different. We must find two injection functions which keep their images in A+A apart, so that we can define partial functions -|||g and f|||- which don't conflict with each other (so that they can be combined into the total function f|||g). The obvious way to do that is to use tagged/disjoint unions, but we can't do that since we've assumed A ~ A+A. Basically, the type A+A isn't big enough (whereas before, the values of type A*A weren't big/informative enough). I'm playing a bit fast and loose with the notion of "big/informative enough". Perhaps someone more familiar with large ordinals can come up with a counter example. But if they do, I'm sure it wouldn't be a very intuitive place to program in. -- Live well, ~wren

1 0

Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?
by wren ng thornton 23 Jun '11

23 Jun '11

On 6/21/11 10:48 PM, Casey McCann wrote: > On Tue, Jun 21, 2011 at 9:51 PM, wren ng thornton<wren(a)freegeek.org> wrote: >> I don't think there are any problems[1]. > (...) >> [1] modulo the A:+:A ~ A issue. Oops, I should've said A:*:A there. > That issue is exactly my concern, though, and it seems a bit too > thorny to handwave aside. Indeed. If we have A:*:A ~ A, then A:*:A is not a categorical product. The reasoning is as follows. An object A*B with morphisms fst :: A*B->A and snd :: A*B->B is a product iff for all objects P with morphisms p1 :: P -> A and p2 :: P -> B, there is a unique morphism p1&&&p2 :: P -> A*B, such that p1 = fst . p1&&&p2 and p2 = snd . p1&&&p2. Given the definition, if we further say that A*A ~ A, then it's clear that we can't come up with any satisfactory definitions of fst and snd which obey the laws--- unless there can be only one morphism between any two objects, in which case we know that p1 = p2 and so it's okay for fst = snd; or unless there can be only two morphisms between any two objects and we have a canonical property for distinguishing them so that we can correlate p1 with fst and p2 with snd. In all other cases, there are simply too many possible choices of p1 and p2, and there's no way for fst and snd to carry enough information to make the equations hold. What that means then is that the category which tries to use :*: to make products would only have products in the cases where the first and second component are different; which would be a strange category indeed. Alternatively, it could always have products but would only allow one morphism between objects; in which case the category is just a meet-semilattice (actually, the preorder generalization thereof). > In contrast, ordered pairs and disjoint unions are tidy, simple, and obvious. Disjoint pairs are sufficient; they needn't be ordered. All we need is that they are "tagged" in the same way that disjoint unions are, so that we can distinguish the components of A*A. -- Live well, ~wren

5 5

Graph diagram tools?
by Dmitri O.Kondratiev 23 Jun '11

23 Jun '11

Hi, I am looking for Haskell library to create graph diagrams in png or similar formats. Thanks!

4 3

Re: [Haskell-cafe] category theory as a design tool
by Brett Giles 22 Jun '11

22 Jun '11

Hi Arnaud, you may want to look at http://mathcs.mta.ca/research/rosebrugh/Easik/ This is a java tool which allows entity design using various cat theory constraints such as sum, product and pullbacks. Brett Giles Sent from my iPhone > Message: 14 > Date: Wed, 22 Jun 2011 14:06:21 -0500 > From: Gregg Reynolds <dev(a)mobileink.com> > Subject: Re: [Haskell-cafe] Category theory as a design tool > To: Arnaud Bailly <arnaud.oqube(a)gmail.com> > Cc: Haskell Cafe <haskell-cafe(a)haskell.org> > Message-ID: <BANLkTingApLo7ysYGgg1DUxbW5iK1kLmrQ(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > On Tue, Jun 21, 2011 at 11:30 PM, Arnaud Bailly <arnaud.oqube(a)gmail.com> > wrote: >> (2nd try, took my gloves off...) >> Hello Caf?, >> I have been fascinated by Cat. theory for quite a few years now, as >> most people who get close to it I think. >> >> I am a developer, working mostly in Java for my living and dabbling >> with haskell and scala in my spare time and assuming the frustration >> of having to live in an imperative word. More often than not, I find >> myself trying to use constructs from FP in my code, mostly simple >> closures and typical data types (eg. Maybe, Either...). I have read >> with a lot of interest FPS (http://homepages.mcs.vuw.ac.nz/~tk/fps/) >> which exposes a number of OO patterns inspired by FP. >> >> Are there works/thesis/books/articles/blogs that try to use Cat. >> theory explicitly as a tool/language for designing software (not as an >> underlying formalisation or semantics)? Is the question even >> meaningful? > > You might try: Category Theory for Computing > Science<http://www.cwru.edu/artsci/math/wells/pub/ctcs.html> (Barr > and Wells) > > and Conceptual Mathematics: a first introduction to > categories<http://books.google.com/books/about/Conceptual_mathematics.html?id=o1tHw4W5…> > (Lawvere) > > "Kinship and Mathematical Categories" (by Lawvere) is also interesting. > > -Gregg > >> >> Thanks in advance, >> Arnaud >> >> _______________________________________________ >> Haskell-Cafe mailing list >> Haskell-Cafe(a)haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >

1 0

Homework help - calculator function
by SM Design 22 Jun '11

22 Jun '11

I have a homework which is very important to be done but I can't complete the task at all. The program i should write is: Make calculator- function in Haskell. The function argument is a list of strings and also form such list, as each string of the argument made definite action. • If the string has the form of an arithmetic expression - calculate this expression. The string result becomes part of the list- result. If the expression contains a variable which is not assigned value, the result is displayed "undefined". • If the string has the form Name = value calculated from the last expression is assigned to the variable with the corresponding name in the list, and in the result list is formed a string with type name = ... where the site stands blank corresponding value. If there is not a calculated expression to be assigned to form a string "no value". • If the string is non-blank, but there is a species different from the above two case, form the string "error". • If the string is empty, incl. when it contains only spaces, in the result there is not form a string. Expressions consist of integers without sign variables, operations + (Addition), - (subtraction), * (multiplication) and / (divide) and parentheses. Where no brackets, the operations are performed from left to right, but * and / precede the + and -. Implementation of any operation gives integer; in the division rejected the fractional part , if any . Variables have names of one letter - from the Latin small letter . In the beginning, end or between the elements of each row can have spaces - they are irrelevant to its correctness. Example: the list-argument ["3 +7 / 2" "2 + x", "= s", "2 * s +4", "", "2 + +4 / 5] function should provide a result-list ["6", "undefined", "s = 6", "16", "error"]. Thank you an advance!

4 3

Verifying Haskell programs vs. generating verified Haskell programs
by Uli Kastlunger 22 Jun '11

22 Jun '11

Hello Haskell fellows, recently there has been a huge progress in generating real programs by specifying them in interactive theorems prover like Isabelle or Coq, in particular a verified C Compiler has been generated out of a specification in Coq [0]. Furthermore it is often stated, that it is easier to reason about functional languages. So in my opinion there are two approaches building verified software (e.g. in case of compilers: verify that the semantics of a high-level language maps correctly to the semantics of a low-level language). (0) Programming in any language and then verifying it with an external theorem prover (1) Specifying the program in a proof language and then generating program code out of it (like in the CompCert project) I think both ideas have their (dis)advantages. The question is, which concept will be used more frequently? In particular how hard would it be to build something like CompCert the other way around (in this case writing a C compiler in SML and proving its correctness?) Best regards, Uli Kastlunger [0] http://compcert.inria.fr/

4 5

Re: [Haskell-cafe] Getting library documentation for installed packages on Windows
by John Ky 22 Jun '11

22 Jun '11

Hi Svein, Where can I find this file on Windows 7 or Windows generally if its all the same? Cheers, -John On 22 June 2011 10:15, Svein Ove Aas <sveina(a)gmail.com> wrote: > Yes, cabal does this if you have haddock installed. > > You'll probably have to edit .cabal/config, though. The relevant options > should be fairly obvious in there. > On Jun 22, 2011 12:52 AM, "John Ky" <newhoggy(a)gmail.com> wrote: > > Hi all, > > > > Lately I've been finding the Network module missing from the docs I > download > > from the GHC website, which brings me to the question: > > > > Is there any way I could generate libraries for this, the core libraries > and > > all installed cabal packages into one reference so I can work offline? > > > > Cheers, > > > > -John >

2 2

Re: [Haskell-cafe] PhD studentship in Functional Programming
by Graham Hutton 22 Jun '11

22 Jun '11

Dear all, Just a quick reminder that the deadline for receiving applications for this PhD studentship position is this Friday (24th June.) Best wishes, Graham > +------------------------------------------------------------------+ > > PhD Studentship in Functional Programming > > School of Computer Science > University of Nottingham, UK > > Applications are invited for a fully-funded PhD studentship in > the Functional Programming Lab in the School of Computer Science > at the University of Nottingham, starting on 1st October 2011, > under the supervision of Prof Graham Hutton. > > The suggested topic for the studentship is to develop a practical > implementation of the worker/wrapper transformation, a simple but > powerful unifying paradigm for program optimisation, but other > ideas for possible topics are welcome too. The studentship is > for three and a half years, and includes a maintenance grant > of 13,590 UK pounds per year, and tuition fees. > > Applicants for the position will require a first-class Honours > degree (or equivalent) in Computer Science and/or Mathematics, > some experience in functional programming, and an aptitude for > mathematical subjects. Additional desirable attributes include > a Masters degree, and/or some experience in programming language > semantics, implementation and optimisation. Due to the nature > of the funding, the position is only open to UK citizens, or EU > citizens who have resided in the UK for the last three years. > > The successful applicant will work under the supervision of Prof > Graham Hutton in the FP Lab in Nottingham, a leading centre for > research on functional programming. The group currently comprises > 5 academic staff, 1 research fellow, and 10 PhD students. > > In order to apply, please submit the following to Prof Graham > Hutton (graham.hutton(a)nottingham.ac.uk) by 24th June 2011: an > up-to-date copy of your CV (including the results of all your > University examinations to date) along with a brief covering > letter that describes your experience in functional programming, > your reasons for wishing to pursue a PhD in this area, and any > ideas you have regarding possible research directions. > > Closing date for applications: 24th June 2011. > > +------------------------------------------------------------------+ > > -- > Graham Hutton > Functional Programming Lab > School of Computer Science > University of Nottingham, UK > http://www.cs.nott.ac.uk/~gmh This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. 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.

1 0

Fwd: Re: Hackage Server not reachable
by Steffen Schuldenzucker 22 Jun '11

22 Jun '11

Forwarding to -cafe. -------- Original Message -------- Subject: Re: [Haskell-cafe] Hackage Server not reachable Date: Wed, 22 Jun 2011 20:43:59 +1000 From: Stuart Coyle <stuart.coyle(a)gmail.com> To: Steffen Schuldenzucker <sschuldenzucker(a)uni-bonn.de> Cabal fails with a timeout like this: stuart@Panforte:~/Code/gift-parser# cabal update Downloading the latest package list from hackage.haskell.org <http://hackage.haskell.org> cabal: timeout From traceroute it seems that I'm having routing problems. traceroute to hackage.haskell.org <http://hackage.haskell.org> (69.30.63.204), 64 hops max, 52 byte packets 1 moodle-server (192.168.1.1) 1.834 ms 0.923 ms 0.904 ms 2 10.67.0.1 (10.67.0.1) 18.781 ms 10.031 ms 14.738 ms 3 rdl2-ge2.gw.optusnet.com.au <http://rdl2-ge2.gw.optusnet.com.au> (198.142.160.5) 13.442 ms 11.920 ms 8.767 ms 4 mas2-ge10-1-0-904.gw.optusnet.com.au <http://mas2-ge10-1-0-904.gw.optusnet.com.au> (211.29.125.138) 55.286 ms 56.473 ms 58.150 ms 5 mas3-ge11-0.gw.optusnet.com.au <http://mas3-ge11-0.gw.optusnet.com.au> (211.29.125.241) 61.473 ms 58.477 ms 56.198 ms 6 203.208.192.169 (203.208.192.169) 202.737 ms 207.018 ms 209.159 ms 7 lap-brdr-03.inet.qwest.net <http://lap-brdr-03.inet.qwest.net> (63.146.26.145) 173.527 ms 174.207 ms lap-brdr-03.inet.qwest.net <http://lap-brdr-03.inet.qwest.net> (63.146.26.149) 172.122 ms 8 tuk-edge-13.inet.qwest.net <http://tuk-edge-13.inet.qwest.net> (67.14.4.206) 235.820 ms 237.548 ms 246.359 ms 9 206.81.193.22 (206.81.193.22) 334.748 ms 511.734 ms 303.460 ms 10 209.162.220.81 (209.162.220.81) 310.886 ms 244.478 ms 241.544 ms 11 * * * 12 * * * 13 * * * continues like this.... I'll get a fix from this end. Time to call the ISP. I wonder if any others in Australia on Optus' network are having the same issue? Thanks all. On Wed, Jun 22, 2011 at 7:16 PM, Steffen Schuldenzucker <sschuldenzucker(a)uni-bonn.de <mailto:sschuldenzucker@uni-bonn.de>> wrote: On 06/22/2011 11:02 AM, Stuart Coyle wrote: I cannot reach the hackage server so cabal can't download packages. Have I the correct address? http://hackage.haskell.org Yes. stuart@rumbaba:~# resolveip hackage.haskell.org <http://hackage.haskell.org> <http://hackage.haskell.org> IP address of hackage.haskell.org <http://hackage.haskell.org> <http://hackage.haskell.org> is 69.30.63.204 Same result for me. I also cannot access any of the Hackage web pages. No problem here. What is the error for you? hackage.haskell.org <http://hackage.haskell.org> doesn't seem to answer pings btw. -- Steffen -- Stuart Coyle stuart dot coyle at gmail dot com

1 0