tag:blogger.com,1999:blog-12622806237205945732024-03-28T07:32:41.440+00:00Dan Ghica's Personal BlogMostly programming language semantics with a dash of armchair philosophy.
The views expressed here are personal and in no way reflect those of my employers. Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.comBlogger23125tag:blogger.com,1999:blog-1262280623720594573.post-42655086730039032252022-05-30T14:47:00.005+01:002022-05-30T16:59:37.879+01:00Understanding the issue of equality in Homotopy Type Theory (HoTT) is easier if you are a programmerWe programmers know something that mathematicians don't really appreciate: equality is a tricky concept. Lets illustrate this with a straightforward example in some generic OO programming language. I am trying to make this language-independent and neither use any exotic concepts nor ban any common ones, but use whatever makes the issue easy to illustrate. interface Real;interface Complex: Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-11510733729551732612022-02-14T15:53:00.006+00:002022-04-14T13:18:42.288+01:00MGS 2022: String diagrams for monoidal closed categoriesBetween 10-13 April 2022 I will teach an advanced course at the Midlands Graduate School, on the topic of string diagrams for monoidal closed categories. String diagrams are a graphical formalism for category theory which found recent widespread applications in areas as diverse as quantum computing or computational linguistics. These languages are based on compact-closed categories, a Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-72680387402456050072020-04-19T10:01:00.003+01:002020-04-21T15:54:08.901+01:00Teaching CompilersFor the first time in my 15 years as a lecturer I got to teach Compilers. I have written compilers before and I have published a bunch of research papers on the topic, so I considered myself reasonably qualified to teach it. I had also taught Compilers Workshop before, a hands-on project oriented course on building a working compiler. So from my own experience and from observing Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com4tag:blogger.com,1999:blog-1262280623720594573.post-50691050021564770302019-11-04T16:27:00.002+00:002019-11-04T20:29:38.587+00:00Making OCaml more like ExcelExcel, spreadsheet programming in general, is broadly considered a very accessible style of programming. Could we make functional programming more like Excel programming? Or, rather, how can we extract what is appealing about spreadsheet programming and graft it onto a functional programming language?
I will give an answer here. This is an answer rather than the answer because whether Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-49136872009062174282019-09-04T14:33:00.000+01:002019-09-04T14:33:00.761+01:00Discovering Category Theory with primary school children
A few years ago I ran a maths circle for primary school children experimenting with teaching category theory. The meetings were documented in a series of blog posts which were recently published as a series of articles by Mathematics Teaching, the journal of the Association of Teachers of Mathematics (issues 264-268).
I am posting a copy of the articles (PDF) with Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-47384585531496524512019-07-16T14:02:00.000+01:002019-07-16T14:03:53.587+01:00This is not a Turing MachineThe Wikipedia page on Turing Machines shows the following picture as an implementation of a Turing Machine:
I didn't see any problem with that picture until I got into an intricate discussion with my colleague and friend Paul Levy about 'realistic' models for costs of computation. One of the basic premises for such a model is that individual atomic operations have fixed and constant costs in Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com3tag:blogger.com,1999:blog-1262280623720594573.post-62096306509015666132019-07-02T20:02:00.003+01:002019-07-02T20:02:39.998+01:00A note on homogeneous integrationThis is a follow-on to my earlier post on automatic application modernisation.
In application modernisation the goal is to reduce a large monolithic application to a modular structure which can be deployed in containers and managed separately, e.g. with Kubernetes. The conventional approach relies on technologies such as web APIs or microservices to integrate the components. In the blog Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-21181474423607419642019-06-28T11:19:00.000+01:002019-09-11T19:59:09.267+01:00An Automatic Application Modernisation Toolkit for the JVMMany large corporations have legacy enterprise applications which are web-enabled, sometimes migrated to the cloud, which are monolithic giants. To fully take advantage of what the cloud can offer, these applications need to be modernised, i.e. broken up into smaller apps which can be then containerised and managed using Kubernetes or related technologies.
There are a variety of technologies forDan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com3tag:blogger.com,1999:blog-1262280623720594573.post-38784412069940914982019-05-04T10:28:00.000+01:002019-05-04T10:28:36.581+01:00The essence of (im)pure computationThis blog post is an informal introduction to a forthcoming research paper in collaboration with my students Koko Muroya and Todd Waugh Ambridge. This is the second post of dedicated to the SPARTAN calculus. The first post was How to make a programming language out of an algebra.
For the impatient reader I will summarise the point of the previous post:
algebra + thunking + copying = pureDan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-13323971138641237162019-05-02T10:35:00.000+01:002019-05-02T10:42:15.638+01:00How to make a programming language out of an algebraThis blog post is an informal introduction to a forthcoming research paper in collaboration with my students Koko Muroya and Todd Waugh Ambridge. This is the first post of a series dedicated to the SPARTAN calculus.
Algebra, invented by the Babylonians in Antiquity and perfected by Muhammad al-Khwarizmi in the Middle Ages, is a formal language for performing calculations Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-24626658196369521902019-04-09T17:32:00.000+01:002019-04-09T17:32:10.183+01:00Andromeda and vegetarian mathematics
This post was inspired by a Twitter dialogue between two mathematicians whom I admire.
Andrej Bauer tweeted to John Baez:
John, you should try programming in a language that guarantees your program is correct. It will feel like proving theorems all the way through. (Agda is a good candidate.)
To which John replied:
Nothing will ever guarantee my programs are correct, because I don't Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-6359956731830507272018-11-12T13:53:00.000+00:002018-11-15T08:03:08.377+00:00Zippers for non-inductive typesFamous mathematician-philosoper Gian-Carlo Rota said that mathematical understanding is all about showing how things that seem different are essentially the same. If that is true, then functional programming is something that we understand quite well.
One of the most celebrated aspects of functional programming is the correspondence that shows that logical propositions and programming Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-55866049999519320822018-07-30T16:46:00.000+01:002018-07-30T16:46:21.691+01:00Haskell: If monads are the solution, what is the problem?Monads have exerted a curious fascination on programmers who turn to Haskell. The incomprehension of the newbies is matched in intensity only by the smugness of the experts. The official monadic doctrine, as espoused by the Haskell Wiki, is that
Monads in Haskell can be thought of as composable computation descriptions. The essence of monad is thus separation of composition timeline from the Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com12tag:blogger.com,1999:blog-1262280623720594573.post-29902181342412011472018-07-23T18:00:00.000+01:002018-07-23T18:00:23.265+01:00Reflections of a PC Chair
We are please to inform you that your paper has been accepted for publication.
These are the words that you wait for as an academic researcher. But how do we get there? What is the process driving the decision of acceptance versus rejection? It is something known as "peer review". To paraphrase Churchill, it is a broken, frustrating, and error-prone process. Just that a better one has yet to be Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com2tag:blogger.com,1999:blog-1262280623720594573.post-25757924019523504142018-07-17T08:11:00.001+01:002018-07-17T08:13:55.506+01:00Haskell ain't mathsA programming language is truly "pure" if all computations produce a value -- Agda is an example of such a language. For all its claims to the contrary, Haskell is not a pure language. Computations in Haskell may produce exceptions (try taking the head of the empty list) or nothing at all (in the case of computations that run forever). I don't hold that against Haskell, I just dislike the Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com2tag:blogger.com,1999:blog-1262280623720594573.post-73654331420272822532018-03-06T18:39:00.000+00:002018-03-06T18:39:36.325+00:00Copying vs. sharing in functional languagesDebugging and profiling functional programs is a challenge, for at least two reasons.
The first reason is that functional programs have no obvious step-by-step flow of control as you would find in imperative programs -- there is no semicolon to induce explicitly a notion of "step". The flow of control is induced implicitly by the evaluation rules of the underlying lambda calculus, for example Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com5tag:blogger.com,1999:blog-1262280623720594573.post-72844744912767461452017-10-22T20:37:00.001+01:002017-10-22T20:38:17.951+01:00The logic of machine learning: inductive and abductive reasoning
"The division of all inference into Abduction, Deduction, and Induction may almost be said to be the Key of Logic." C.S. Peirce
Deduction, Induction, Abduction
C.S. Peirce, in his celebrated Illustrations of the Logic of Science, re-introduced three kinds of Aristotelian reasoning: deductive, inductive, and abductive. Deduction and induction are widely used in mathematics and computerDan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-13933864180298386392017-08-04T21:23:00.000+01:002017-08-04T21:23:27.857+01:00Can we machine-learn a programming language semantics?In this post I will talk about whether denotational semantics of programming languages can be machine-learned and why that could be useful.
But let's set some background first.
Programming language semantics is a collection of mathematical theories about representing the meaning of programming languages in an abstract, machine-independent ways. The semantics of a language can be given either Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com0tag:blogger.com,1999:blog-1262280623720594573.post-2557191631878285262017-07-23T09:16:00.000+01:002017-07-23T09:16:39.366+01:00Logical Inference in Computer Science: deduction, induction, abductionLogic acknowledges three kinds of inference: deductive, inductive, and abductive. What kind of impact did they have on computer science and programming languages in particular?
Deduction is in some sense the golden standard of logical inference. It represents a set of fixed rule through which general statements are made more particular in a way which can be guaranteed to be sound, that is to Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com5tag:blogger.com,1999:blog-1262280623720594573.post-50474276072367864702017-05-22T14:55:00.001+01:002017-05-22T14:55:56.426+01:00Reasoning about digital circuits using string diagrams
Hardware and software, two worlds apart
As I drifted between the worlds of programming languages and hardware design over the last ten years or so, I was quite struck by one significant and maybe difficult to explain difference when it comes to modelling and semantics.
In the world of software the workhorse of formal verification and validation is operational semantics: Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com1tag:blogger.com,1999:blog-1262280623720594573.post-1557657263814992822017-01-16T16:38:00.000+00:002017-01-16T16:38:01.667+00:00Comparing apples with oranges: OCaml vs Java in teachingCan we compare programming languages? Can we ever say that subject to some criteria one language is better than the alternatives? Very hard, in general. But this year I was in a position to do this comparison in a way which even though far from perfect is at least vaguely meaningful.
We teach our freshmen two programming languages simultaneously in Year 1 Term 1: Java and OCaml. We don't Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com3tag:blogger.com,1999:blog-1262280623720594573.post-68879608172223572242016-09-26T16:46:00.004+01:002016-10-30T18:37:38.156+00:00What else are we getting wrong?
I like reading history of science and, as a working academic, I am amused by theories that used to be widely accepted yet false, such as the miasmatic theory of disease or the phlogiston theory of combustion. The examples are numerous enough to have their own Wikipedia Category. It makes me wonder which of the current orthodoxies are as spectacularly misguided (this is my personal bet). But the Dan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com16tag:blogger.com,1999:blog-1262280623720594573.post-16134321866412955462016-09-10T18:01:00.003+01:002016-09-17T14:23:07.207+01:00Welcome to my blogThis is a continuation of my old blog, The Lab Lunch. My old posts remain there. The main topics I covered in that blog are:
game semantics, an interactive approach to denotational semantics
Geometry of Synthesis, a new approach to high-level synthesis
programming languages, the general area in which I do research
proof assistants, such as Coq or Agda
seamless computing, a new way to compile forDan Ghicahttp://www.blogger.com/profile/14866637943603692944noreply@blogger.com1