Programming Languages

Background: What are denotational semantics, and what are they useful for?

Also: Operational and Denotational Semantics

> Denotational semantics assign meaning to a program (e.g. in untyped lambda calculus) by mapping the program into a self-contained domain model in some meta language (e.g. Scott domains). Traditionally, what is complicated about denotational semantics is not so much the function that defines them; rather it is to find a sound mathematical definition of the semantic domain, and a general methodology of doing so that scales to recursive types and hence general recursion, global mutable state, exceptions and concurrency¹². > > In this post, I discuss a related issue: I argue that traditional Scott/Strachey denotational semantics are partial (in a precise sense), which means that > > 1. It is impossible to give a faithful, executable encoding of such a semantics in a programming language, and > 2. Internal details of the semantic domain inhibit high-level, equational reasonining about programs > > After exemplifying the problem, I will discuss total denotational semantics as a viable alternative, and how to define one using guarded recursion. > > I do not claim that any of these considerations are novel or indisputable, but I hope that they are helpful to some people who > > - know how to read Haskell > - like playing around with operational semantics and definitional interpreters > - wonder how denotational semantics can be executed in a programming language > - want to get excited about guarded recursion. > > I hope that this topic becomes more accessible to people with this background due to a focus on computation. > > I also hope that this post finds its way to a few semanticists who might provide a useful angle or have answers to the conjectures in the later parts of this post. > > If you are in a rush and just want to see how a total denotational semantics can be defined in Agda, have a look at this gist.

I’ve started putting the (long) forum posts I make about ArkScript on my blog, so that more people can follow the development. I must say I like the look of it, that’s also helping me getting back into blogging!

This presents a method to reduce the overhead of the garbage collector, in a language with multi-stage programming (specifically two-level type theory) using regions.

cross-posted from: https://programming.dev/post/18859576

> This past few weeks, Python 3.13 and the possibility to disable the GIL has seen a lot of coverage and that pushed me to dig into my own language, to see how different our approaches are. > > So if you’re curious about the rambling of a pldev, that might be for you!

From homepage:

> Hy (or "Hylang" for long) is a multi-paradigm general-purpose programming language in the Lisp family. It's implemented as a kind of alternative syntax for Python. Compared to Python, Hy offers a variety of new features, generalizations, and syntactic simplifications, as would be expected of a Lisp. Compared to other Lisps, Hy provides direct access to Python's built-ins and third-party Python libraries, while allowing you to freely mix imperative, functional, and object-oriented styles of programming. (More on "Why Hy?")

Some examples on the homepage:

