It is well known that, both in constructive mathematics and in programming languages, types are secretly topological spaces and functions are secretly continuous. I have previously exploited this in the posts Seemingly impossible functional programs and A Haskell monad for infinite search in finite time, using the language Haskell. In languages based on Martin-Löf type theory [...]
|
|||||
|
While making a comment on Stackoverflow I noticed something: suppose we have a term in the $\lambda$-calculus in which no abstracted variable is used more than once. For example, $\lambda a b c . (a b) (\lambda d. d c)$ is such a term, but $\lambda f . f (\lambda x . x x)$ is not because [...] In an earlier post I talked about the modulus of continuity functional, where I stated that it cannot be defined without using some form of computational effects. It is a bit hard to find the proof of this fact so I am posting it on my blog in two parts, for Google and everyone else to find more easily. In the first part I show that there is no extensional modulus of continuity. In the second part I will show that every functional that is defined in PCF (simply-typed $\lambda$-calculus with natural numbers and recursion) is extensional. Continue reading Definability and extensionality of the modulus of continuity functional As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together. Using Berardi-Bezem-Coquand functional, or alternatively, for giving a [...] Jens Blanck and I presented a paper at Computability and Complexity in Analysis 2009 with a complicated title (I like complicated titles):
which has been published in Volume 16, Issue 18 of the Journal of Universal Computer Science. I usually just post the abstract, but this time I would like to explain the general idea informally, the way one can do it on a blog. But first, here is the abstract: Abstract: We prove general theorems about unique existence of effective subalgebras of classical algebras. The theorems are consequences of standard facts about completions of metric spaces within the framework of constructive mathematics, suitably interpreted in realizability models. We work with general realizability models rather than with a particular model of computation. Consequently, all the results are applicable in various established schools of computability, such as type 1 and type 2 effectivity, domain representations, equilogical spaces, and others. Download paper: effalg.pdf or directly from JUCS Alg is a program for enumeration of finite models of single-sorted first-order theories. These include groups, rings, fields, lattices, posets, graphs, and many more. Alg was written as a class project by Aleš Bizjak, a student of mine whose existence I cannot confirm with a URL. I joined the effort, added bells and whistles, as well as an alternative algorithm that works well for relational structures. Alg is ready for public consumption, although it should be considered of “beta” quality. Instructions for downloading alg are included at the end of this post. Alex Simpson, Matija Pretnar and I are organizing a workshop on computational effects. It will take place in Ljubljana on March 17th and 18th 2011. More information is available at the workshop [...] [UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.] This is a second post about the programming language eff. We covered the theory behind it in a previous post. Now we turn to the programming language itself. Please bear in mind that eff is an academic experiment. It is not meant to take over the world. Yet. We just wanted to show that the theoretical ideas about the algebraic nature of computational effects can be put into practice. Eff has many superficial similarities with Haskell. This is no surprise because there is a precise connection between algebras and monads. The main advantage of eff over Haskell is supposed to be the ease with which computational effects can be combined. Continue reading Programming with effects II: Introducing eff [UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.] I just returned from Paris where I was visiting the INRIA ?r² team. It was a great visit, everyone was very hospitable, the food was great, and the weather was nice. I spoke at their seminar where I presented a new programming language eff which is based on the idea that computational effects are algebras. The language has been designed and implemented jointly by Matija Pretnar and myself. Eff is far from being finished, but I think it is ready to be shown to the world. What follows is an extended transcript of the talk I gave in Paris. It is divided into two posts. The present one reviews the basic theory of algebras for a signature and how they are related to computational effects. The impatient readers can skip ahead to the second part, which is about the programming language. A side remark: I have updated the blog to WordPress to 3.0 and switched to MathJax for displaying mathematics. Now I need to go through 70 old posts and convert the old ASCIIMathML notation to MathJax, as well as fix characters which got garbled during the update. Oh well, it is an investment for the future. Martin Escardo and Paulo Oliva have been working on the selection monad and related functionals. The selection monad `S(X) = (X -> R) -> X` is a cousin of the continuation monad `C(X) = (X -> R) -> R` and it has a lot of useful and surprising applications. I recommend their recent paper “What Sequential Games, [...] |
|||||
|
|
|||||