David MacQueen on his Ideas for Successor ML

See https://github.com/dmacqueen/NewFrontEnd and https://standardml.zulipchat.com.

9:33 On disallowing static declarations within expressions: from MLFW2025.txt:

1.3. [Core] No static (type/module) declarations within expressions

  Moto: "Keep the core and module levels separate", or "no static declarations within
  dynamic expressions".

  What does it, or should it, mean to have a (statically generative) datatype declaration
  in the body of a recursive function.

  [Karl Crary (and Bob Harper?) won't like this, since definition of modules within
  expressions is a feature of his dialect of (S)ML. It also appears to be supported in
  Moscow ML. The CMU (Harper, Crary, etc.) view of the static semanatics of (S)ML seems to
  base on some fundamental "type theoretic" notion of a _module_ that seems to be
  different from my own intuitive understanding of the module system of (S)ML. Their ideas
  are described in papers such as Harper-Stone and Sterling-Harper (?). In their view,
  modules are fundamental and the Core constructs are secondary or definable.
  
  Crary talks about "old" and "new" type theoretic definitions of the semantics of (S)ML,
  but I don't yet know what he is referring to.] 

I suspect this is because Bob Harper has big plans for generalising the notion of phase distinction and perhaps then it applies in some dynamical contexts. See System Fω And ML Module Semantics and Bob Harper's Course on Principles of Programming Languages.

See also his ideas about data types as modules in his 2021 OPLSS talk on the ML Module System (first mentioned at 1:04:49). 

The playlist of ML language talks is here. Another excellent talk was by Mizuki Arata implementing a transpiler from Standard ML to lua and JavaScript.

This is written in Standard ML and is self-hosting. See https://github.com/minoki/LunarML. This is much closer to my idea, which was to take seriously the idea of a Standard Metalanguage and see how far you can get by using Standard ML '97 to define various successor MLs. Then the ideas of meta-programming runtime environments and eventually the whole Operating System can be bootstrapped from there. See On Getting Machines to do Stuff and A New Kind of Science.

Subscribe to ACM SIGPLAN.


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