> Hy: > > hy > (defmacro do-while [test #* body] > `(do > ~@body > (while ~test > ~@body))) > > (setv x 0) > (do-while x > (print "Printed once.")) > > > Python: > > python > x = 0 > print("Printed once.") > while x: > print("Printed once.") >

Interestingly programming.dev's Markdown renderer highlights \\\hy code blocks. Maybe it knows the language ([highlight.js has it](https://github.com/highlightjs/highlight.js/blob/main/SUPPORTED_LANGUAGES.md)). Maybe it's using [Hybris](https://it-m-wikipedia-org.translate.goog/wiki/Hybris_(linguaggio_di_programmazione)?_x_tr_sl=it&_x_tr_tl=en&_x_tr_hl=en&_x_tr_pto=wapp) (another language that could get its own post, one of its extensions is *.hy`).

GitHub

Online REPL

1.0 announcement

> ### Key Features > > - Multiple types (number, bool, datetime, string and error) > - Memory managed by user (no allocs) > - Iterator based interface > - Supporting variables > - Stateless > - Expressions can be compiled (RPN stack) > - Fully compile-time checked syntax > - Documented grammar > - Standard C11 code > - No dependencies > > ### Examples > > c > # Numerical calculations > sin((-1 + 2) * PI) > > # Dates > datetrunc(now(), "day") > > # Strings > "hi " + upper("bob") + trim(" ! ") > > # Conditionals > ifelse(1 < 5 && length($alphabet) > 25, "case1", "case2") > > # Find the missing letter > replace($alphabet, substr($alphabet, 25 - random(0, length($alphabet)), 1), "") >

GitHub (source code for all languages), also linked above.

• Assembly
• BASIC
• Forth/MOUSE
• Lisp
• APL/K
• PL/0

The GitHub says "50 lines of code" but the largest example is 74 lines excluding whitespace and comments.

> Dune is a shell designed for powerful scripting. Think of it as an unholy combination of bash and Lisp. > > You can do all the normal shell operations like piping, file redirection, and running programs. But, you also have access to a standard library and functional programming abstractions for various programming and sysadmin tasks! > > !screenshot

> Fennel is a programming language that brings together the simplicity, speed, and reach of Lua with the flexibility of a lisp syntax and macro system. > > - Full Lua compatibility: Easily call any Lua function or library from Fennel and vice-versa. > - Zero overhead: Compiled code should be just as efficient as hand-written Lua. > - Compile-time macros: Ship compiled code with no runtime dependency on Fennel. > - Embeddable: Fennel is a one-file library as well as an executable. Embed it in other programs to support runtime extensibility and interactive development. > > Anywhere you can run Lua code, you can run Fennel code.

Example:

> lisp > ;; Sample: read the state of the keyboard and move the player accordingly > (local dirs {:up [0 -1] :down [0 1] :left [-1 0] :right [1 0]}) > > (each [key [dx dy] (pairs dirs)] > (when (love.keyboard.isDown key) > (let [[px py] player > x (+ px (* dx player.speed dt)) > y (+ py (* dy player.speed dt))] > (world:move player x y)))) >

Abstract:

> We say that an imperative data structure is snapshottable or supports snapshots if we can efficiently capture its current state, and restore a previously captured state to become the current state again. This is useful, for example, to implement backtracking search processes that update the data structure during search. > > Inspired by a data structure proposed in 1978 by Baker, we present a snapshottable store, a bag of mutable references that supports snapshots. Instead of capturing and restoring an array, we can capture an arbitrary set of references (of any type) and restore all of them at once. This snapshottable store can be used as a building block to support snapshots for arbitrary data structures, by simply replacing all mutable references in the data structure by our store references. We present use-cases of a snapshottable store when implementing type-checkers and automated theorem provers. > > Our implementation is designed to provide a very low overhead over normal references, in the common case where the capture/restore operations are infrequent. Read and write in store references are essentially as fast as in plain references in most situations, thanks to a key optimisation we call record elision. In comparison, the common approach of replacing references by integer indices into a persistent map incurs a logarithmic overhead on reads and writes, and sophisticated algorithms typically impose much larger constant factors. > > The implementation, which is inspired by Baker's and the OCaml implementation of persistent arrays by Conchon and Filliâtre, is both fairly short and very hard to understand: it relies on shared mutable state in subtle ways. We provide a mechanized proof of correctness of its core using the Iris framework for the Coq proof assistant.

Back from break, I'm going to start posting regularly again.

This is an interesting node-based visual programming environment with very cool graphics. It's written on Clojure but the various "cards" (nodes) can include SQL, R, DALL-E API calls, or anything else.

> !RVBBIT

GitHub

> Haxe-based language for defining 2D shmups bullet-hell patterns.

The VM also runs in Haxe.

> Soundly handling linearity requires special care in the presence of effect handlers, as the programmer may inadvertently compromise the integrity of a linear resource. For instance, duplicating a continuation that closes over a resource can lead to the internal state of the resource being corrupted or discarding the continuation can lead to resource leakage. Thus a naïve combination of linear resources and effect handlers yields an unsound system.

...

> In the remainder of this blog post we describe a novel approach to rule out such soundness bugs by tracking control-flow linearity, a means to statically assure how often a continuation may be invoked which mediates between linear resources and effectful operations in order to ensure that effect handlers cannot violate linearity constraints on resources. We focus on our implementation in Links. The full technical details are available in our open access POPL'24 distinguished paper Soundly Handling Linearity.

> Programming models like the Actor model and the Tuplespace model make great strides toward simplifying programs that communicate. However, a few key difficulties remain. > > The Syndicated Actor model addresses these difficulties. It is closely related to both Actors and Tuplespaces, but builds on a different underlying primitive: eventually-consistent replication of state among actors. Its design also draws on widely deployed but informal ideas like publish/subscribe messaging.

For reference, actors and tuple-spaces are means to implement concurrent programs. Actors are essentially tiny programs/processes that send (push) messages to each other, while a tuple-space is a shared repository of data ("tuples") that can be accessed (pulled) by different processes (e.g. actors).

...

> A handful of Domain-Specific Language (DSL) constructs, together dubbed Syndicate, expose the primitives of the Syndicated Actor model, the features of dataspaces, and the concepts of conversational concurrency to the programmer in an ergonomic way.

...

> To give some of the flavour of working with Syndicate DSL constructs, here's a program written in JavaScript extended with Syndicate constructs: > > javascript > function chat(initialNickname, sharedDataspace, stdin) { > spawn 'chat-client' { > field nickName = initialNickname; > > at sharedDataspace assert Present(this.nickname); > during sharedDataspace asserted Present($who) { > on start console.log(`${who} arrived`); > on stop console.log(`${who} left`); > on sharedDataspace message Says(who, $what) { > console.log(`${who}: ${what}`); > } > } > > on stdin message Line($text) { > if (text.startsWith('/nick ')) { > this.nickname = text.slice(6); > } else { > send sharedDataspace message Says(this.nickname, text); > } > } > } > } >

Documentation

Comparison with other programming models

History

Author's thesis

Even though it's very unlikely to become popular (and if so, it will probably take a while), there's a lot you learn from creating a programming language that applies to other areas of software development. Plus, it's fun!

The blog post is the author's impressions of Gleam after it released version 1.4.0. Gleam is an upcoming language that is getting a lot of highly-ranked articles.

It runs on the Erlang virtual machine (BEAM), making it great for distributed programs and a competitor to Elixir and Erlang (the language). It also compiles to JavaScript, making it a competitor to TypeScript.

But unlike Elixir, Erlang, and TypeScript, it's strongly typed (not just gradually typed). It has "functional" concepts like algebraic data types, immutable values, and first-class functions. The syntax is modeled after Rust and its tutorial is modeled after Go's. Lastly, it has a very large community.

> Zyme is an esoteric language for genetic programming: creating computer programs by means of natural selection. > > For successful evolution mutations must generate a wide range of phenotypic variation, a feat nearly impossible when randomly modifying the code of conventional programming languages. Zyme is designed to maximize the likelihood of a bytecode mutation creating a novel yet non-fatal change in program behavior. > > Diverging from conventional register or stack-based architectures, Zyme uses a unique molecular automaton-based virtual machine, mimicking an abstract cellular metabolism. This design enables fuzzy control flow and precludes invalid runtime states, transforming potential crashes into opportunities for adaptation.

Very unique, even for an esoteric language. Imagine a program that gets put through natural selection and "evolves" like a species: the program is cloned many times, each clone is slightly mutated, the clones that don't perform as well on some metric are discarded, and the process is repeated; until eventually you have programs that do great on the metric, that you didn't write.

Key excerpt:

> At OOPSLA 2020, Prof. Dietrich Geisler published a paper about geometry bugs and a type system that can catch them. The idea hasn't exactly taken over the world, and I wish it would. The paper's core insight is that, to do a good job with this kind of type system, you need your types to encode three pieces of information: > > - the reference frame (like model, world, or view space) > - the coordinate scheme (like Cartesian, homogeneous, or polar coordinates) > - the geometric object (like positions and directions) > > In Dietrich's language, these types are spelled scheme<frame>.object. Dietrich implemented these types in a language called Gator with help from Irene Yoon, Aditi Kabra, Horace He, and Yinnon Sanders. With a few helper functions, you can get Gator to help you catch all the geometric pitfalls we saw in this post.

Abstract:

> File formats specify how data is encoded for persistent storage. They cannot be formalized as context-free grammars since their specifications include context-sensitive patterns such as the random access pattern and the type-length-value pattern. We propose a new grammar mechanism called Interval Parsing Grammars IPGs) for file format specifications. An IPG attaches to every nonterminal/terminal an interval, which specifies the range of input the nonterminal/terminal consumes. By connecting intervals and attributes, the context-sensitive patterns in file formats can be well handled. In this paper, we formalize IPGs' syntax as well as its semantics, and its semantics naturally leads to a parser generator that generates a recursive-descent parser from an IPG. In general, IPGs are declarative, modular, and enable termination checking. We have used IPGs to specify a number of file formats including ZIP, ELF, GIF, PE, and part of PDF; we have also evaluated the performance of the generated parsers.

> I created Bril, the Big Red Intermediate Language, to support the class's implementation projects. Bril isn't very interesting from a compiler engineering perspective, but I think it's pretty good for the specific use case of teaching compilers classes. Here's a factorial program: > > ruby > @main(input: int) { > res: int = call @fact input; > print res; > } > > @fact(n: int): int { > one: int = const 1; > cond: bool = le n one; > br cond .then .else; > .then: > ret one; > .else: > decr: int = sub n one; > rec: int = call @fact decr; > prod: int = mul n rec; > ret prod; > } > > > > Bril is the only compiler IL I know of that is specifically designed for education. Focusing on teaching means that Bril prioritizes these goals: > > - It is fast to get started working with the IL. > - It is easy to mix and match components that work with the IL, including things that fellow students write. > - The semantics are simple, without too many distractions. > - The syntax is ruthlessly regular. > > Bril is different from other ILs because it prioritizes those goals above other, more typical ones: code size, compiler speed, and performance of the generated code. > > Aside from that inversion of priorities, Bril looks a lot like any other modern compiler IL. It's an instruction-based, assembly-like, typed, ANF language. There's a quote from why the lucky stiff where he introduces Camping, the original web microframework, as "a little white blood cell in the vein of Rails." If LLVM is an entire circulatory system, Bril is a single blood cell.

Reference

GitHub

GitHub

> Glisp is a Lisp-based design tool that combines generative approaches with traditional design methods, empowering artists to discover new forms of expression.

> Glisp literally uses a customized dialect of Lisp as a project file. As the Code as Data concept of Lisp, the project file itself is the program to generate an output at the same time as a tree structure representing SVG-like list of shapes. And even the large part of the app's built-in features are implemented by the identical syntax to project files. By this nature so-called homoiconicity, artists can dramatically hack the app and transform it into any tool which can be specialized in various realms of graphics -- daily graphic design, illustration, generative art, drawing flow-chart, or whatever they want. I call such a design concept "purpose-agnostic". Compared to the most of existing design tools that are strictly optimized for a concrete genre of graphics such as printing or UI of smartphone apps, I believe the attitude that developers intentionally keep being agnostic on how a tool should be used by designers makes it further powerful.

Intro:

> CF Bolz-Tereick wrote some excellent posts in which they introduce a small IR and optimizer and extend it with allocation removal. We also did a live stream together in which we did some more heap optimizations. > > In this blog post, I'm going to write a small abtract interpreter for the Toy IR and then show how we can use it to do some simple optimizations. It assumes that you are familiar with the little IR, which I have reproduced unchanged in a GitHub Gist. > > Abstract interpretation is a general framework for efficiently computing properties that must be true for all possible executions of a program. It's a widely used approach both in compiler optimizations as well as offline static analysis for finding bugs. I'm writing this post to pave the way for CF's next post on proving abstract interpreters correct for range analysis and known bits analysis inside PyPy.

Abstract Interpretation in a Nutshell

This blog post explains why algebraic data types are "algebraic" - how every algebraic data type corresponds to a mathematical equation - and describes some ways to use a type's corresponding equation to reason about the type itself.

Abstract:

> We propose a novel type system for effects and handlers using modal types. Conventional effect systems attach effects to function types, which can lead to verbose effect-polymorphic types, especially for higher-order functions. Our modal effect system provides succinct types for higher-order first-class functions without losing modularity and reusability. The core idea is to decouple effects from function types and instead to track effects through relative and absolute modalities, which represent transformations on the ambient effects provided by the context. > > We formalise the idea of modal effect types in a multimodal System F-style core calculus Met with effects and handlers. Met supports modular effectful programming via modalities without relying on effect variables. We encode a practical fragment of a conventional row-based effect system with effect polymorphism, which captures most common use-cases, into Met in order to formally demonstrate the expressive power of modal effect types. To recover the full power of conventional effect systems beyond this fragment, we seamlessly extend Met to Mete with effect variables. We propose a surface language Metel for Mete with a sound and complete type inference algorithm inspired by FreezeML.

Modal logic and modal types have also been used to implement Rust-like "ownership", staged metaprogramming, distributed programming, and more.

IELR(1) a niche LR(1) parser generator. More well-known are LALR and Pager's "minimal" LR(1) algorithm (PGM(1)), but IELR(1) can generate a parser for certain grammars that those cannot. This post by the same authors goes into more detail about the problem IELR(1) solves.

The linked post is about implementing IELR(1), in particular the challenges the authors faced doing so.

They've implemented IERL(1) in their own parser generator, hocc, that they're writing for their own language, Hemlock: "a systems programming language that emphasizes reliable high performance parallel computation" that is (or at least very similar to) an ML dialect.

> Bio is an experimental Lisp dialect similar to Scheme, with an interpreter written in Zig > > Features include macros, garbage collection, error handling, a module facility, destructuring, and a standard library. > > Example: > > lisp > (filter > (quicksort '(5 40 1 -3 2) <) > (λ (x) (>= x 0))) > > (1 2 5 40) >

> Most visual programming environments fail to get any usage. Why? They try to replace code syntax and business logic but developers never try to visualize that. Instead, developers visualize state transitions, memory layouts, or network requests. > > In my opinion, those working on visual programming would be more likely to succeed if they started with aspects of software that developers already visualize.

...

> Developers say they want "visual programming", which makes you think "oh, let's replace if and for". But nobody ever made a flow chart to read for (i in 0..10) if even?(i) print(i). Developers familiar with code already like and understand textual representations to read and write business logic². > > Let's observe what developers do, not what they say. > > Developers do spend the time to visualize aspects of their code but rarely the logic itself. They visualize other aspects of their software that are important, implicit, and hard to understand. > > Here are some visualizations that I encounter often in serious contexts of use: > > - Various ways to visualize the codebase overall. > - Diagrams that show how computers are connected in a network > - Diagrams that show how data is laid out in memory > - Transition diagrams for state machines. > - Swimlane diagrams for request / response protocols. > > This is the visual programming developers are asking for. Developers need help with those problems and they resort to visuals to tackle them.

> Supercompilation¹ is a program transformation technique that symbolically evaluates a given program, with run-time values as unknowns. In doing so, it discovers execution patterns of the original program and synthesizes them into standalone functions; the result of supercompilation is a more efficient residual program. In terms of transformational power, supercompilation subsumes both deforestation² and partial evaluation³, and even exhibits certain capabilities of theorem proving. > > Mazeppa is a modern supercompiler intended to be a compilation target for call-by-value functional languages. Unlike previous supercompilers, Mazeppa 1) provides the full set of primitive data types, 2) supports manual control of function unfolding, 3) is fully transparent in terms of what decisions it takes during transformation, and 4) is designed with efficiency in mind from the very beginning.

