![programming_languages](https://programming.dev/pictrs/image/aa43d40c-a1ab-48e1-bc89-2f60606741b9.png?format=webp&thumbnail=48)
Programming Languages
- March 2024 monthly "What are you working on?" thread
> How much progress have you made since last time? What new ideas have you stumbled upon, what old ideas have you abandoned? What new projects have you started? What are you working on? > > Once again, feel free to share anything you’ve been working on, old or new, simple or complex, tiny or huge, whether you want to share and discuss it, or simply brag about it - or just about anything you feel like sharing! > > The monthly thread is the place for you to engage /c/programming_languages on things that you might not have wanted to put up a post for - progress, ideas, maybe even a slick new chair you built in your garage. Share your projects and thoughts on others’ ideas, and most importantly, have a great and productive month!
Also see: https://www.reddit.com/r/ProgrammingLanguages/comments/1b3fqrz/march_2024_monthly_what_are_you_working_on_thread/
- Associated Effects: Flexible Abstractions for Effectful Programming (paper)dl.acm.org Associated Effects: Flexible Abstractions for Effectful Programming | Proceedings of the ACM on Programming Languages
We present associated effects, a programming language feature that enables type classes to abstract over the effects of their function signatures, allowing each type class instance to specify its concrete effects. Associated effects significantly ...
Abstract:
> We present associated effects, a programming language feature that enables type classes to abstract over the effects of their function signatures, allowing each type class instance to specify its concrete effects. > > Associated effects significantly increase the flexibility and expressive power of a programming language that combines a type and effect system with type classes. In particular, associated effects allow us to (i) abstract over total and partial functions, where partial functions may throw exceptions, (ii) abstract over immutable data structures and mutable data structures that have heap effects, and (iii) implement adaptors that combine type classes with algebraic effects. > > We implement associated effects as an extension of the Flix programming language and refactor the Flix Standard Library to use associated effects, significantly increasing its flexibility and expressive power. Specifically, we add associated effects to 11 type classes, which enables us to add 28 new type class instances.
See also: the Flix programming language
- International Conference on Functional Programming 2024 Accepted Papersicfp24.sigplan.org ICFP 2024 - ICFP Papers - ICFP 2024
PACMPL (ICFP) seeks contributions on the design, implementations, principles, and uses of functional programming, covering the entire spectrum of work, from practice to theory, including its peripheries. Authors of papers published in this issue of PACMPL will present their work at during the in-per...
- Deriving Dependently-Typed OOP from First Principles (paper)
Abstract:
> The expression problem describes how most types can easily be extended with new ways to produce the type or new ways to consume the type, but not both. When abstract syntax trees are defined as an algebraic data type, for example, they can easily be extended with new consumers, such as
print
oreval
, but adding a new constructor requires the modification of all existing pattern matches. The expression problem is one way to elucidate the difference between functional or data-oriented programs (easily extendable by new consumers) and object-oriented programs (easily extendable by new producers).> This difference between programs which are extensible by new producers or new consumers also exists for dependently typed programming, but with one core difference: Dependently-typed programming almost exclusively follows the functional programming model and not the object-oriented model, which leaves an interesting space in the programming language landscape unexplored.
> In this paper, we explore the field of dependently-typed object-oriented programming by deriving it from first principles using the principle of duality. That is, we do not extend an existing object-oriented formalism with dependent types in an ad-hoc fashion, but instead start from a familiar data-oriented language and derive its dual fragment by the systematic use of defunctionalization and refunctionalization
> Our central contribution is a dependently typed calculus which contains two dual language fragments. We provide type- and semantics-preserving transformations between these two language fragments: defunctionalization and refunctionalization. We have implemented this language and these transformations and use this implementation to explain the various ways in which constructions in dependently typed programming can be explained as special instances of the general phenomenon of duality.
Background:
Expression problem (wikipedia)
- A reckless introduction to Hindley-Milner type inference
> Several months ago I gave a talk at work about Hindley-Milner type inference. When I agreed to give the talk I didn't know much about the subject, so I learned about it. And now I'm writing about it, based on the contents of my talk but more fleshed out and hopefully better explained. > > I call this a reckless introduction, because my main source is wikipedia. A bunch of people on the internet have collectively attempted to synthesise a technical subject. I've read their synthesis, and now I'm trying to re-synthesise it, without particularly putting in the effort to check my own understanding. I'm not going to argue that this is a good idea. Let's just roll with it.
- Writing an IR from Scratch and survive to write a post (long)farena.in Writing an IR from Scratch and survive to write a post
The following post will talk about the design of the first version of the Intermediate Representation of Kunai, the design decisions and how it was implemented.
> In this post, I will talk about the first version of the Intermediate Representation I designed for Kunai Static Analyzer, this is a dalvik analysis library that I wrote as a project for my PhD, also as a way of learning about the Dalvik file format and improving my programming skills.
- The Pre-Scheme Restoration
Pre-Scheme is an interesting Scheme dialect which is being ported to modern systems. The language, why its being ported, and the porting effort are described in the linked post.
> As described in the Pre-Scheme paper, the language offers a unique combination of features: > > - Scheme syntax, with full support for macros, and a compatibility library to run Pre-Scheme code in a Scheme interpreter. The compiler is also implemented in Scheme, enabling both interactive development and compile-time evaluation. > - A static type system based on Hindley/Milner type reconstruction, as used in the ML family of languages (eg. Standard ML, OCaml, Haskell). Pre-Scheme supports parametric polymorphism, and has nascent support for algebraic data types and pattern matching, which are recently gaining popularity in mainstream languages. > - An optimizing compiler targeting C, allowing for efficient native code generation and portable low-level machine access. C remains the common interface language for operating system facilities, and compatibility at this level is essential for modern systems languages. > > Due to the restrictions of static typing and the C runtime model, Pre-Scheme does not (currently) support many of Scheme's high-level features, such as garbage collection, universal tail-call optimization, heap-allocated runtime closures, first-class continuations, runtime type checks, heterogenous lists, and the full numeric tower. Even with these limitations, Pre-Scheme enables a programming style that is familiar to Scheme programmers and more expressive than writing directly in C.
Ironically, Pre-Scheme's original purpose was to implement the interpreter for another Scheme dialect, Scheme 48 (Wikipedia). But the lower-level Pre-Scheme is now getting its own attention, in part due to the popularity of Rust and Zig. Pre-Scheme has the portability and speed of C (or at least close to it), but like Rust and Haskell it also has a static type system with ADTs and parametric polymorphism; and being a LISP dialect, like most other dialects it has powerful meta-programming and a REPL.
- Lady Deirdre: Unified compiler framework
From README:
> Lady Deirdre is a framework for incremental programming language compilers, interpreters, and source code analyzers. > > This framework helps you develop a hybrid program that acts as a language compiler or interpreter and as a language server for a code editor's language extension. It offers the necessary components to create an in-memory representation of language files, including the source code, their lexis and syntax, and the semantic model of the entire codebase. These components are specifically designed to keep the in-memory representation in sync with file changes as the codebase continuously evolves in real time. > ### Key Features > - Parser Generator Using Macros. > - Hand-Written Parsers. > - Error Resilience. > - Semantics Analysis Framework. > - Incremental Compilation. > - Parallel Computations. > - Web-Assembly Compatibility. > - Source Code Formatters. > - Annotated Snippets. > - Self-Sufficient API.
- Staged compilation with dependent types (GitHub)github.com GitHub - AndrasKovacs/staged: Staged compilation with dependent types
Staged compilation with dependent types. Contribute to AndrasKovacs/staged development by creating an account on GitHub.
Abstract from the ICFP 2024 paper:
> Many abstraction tools in functional programming rely heavily on general-purpose compiler optimization\ to achieve adequate performance. For example, monadic binding is a higher-order function which yields\ runtime closures in the absence of sufficient compile-time inlining and beta-reductions, thereby significantly\ degrading performance. In current systems such as the Glasgow Haskell Compiler, there is no strong guarantee\ that general-purpose optimization can eliminate abstraction overheads, and users only have indirect and\ fragile control over code generation through inlining directives and compiler options. We propose a two-stage\ language to simultaneously get strong guarantees about code generation and strong abstraction features. The\ object language is a simply-typed first-order language which can be compiled without runtime closures. The\ compile-time language is a dependent type theory. The two are integrated in a two-level type theory.\ We demonstrate two applications of the system. First, we develop monads and monad transformers. Here,\ abstraction overheads are eliminated by staging and we can reuse almost all definitions from the existing\ Haskell ecosystem. Second, we develop pull-based stream fusion. Here we make essential use of dependent\ types to give a concise definition of a concatMap operation with guaranteed fusion. We provide an Agda\ implementation and a typed Template Haskell implementation of these developments.
The repo also contains demo implementations in Agda and Haskell), and older papers/implementations/videos.
- F - A tiny functional concatenative language
F is written in K, another small language. In fact, the entire implementation is in one file: <http://www.nsl.com/k/f/f.k>.
Example program (defines factorial and computes
fac(6)
, from <http://www.nsl.com/k/f/f/fac.f>):>
f > [[1=][][dup!pred!fac!*]cond!]fac >
The main site, "no stinking loops", is full of links including to other languages (scroll down) and resources on K. Although many are broken 🙁.
- The design decisions and evolution of a method definition - Ruby case studyzverok.space The design decisions and evolution of a method definition - Ruby case study
Episode 01 of studying Ruby programming language design decisions, how they evolved with time, and how they look in a wider context.
A blog post on the evolution of method syntax in Ruby.
The author (Victor Shepelev AKA zverok) lives in Ukraine and is part of the Armed Forces. See his other posts (about Ruby, the war, and more) here.
- AUTOMAP: How to do NumPy-style broadcasting in Futhark (but better)futhark-lang.org AUTOMAP: How to do NumPy-style broadcasting in Futhark (but better)
A high-performance and high-level purely functional data-parallel array programming language that can execute on the GPU and CPU.
NumPy-style broadcasting = being able to write code like
futhark [[1, 2, 3], [4, 5, 6], + [10, 11, 12] [7, 8, 9]]
and have it evaluate the same as
futhark [[1, 2, 3], map (map (+)) [4, 5, 6], (rep 3 [10, 11, 12]) [7, 8, 9]]
(which evaluates to
[[11, 13, 15], [14, 16, 18], [18, 19, 21]]
).numpy docs. Numpy and most other languages do this at runtime, which is typically easier. But Futhark is statically-typed, so the type of the result must be known at compile time, and this means the broadcasting must also be done at compile time.
- Crossing the Impossible FFI Boundary, and My Gradual Descent Into Madness (Vale)
Adding Rust FFI into Vale, in particular the part where the Vale compiler determines the signature and proper overload of a Rust function.
> Our ultimate goal is to write this Vale code: > >
vale > import rust.std.vec.Vec; > > exported func main() { > vec = Vec<int>.with_capacity(42); > println("Length: " + vec.capacity()); > } >
>stdout > Length: 42 >
> > ...which would successfully make a Rust Vec and call capacity on it. - vvvv - visual live-progamming for .NETvisualprogramming.net vvvv - visual live-progamming for .NET
A visual live-programming environment that takes you from rapid prototyping to final production.
vvvv is a node-based visual programming environment whose programs run on the CLR (same virtual machine as C#). It has hot reloading (compilation happens in the background) and can be extended with custom nodes written in C#. It has built-in libraries for 2D and 3D rendering, image recognition, machine learning, networking, and IO for various devices (Kinect and cameras). It's been used for a lot of interactive art installations, as seen in the "showcase" section on the website.
- The Swift compiler is slow due to how types are inferreddanielchasehooper.com Apple didn't fix Swift's biggest flaw
How a 10 year old design choice for Swift’s type checker still haunts us to this day
A notable case study for anyone designing a type system for their own language.
Swift's compiler can infer ambiguous expressions like enum case names based on their type, inferred from surrounding context. This makes the syntax less verbose, but at a cost; some seemingly benign expressions take several seconds to type-check, after which the compiler ultimately gives up with an unhelpful error message: "the compiler is unable to type-check this expression in reasonable time".
The linked post goes into more detail.
- Forsp: A Forth+Lisp Hybrid Lambda Calculus Language
> Forsp has: > > - An S-Expression syntax like Lisp > - Function abstraction like Lisp > - Function application like Forth > - An environment structure like Lisp > - Lexically-scoped closures like Lisp (Scheme) > - Cons-cells / lists / atoms like Lisp > - A value/operand stack like Forth > - An ability to express the Lambda Calculus > - A Call-By-Push-Value evaluation order > - Only 3 syntax special forms: ' ^ $ > - Only 1 eval-time special form: quote > - Only 10 primitive functions need to self-implement > - Ability to self-implement in very little code > > It's evaluator is very simple. I suspect simpler than a McCarthy Lisp eval() function, but I haven't defined a "simplicity function", so you can be the judge. > > In contrast to Lisp, apply() is trivial in Forsp, and instead we have a core function called compute()
- How we test(ed) the Futhark compilerfuthark-lang.org How we test(ed) the Futhark compiler
A high-performance and high-level purely functional data-parallel array programming language that can execute on the GPU and CPU.
> In this post I will go through the evolution of the tools we use for testing the Futhark compiler. Along the way, these also became
futhark test
, the user-facing tool for testing Futhark programs, and although rather convenient, it is still pretty crude compared to the testing tools you will find in other languages. This post is perhaps most interesting to other language implementation hobbyists.For reference, Futhark is an up-and-coming language for writing efficient parallel code, sort of like a more functional (Haskell-like) version of CUDA or OpenCL.
- TypeLoom: Gradual Typing with the LSPgithub.com GitHub - frroossst/TypeLoom: Weaving LSP-based Gradual and Optional Typing into Dynamic Languages
Weaving LSP-based Gradual and Optional Typing into Dynamic Languages - frroossst/TypeLoom
Abstract (emphasis added):
> This paper introduces TypeLoom, a tool utilising a novel approach to add gradual, optional typing into legacy code bases of dynamically typed languages. TypeLoom leverages the Language Server Protocol (LSP) to provide in-editor type information through inlay hints and collect subsequent through code actions to type information. This approach differs from the ones that exist in so far as it requires no syntactical changes to add type hints (like in Python, TypeScript) and it does not require syntactically correct comments to provide type information (like in @ts-docs and Ruby). TypeLoom utilises a graph based data structure to provide type inference and type checking. This graph-based approach is particularly effective for gradual typing as it allows flexible representation of type relationships and dependencies.
- MegaLibm: A DSL for Implementing Math Functionsblog.sigplan.org A DSL for Implementing Math Functions
Numerical code needs to carefully balance accuracy and performance. A new DSL, MegaLibm, makes this easier by checking for numerical correctness and offering flexible compilation to efficient code.…
Excerpt:
> Typically, math library functions are written in a low-level language like C or raw assembler to maximize performance. But general purpose languages (like these) don't help developers avoid semantic errors in mathematical code. > > How many times has this happened to you: you're writing some math computation, and you accidentally write a plus sign instead of a minus sign, or put in the wrong constant? Your programming language can't catch these bugs for you because its types, like
float
anddouble
, don't distinguish betweenx
and-x
or between different constants. > > But numerical code could really benefit from compiler assistance with precisely this task, especially since we expect the user to test out several different implementations of some mathematical expression and compare them for accuracy and performance. Numerical errors really throw a wrench in that process (through misleading performance or accuracy numbers) and MegaLibm therefore aims to prevent them. - The Skew Programming Language
A language which was used by Figma until recently. It compiles to JavaScript or C#.
Why and how Figma migrated from Skew to Typescript.
Differences between Skew and TypeScript
Example from the homepage:
>
skew > # Execution starts at the entry point > @entry > def fizzBuzz { > for i in 1..101 { > var text = mod(i, 3, "Fizz") + mod(i, 5, "Buzz") > document.write((text == "" ? i.toString : text) + "\n") > } > } > > # The compiler inlines this function in release mode > def mod(i int, n int, text string) string { > return i % n == 0 ? text : "" > } > > # Imported declarations are just for type checking > @import > namespace document { > def write(text string) > } >
- A baseline scrapscript compilerbernsteinbear.com A baseline scrapscript compiler
Scrapscript is a small, pure, functional, content-addressable, network-first programming language. fact 5 . fact = | 0 -> 1 | n -> n * fact (n - 1)
> Scrapscript is a small, pure, functional, content-addressable, network-first programming language. > >
> fact 5 > . fact = > | 0 -> 1 > | n -> n * fact (n - 1) >
> > My previous post introduced the language a bit and then talked about the interpreter that Chris and I built. This post is about the compiler that Chris and I built. - The borrow checker within · baby steps
This is about Rust, but it's a great post and likely relevant to languages with Rust-style ownership. It describes four features planned for Rust to make its borrow checker more expressive and permissive:
- Allow a function to return a reference in one branch of a conditional and not consider it "borrowed" in the other branch (this is supported by the new borrow checker, Polonius, which should be in stable Rust very soon).
- Allow "place" lifetimes; that is, lifetimes that refer to other variables or their fields (e.g.
'foo.bar
is a lifetime that, when attached to a reference, means the reference is borrowingfoo.bar
or some data within it). - View types and inter-procedural AKA "partial" borrows: define a function that can only borrow specific fields in a structure, so that the function can be called with a structure whose other fields (at the call-site) are mutably borrowed or moved.
- Self-referential structures: structures where one field borrows another owned field (e.g.
Foo { foo: String, bar: &'self.foo str }
,foo
is owned andbar
borrows from it). Crates like self_cell and ouroboros provide this feature, but the goal is to have it in safe Rust with a cleaner syntax.
- Circle C++: C++ superset to add Memory Safety based on Rust's borrow checking
From the page:
> My aim is to produce a superset of C++ that has a rigorously safe subset. Start a new project, or take an existing one, and write safe code in C++. Code written in the safety context exhibits the same strong safety guarantees as safe code programmed in Rust. Indeed, lifetime safety is enforced statically with borrow checking, the signature safety technology first introduced in Rust
...
> What properties characterize Safe C++? > > - A superset of C++ with a safe subset. Undefined behavior is prohibited from originating in the safe subset. > - The safe and unsafe parts of the language are clearly delineated, and users must explicitly leave the safe context to use unsafe operations. > - The safe subset must remain useful. If we get rid of a crucial unsafe technology, like unions or pointers, we should supply a safe alternative, like choice types or borrows. A perfectly safe language is not useful if it's so inexpressive you can't get your work done. > - The new system can't break existing code. If you point a Safe C++ compiler at existing C++ code, that code must compile normally. Users opt into the new safety mechanisms. Safe C++ is an extension of C++. It's not a new language. > >
cpp > #feature on safety > #include "std2.h" > > int main() safe { > std2::vector<int> vec { 11, 15, 20 }; > > for(int x : vec) { > // Ill-formed. mutate of vec invalidates iterator in ranged-for. > if(x % 2) > vec^.push_back(x); > > unsafe printf("%d\n", x); > } > } >
> >shell > $ circle iter3.cxx > safety: iter3.cxx:10:10 > vec^.push_back(x); > ^ > mutable borrow of vec between its shared borrow and its use > loan created at iter3.cxx:7:15 > for(int x : vec) { > ^ >
A couple other languages aiming to create a "C++ successor" which is fully interoperable with C++ (analogous to TypeScript and JavaScript):
- Carbon: an entirely new language which compiles straight to LLVM, but still strives to be highly interoperable with C++. Its goal is to add "modern" features: new syntax, parametric polymorphism, as well as removing C++'s backwards-compatibility quirks.
- It has a section on memory safety which mentions a "safe Carbon subset". But this is a longer-term goal, whereas it's the main goal of Circle.
- Cpp2: an alternate syntax for C++. It compiles to C++, but makes new features such as modules and concepts less verbose, while hiding or removing backwards-compatibility quirks (e.g. lists are
std::array
and string literals arestd::string
).- 100% memory safety is a non-goal: AFAIK it doesn't do static analysis and syntactic rewrites alone aren't powerful enough to enforce it.
Compared to the other languages, Circle remains closest to C++. The other languages try to fix other C++ "problems"; Circle's only goal is to fix memory unsafety, and otherwise keep syntax and semantics the same for maximum interoperability.
- Carbon: an entirely new language which compiles straight to LLVM, but still strives to be highly interoperable with C++. Its goal is to add "modern" features: new syntax, parametric polymorphism, as well as removing C++'s backwards-compatibility quirks.
- Help me find my new "MIDI Assembly" a new name!
Design documentation: https://github.com/ZILtoid1991/pixelperfectengine/blob/master/docs/formats/m2.md
It has some weird solutions due to my limited experience with the subject and the target usage favor preallocation instead of live allocation. I took some inspirations from Music Macro Language, Assembly, and Lua. Due to the lack of a MIDI 2.0 format, I thought I'd come up with my own, adding capabilities to program adaptive soundtracks (emitting MIDI commands with calculated values, conditional emitting of MIDI commands, conditional looping and pattern playback, etc).
I initially gave it the name
.m2
but while M.2 is an entirely different thing, an MML format by the name.m2
does exist on the PC98, thus I'm looking for some new name for mine. The only thing I can come up on the spot is MASM (or MIDI Assembly), but it's close to an already existing MASM (Microsoft Macro Assembler). - Decker: Apple-II themed "multimedia platform" with an integrated scripting language
From the homepage:
> Decker is a multimedia platform for creating and sharing interactive documents, with sound, images, hypertext, and scripted behavior. You can try it in your web browser right now. > > [!](https://beyondloom.com/decker/tour.html)
...
> For more complex projects, Decker features a novel scripting language named Lil which is strongly influenced by both Lua, an imperative language popular for embedding in tools and game engines, and Q, a functional language in the APL family used with time-series databases. Lil is easy to learn and conventional enough not to ruffle any feathers for users with prior programming experience, but also includes pleasant surprises like implicit scalar-vector arithmetic and an integrated SQL-like query language. A few lines of Lil can go a long way. > > !
There are lots more examples and documentation on the site.
- Oxidizing OCaml with Modal Memory Management (paper)
This paper describes adding Rust-like ownership semantics to OCaml via the following "modes".
- Uniqueness: an instance of a type with the
unique
mode is guaranteed to have a unique reference to its value, i.e. no instance anywhere else references the same value, so it can be mutated without unexpectedly mutating a seemingly-unrelated value. - Affinity: an instance of a type with the
affine
mode can only be used once; for example, an affine function can only be called once. In particular, a closure that in-place mutates a unique value must be affine, since in-place mutations are implemented by "consuming" the unique value and returning it mutated (see the example in section 2.2). - Locality: an instance of a type with the
local
mode can't leave its lexical scope, i.e. is guaranteed to be allocatable on the stack. Locality allows a sort of "immutable borrow": a unique value can be aliased as a local value, and when the local value's scope ends, the value once again becomes unique (if it was aliased as a non-local value, the alias could've been stored somewhere else, so the original value is shared permanently).
Abstract:
> Programmers can often improve the performance of their programs by reducing heap allocations: either by allocating on the stack or reusing existing memory in-place. However, without safety guarantees, these optimizations can easily lead to use-after-free errors and even type unsoundness. In this paper, we present a design based on modes which allows programmers to safely reduce allocations by using stack allocation and in-place updates of immutable structures. We focus on three mode axes: affinity, uniqueness and locality. Modes are fully backwards compatible with existing OCaml code and can be completely inferred. Our work makes manual memory management in OCaml safe and convenient and charts a path towards bringing the benefits of Rust to OCaml.
Another language with different modes is Granule.
- Uniqueness: an instance of a type with the
- Compilers for free with wevalbernsteinbear.com Compilers for free with weval
With some partial evaluation and specialization hints, it is possible to get pretty decent speedups on interpreters by turning them into compilers.
> Partial evaluation is neat. In short, it's all about taking an existing program, modifying it to hold some of its inputs as constants, and then letting the compiler/optimizer go hog wild on it. The result is still a program---not a value---and it's usually faster than the original program. > > The usual small example is the power function. If you have a function that takes two arguments,
x
andy
, and returnsx^y
: > >c > int power(int x, int y) { > int result = 1; > for (int i = 0; i < y; i++) { > result *= x; > } > return result; > } >
> > If you partially evaluate this function with respect toy
aty = 5
, you get a new function that takes one argument,x
, and returnsx^5
: > >c > int power_5(int x) { > int result = 1; > for (int i = 0; i < 5; i++) { > result *= x; > } > return result; > } >
> > Now, to you, this might not look that different from the original function. But to an optimizer, it is a new world of opportunity. The optimizer can unroll the loop and remove the conditional: > >c > int power_5(int x) { > return x * x * x * x * x; > } >
> > weval does that for entire WebAssembly modules. WebAssembly modules that are normally much bigger than a smallpower
function. You might want to use it if, for example, your WebAssembly module is an interpreter. Imagine a world where you have compiled a runtime such as SpiderMonkey or CPython to WebAssembly. You could then run your Python or JavaScript programs on the WebAssembly runtime, but they would be slower than if you had compiled them directly to WebAssembly. And even if you compiled the JS/Python directly to Wasm, it would probably be slow unless your compiler did some fancy static analysis. This is where weval comes in.This concept -- partially evaluating an interpreter with a specific program to make a faster "compiled" program -- is known as the first Futamura projection (longer explanation).
- Type Theory Forall #38: Haskell, Lean, Idris, and the Art of Writing (podcast)
> In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer. > > He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris. > > David is a super upbeat person and I feel that we could spend hundreds of hours talking about Functional Programming Writing and Dependent Types, and we still wouldn't run out of topics!
- Higher Order Company: developing a massively parallel language, proof checker, and runtime using interaction nets/combinatorshigherorderco.com Higher Order Company
We're the HOC, a tech startup revolutionizing computing with massively parallel runtimes and processors using our HVM runtime and Bend programming language.
-
HMV2 (GitHub): an IR, runtime, and interaction combinator evaluator which allegedly "achieves near-ideal speedups as a function of available cores."
-
Bend (Github): a high-level language that targets the CPU and GPU via HVM2.
-
Kind (GitHub): another language that uses HVM2, designed for proving theorems (no MVP yet).
Interaction combinators were devised by Yves Lafont. Interaction combinators compose to form interaction nets like how SKI combinators compose to form lambda terms. Interaction nets are a model of computation like lambda calculus or Turing machines. In fact, any lambda term can be translated into an interaction net. The key property of interaction nets, unlike Turing machines, is that you can reduce separate parts of an interaction net (i.e. evaluate separate parts of the program it encodes) in parallel, without data races or locks.
For more info, see:
- The original papers on interaction nets and interaction combinators.
- The lead developer of HVM2 is also writing a paper on HVM2.
- Video demonstrating interaction net reduction (from HOC).
- iNet, an interaction net implementation with a graphical demo; and inet-js (GitHub) the implementation (not HOC).
The above repos are in very early stages and the team/company has previous attempts that they ended up rewriting:
-
- Question about 'Design Concepts in Programming Languages' -- 3 Types of Semantics, what do the mean?
Based on my understanding of what is written in this book, I understood that 'Operational Semantics' is something for imperative language, and 'Denotational semantics' is for functional languages. In a way, the former is more 'practical 'and the latter is more 'theoretical'.
So I made the thread in the Rust instance about GC being possible by Rust being an 'imperative language with denotational semantics' and people told me I am wrong.
I kinda knew I am wrong, I just went all brazen-like. So I am not brazen anymore.
What exactly did I get wrong about the difference between Operational vs. Denotational semantics? Just a hint would be good.
There's another type of semantics, Axiomatic. That I don't even attempt or try to understand! This one is really puzzling for me.
These are complex subjects and I wanna understand them; and you only understand complex subjects if you ask people.
Thanks.
PS: No academic dishonesty, I am not a student.
- buzz, A small statically typed scripting language 👨🚀
From the README on GitHub:
> - Small in size and complexity (just a bit more than Lua though) > - Statically typed > - Unambiguous > - No nonsense coercion > - Fibers > - JIT compilation with MIR > - Tooling > - Generate doc from docblocks (in progress) > - VS Code extension > - Syntax highlighting > - LSP (in progress) > - Debugger and DAP (planned) > > !buzz code example
The compiler is written in Zig.
- Higher RAII, and the Seven Arcane Uses of Linear Types
Another post from the creator of Vale, the last one was "Borrow checking, RC, GC, and the Eleven (!) Other Memory Safety Approaches".
This discusses Vale's higher RAII, a feature implemented using linear types. Vale has linear types as opposed to Rust's affine types: affine types prevent using a value after it's "moved", but linear types also prevent not moving a value (i.e. cannot just let it go out of scope). Additionally in Vale, one can define a set of functions that destroy a type, and in order to destroy a value of that type, one must call a function from that set; that is what Vale calls "higher RAII".
This part of the linked post contains seven examples where Vale's higher RAII enforce invariants that Rust's affine types cannot. In a language like C, you can "forget" to use a value and it will leak. In a language like Rust, the value will be properly deallocated, but you can still have "forgotten" about it, e.g. perhaps the value represents a transaction that you meant to commit (one of the seven examples). In Vale, you can't forget about a value as long as it has a linear type, because doing so will raise a compile-time error.
The rest of the post further discusses higher RAII, elaborating on what it is and why its useful, explaining why it's more general than other languages'
defer
and how it could be integrated into other languages, and more. - Meta, a Human-Friendly Programming Language
From the site:
> We have entered a world in which we need to do more with less. If you, like us, have frowned at the difficulty and inefficiency of creating software, and wondered if there is a better way, Meta is for you. It is a descendant of the acclaimed REBOL and Logo computer languages. Logo was designed in academia to teach programming in a simple yet powerful way. It is widely used in education and influenced many newer systems and languages. REBOL extended this concept to professional programming. It was invented by Carl Sassenrath, the chief software designer of the famous Amiga computer, the first consumer multimedia system. Meta takes the next step by combining this design with the virtues of the C programming language, which has been the standard for software interoperability and performance for half a century.
- Seems to be primarily inspired by REBOL but designed to be faster [1].
- Can compile to various 8-bit Atari machines and αcτµαlly pδrταblε εxεcµταblε (which means it can run on almost anything) [2].
- Has an official Bluesky account, which AFAIK is the main social media presence.
- Exploring the c4... compiler?registerspill.thorstenball.com Exploring the c4... compiler?
This week I found myself digging through the code of c4, an implementation of C “in four functions”, by Robert Swierczek. I remember coming across c4 when it was released ten years ago. It got me excited: hey, C in four functions, that means it’s easy to understand right?
c4 ("C in four functions"; GitHub)
> I remember coming across c4 when it was released ten years ago. It got me excited: hey, C in four functions, that means it’s easy to understand right? > > That excitement turned into “oh, I see” as soon as I scrolled through the code. c4 is dense, barely commented, and, frankly, strange. It’s unlike anything else I had come across in compiler land. > > After reading through the code this week here are the other adjectives I would add to the list: clever, tricky, fascinating, cool. It’s a compiler, it’s a VM, it’s an interpreter, it’s a parser, it’s art, it’s trickshot programming.
Not to be confused with C3, "a programming language that builds on the syntax and semantics of the C language, with the goal of evolving it while still retaining familiarity for C programmers".
- Compiling higher order functions with GADTsinjuly.in Compiling higher order functions with GADTs
Compile higher order functions using the defunctionalization transform. Compiler authors HATE this one weird trick!
> Implementing first class functions in a bytecode interpreter is trivial. > > But how do compilers that generate machine code (or lower to C, or SSA) implement higher order functions? Back in 2021, I found an answer when contributing closures to the Pallene compiler. > > Today I was researching something loosely related, and found yet another neat trick called defunctionalization in this paper. > > Defunctionalization is a transform -- a way to re-write the original program without using higher order functions such that it can be trivially compiled to a flat IR in subsequent compiler passes. > > The paper uses an OCaml example, and I'll be porting the same program to Haskell. Our implementation will assume that the language being compiled supports GADTs, though it's certainly possible to defunctionalize without them.
- Should I continue making my own VM, or scrap it for some preexisting solution?
After getting angry at Lua for bugs reappearing after fixing them, and otherwise having issues with making it interoperable with my own language of choice (D), I decided to roll out my own VM out, with some enhanced optional features compared to regular Lua (type safety, static arrays on the stack, enhanced metatables, etc.), and also allowing the potential of other scripting languages to be ported to the VM. As I already have crafted a VM for a programmable MIDI format (M2: Docs / Implementation ; bit incomplete as of now), I thought it'll be easy, just don't optimize this time entirely around preallocation (M2 has 128 not entirely general purpose registers per pattern (musical thread) + 128 shared registers + shared arrays), add stack handling, add heap handling, add more types, etc.
Thus I begun working on PingusVM, to contribute to the problem of ever growing number of standards.
However, as time went by, I had to realize (just like every time I've added another engine feature) that it's way more complicated, especially as I have realized mid-development that I had a lot of oversight on design. Not only that, I have a lot of other projects, such as the game engine I've originally intended the VM for. My main issue is, potential candidates either lack integer support, or are very bloated (I don't need a second XML DOM parser, etc). Lua kind of worked, but after I fixed an issue (which was hard as every tutorial implied you just wanted to load a file directly instead of having the ability of loading the text directly) a very similar one reappeared, while following every tutorial possible. Others would lead me to introduce some C-style build system, as they would need "hard linking" to my engine, and that "hard linking" is why I had to halt development of my image library, as I would have needed to introduce a build system into my project for the LZW codec (required for GIF files).
- The search for easier safe systems programming (blog post + language)
> For the last year and a half, I and my recently-added collaborator Jane Losare-Lusby have been working in secret on a safe systems language that could be learned about as quickly as one can learn Go. I think we might have something worth exploring.