William Byrd on Relational Programming and Quines

This idea about elaborating relations under constraints is really interesting. See Thorsten Altenkirch on NaÏve Type Theory and An Interesting and Useful Duality and Condensing Programs. 
 
See miniKanren, live and untagged: quine generation via relational interpreters (programming pearl) by William E. Byrd, Eric Holk and Daniel P. Friedman and https://minikanren.org/ for more on Micro Kanren (21:00).

See also What is Formal Logic? and Nada Amin - Metacircular Interpretation ad infinitum.

Subscribe to Strange Loop.

See A small embedding of logic programming with a simple complete search by Jason Hemann, Daniel P. Friedman, William E. Byrd and Matthew Might and Visualizing miniKanren Search with a Fine-Grained Small-Step Semantics by Brysen Pfingsten and Jason Hemann where they describe a web interface to  a semantic model which lets users interactively view the reduction steps.

Here are some related clever things people have done: Extensional Normalisation and Type-Directed Partial Evaluation for Typed Lambda Calculus with Sums (2004) by Vincent Balat, Roberto Di Cosmo and Marcelo Fiore and Tillmann Rendel - Automatic Refunctionalization to a Language with Copattern Matching.  Also Jesper Cockx - Elaborating Dependent (Co)pattern Matching.

Subscribe to Erlang Solutions.


Reactive systems have been the focus of decades of research starting in the 1990s. See e.g. The synchronous dataflow programming language LUSTRE (1991) by N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud and ReactiveML, ten years later (2015) by Louis Mandel, Cédric Pasteur and Marc Pouzet. Also Feasible reactivity in a synchronous π-calculus (2007) by Roberto M. Amadio Frédéric Dabrowski.

It works for non-deterministic processes like parsing and language recognition too. See Multi-stage Relational Programming by Michael Ballantyne, Rafaello Sanna, Jason Hemann, William E. Byrd and Nada Amin. 

I'd never heard of staging interpreters before. Is Normalisation by Evaluation just a kind of staged interpreter? 

Subscribe to ACM SIGPLAN.

Tomas Petricek thinks of type inference as a constraint solver:

Subscribe to Tomas Petricek. 

Paul Dancstep on the Finset interpretation of The Library of Babel:


See On Getting Machines to do Stuff and David Spivak on The Category of Polynomial Functors in One Variable. 

Subscribe to Topos Institute.

It's all loose ends! What a pity nobody can be employed to tidy them up, .... Everyone's too busy inventing new clever things.

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

How Could One Unify CMU and MIT

Image
I mean, how to get the best of the two different philosophies of computation. One is based on typed programming languages and the other on engineering with diagrams . This is about practical computing and the cost and feasibility of software development in general. Here is the problem: We have a lot of algorithms which can all be described abstractly using some sort of pseudocode, or perhaps using some particular language (usually Python!). These algorithms are often well-studied and a lot is known about them in terms of their computational complexity in time and space. Substantive practical software systems invariably employ many such algorithms, often implemented in libraries with more or less well-specified APIs. But very few of these libraries are capable of interoperating because they are either packages written in some specific programming language like Java or Haskell, say, or they are written in C and used as object code, or they are written in an interpreted language like Sc...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more