Supercompilation explained on Stack Overflow

Mazeppa example (https://github.com/mazeppa-dev/mazeppa/blob/master/examples/sum-squares/main.mz):

> mazeppa > main(xs) := sum(mapSq(xs)); > > sum(xs) := match xs { > Nil() -> 0i32, > Cons(x, xs) -> +(x, sum(xs)) > }; > > mapSq(xs) := match xs { > Nil() -> Nil(), > Cons(x, xs) -> Cons(*(x, x), mapSq(xs)) > }; >

Mazeppa automatically translates the above program into the semantically-equivalent but more efficient:

> mazeppa > main(xs) := f0(xs); > > f0(x0) := match x0 { > Cons(x1, x2) -> +(*(x1, x1), f0(x2)), > Nil() -> 0i32 > }; >

It also generates a graph to visualize and debug the transformation (SVG if it doesn't load):

> !

Mazeppa is written in OCaml and can be used as an OCaml library.

> Think Repl.it, but a simpler version for esoteric languages, with a visual debugger catered to each language, that runs in your browser.

The linked example shows a Brainfuck "Hello world!" program. You can run it and visualize instructions executed in real time, the memory, and the output. You can pause/step, insert breakpoints, adjust the delay after each instruction, and enter user input. There's also syntax highlighting and checking.

All languages

Some features:

• Ruby-like syntax, terse lambdas that look like regular control statements.
• Everything is an object.
• Integrated package manager.

Jaguar is a small app that wirelessly connects to an ESP32 and can load and live-reload Toit programs. This is opposed to something like connecting the device via USB and re-installing the program every time you make a change.

Example (https://github.com/toitlang/toit/blob/master/examples/wifi/scan.toit, see the GitHub link for syntax highlighting):

> toit > // Copyright (C) 2022 Toitware ApS. > // Use of this source code is governed by a Zero-Clause BSD license that can > // be found in the examples/LICENSE file. > > // This example illustrates how to scan for WiFi access points. > > import net.wifi > > SCAN-CHANNELS := #[1, 2, 3, 4, 5, 6, 7] > > main: > access-points := wifi.scan > SCAN-CHANNELS > --period-per-channel-ms=120 > if access-points.size == 0: > print "Scan done, but no APs found" > return > > print """ > $(%-32s "SSID") $(%-18s "BSSID") \ > $(%-6s "RSSI") $(%-8s "Channel") \ > $(%-8s "Author")\n""" > > access-points.do: | ap/wifi.AccessPoint | > print """ > $(%-32s ap.ssid) $(%-18s ap.bssid-name) \ > $(%-6s ap.rssi) $(%-8s ap.channel) \ > $(%-8s ap.authmode-name)""" >

> Scrapscript is a small, pure, functional, content-addressable, network-first programming language. > > scrapscript > fact 5 > . fact = > | 0 -> 1 > | n -> n * fact (n - 1) > > > My previous post talked about the compiler that Chris and I built. This post is about some optimization tricks that we've added since. > > Pretty much all of these tricks are standard operating procedure for language runtimes (OCaml, MicroPython, Objective-C, Skybison, etc). We didn't invent them. > > They're also somewhat limited in scope; the goal was to be able to add as much as possible to the baseline compiler without making it or the runtime notably more complicated. A fully-featured optimizing compiler is coming soon™ but not ready yet.

The blog explains how to solve the following problem using Picat and planner programming, a form of logic programming:

> Suppose that at the beginning there is a blank document, and a letter "a" is written in it. In the following steps, only the three functions of "select all", "copy" and "paste" can be used. > > Find the minimum number of steps to reach at least 100,000 a's (each of the three operations of "select all", "copy" and "paste" is counted as one step). If the target number is not specified, and I want to get the exact amount of "a"s, is there a general formula?

\- Math Stack Exchange

A programming model that is a graph, where code is written on the edges to add behavior and interactivity to the connected nodes.

Video demo:

> !

Live demo

I wanted people to be able to try out my language online, and it’s now possible with a vscode like interface, sending code to a docker image running the interpreter!

It was easier than I thought to implement, and yes, security was a concern, but I have been able to harden the docker container as well as implement restrictions on the websocket server to avoid having users escaping the docker image and getting access to the VM it’s running on.

> This pattern [(multi-stage programming)], which I'll refer to as "biphasic programming," is characterized by languages and frameworks that enable identical syntax to express computations executed in two distinct phases or environments while maintaining consistent behavior (i.e., semantics) across phases. These phases typically differ temporally (when they run), spatially (where they run), or both.

An older (2017) page on multi-stage programming

Winglang ("a programming language for the cloud"), the author's language

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

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 or eval, 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)

Defunctionalization (wikipedia)

Codata in action, or how to connect Functional Programming and Object Oriented Programming (Javier Casas)

> 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.