DEV Community: DrBearhands

The glTF file format for 3D models has some issues

DrBearhands — Thu, 19 Dec 2024 15:00:52 +0000

The glTF 2.0 file format has become a standard for sharing 3D assets between applications. Unfortunately, it has a few unnecessary problems, and these problems are quite typical for our industry and the sad state it is in: rushed development, additive thinking, and a disdain for formal correctness. I'm going to rant about them here in the hope that others might avoid them, and that perhaps one day we will have a sane standard.

The WebGL-first problem

glTF 2.0 comes from glTF 1.0, the WebGL Transfer Format. This name is apt, as it heavily focussed on WebGL. It allowed specifying glsl shaders and structured its data as though it is arguments to WebGL API calls. Supporting glTF 1.0 in other graphic APIs, such as APIs such as Vulkan, Direct3D, WebGPU, would have been difficult and inefficient. The industry later standardized around PBR shaders/materials. For glTF 2.0, the API-specific shaders where therefore replaced by PBR materials. In other words while glTF 1.0 was specific about API (WebGL) and generic in materials (any shader), glTF 2.0 is specific about materials (PBR) but generic about API, except glTF 2.0 still declares data in a very WebGL-centric fashion. The focus of the project shifted, but decision-makers were unwilling to "redo" work they had already crossed off once. The standard was rushed and is now in a permanently bad state and all us implementors must suffer because of it. Let's get into some examples where this shows.

Meshes are defined using variable attributes. Rather than being a list of values, as in e.g. obj files, the attributes reference (by id) an accessor, defining stride, offset and bufferView id. The buffer view defines an offset and index into a buffer, where finally we get the data. This is basically the input to ArrayView, gl.bufferData() and gl.vertexAttribPointer(), respectively. The specification essentially admits this tight coupling at https://registry.khronos.org/glTF/specs/2.0/glTF-2.0.html#_accessor_componenttype:

Related WebGL functions: type parameter of vertexAttribPointer(). The corresponding typed arrays are Int8Array, Uint8Array, Int16Array, Uint16Array, Uint32Array, and Float32Array.

In glTF 2.0, specifying data as input to WebGL functions like this is pointless. Not only is it supposedly targeting other APIs as well, switching to PBR also requires changing the data in some cases, so it will not be fed directly to WebGL functions even on applications running on WebGL. Normals and tangents, for instance, need to be generated if absent, which alter the vertex indices.

What's more, even in glTF 1.0, which was specifically targeting WebGL, a model should not be defined as arguments to API calls. Because neither the modeler, nor the glTF exporter used, can know what the most efficient way to do this is. For instance, interleaving vertex attributes is a performance consideration that can be highly dependent on the application and deployment target. I was once maintaining a WebGL rendering engine for room planning. The graphics were fairly simple, but it did have 4 shadow-casting lights, which is 3 more than normal. As an optimization, I decided to interleave the vertex data. Essentially that means you have a single array with all the information you need for every vertex close together, rather that having a different array for every "field". Performance benefits on my laptop - with integrated graphics - were within margin of error. As it turned out, the same change tanked performance on GPUs and ARM architectures. The 4-shadow casters each needed to draw every object in the entire scene, but only needed the vertices' position to do it. Were first they had a tightly-packed array of positions, simply not using the other arrays, now each position was separated by strides of useless data, causing cache misses. The more advanced CPU caching strategy of my laptop with integrated graphics had likely hidden that issue.

The advantages of defining buffersViews and accessors to match the structure of WebGL just aren't there for glTF 2.0, and were arguably never there for glTF 1.0 either, but this indirection makes extracting the actual data we need a lot more strenuous. A few of my colleagues had just given up, and while it didn't take me that long, the code I wrote definitely isn't the most readable. In comparison, an array of values would have been trivial.

There's another place where it shows that glTF 2.0 was intended to define inputs to WebGL functions: default values and constants. In some places, defaults are missing from the spec, and you will have to look up the matching WebGL function. E.g. in samplers' magFilter and minFilter. They are optional, but no default is given at the time of writing.

The accepted values for such variables are also nonsensical outside the context of WebGL. Does 9728 read like a magnification filter? No? Well it is and means NEAREST. In WebGL.

The moral here is: when performance allows, define data as what it is, rather than trying to be clever about how some application would like to have it internally, leave that to the application.

Too much stuff

Besides rushed development, glTF 2.0 is also plagued by what I've started to call "additive thinking", as I do not know of an existing name for it. People tend to think adding feature will make a thing better. Quite often, the opposite is true. Whether you want to call it the Unix Principle, orthogonality or encapsulation, a driving principle of good software engineering is easy composition: you make a thing that performs a function, and can be easily combined with other things to make bigger things. This is what makes category theory interesting for software developers; it is the study of composition. The opposite is the God object anti-pattern, where you give too much stuff to something, rather than making many small things that can interact.

glTF 2.0 suffers from this too. Not a lot, but it does. I'll name a few things that, in my opinion, should not be in the specification in the way they currently are.

The worst offender is using negative scale as a mirror function. When you scale by a negative value (in a single axis), you mirror the position of the vertices, but you also flip their rotational order. Where first their internal side would get culled because it was e.g. clockwise, now the external side is clockwise and gets culled. This prevents using negative scaling to mirror a mesh as-is. Nevertheless, some engines do allow for this. You can check if a mesh has a negative scale (by its matrix determinant), and cull the other side of the triangle if it does. Changing cull side requires changing the pipeline, which is detrimental to performance, so we probably don't want to do that while iterating meshes in the render function. Instead, we complicate the renderer by pre-sorting objects into positive and negative determinants.

There are other features that I don't think are good defaults to have in the format: vertex animations, multiple texture coordinates, sparse accessors, lines and points... I would much rather have seen them in extensions to keep simple things simple. These features aren't necessary for a lot of e-commerce applications for instance. As it stands, an engine supporting glTF 2.0 needs to be pretty bloody robust and feature-complete, wasting developer time and bloating their engine.

Then again, the cynic in my says that might have been the point. Make the standard format complicated enough to incentivize smaller companies to buy into the commercial engines whose owners are part of the Khronos group.

Supposing your goal is to make a good standard, the point I'm making is: try to keep it simple, and allow for extensions. On that last part at least, glTF 2.0 is pretty good as far as I can see, though I plan to verify this in the future by writing my own extension.

Please use sum types

Finally, and I am getting tired of this being everywhere, glTF does not leverage sum types to ensure type-safety. These are not toys for academics. They are essential in accurately defining your data. Sum types are the dual to product types every programmer knows as structs, classes, objects, or dicts: they consist of one type and another type. Sum types consist of some type or another type. Let's take a look at glTF's camera definition:

That's a lot of text to say a camera needs to be either orthographic or perspective. The used type provides no information about this, orthographic and perspective field look independent of each other. A better approach would have been to use a sum of an orthographic camera and a perspective camera, placing the tag (type) as a fixed string with the data. E.g. in JavaScript with JSDoc:

/** 
 * @type { { 
 *    type: "orthographic", 
 *    orthographic : camera.orthographic
 *  } | {
 *    type : "perspective", 
 *    perspective : camera.perspective
 *  } } 
 */
camera

This would immediately inform the programmer and the type checker of the right intention. If it has type field "orthographic", it will have an orthographic camera, if it has a type field "perspective", it will have a perspective camera, and there are no other option. Much shorter than all that text explaining the same thing but in a format my type checker can't read.

The good

I should also take some time to mention what glTF 2.0 does well. First off, it exists and can do basically everything I want it to do. When I was modding games, we had complex toolchains between proprietary formats that would always lose the material, animation, or more likely both. glTF 2.0 is, at least, a standard, and a well-documented one, with a lot of test-cases to boot. This is all the reason I need to implement it over obj, ply, or other formats. It's also not going to change every few months.
There's also PBR, glTF 2.0's binary format, which is very nice to have. It allows packing all data, such as textures and meshes, into a single file, keeping everything together that belongs together and making it more portable. I've seen enough broken links in mesh and material files to appreciate this. On the other hand, referencing external resources is still possible, so no efficiency is lost due to data duplication in applications that reuse assets.
Finally, glTF 2.0 is built to support extensions, which means it can stay relevant if market demand for some new feature emerges. I myself look forward to toying with an extension in the future.

Out of the file formats for 3D virtual display, glTF is the best we have, but that fact should be rather embarrassing for our industry.

Credits

Environment map in article header from Andreas Mischok
gltf files in article header from khronos

Web Monetization debunked

DrBearhands — Wed, 31 Aug 2022 06:58:41 +0000

Over the last few years, grifters have been preying on naive content creators through the Web Monetization proposal. The companies involved are Coil, Ripple, and the Interledger foundation, while Mozilla and Creative Commons seem to have fallen for Coil's marketing material and became unwitting accomplices. Web Monetization is presented as an "open" and "fair" protocol for micropayments on the web. The idea being that, when browsing a website, you send tiny payments to said website, rather than watching ads. A cursory technical evaluation reveals that if that were truly the intention, it is an abysmal failure. Instead, it has all the hallmarks of a pyramid scheme, where its proponents attempt to sell a made-up currency they created themselves for real FIAT currencies, specifically US dollars, while at the same time forcing a more favorable exchange rate. Because of the lackluster design as a payment system, wide adoption of Web Monetization could have disastrous consequences on our society.

Let's get into the details.

Shortcomings

Web Monetization is woefully underspecified in many places. That is not acceptable for a payment protocol. I believe this to be intentional, as some of the unspecified elements involve complex problems, core reasons why micropayments don't exist yet. Interested readers who are unfamiliar with the subject can easily miss such omissions. They would only notice the well-specified bits of the proposal, which are typically easy problems to solve, thus making the proposal seem much better than it is.

When such issues come up, proponents of Web Monetization refer to vague future technology that is not part of the spec. They might as well hire a shaman to cast a spell on the specification, for all the technical validity such an argument has.

This is a fairly common strategy in "new technology" scams. It was already used by more-or-less the same grifters in earlier scams, the XRP Ledger and Interledger, among others. More about those in the appendices.

Price

One example of an important omission is price. Price determination is a key problem of micropayments. You don't want users to think about, or interact with, every micropayment. The effort and mental load would be too great for sub-cent values. Payment initiation and price determination are critical design considerations that must carefully balance UX, safety, and legal requirements. Some experts even believe these requirements to be so stringent, that they make micropayments altogether impossible. Web Monetization offers no solution here. It instead leaves the problem up to undefined "agents". An agent, in this context, is a computer program acting on your behalf, deciding when you want to pay and how much you want to pay. The agent isn't controlled or directed by you, but by the company that acts as your Web Monetization service provider. If you like Net Neutrality, this should absolutely horrify you. It essentially means that Coil decides who gets how much money from Web Monetization. Potential recipients, of course, include their own websites.

How will websites react to agents that unfairly disparage them? Will they block users with such agents? Or will they accept everyone and take what they can get? In the latter case, or if it's not possible to detect unfair agents, Web Monetization devolves to pay-what-you-want. Pay-what-you-want is an incredibly easy model for which we already have a variety of legitimate services. On the other hand, if websites would indeed start blocking users with underpaying agents, we would see a fragmentation of the web, where different Web Monetization providers would give access to different websites. Again, we already have fragmented content subscription services, and they don't require harebrained payment protocols based on cryptocurrencies.

Biased agents aside, the idea that a computer program could analyze a website to determine how much money to send it, is ludicrous. Websites are free to act on payments however they want. They are Turing-complete, with all the unpredictability that entails. There is also no way an agent can assess the value of a website, much less the subjective value to a specific user.

What's more, a set price cannot be added to the Web Monetization specification, because it is not tied to a specific currency. The use of an exchange network (Interledger) creates a disconnect between what is sent and what is received. Tying price specification to XRP would obviously favor Coil/Ripple, whereas tying price to dollars, or anything else they can't make up themselves, would make the scam a lot less profitable.

The use of agents controlled by service providers only favors Coil, as it allows Coil to set its own exchange rate. More on that later.

Worse than ads

The lack of price negotiation in the specification is serious enough that it alone should stop adoption. Yet there's another equally serious problem. Although a payment agent can pretty much do whatever it wants, Web Monetization is typically presented as a system that continuously sends payments over time. This is a horrible idea.

Let's remember why we want to get rid of ads. It's not just that they are annoying. Ads cause platforms to drive "engagement": keeping users on a website as long as possible so they can be made to watch more ads, which means more revenue for the website. This has resulted in some pretty awful strategies: social media driving insecurities, padding content with filler, clickbaiting, and most importantly, serving ever more extreme, shocking, dangerous, and polarizing content.

Since Web Monetization is a pay-by-second scheme, it creates a more direct incentive to keep users around as long as possible. This makes it worse. Advertisers don't want to be associated with negative content, and have on multiple occasions pulled their money when it financed hatred, misinformation, or shock videos. There is no such pushback mechanism in Web Monetization.

Another reason why one might want to move away from advertisements is to avoid tracking. I find it hard to believe that Web Monetization will offer anything of value here. Tracking is being used on noncommercial websites as well, as some of them have blindly added external elements that came with tracking. Ad-free stores are still asking users for permission to place tracking cookies. It's bad, but unfortunately that's the way things are.

In short, the Web Monetization pay-by-use model is so harmful that it more than undoes any good that could come from a reduction of advertisements. What's more, there is no reason why websites wouldn't double dip, serving you ads while also enabling web monetization.

The grift

So the specification is terribly broken. This is not the kind of oversight someone genuinely trying to solve this issue would make. It is because the specification has been designed for something else entirely. Let's get into why I'm calling this bad specification a actual grift.

The company pushing Web Monetization is Coil. Coil offers a Web Monetization "service" where you pay the company a fixed monthly amount in dollars and they pay websites in XRP. Remember that Web Monetization agents may decide how much they pay. So Coil's "service" is about them getting 5 dollars every month, and deciding themselves how much of some cryptocurrency they send out to participating websites. That sounds mighty convenient... but it gets worse. Coil was funded by Ripple for a billion XRP, and Coil's CEO was CTO at Ripple. Ripple created XRP. From nothing. It's fake money that is not backed by anything.

Most cryptocurrencies typically have some kind of mining scheme. Mining is the system that both creates new coins and allows a ledger to be decentralized. The creators of XRP discarded mining (and decentralization), to instead award every coin that would ever exist to themselves.
This was too obvious for many investors, and so XRP didn't do amazingly well. I will cover the original excuse for XRP, and how that too was a scam, in an appendix.

This left Ripple in an awkward spot: the company had billions worth of fake money, but couldn't really spend it. XRP was already heavily criticized for being a centralized scam coin. An obvious dump of XRP by its creator would likely result in a market crash and a number of lawsuits. Considered they had previously targetted banks, those lawsuits could hurt. Ripple needed to obfuscate things, so they created Coil.

Since Coil is receiving dollars and sending out XRP at their own discretion, it is essentially letting Ripple covertly exchange their supply of made-up money at a valuation of their own choosing. Coil may technically be a different company from Ripple, but as its people come from Ripple, its money comes from Ripple, and its goals come from Ripple... that doesn't really matter.

But this is just the first phase of the scam. Things get even worse in the off-chance the specification gets wider support.

Absolutely closed

The fact that Coil is using it's own, made-up money for use in Web Monetization isn't just a bad deal for users, it is also an unfair competitive advantage that effectively closes up the specification. Will other companies offering Web Monetization services also get to use their own made up money? Of course not, and Coil's subscription service exacerbates that unfairness.

A fixed subscription is typically much preferred by consumers than pay-by-use. This is a well known problem in micropayments. Coil can offer such a service because they are using made-up money. Sending a payment doesn't actually cost them anything. Normally, companies cannot offer to cover your payments for a monthly fee. That would be way too easy to exploit. You could just send money to yourself, paid by the service provider, and only pay the monthly fee. If you were to try it with Coil, you are essentially just buying XRP, which is what they want you to do in the first place.

But that's not all. Interledger is the technology supposed to make the protocol "fair" and "open". It's a network of exchanges that allows for the use of multiple (crypto-)currencies. Interledger is controlled by Coil/Ripple. At the top of its board of directors sits the Coil CEO, followed by someone from Ripple. That's already suggests a blatant conflict of interests. Even if it weren't, Interledger still would not make the protocol fair or open, quite the contrary. Every exchange between a payment sender and recipient adds fees and delays. That means it's convenient for users to centralize onto a single currency. With Coil being the initial proponent of Web Monetization, that currency is going to be XRP. If new Web Monetization service providers are to be attractive for content creators, they will have to buy XRP.

Interestingly, if you want to receive XRP, you must first buy and spend XRP to create a wallet. While this is supposedly done to prevent span, it is also the exact approach of pyramid schemes: new entrants must pay old entrants (often by buying some asset for much more than it is worth).

Conclusion

The marketing material of Web Monetization is incredibly appealing. It would be great to have a straightforward system to pay for the content we enjoy directly. Advertisements are a roundabout way of achieving this, and are ultimately much more expensive if we factor in advertisers' return on investment. But Web Monetization is worse. It appears to be designed to pump and dump XRP, and suffers as a payment system as a result. Even Ripple themselves proclaimed their "investment" in Coil was to pump XRP. As a scam it is quite clever, because the victims can't easily recognize themselves as victims, and the difference between victim and scammer is quantitative, as with most (pseudo-)pyramid schemes.

There are going to be some people other than Coil/Ripple who earn money from Web Monetization. They will receive their made up currency, and sell it to the next biggest fool for FIAT. This just means they are higher on the pyramid.

Web Monetization needs to go away to make place for legit suggestions, free of cryptocoins or other asset pumps. In the meantime, it's better to fight against ads with new legislation, and making more people aware of the hidden costs of ads. GDPR, for instance, has done wonders exposing hidden privacy costs, and just how widespread unnecessary invasions of our privacy are.

Ultimately, Web Monetization only covers voluntary payments, and is inadequate for anything else, due to a lack of price determination. Such voluntary payments are easy. If you're willing to spend 5 dollars a month to support creators you enjoy, use the randomized donation model: bookmark the pages you enjoyed, pick one at random at the end of the month, and send them the 5 dollars. If the website is not taking donations, send the money to a charity.

Appendix 1: The XRP ledger is also a scam

If you've read this far you may also be interested in more details about Ripple's earlier scam, the XRP ledger.

Let's start with some background. There is a bit of an open problem for banks: how to transfer money from an account on bank A, to an account on bank B. Your account balance is knowledge. It cannot be "moved" like a physical object. That means that if you want to transfer money from an account on bank A to an account on bank B, someone has to physically move the money between the banks.

An alternative does exist: nostro/vostro accounts. Slightly simplified: bank A keeps an account with bank B. Bank A can then transfer money to clients of B, from its own account with B. That way an inter-bank payment becomes a payment from an account within the same bank. A nostro/vostro account is essentially a monetary buffer that creates trust. There are other solutions, such as payment channels, that operate on essentially the same principle: set money aside to quantify trust.

The problem of nostro/vostro accounts and similar systems is combinatorial explosion: there are too many banks to set up buffers to each of them. A more advanced solution is to create these buffers with a shared centralized party (the intermediary), such as the European Banking Association, or a large international bank. This works as long as everyone joins the same payment rail, i.e. so long as everyone maintains buffers with the same entity. Since changing payment rail is usually incredibly expensive, this would give a lot of power to those intermediaries.

The key takeaway here is that making payments between banks can be done, but requires setting up trust buffers.

Cryptocurrencies caught the interest of banks because they seemed to offered a solution to this problem. With decentralized cryptocurrencies, money is fully digital. Changing who owns/controls money does not require physically moving something, making trust buffers redundant. On the other hand, banks don't want to deal with cryptocurrencies. They are volatile, lawless, not backed by anything, and it's not what their clients are using. Furthermore, the biggest cryptocoin, Bitcoin, had way too low throughput.

Ripple decided to capitalize on this niche with the XRP Ledger. The main idea behind the XRP Ledger was that banks could declare that they owned a certain asset (e.g. USD banknotes). A claim of ownership of that asset would be written to the XRP ledger, where the claim could then be traded with other parties on the XRP ledger. Essentially, the bank creating the claim is promising they would pay out the asset to the final owner.

This doesn't solve the problem any better than nostro/vostro accounts. There is no certainty that an asset on the ledger can be cashed in, it's still a matter of trusting the issuing party. The XRP Ledger assumes banks have a precise trust score in the claims made by other banks, more-or-less expressed as the expected probability that a given asset is valid. That is highly dubious, and if present could also be used for implicit nostro/vostro accounts. It is a bad assumption in any case, as any nonzero trust score can in principle be exploited without limit, by creating infinite virtual assets they do not intend to pay out. In comparison, the balance of a nostro/vostro account sets a precise upper limit for how much one bank could damage another bank.
Sure, the XRP Ledger would allow parties with a low trust score to receive a trust injection by using assets from parties with a high trust score, but this is not fundamentally any different from opening an account with an intermediary.

So this system is fundamentally broken, but where does XRP factor in? The reported purpose of XRP is to function as spam prevention. Trading or opening an account on the XRP Ledger requires functionally destroying XRP coins. Yes, adding small payments to actions is a known way to prevent spam, but there are other methods. This one just so happens to be incredibly convenient for Ripple. XRP isn't a mined coin, and the XRP Ledger does not use proof-of-work algorithms. That does make transactions faster, but it also allowed Ripple to "pre-mine" every XRP coin when they created the XRP Ledger. That means they gave them all to themselves. Without coin mining, they need a different way to achieve consensus over multiple parties. A more traditional consensus strategy was chosen that relies on validators. Since the XRP Ledger need to at least appear decentralized, most of these validators are not (known to be) Ripple themselves. In other words, the validators are doing the work, and Ripple gets paid.

Relying on validators is an old strategy with some serious issues. When Satashi Nakamoto created Bitcoin, he invented the proof-of-work strategy. Ripple's consensus algorithm already existed at the time. It just wasn't good enough for Bitcoin. Validators must be appointed by someone, some authority. It's not a free-for-all type of decentralization as with proof-of-work. It matters who the validators are, as they are, as a whole, a trusted central party. While I myself haven't done any research into who the validators are, it appears the state of XRP validators is pretty horrific. Validators are appointed by Ripple, and we often don't know who they are. Most of them might be the same colluding entity, or even Ripple themselves. This is the kind of information you don't find out until you are already very deeply on board with Ripple and XRP. I personally only came across it by chance. XRP Ledger proponents might tell you that you choose your own validators, but that is utterly irrelevant. If a validator were to go against the majority, it essentially wouldn't be participating in the XRP Ledger. The point is to achieve consensus. It's like saying you can choose to be rich by killing yourself if you are poor.

In short, the Ripple protocol, the alleged reason for XRP's existence, is inferior to preexisting technology, and even quite dangerous. So why did it rise to prominence?

After Ripple gave all the XRP to themselves, they had a lot of potential money to play with, as long as people were buying XRP. They lured initial adopters by giving away large sums of XRP. Those investors would then also benefit if the market value of XRP were to rise. They would have incentives to make the XRP Ledger and XRP itself look legit. Making people think the market rate of XRP was going to go up even further, thereby driving the price of their vacuous assets. Let me spell it out: this is basically a pyramid scheme. But it has a twist. Even the most well-intentioned bank would have to consider investing in the XRP ledger. You see, technical qualities, or the lack thereof, are not the main driving force in banks' decisions. If there is a global shift in payment rail, individual banks must switch to that payment rail, or they will no longer be able to provide their service to customers. If customers cannot make payments through their bank anymore, they are probably going to go elsewhere, and the bank goes belly-up. So banks cannot be allowed to be blindsided by global developments, such as potential wide adoption of the XRP Ledger for international payments. Switching payment rail is slow and expensive. Not something to which they can react on the fly. Hiring a few developers to play with XRP is relatively cheap. It is therefore the safest decision for banks to make small investments in XRP to gain experience with the emerging protocol. How unimpressive the technology behind it is, is simply irrelevant in this decision.

To summarize the business strategy of the XRP Ledger: the first "adopters" could be won over and turned into co-conspirators with XRP gifts, and the rest would have to follow because of the threat of a changing global payments environment.

Luckily, people weren't quite as stupid as Ripple Labs expected. The European Banking Association started warning banks against the dangers of virtual currencies. Many people were calling XRP a scam coin because it was centralized and pre-mined. The SEC started a lawsuit. Coinbase stopped trading XRP. Banks also started to realize there already was a central party they all trusted: the central banks. We will likely soon see Central Bank Digital Currencies emerge, which are far superior to Ripple in handling inter-bank payments. So, it appears Ripple has now changing strategy, and trying to pump-and-dump their worthless coin through Web Monetization and the XRP Ledger.

Appendix 2: interledger is not new technology

Interledger is presented as something sort-of separate from Web Monetization. I don't think the two can truly be separated. Interledger is set up as a nonprofit to appear coin agnostic, while really being led by Ripple/Coil, and soft-locking other cryptocurrencies out of the market. However, I want to briefly consider the merits of Interledger on its own.

Interledger is a specification for how a network of cryptocoin traders could communicate. The idea is to identify chains of multiple traders, allowing for more conversions than any individual trader might offer. As I explained earlier, the hardest part about enabling two parties to transfer digital currencies, is setting up the trust buffer between those parties. It doesn't really matter if it's a nostro/vostro account, a payment channel or something else. Interledger leaves that problem to the participants of the network themselves. They don't have a solution for it. They have, again, skipped the hard part. Interledger merely expects parties that have overcome this obstacle, to adhere to their silly protocol.

This supposedly groundbreaking new technology is adds so little that it's hard to criticize. Path planning on a graph of exchanges, amazing!

Eugh.

The Abstract Syntax Tree

DrBearhands — Thu, 02 Dec 2021 11:59:46 +0000

Introduction

One of the first steps a compiler must take is parse the human-readable program format, usually a plain text file, and put it into a structure the compiler can work with; the Abstract Syntax Tree (abbreviated to AST).

Here's a simple example with code followed by an AST:

f 2

and a slightly more complex example:

( \x -> x + x ) 2

in this post I wish to define the AST for my language based on requirements set forth previously.

Underlying litterature

I'm primarily basing myself on the following work:

[Peyton Jones & Lester 1992] Implementing Functional Languages: a tutorial. The title of this book is self-explanatory, though I should mention it covers lazy languages specifically.
[Martin-Löf 1973] An intuitionistic theory of types: predicative part. This article first describes the Martin-Löf type system, that is, dependent types. It explains how propositions about values in a program can be expressed themselves as types and terms.
[Atkey 2018] Syntax and Semantics of Quantitative Type Theory. This article describes quantitative type theory, which marries dependent types with linear values and erasure.

Of course, I'm also using a lot of transitive knowledge and things I picked up here and there, but have no specific source for.

A default AST

To define how an AST might look, we must specify a language grammar. This is often done using BNF (Backus-Naur Form) notation. In languages like Haskell and Idris it is incredibly easy to express it directly in a type, so I will do that instead.

I start from the AST given in [Peyton Jones & Lester 1992] p.17, translated to Idris:

data Expr a
  = EVar String
  | ENum Int
  | ECtr Int Int
  | EAp (Expr a) (Expr a)
  | ELet IsRec (List (a, Expr a)) (Expr a)
  | ECase (Expr a) (List (Alt a))           
  | ELam (List a) (Expr a)

data Alt a = (Int, List a, Expr a)

Here, the type-variable a is the "binder" of values. Generally this will be a String representing the name of a variable, but different types could be used as well.

EVar represents named variables, such as x.

ENum is for number primitives: 1, 2, 42, etc.

ECtr is less intuitive, when we define a type, such as data MaybeInt = Just Int | Nothing, each constructor can be given a number, called the tag. The tag can be used internally by case expressions to match on the right constructor. The other Int argument to ECtr is the arity: how many arguments the constructor takes. In the example Just has arity 1 and Nothing has arity 0.

EAp is function application. For instance, f x would parse to EAp (EVar "f") (EVar "x").

ELet is for let ... in expressions, where the (a, Expr a) values are the variable definitions.

ECase is a case expression. The Alt a type has a tag value to match, with a list of constructor arguments, and an expression.

ELam is for lambda functions.

There are a few changes I wish to make based mostly on preference.

First, we can determine whether a let-expression is recursive, e.g. let xs = 1 : xs in ..., by static analysis of the enclosed definitions. [Peyton Jones & Lester 1992] does this, more or less, in 6.8.3. I prefer not to have a specific field for it so that I have a single source of truth. I will remove the IsRec field. I suspect the book only uses this field to avoid having to explain dependency analysis first.

Second, numbers are just constructors that should really check their priviledge. Defaulting to int is a fantastic source of bugs. By giving numbers special treatment we are also overlooking more generic optimizations. ENum goes.

Third, I'm taking a hint from Elm style guidelines and replacing builtin types by more meaningful custom ones.

After those basic changes we are left with:

data Expr a
  = EVar VarID
  | ECtr CtrID
  | EAp (Expr a) (Expr a)
  | ELet (List (Def a)) (Expr a)
  | ECase (Expr a) (List (Alt a))           
  | ELam (List a) (Expr a)

data Alt a = MkAlt CtrID (List VarID) (Expr a)

data Def a = MkDef a (Expr a)

I have left the various IDs intentionally undefined.

Making the AST hollistic

To consider what changes are necessary to support hollistic programming, we must go back to the language's goals.

If we wish to define the whole system in a language, rather than one particular program, we must start considering changes in code over time. Typically, it is the responsibility of the developer to ensure that changes to not break compatibility with persistent systems, such as databases. If such systems are generated by the compiler, it is the compiler that must be able to prove compatibility with some previous version. Immutability helps a great deal here. Just as Elm uses immutability to quickly determine what areas of a DOM need updating, so too we wish to have immutability in program definitions themselves, so we can correctly determine what is compatible. It would be nice if we had some kind of "metapurity": make the act of programming itself pure.

To achieve this, I will copy the identify-by-hash approach of unison. Where names are stateful and may point to different functions over time, hashes are stateless. If a function changes, so does its hash.

Of course, programming with hashes directly is infeasible for programmers. We need a human-compatible language, let's call it the display language. In most other programming languages, the display language is the source of truth. The core language AST is derived from it during compilation. There is a missed opportunity here.

A lot of effort is being wasted by developers fighting about pure display concerns: tabs vs spaces, camelCase vs PascalCase vs snake_case vs kebab-case, operators vs functions, import definitions, naming, alignment, egyptian brackets... after removing names as identifiers, none of these concerns change a program's AST in the core language. If we make the core language the source of truth, and define the display language as (isomorphic to) the core language plus some display information (e.g. variable names), we can do away with those issues entirely.

Now, back to the AST

Many naming issues are already resolved by resorting to hashes, but variables may also be bound by let-expressions, lambdas, and supercombinators. For there, we don't really need hashes. We can use a de Bruijn index, slightly adapted to work with let-expressions and supercombinators as well (both can be converted to lambda functions, but that seems counter-productive).

I will have to distinguish between local variables, using de Bruijn indices, and global variables. Binder types have become superfluous, we just need to know how many binders a binding-expression has.

data Expr
  = ELVar Nat               ||| de Bruijn index of locally-bound variable
  | EGVar Hash              ||| Hash of globally bound supercombinator
  | ECtr CtrID                    
  | EAp Expr Expr
  | ELet (List Expr) Expr   ||| 1st arg is definitions, second is the "in" part
  | ECase Expr (List Alt)           
  | ELam Nat (Expr a)       ||| Only need to know number of arguments

data Alt = MkAlt CtrID Expr ||| # arguments derived from CtrID

Dependent typing

This leaves us with 2 problems: CtrID is not defined, and we are missing a way to use types as values.

unfortunately, I start using math heavily here, and have not found a satisfactory way to display it on dev.to that does not require a lot of manual work. I ask you to continue reading on my website instead.

On automated versioning strategies for CI/CD pipelines

DrBearhands — Thu, 25 Nov 2021 12:15:31 +0000

It is quite likely that one of your projects will need version numbers at some point in time. You might also want to generate them automatically in a CI/CD pipeline.

The popular way of reporting version numbers is semver. Three numbers, MAJOR.MINOR.PATCH, denoting breaking changes, new backward compatible features, and backward compatible bugfixes, in that order. Unfortunately, this strategy is wrong in such a way it will never result in correct automated versioning systems. At least, not beyond the trivial increment counter.

The problem lies in the words "backward compatible". It is basically impossible to make changes to code that won't break some theoretical dependent project. In many programming languages, adding new functions and leaving the old ones as is does not result in breaking changes, but doing that is often bad practice. New features are bloat. Here's another explanation about the problems with semver that is more in-depth.

In practice, developers label versions based on what they think won't break too many dependent projects. It is useful in practice, but an automated tool has no way of doing that.

If semver cannot be automated, is there a useful strategy that can?

A more "correct" versioning scheme would be MAJOR.PATCH.FEATURE, were MAJOR is for changes of which the author thinks will break projects, PATCH is for changes that can break projects in ways the author thinks are niche, and FEATURE is ~~an inverse function of quality~~ for changes that maintain trace-equivalence with previously-existing endpoints. This versioning system of "descending chances of breakage" is not how we usually think about dependencies. We want the numbers that tell us what features can be used first. If I'm using dependency version X and read about a feature introduced in version Y, it should be immediately clear if I can use the feature from Y in X. There is a conflict in using version numbers to denote the feature set, and using version numebrs to describe potential breaking changes.

This leads me to the following: versioning is multidimensional. We must first realize which dimensions are interesting for our use-case and, if we can, derive them automatically.

Let's look at a few strategies that are not semver.

Type-level "semver"

Elm uses automatic "semver", but it is not actually semver. Or rather, it is semver over the metalanguage of Elm types, not Elm itself. "Breaking changes" are changes to any pre-existing type definitions, MINOR changes are new type declarations, and PATH is no changes in type declarations.

For instance, if we previously commited:

seven : Int
seven = 7

then

seven : Int
seven = 3

will be a PATH version bump.

Type level semver indicates what will not break at compile time.

Commit SHA

Using commit hashes is probably the most precise way to specify dependency versions. It is also stateless, which comes with its own benefits. You can use it with shallow clones, for instance.

Unfortunately it is also a bit inflexible. It does not give you a notion of backward compatibility. If there is a security patch you won't be able to pull it in automatically. If you have two dependencies that share a sub-dependency but require different but compatible versions of it... tough shit.

Furthermore, it's hard to read by humans, and given only two version descriptors, it is unknown which one is the latest.

Commit SHA are about the best identifiers you could have. Assuming you don't change your repository's history, which will lose references.

git describe

Another way tool that is available to us is git describe. This commands spits out TAG-OFFSET-gCOMMIT, where TAG is the most recent (manually created) tag, offset it the number of commits since that tag, and COMMIT is the current (abbreviated) commit SHA.

This has an advantage over simple commit SHAs in that they accurately allow to compare version numbers. We might consider TAG to be feature information, and OFFESET or gCOMMIT to be compatibility information. It is still as inflexible as simple commit hashes, unfortunately.

The biggest problem with this approach is that it requires pulling the repository up to unknown depth. In a CI/CD pipeline you would generally pull only a shallow copy of the repository. Why slow down your jobs by downloading every commit since the beginning of time? Well, you rather have to with this strategy, or git describe might suddenly return something unexpected if the tag is more commits away than the clone depth.

Git describe gives us stateful identity with a partial order, potentially even a total order if tags have a total order. This strategy also only works assuming no history changes in your repository.

Release/build date

Dates are nice for humans, but horribly inaccurate. The downsides are obvious: no compatibility information, no support for branches. Also, dates are subjective at best due to timezones, daylight savings time, and other more obscure changes to our timekeeping standards.

You can get the date of a commit using

git show -s --format=%ci <commit>

Alternatively, you may be able to use the date when a commit was pushed to a central repository, provided you can configure said repository. That solves the subjectivity problem.

Dates technically only offer a preorder, but result in total order quite often.

Not needing versions

This is a bit of a copout, but there are situations where you can avoid version numbers altogether. The Unison language uses hashes as identifiers, and as such identifiers point to exact objects. Adding version information would be redundant. Except perhaps as a global restriction.

Usage

So, no solution is perfect, and I'm sure there's more possibilities than this. How do we chose what is right for our project?

If you're making a library, I suggest following the standards people expect. Usually that will be semver. Haskell has Haskell PVP. It's likely that there are a few other standards that I'm not aware of. Is cases where you're supposed to denote backward compatibility, just give up on automated versioning. This is a fuzzy quantitative problem that requires a human. It is more important to match people's assumptions than to automate versioning.

In general, I'm rather skeptical of type-level "semver". It prevents type mismatches, not behavioral changes. Type mismatches cause failures at compile time. Sure, the CI pipeline breaks, but that's what it's for. Unnoticed changes in runtime behavior are far more dangerous, and automatic semver might give us an unwarranted sense of security about them when all we've done is appease the CI pipeline. In fact, for the purpose of catching potential security issues, it would be best if compile-time errors bump only the lowest version pin possible. Compile-time failures can be caught before going into production. They are not something we need extra protection against in the form of

You should still use type-level "semver" when distributing through channels that expect it.

But what if you're not making libraries?

There are too many variables to give a single correct answer. I will insteads detail an example for choices I made on a project of my own.

By example

The project I want to version is a specification in the form of text in a pdf document. What kind of changes can I expect to make?

Since this is a specification, any addition of features is equally breaking. Implementations would have to support the new feature, therefore their implementation would break. However, we can perhaps subdivide changes in a more linguistic approach.

First there is semantic changes. The intention of the document changes. The Bedeutung from Frege's Über Sinn und Bedeutung.

Then there is changes in wording without changing the intent of the document. Frege's Sinn.

Finally, there's plain old typos.

Unfortunately there is not automated tool that can reliably tell such changes appart. A comma can be an innocent mistake or completely change the meaning of a sentence. A repeated "not" can be a real double negation or word that accidentally got typed twice in editing. If the potential interpretation of a sentence does not change, why would I even release a new version?

It appears sensible to consider any change a breaking change. If typo's are so frequent they cause too many major version bumps, I just won't release typo corrections as often. So, semantic versioning (or a similar concept) does not seem like a good choice for this project.

Going back to why I want version numbers

People should easily be able to tell who has the newest version. I need a partial order, even better if it's total.
I want to be able to find the source/repository state of a specific document.
I thought about distringuishing between large changes and small changes, but thought better of it. Any change may be breaking, so let's act like it.

Commit hashes are insufficient because I want people to immediately know which version of a document is the latest.

Commit dates would work fine for the moment. I only have 1 branch that gets released in the wild, only work from my own timezone, and don't release more often than once daily. But I don't want to be forced to maintain that situation indefinitely.

Git describe would be nice, but my CI/CD pipeline is using shallow clones, so versioning may suddenly break if the last tag is farther away than the clone depth. I could parse the result of git describe and throw an error if it is unexpected. That way bad versions don't make it to release, but how would should such a broken pipeline be fixed? Bump the release number? Increase clone depth? Neither option I particularly like.

But versioning is a multidimensional problem, so I'm using two strategies. Commit hashes and commit dates. That will give me both identifiers and comparability (most of the time).

In practice

I took the above concepts into practice with the following steps:

1) Make sure the version number is being used in the document.

I'm creating the document in latex and using this trick

2) Adapt the CI/CD pipeline, my build stage:

build:
  stage: build
  artifacts:
    paths:
    - ${DOC}.pdf
  image: <my latex container>
  script:
    - export DATE=$(echo ${CI_COMMIT_TIMESTAMP} | sed 's/T.*//')
    - export VERSION=${CI_COMMIT_SHA}
    - pdflatex ${ARGS} -jobname=${DOC} "\def\version{${VERSION}} \input{${DOC}.tex}" -draftmode
    - pdflatex ${ARGS} -jobname=${DOC} "\def\version{${VERSION}} \input{${DOC}.tex}" -draftmode > /dev/null
    - bibtex ${DOC}
    - pdflatex ${ARGS} -jobname=${DOC} "\def\version{${VERSION}} \input{${DOC}.tex}" -draftmode > /dev/null
    - pdflatex ${ARGS} -jobname=${DOC} "\def\version{${VERSION}} \date{${DATE}} \input{${DOC}.tex}"

DOC and ARGS are defined alsewhere in the .gitlab-ci.yml file

Latex requires you to repeat build commands. Don't ask, I don't know either.

That's it!

In conclusion

It is harder that one would expect to do automated versioning right. The main problem is statelessness. Versions generally depend on information from past commits, but that information may not be available for efficiency. It is also quite difficult to determine useful, correct semantics for version numbers.

Planning my own programming language.

DrBearhands — Thu, 04 Nov 2021 10:27:17 +0000

During my years of writing software, I've come across a few issues with how we write software. Since I've covered my reasoning before, I will only summarize them here: type safety is nice, but doesn't extend past the memory of a single machine. I therefore want to introduce "holistic programing": instead of writing individual programs, we write the entirety of the multi-machine system.

There's a few more things I want for this language.

Accessible: nothing about a language matters if nobody can use it because it is too complicated.
Functional, dependently typed: this is the current standard for type safety. Dependent typing is not difficult, it is just very poorly supported by documentation and examples. It also requires tearing down the mental barriers between types and terms if you have prior experience in strongly typed programming.
Support for linear values: linearity is the best way to handle resources and communication that I know of. In my experience, it is not particularly hard, removes the need for other complicated language structures, and catches more problems that traditional approaches like the with keyword. Unfortunately, few languages support it well.
Architecture agnostic: when creating systems the traditional way, we must architect the solution before writing code, because we need to identify what programs to write before we can write them. That requirement disappears with hollistic (purely declarative) programming. By omitting considerations tied to an architecture or backend from the code, we can postpone optimization and architecting to a later moment. This includes all performance considerations.

Additionally, I want to adopt unison's hash-based function identifiers. Rather than using names to identify functions, it generates hashes based on its contents. This way there is a single source of truth for function references, and human-readable formatting is decoupled from program specification. Hash-based identifiers should make some things a lot easier, with modest up-front development time, as the people who made unison already did the hard work of figuring out what to do. Among other things, it should simplify modules, and once I get to it, database changes.

So, with the feature set of the core language broadly laid out, where do I start?

I decided not to fork Idris 2. Not just because I'm a sucker for peer pressure, but also because Idris 2 is a bit too far from where I want to go, and the compiler seems a tad too complicated to boot.

That said, I will use it to build my language. I sorely missed dependent types the last time I decided to make a functional programming language and there are not many languages that support them. Plus, none of the problems I've encountered with Idris in the past would be relevant for a compiler. That's no coincidence, since Idris 2 is self-hosted, so any such problems are likely caught by the developers.

Since I'm starting from scratch, I should begin by making an AST (Abstract Syntax Tree, the type representation of the language syntax), followed by an evaluator and a parser. I will also need to research & implement a type calculus (likely quantitative type theory), and I will need to implement hash-generation. That seems like a solid beginning. Concurrently, there is a fundamental issues I need to resolve: "real" async interop, particularly concurrent database use.

With real async interop, I mean operations that are fundamentally asynchronous. A Turing-complete language may be able to compute anything that is computable, but that does not include real-world interactions, nor does it mean there is a clear mapping from/to asynchronous and functional representation. For the most part, I am fine with the worst case scenario where I just cannot do this, with one exception: concurrent database use.

Databases are pretty common, and so is having multiple users/processes accessing one concurrently. Unfortunately I am not aware of any calculus that expresses concurrent database read/write in such a way that meaningful analysis and optimization can be performed. Linear types can sort-of model database changes, but not concurrent ones.

someWriteOp :: Table ⊸ Table 
someWriteOp (row : rows) =
  let
    row' = doSomethingToRow row
  in
    (row' : rows)

The above may be correct, but consumes the entire table for just 1 row. Native lenses may be of help, but I rather stay away from anything native.

Prematurely hand-optimizing C++ code for shits and giggles

DrBearhands — Mon, 01 Nov 2021 06:50:18 +0000

Left in the void that comes after abandoning a project, I decided to port a previous JavaScript / WebGL project to C++. Changing languages meant a complete overhaul of some core systems. I was looking at a post by Austin Morlan about ECS achitectures for inspiration.

Here I saw this procedure:

EntityManager()
{
  // Initialize the queue with all possible entity IDs
  for (Entity entity = 0; entity < MAX_ENTITIES; ++entity)
  {
    mAvailableEntities.push(entity);
  }
}

this isn't bad code. Nonetheless, I did not like it. And not just because I have a distaste for CamelCase.

Initializing the value mAvailableEntities potentially takes a long time. In the example MAX_ENTITIES was set to 5k, so it's not so bad, but I may require far more entities than that.

Had this been a regular project with a clear goal, the correct approach would be to leave the code as is, since it's certainly readable. Then if we run into performance issues in practice, find the procedures taking up the most times and optimize those, and use statistical analysis to determine if our changes actually mattered. That is the correct way to optimize performance. That's not what I'm going to do here.

In this particular architecture, mAvailableEntities is a pool of all available entities. That is why it must be filled. We cannot use a simple incrementing counter because entities can be destroyed as well, in which case we'd want to recycle them.

Instead, we can combine the incrementing counter and the recycling pool. If the pool is not empty, grab an element from there, otherwise, use the counter. Unfortunately, that sentence contains the word "if".

Naive implementation of the above is:

#include <queue>
#include <cstdint>

using entity = std::uint32_t;
entity counter = 0;
std::queue<entity> recycling_pool;

entity create_entity() {
  if (recycling_pool.empty()) {
    return counter++;
  } else {
    auto e = recycling_pool.front();
    recycling_pool.pop();
    return e;
  }
}

(I've left out the check to prevent going over MAX_ENTITIES)

and as we see on compile explorer, this compiles to conditional jumps (jne):

create_entity():
        movq    recyclingPool+16(%rip), %rax
        cmpq    recyclingPool+48(%rip), %rax
        pushq   %r12
        jne     .L9
...

conditional jumps can be a performance problem.

Modern CPUs have deep pipelines. Rather than fully executing one instruction and then moving on to the next one, they execute every instruction in multiple steps like an assembly line. While instruction n is going through step x, instruction n-1 (the instruction that came before n) is going through step x+1 and n+1 is going through step n-1. A pipeline of 20 steps is essentially doing 20 things at the same time and therefore ~20x as fast as it would be executing instructions one-by-one.

These pipelines require knowing ahead of time which instructions are coming up, which is uncertain with conditional jumps. Branch prediction works in some cases, such as loops, but not always.

So how do we get rid of branching?

The concept is conditional write-back. Rather than pick one branch or another, we do all branches, but don't write back the result in some cases.

C++ does not support conditional writeback directly, so we improvise a bit.

First, replace std::queue with a stack, and just use a primitive array entity recycling_pool[MAX_ENTITIES]. This will be a bit easier to hack.

Then, we specify entity 0 to be invalid. We initialize recycling_pool with a 0 in the first element. Now we can take the head of recycling_pool and it will function both as condition and value. This is rather like Maybe Entity in e.g. Haskell, but more efficient and far less safe.

entity create_entity()
{
  entity new_entity = recycling_pool[unused_idx];
  bool b_stack_empty = !new_entity;
...
}

Now we have divergence: if not b_stack_empty, we want to pop the stack, otherwise, we want to increment the counter.

b_stack_empty is a boolean with the value 0 or 1, since it was generated from the ! operation (anything that isn't 0 counts as true in C++, but true as output is 1). we can abuse this:

  unused_idx -= !b_stack_empty;
  gen_counter += b_stack_empty;

(NOTE: gen_counter starts at 0, but valid values start at 1, so it's increment-then-use)

this is a specialized form of conditional write-back.

Then, if b_stack_empty, we want to replace new_entity, which will be an all-0 bits invalid value, with the current value of gen_counter:

  new_entity += -b_stack_empty & gen_counter;

since b_stack_empty can have values 0 or 1, a non empty stack will evaluate to 0 & gen_counter, which equals 0, whereas an empty stack will give -1 & gen_counter and since we're dealing with unsigned integers, -1 is all 1's in binary, so -1 & gen_counter equals gen_counter. In the latter case we also know new_entity = 0, and 0 + gen_counter = gen_counter.

And so the full code (minus checking MAX_ENTITIES violation) is:

#include <cstdint>

using entity = std::uint32_t;
entity unused_idx;
entity gen_counter;
const entity MAX_ENTITIES = 5000;
entity recycling_pool[MAX_ENTITIES];

entity create_entity()
{
  entity new_entity = recycling_pool[unused_idx];
  bool b_stack_empty = !new_entity;
  unused_idx -= !b_stack_empty;
  gen_counter += b_stack_empty;
  new_entity += -b_stack_empty & gen_counter;
  return new_entity;
}

Compiler explorer confirms there are no conditional jumps.

The resulting assembly is also a lot smaller (24 lines vs 103), but I expect that is mostly due to the omission of std::queue.

I want to reiterate that this is dumb. The code is likely to have gotten slower in practice, even though it is more consistent, because branch prediction is probably right more often than not, and now we're executing all the branches. Code maintainability has also suffered.

This is merely an interesting learning experience.

Idris2+WebGL: Hiatus

DrBearhands — Thu, 28 Oct 2021 14:35:33 +0000

I'm putting my WebGL in Idris project on hiatus.
I started this project to get a feeling for how far I could take type-safety using dependent typing. Unfortunately, I am no longer constrained by dependent typing in general, but by Idris in particular. I might continue once significant progress has been made on the Idris compiler.

I've spent days debugging problems that turned out to be compiler problems. Error messages are extremely unhelpful. The prelude sometimes gets in the way. The syntax can be hard to read. Linear types exist but are not well-supported. The compiler code base is hard to get in to. Documentation is quite basic. In short, using Idris "in anger" is a pain in the butt, and if your problem requires Idris' particular feature set, you are probably already very angry. One doesn't typically use quantitive type theory to increment a counter. Although that is exactly whet I did in the last entry.

I'm not blaming Idris' devs for these problems. Their scope is large and time limited. Working in academia probably also forces a focus onto e.g. publications rather than nice error messages.

I don't like ending this project, because I hoped it could unify my love for type-safety with my love for 3D graphics, but after months of development I still only have a spinning white trianle, while I'm considering how supermonads qualified with dependently-typed destructors might allow monadic error handling for linear values if I can get idris to auto-construct destructors for values derived from function application. Needless to say my love for 3D graphics isn't particularly fulfilled.

However, I did sort-of get my answer.

I'm sold on dependent typing. It is actually easier to use dependent types. At some point there will be something you wish to express that is easy with dependent types, but quite complex otherwise. Dependent types are just doing to types what you are already doing in terms. Not conceptually difficult, just a different way of doing things that takes some "unlearning".

Linear types on the other hand are an entirely new thing. More research is needed to make them fun to use in practice, but they are already damned useful.

Steam blockchain ban: pragmatic or essential?

DrBearhands — Wed, 20 Oct 2021 07:58:32 +0000

Steam has recently explicitly banned games built on blockchain. Specifically, ones that allowed the exchange of cryptocurrencies and NFTs. Reactions on reddit suggest this was a pretty popular move. It appears these games are perceived to be pyramid schemes; an excuse with little inherent worth, existing merely to drive value of the underlying NFTs or cryptocurrencies. In this sense, they have a similar role to cosmetics products in multi-level marketing.

I tend to agree with the sentiment, for reasons that will become apparent.

Regardless, the ban raises an interesting question. Let's accept blockchain games were low-quality facades for pyramid schemes. Is this causation or correlation? Can there be any legitimate reason for using a blockchain or some other DLT* in gaming? Or are games and DLTs theoretically incompatible?

At their core, DLTs are methods used to agree on the order of events when nobody can be trusted**.

Initially that would appear to make DLTs a bad fit for games. In games, everybody trusts the developer. You run their code on your machine, you use their servers. This is doubly true for steam games, where steam/valve is also a trusted party.

But let's suppose we don't want to maintain servers throughout the life of our game and still want some kind of persistent public state (as in MMOs or competitive speed running). I will be generous and ignore software updates. Can blockchain help?

There are a few major limitations to DLTs that are relevant for gaming:

Not real time

Time is subjective. So relativity theory tells us. This is not a problem for games with trusted, authoritative servers, as the discrepancies are small in practice. But if the point is to avoid trusted parties, time must be expressed objectively, which is impossible even before accounting for things like latency and partitions. A blockchain game can therefore not have meaningful real-time mechanics.

Replication delays

Blockchains are replicated. That means every change in public data will be somewhat slow. Changes need to be replicated to other servers. Moving away from proof-of-work does nothing against it. Many white papers conveniently forget to mention this.

Leavers

While players could interact with low latency through a side-channel, these channels can be stopped by either party at any time. It is not possible to determine who left a game without a central party, just that communication between x and y has not finished (yet). Partitions are subjective.

No hosting incentives

It is unclear how to incentivize hosting blockchains without some kind of cryptocoin pyramid scheme. Blockchains are not free, they are even more expensive than trusted servers.

Code limitations

A lot of the code used in game is not well defined or non-deterministic. Drivers for instance are often an unknown. It may be possible to "fix" this issue, but doing so is a lot of work, much more than making the game itself.

Permanent mistakes

It is quite common for exploits in-game to lead to some kind of undesirable global state. Items are stolen, in-game economy gets trashed, scarce virtual resources are depleted... without trusted authoritative parties exploits cannot be rectified.

Conclusion

I started writing this article thinking there might be an interesting theoretical benefit to using blockchain in gaming. The fact that the entire game world is virtual appeared to make the approach more sensible than many of the real-life usage proposals. I no longer believe so.

Because of aforementioned restrictions, I don't see any avenues for bona fide game development using blockchain. Many game mechanics simply cannot be expressed objectively, without trusts. A game built on top of blockchain is effectively an overblown graphical interface over virtual asset trading.

Furthermore, the benefits of blockchains to consumers are outclassed by 3rd-party servers. Trust is an incredibly useful resource, and getting rid of it just isn't particularly beneficial to gaming.

Footnotes:

* Distributed Ledger Technology. A class of systems developed to do accounting without a trusted central party.
** This is an oversimplification, but far more accurate than most blockchain/DLT articles. Even in well-trusted newspapers.

Feedback request on "hollistic" programming language idea

DrBearhands — Fri, 15 Oct 2021 11:09:29 +0000

I want to make my own programming language, but I don't want to waste years of my life on a silly idea nobody would ever want, so here I am writing down my ideas and asking for feedback.

Pure, functional programming, particularly the dependently typed variety, holds a lot of potential business value. It lets me express (parts of) the spec as types, and ensures my implementation matches the types, and therefore the spec. If there was no spec, the types are now the (proto-)spec. The same program in Haskell or Idris will have fewer faults than something in, say, Javascript, C++, or Java. At least, that is both my personal experience and what I keep hearing from other users. When strictly enforced, it is also a huge boon to security, especially when using third party libraries, which sometimes steal your cryptocurrencies.

There is a huge limitations in this approach: specifying a solution as programs. Type-safety ends at I/O, so defining a solution in terms of multiple communicating programs right from the get-go loses type-safety unnecessarily. E.g. in a CRUD application it is more insightful to declare how responses are produced for requests on an API endpoint, without mixing in explicit I/O operations to get data from one machine to the next. In theory, pure functions have explicit data-dependencies, so we can split off evaluation over nodes at a later point.

I will call the approach of leaving program I/O undefined "hollistic programming", as it only specifies I/O of the whole system/solution.

As an example, if we have a function:

f : Int
f = g + h

we could leave the definition as-is in the code, and at compile/deploy time decide to evaluate g on a different node/thread/whatever. If we had to specify this as a program immediately, the type of f would be lifted to IO Int, which tells us next-to nothing about error handling, security, or correctness. The code would also be full of explicit communication.

There are other such decisions that are often made in code, but (assuming temination and infinite resources) make no difference to the result of the evaluation: forking, vectorizing, monomorphizing, boxing, type-unrolling, type-mapping, evaluation strategy, heap recycling, choice of allocator...

What I'm suggesting is, essentially, a fairly extreme separation of concerns.

But if not with an IO monad, how should I/O be modelled? The precise model would be user-defined, specific to a solution. A CRUD application has conceptually different I/O than an embedded system, or a video game. IO would be declared by abstract linear types c, denoting independent I/O channels, and handler functions c ⊸ c. This is a generalized case of IO ().

Caveats

I realize there are some caveats that make hollistic programming non-trivial. I will list the ones I already thought about:

Databases/shared state.
- How do I model inherently concurrent state changes? (as opposed to concurrency for the sake of speed optimization). I will have to formalize transactional state changes. I do not know how to do this elegantly. Examples are multiple clients accessing the same database and asynchronous display/update in videogames.
- Data in databases persists over code changes. To preserve correctness and data, compilation would become stateful. This is difficult, but on the flipside, anything is a step up from current ignoramus (et ignorabimus) approaches.
Adding communication adds potential for errors by partitions. Bottoms are inevitable even in the best case due to potential power loss. Nevertheless, smaller bottoms are better. I want to decrease uncertainty, not increase it. Could be adressed by lifting to arrows with timeout condition in spec, or ignored with compile argument for non-critical applications.
Some evaluation strategies (lazy, eager, greedy) may bottom when others don't. I'm not very concerned about this in practice. Most functions in BLOBA (Boring Line-of-Business Applications) are provably terminating in O(n) in my experience. In the worst case scenario, I can just force lazy evaluation on functions that cannot be proved to terminate by argument reduction. Good enough.
Other processes on a system might break assumptions made by the compiler. E.g. a large constant value stored in a file might get deleted. I don't find this a valid concern. Messing with a system that the compiler assumes is dedicated is like changing bytecode, things will break.

Other stuff

There are a few other, less novel and ambitious, things I want to achieve in my language

Limited feature set. I want people to actually try this out. Make dependently typed programming as approachable as possible.
Removing primitive types from the language. What is primitive depends on architecture. Booleans and floats are good examples of common primitives that don't always exist. User-specified mappings defined at compile-time should be used instead.
(Semi-)automatic type unrolling/optimization: e.g. {Fin x | x <= (2^32)} to int32, and Vect a n to a[n].
Encourage using correct types over "one size fits all". E.g. fixed point over floats and pretty much anything over string. If nothing else, strings and floats should not be in the prelude.
Raise warnings, or have a similar mechanism, for dubious bits/changes in code (e.g. unsafe operations).

My current plan of attack is to fork Idris 2, remove the things that are incompatible with my ideas (primitive types, interfaces, probably every single library), mock about to get a better feeling about how to define systems if not I/O monads, and start building a custom, interactive backend. I am not sure that this is sensible, or that I will stray too far from Idris to benefit from future updates.

Your feedback is appreciated.

Idris2+WebGL, part #17: A Hoare state failure

DrBearhands — Fri, 08 Oct 2021 11:21:01 +0000

As explained in the last log entry, I set out to use decorated state monads to prove certain properties of a program.

Since I have once already, somewhat unsuccesfully, used indexed monads in Haskell, I decided to aim big and tackle Hoare state monads. I've changed a few details since writing that article, such as adding a >> operator and replacing my custom exists function with a standard dependent pair (both are existential quantification, but the latter has nicer syntactic sugar).
While I did manage to get Hoare state monads working in Idris, I found their use rather frustrating. The main problem is that the type checker is strugling to find proofs, requiring manual proofs from the programmer. What's more, vague error messages in Idris 2 and the unability to put holes in some places makes the job substantially harder.

For example, consider the following code:

init0 : HoareStateMonad Nat Top () (\_, _, s => s = 0)
init0 = MkHSMonad $ \_ => MkPostS () 0

increment : HoareStateMonad Nat Top () (\s1, _, s2 => s2 = s1 + 1)
increment = MkHSMonad $ \s => MkPostS () (s + 1)

init1 : HoareStateMonad Nat Top () (\_, _, s => s = 1)
init1 = init0 >> increment

Remember that HoareStateMonad s pre a post considers a state s, a precondition pre : s -> Type over an input state of type s, a return-type a and a postcondition post : s -> a -> s -> Type over input state, return type, and output state.

As such, init0 changes the state of a Nat, works for any input state (Top holds for any value), returns a unit, and guarantees that the output state is 0. Similarly, the increment function guarantees that the output state is the input state + 1. It is obvious to a human that the postcondition of init1, which first sets the state to 0 and then adds 1 to it, is that the output state is 1.

For the typechecker, this is a little harder. First is the simple issue of how the bind (>>=) operation has been defined, the type signatures end in:

HoareStateMonad s p1 a q1
-> ((x : a) -> HoareStateMonad s (p2 x) b (q2 x))
-> HoareStateMonad s (bind_pre p1 q1 p2) b (bind_post q1 q2)

so idris excepts the resulting postconditions to be bind_post q1 q2, which specifically results in

(x : a ** (s2 : s ** (q1 s1 x s2, q2 x s2 y s3)))

and not any arbitrary thing that can be derived from bind_post q1 q2. In our case, the typechecker will conclude:

(x : a ** (s2 : s ** (s2 = 0, s3 = s2 + 1)))

rather than

s3 = 1

Nevertheless, since we can prove the latter from the former, we want the typechecker to accept this. A similar, but contravariant rather than covariant, situation occurs for the precondition.

So I've experimented with a simplify function:

simplify : {0 s : Type} 
        -> {0 a : Type}
        -> {0 preA : s -> Type}
        -> {0 preB : s -> Type}
        -> {auto 0 fPre : {s1 : s} -> preB s1 -> preA s1}
        -> {0 postA : s -> a -> s -> Type} 
        -> {0 postB : s -> a -> s -> Type} 
        -> {auto 0 fPost : {s1 : s} -> {x : a} -> {s2 : s} -> postA s1 x s2 -> postB s1 x s2} 
        -> HoareStateMonad s preA a postA
        -> HoareStateMonad s preB a postB

I can use this explicitely:

init1 : HoareStateMonad Nat Top () (\_, _, s => s = S Z)
init1 = simplify {fPost=fPost} $ init0 >> increment
  where
    fPost : {s2 : Nat} 
          -> (((e1 : () ** (e2 : Nat ** (e2 = Z, s2 = S e2)))))
          -> (s2 = S Z)
    fPost (() ** (e2 ** (p1, p2))) = replace {p = \e => s2 = S e} p1 p2

but this is not a particularly easy task. Expecting programmers to provide these proofs all throughout the code base is not realistic. I have not found a way to derive them automatically (although I believe it could theoretically be done).

This, for now, concludes my forray into Hoare state monad. The conclusion being that it is too cumbersome in the current state of Idris 2. Perhaps language updates will change things. If you want to mess with it yourself you can get the code in the hoare-state branch of my idris-linear repository (there is no actual linear variant of the Hoare state monad yet), and in particular the latest commit at the time of writing in that branch.

The hardest thing I ever did explained as simply as possible.

DrBearhands — Sun, 05 Sep 2021 08:58:17 +0000

A while ago, I came across a situation where I needed to know things about some hidden state at compile time. Traditionally, this is done using Hoare logic. In Hoare logic, every statement has a precondition and a postcondition. That is, what must be true before the statement and what will be true after the statement. For the statement "set x to 7", the precondition is that x exists, and the postcondition is that is x = 7. We can chain multiple statements and get a final postcondition using the rules of Hoare logic.

Hoare logic is limited, which is one reason I strongly prefer (total) functional programming over imperative programming. Nevertheless, even functional programmers must deal with mutable state at some point. Generally we do this with a function of type

s -> s

where s is the type of the state. That is, a function that takes as state as input, and produces a new state as output. A state-changing function may also return some value, so the actual type of the function is

s -> (a, s)

where a is the type of the return value. In functional programming we use tuples to "return" multiple values. When we define how several state-changing functions can be chained together, they are called monads. You don't need to understand what that means exactly. "Monad" is just a mathematical name for a certain pattern.

It seemed what I wanted was Hoare logic over state monads. I came across a paper about the Hoare state monad. With the knowledge I had, this was one of the most difficult things I have ever implemented. I had already given up on Hoare state monads at least twice. This time I finally managed it after a full week. I feel that not sharing this journey would be a waste. Especially since they will probably turn out to be too complicated for the purpose I had in mind.

The code in this article is what I actually used to deconstruct the problem for myself. Plus a few extras for things that are only obvious to me.

Not every language can express Hoare state monad, we will need a sufficiently powerful type system. I was using Idris 2, so this was not a problem. Don't worry, I will go through any unusual concepts before using them.

First, let's make our own state monad. I'm going to use a hardcoded state, usually this would be variable.

data MyState = Foo | Bar

For those unfamiliar with sum-types: the above declares that a value of type MyState can be either Foo or Bar.

We go on to create a state monad for MyState, you might be unfamiliar with the notation so I will explain it afterward.

data MyStateMonad : a -> Type where
  MkMyStateMonad : (MyState -> (a, MyState)) -> MyStateMonad a

Note that a single colon indicates a type declaration in Idris. E.g. x : Int means "x is an integer".

The first line, data MyStateMonad : a -> Type where declares that the MyStateMonad needs some a as input to make a Type. This is similar to arrays. In statically typed languages, we don't have just "an array", we have e.g. "an array of integers". We must specify what's "inside" it. Similarly we can have a state monad (think of it as a statement) that returns an integer MyStateMonad Int, or a string MyStateMonad String, or something else.

Below the data declaration are all the type's constructors, only MkMyStateMonad in this case. The constructor has certain arguments, (MyState -> (a, MyState)) in this case. Recall state-changing functions are s->(a,s), with s=MyState in this case. The constructor also has a return type, MyStateMonad a, which must match the type given in the data declaration header. The a is variable in this context, but every a must match, so the return type of the function defines what the type of MyStateMonad a is. E.g.: for a function f : MyState -> (Int, MyState), we know MkMyStateMonad f : MyStateMonad Int.

But what about input? Idris is a curried language, meaning we can have the function:

someFunction : Int -> Int
someFunction = (+) 1

In other words, a function of type MyState -> (a, MyState) can be a closure
of as many arguments as you want.

State monads are useful as is. They let us use do-notation rather than less readable pattern matching:

do
  x <- actionA
  actionB
  actionC x

vs.

\s1 =>
  let
    (x, s2) = actionA s1
    s3 = actionB s2
  in
    actionC x s3

this is not what we set out to do though, so let's talk about proofs in Idris.

You may have heard that types are propositions and values are proofs of propositions. The value 7 is proof that Ints exist. 7 inhabits Int. But we can do something a bit more interesting.
Remember how MyStateMonad needed some a? We can do something similar with some other type over a, say P, so that P a only holds for some a. We do this by restricting what constructors are available.

A good example is the Equal type:

data Equal : a -> b -> Type where
  Refl : Equal x x

Here, we can use the Refl constructor to prove Equal x x, but there is no way to get an Equal x y value. Equal x y is a valid type, but there is no value of that type unless x = y. Therefore, if you can pass a value with type Equal x y to a function, you know within that function that x = y. There are more complex cases, of course, such as restricting inputs to members of a list.

In the above example, Equal is a predicate, Equal x y is a proposition, and Refl is a proof of Equal x x.

We can use proofs in a function without adding runtime overhead:

acceptsOnlyFoo : (s1 : MyState)
              -> {auto 0 prf : Equal Foo s1}
              -> (Int, MyState)
acceptsOnlyFoo inState = (7, Bar)

Let's dissect the function type line by line:

(s1 : MyState): this is similar to MyState, but we have given the argument a name (s1). In dependently typed programming, types can depend on values, so it's useful to have value names in the type.
{auto 0 prf : Equal Foo s1}: the curly brackets make this argument implicit. We don't have to specify it when calling the function, provided the compiler can figure it out itself. The 0 means this argument will not exist at runtime. auto denotes that the compiler will try to find a value for the type itself from the context. prf is again the variable name and Equal Foo s1 is the type. In other words, we ask the compiler to find us some value of type Equal Foo s1, with information known at compile time only. The compiler can only succeed in this by finding Refl if it knows for sure the first argument is Foo.
(Int, MyState) the output type as you are already familiar with.

This means we can call acceptsOnlyFoo as:

acceptsOnlyFoo Foo

but not

\x => acceptsOnlyFoo x

unless we already know Equal Foo x at compile time some other way.

You might be able to see where this is going now. If we have one function that implicitly requires Equal Foo x, and another that "returns" an Equal Foo x, those could be safely chained together.

While acceptsOnlyFoo specifically requires a proof Equal Foo, we do not want to limit ourselves to just proving equality. We need a more generic type for the precondition. A precondition could be any MyState -> Type. A state monad with a precondition is therefore:

data MyPreconditionMonad : (pre : MyState -> Type) -> a -> Type where
  MkMyPreconditionMonad :
    ( ( s1 : MyState) ->
      { auto 0 prf_pre : pre s1 } ->
      (a, MyState)
    ) ->
    MyPreconditionMonad pre a

Notice { auto 0 prf_pre : pre s1 }. The proof that must be found must be of type pre s1. The initial state s1 is passed to it as argument at compile-time. Even though we don't really know what it will be. In our previous example pre was Equal Foo.

An example of how to construct the state monad with precondition:

testPrecondition1 : MyPreconditionMonad (Equal Foo) Int
testPrecondition1 = MkMyPreconditionMonad acceptsOnlyFoo

But what if we want to chain state monads that don't have a precondition? We create a Top proposition, which can always be satisfied:

data Top : a -> Type where
  MkTop : Top a

Whatever a we have, MkTop will be proof that Top a.

The name Top comes from formal logic, where it is indicated with the symbol ⊤. It shouldn't actually take any arguments, but this servers our purpose well.

And this is how you might use it:

testPrecondition2 : MyPreconditionMonad Top Int
testPrecondition2 = MkMyPreconditionMonad f
  where
    f : (s1 : MyState) -> {auto 0 prf : Top s1} -> (Int, MyState)
    f s1 = (7, s1)

So that about covers preconditions. Postconditions are a little bit harder.
As far as I know, Idris has no implicit results. Instead, we must return something like a tuple with an implicit argument.
To do this we create a special type PostS'. I've added the apostrophe because the actual PostS will be a little different.

data PostS' : (s : Type) -> (s -> Type) -> Type where
  MkPostS' : (val : s)
          -> {auto 0 prf : prop val}
          -> PostS' s prop

PostS' is parametrized by a Type s and a predicate about s. Note that we pass val to prop, not s, since s is the type, and we want the proposition to hold about the value. For a concrete example, we want to be able to say PostS' Int (Equal 7), not PostS' Int (Equal Int).

Now let's use PostS' in a function that increases a counter by 1. The type of the counter will be Nat, a built-in type for natural numbers:

testPostS' : (s1 : Nat) -> PostS' Nat (Equal (s1 + 1))
testPostS' x = MkPostS' (x+1)

As you can see, we don't need to pass a proof, Idris has figured out Equal (s1+1) (x+1) automatically, by unifying s1 and x. More or less. I think. Honestly I'm not that knowledgeable about how Idris searches for proofs.

But the real PostS needs to be a bit more complex. We don't just want the postcondition to be about the output state, it also needs to consider the returned value and input state. For instance we might want to declare that s2 = s1 + x.

Luckily, if you understand the previous code, the next step is not particularly complicated:

data PostS : (a : Type) -> (s : Type) -> (a -> s -> Type) -> Type where
  MkPostS  : (val : a)
          -> (state : s)
          -> {auto 0 prf : prop val state}
          -> PostS a s prop

A MkPostS consists of a value, a state, and a proof that a proposition about said state and value holds (at compile time). You may have noticed that prop takes no input state. That is because PostS does not know about input state. If we want a predicate about input state, that input state must already be passed to it outside of PostS. For instance, if we want to express a resulting state is equal to the input state plus the returned values:

testPostS : (s1 : Nat) -> PostS Nat Nat (\n => Equal (s1 + n))
testPostS s1 = MkPostS 7 (s1+7)

With that out of the way, let's make a Hoare monad for a specific state. We will keep using Nat now instead of MyState, since there's not much to prove about a MyState:

data MyHoareMonad : (pre : Nat -> Type) -> (a : Type) -> (post : Nat -> a -> Nat -> Type) -> Type where
  MkMyHoareMonad :
    ( ( s1 : Nat) ->
      { auto 0 _ : pre s1 } ->
      PostS a Nat (post s1)
    ) ->
    MyHoareMonad pre a post

And we can use it as follows:

testMyHoareMonad : MyHoareMonad (Equal 0) Nat (\s1 => Equal)
testMyHoareMonad = MkMyHoareMonad f
  where
    f : (s1 : Nat) -> {auto 0 prf : Equal 0 s1} -> PostS Nat Nat (Equal)
    f inState {prf} = MkPostS{prf=Refl} (inState+1) (inState+1) --{prf=Refl} is needed here because of a compiler bug.

Unfortunately there currently appears to be a bug in Idris' auto strategy. It means that, for now, we won't be able to rely on auto as much. It's not a huge deal provided it will get fixed in the future, but a tad annoying.

But it's time for the real thing, make a Hoare state monad without hardcoded state type:

data HoareStateMonad : (s : Type) -> (pre : s -> Type) -> (a : Type) -> (post : s -> a -> s -> Type) -> Type where
  MkHSMonad :
    ( ( s1 : s ) ->
      { auto 0 prf : pre s1 } ->
      PostS a s (post s1)
    ) ->
    HoareStateMonad s pre a post

it's not much different, we just replaced Nat with a variable type s.

Unfortunately, the hardest part is still to come. We want to use a Hoare state monad as a monad, or sort-of a monad. Technically we won't be making a monad. A monad requires the rule m m a -> m a, but since our "m" has been decorated with pre- and postconditions, every "m" in that formula would be different. Doesn't really matter for us though, it's close enough.

We need to define a pure and a >>= (bind) function.

A pure function lifts a value to a monadic value, like making a list with a single element, doing a no-op, or, in the case of a regular state monad, leave the state unchanged and return the lifted value:

pure : a -> MyStateMonad a
pure val = MkMyStateMonad ((,) val)

So what should the pre- and postconditions be for pure? Since we're not using the state in any way, the precondition can just be Top. Anything goes.

We could also use Top as the postcondition, but that would lose some useful information. We know the input state is equal to the output state (Equal s1 s2), and the output value is equal to the lifted value. We can use a tuple as a conjunction to indicate to predicates must both hold. After all, we must be able to provide both values of a tuple to construct it.

With that, pure becomes:

pure : (a1 : a) -> HoareStateMonad s Top a (\s1, a2, s2 => (Equal s1 s2, Equal a1 a2))
pure a1 = MkHSMonad $ \s1 => MkPostS a1 s1

And now for the tricky bit, the bind operator.

For regular state monads, the bind operator chains the state-changing functions together:

(>>=) : MyStateMonad a -> (a -> MyStateMonad b) -> MyStateMonad b
(>>=) (MkMyStateMonad f1) act2 = MkMyStateMonad $ \s1 =>
  let
    (val1, s2) = f1 s1
    (MkMyStateMonad f2) act2 val1
  in
     f2 s2

So what we're really doing, is first executing action A, the executing action B, potentially using A's output. I will be using a notation from program algebra for clarity: A ; B means "first do A, then do B".

But, again, what should the pre- and postconditions be? Let's first look at the part of bind's type signature we do know:

(>>=) :  HoareStateMonad s p1 a q1
      -> ((x : a) -> HoareStateMonad s (p2 x) b (q2 x))
      -> HoareStateMonad s ?p3 b ?q3

Here, s is the state type, p1 is the precondition of action A, a is the return type of action A, q1 is the postcondition of action A, and x is the input to action B. p2 and q2 are a bit different than p1 and q1. They are applied not just over input state, return value and output state, but also over the input value x. Why? Consider the following function:

trySetState : (x : Nat) -> (s1 : Nat) -> (Bool, Nat)
trySetState x s1 =
  if (someCondition)
    then (True, x)
    else (False, s1)

The function sets the state based on some condition. This is a common pattern. A reasonable postcondition for trySetState would express that if the return type is True, then Equal x s2 is proven, and if it is False, then Equal s1 s2 is proven. Declaring this proposition requires using x as input.

As the example shows, it is useful to also consider inputs in the pre- and postconidtion for the second argument of bind.

Back to the bind operation. What is p3, the precondition of the "first A then B"? Since A executes first, p3 must contain p1. Furthermore, to satisfy p2, p3 must ensure that p2 holds after A has executed, so the postcondition q1 of A must imply the precondition p2 of B. Remember also that the type of p3 is s -> Type.

We define a function bind_pre that constructs a new precondition from p1, q1 and p2:

bind_pre
  :  {s : Type}
  -> {a : Type}
  -> (p1 : s -> Type)
  -> (q1 : s -> a -> s -> Type)
  -> (p2 : a -> s -> Type)
  -> s -> Type
bind_pre p1 q1 p2 s1 =
  ( p1 s1
  , {x : a} -> {s2 : s} -> q1 s1 x s2 -> p2 x s2
  )

This isn't easy, so let's go through it line by line:

bind_pre: the function name
: {s : Type}: the type declaration for an implicit argument. You can read this as "for any s that is a type"
-> {a : Type}: Read as "for any a that is a type"
-> (p1 : s -> Type): first argument to the function (not counting implicits). A predicate over s. The precondition of the first action.
-> (q1 : s -> a -> s -> Type): Postcondition of the first action
-> (p2 : a -> s -> Type): precondition of the second action. Based on the output of the first action.
-> s -> Type: The return type. Remember p3 must be s -> Type. Idris is curried to x -> s -> Type and x -> (s -> Type) are exactly the same thing.
bind_pre p1 q1 p2 s1 =: begin of function body. We give the arguments new names here, that is because the names in the type declaration are only valid within that type declaration. I used matching names for clarity.
( p1 s1: The result is a tuple, with as first value the regular precondition of the first action.
, {x : a} -> {s2 : s} -> q1 s1 x s2 -> p2 x s2: for any x of type a, and any s2 of type s, if we can prove q1 s1 x s2, then we must also be able to prove p2 x s2.

Well, that was hard enough, but the postcondition is worse. q1 and q2 are qualified on intermediate results. These intermediate values won't appear in the resulting monad's type declaration. We only know that they exist and that the postconditions hold for them. We're going to need a function for existential quantification:

exists : {p : _} -> (p -> Type) -> Type
exists f = {b : Type} -> ({a : _} -> f a -> b) -> b

What we did here, is reverse universal quantification to get existential qualification. {a : Type} -> a -> Type is a predicate that works for all as that are Types. Top is such a predicate. Conversely, we want to state that some a exists that satisfies a certain predicate. There is a duality here: if all you know is that something exists, you can only reason about it using predicates that work for all values. In programming, that means an existentially quantified ouput is mathematically the same as a universally quantified continuation. In other words: exists x. x is the same as forall y . (forall x . x -> y) -> y. The latter can be read as "you can prove any statement of type y so long as you can prove it using any statement of type x". Since we know nothing about y, only that it can be proven using any x, this tells us that some x must exist. The other way works too: if we know some x exists, we know that a y can be proven if it can be proven for any x.

Now finally we can get to the postcondition of A; B.

Remember that q1 and q2 are qualified over intermediate values, of which we only know they exist in the type signature. We therefore have:

bind_post
  :  {s : Type}
  -> {a : Type}
  -> {b : Type}
  -> (q1 : s -> a -> s -> Type)
  -> (q2 : a -> s -> b -> s -> Type)
  -> (s -> b -> s -> Type)
bind_post q1 q2 s1 y s3
  =  exists (\x => exists (\s2 => (q1 s1 x s2, q2 x s2 y s3)))

Which leaves the final declaration of bind, I'll explain it line-by-line later:

(>>=)  : {a : Type}
      -> {b : Type}
      -> {s : Type}
      -> {p1 : s -> Type}
      -> {q1 : s -> a -> s -> Type}
      -> {p2 : a -> s -> Type}
      -> {q2 : a -> s -> b -> s -> Type}
      -> HoareStateMonad s p1 a q1
      -> ((x : a) -> HoareStateMonad s (p2 x) b (q2 x))
      -> HoareStateMonad s (bind_pre p1 q1 p2) b (bind_post q1 q2)
(>>=) (MkHSMonad f1) act2 = MkHSMonad f
  where
    f :  ( s1 : s )
      -> { auto 0 pre3 : bind_pre p1 q1 p2 s1 }
      -> PostS b s (bind_post q1 q2 s1)
    f s1 {pre3} =
      let
        MkPostS v1 s2 {prf=post1} = f1 s1
        MkHSMonad f2 = act2 v1
        MkPostS v2 s3 {prf=post2} = f2{prf= (snd pre3) post1} s2
      in MkPostS v2 s3 {prf=(\e1 => (e1 $ \e2 => e2 (post1, post2)))}

{a : Type}: implicit argument. Read as "for all as that are types"
{b : Type}: for all bs that are types
{s : Type}: for all ss that are types
{p1 : s -> Type}: for all predicates p1 about an s (this is the type of our first precondition)
{q1 : s -> a -> s -> Type} for all predicates q1 about an s, a and another s (the type of our first postcondition)
{p2 : a -> s -> Type}: for all predicates p2 over a and s (second precondition, extra qualified over the input)
{q2 : a -> s -> b -> s -> Type}: second postcondition
HoareStateMonad s p1 a q1: the first argument, a HoareStateMonad about state s, with precondition p1, return value a, and postcondition q1.
((x : a) -> HoareStateMonad s (p2 x) b (q2 x)): the second argument, a function that takes an a (with value x), and yields a HoareStateMonad about state s, with precondition p2 x, returning a b, and with postcondition q2 x
HoareStateMonad s (bind_pre p1 q1 p2) b (bind_post q1 q2): results in a HoareStateMonad about state s, with precondition bind_pre p1 q1 p2, returning a value b, and with postcondition bind_post q1 q2

And for the function body:

(>>=) (MkHSMonad f1) act2 = MkHSMonad f: unwrapping and wrapping the state-changing functions in monad constructors. f is the new state-changing function we create as the sequence of our inputs.
f : ( s1 : s ): the first argument to the new function is the input state
-> { auto 0 pre3 : bind_pre p1 q1 p2 s1 }: we also require a proof that the combined preconditions hold
-> PostS b s (bind_post q1 q2 s1): and produce a value with suitable postconditions
f s1 {pre3} =: we note the precondition proof pre3 explicitely as we will need to use it manually in the function body.
MkPostS v1 s2 {prf=post1} = f1 s1: "Run" the first action with the input state. This will result in a return value v1, a new state s2 and an proof of the postcondition post1. Note that post1 still has multiplicity 0 so it will not exist at runtime.
MkHSMonad f2 = act2 v1: pass the return value of the first action, this will result in a new state-changing function f2, wrapped in a HoareStateMonad.
MkPostS v2 s3 {prf=post2} = f2{prf= (snd pre3) post1} s2: we "run" f2 with state s2, but must also prove its precondition. The precondition pre3 is ( p1 s1 , {x : a} -> {s2 : s} -> q1 s1 x s2 -> p2 x s2 ) The second argument is of interest here, and we have q1 s1 v1 s2 from post1, and so (snd pre3) post1 is proof of p2 v1 s2.
MkPostS v2 s3 {prf=(\e1 => (e1 $ \e2 => e2 (post1, post2)))}: we create a return value with postcondition, but must provide proof of our new postcondition. Recall existential types are continuations, and so we create a continuation as proof.

Next steps

I still have to use HoareStateMonads in practice. I planned to use them to reduce what mistakes can be made when writing a WebGL program. Those can be very tricky to debug. I fear HoareStateMonads require passing around proofs far too much to be useful in most cases. The extra programming work might not weigh up against the reduction of bugs. But perhaps Idris will be able to find many proofs by itself. Or perhaps I will need a different data type entirely.

Idris2+WebGL, part #16: Binding programs again

DrBearhands — Fri, 20 Aug 2021 14:27:08 +0000

It's time to take up the issue I've been avoiding since part 9. The compiler somehow needs to more-or-less know what program is bound in order to determine whether certain commands are correct. This sucks, because it means we have to keep track of state statically, which is traditionally hard to do. But let's first take a step back.

My initial idea was to use existential types to bind programs and uniform locations together. I realize now this was a bad idea. A quick recap.

given the (simplified) types:

export
data Program : ProgramID -> Type where
  ...

export
data UniformLocation : ProgramID -> Type where
  ...

We can define functions to work on a Program pid and UniformLocation pid, requiring that pid values are the same. There is a trick we can pull with this:

someFunction : forall a . (forall pid . Program pid -> UniformLocation pid -> a) -> a

because forall pid is part of the first argument, the first argument for someFunction must be a function able to handle any value of pid. Because of that, it cannot know anything about pid other than that it exists and it's the same between Program and UniformLocation. This way it's possible to tie specific variables together in their type.

The problem is that this is not the correct restriction.

When we call e.g. unifom2fv, the rule is that the passed location in the bound program must be for a 2-element array of floats. It's perfectly fine to have the same uniform locations for different programs. While that seems silly for individual uniforms, WebGL2 introduced uniform blocks, which can be shared between programs to improve performance.

Rather than typing programs with a phantom ID, I should type them by their attributes and uniforms. So long as they match our expectations, everything is fine, wherever we got a uniform location from.

The program type signature should therefore be something like:

public export
Attribute = (String, Int32, GLEnum) --name, size, type

public export
Uniform = (String, Int32, GLEnum) -- same

export
data Program : List Attribute -> List Uniform -> Type where
  ...

The real code is a bit more complicated, for instance to ensure only correct GLEnum values can be used, but that's the gist of it.

This still leaves the problem of keeping track of what program is in use, to which I have no nice solution.

When we call e.g. uniform2fv, we know the location and type of the passed variable, but not the program (not at compile time). This means we cannot compare the passed data to the inputs of the program, and a runtime type mismatch is possible. OpenGL4 allows for binding uniforms to specific programs, which circumvents the need of keeping track of used program. Unfortunately WebGL2 does not have these nice new functions. I could emulate them, but that's overhead I'm loathe to add.

So we're back to indexed state monads, hoare monads, and passing linear values around.

Consider the function to use a program:

useProgram : MonadState WebGL2.WebGLRenderingContext m =>
  (1 _ : WebGLProgram attributes uniforms) ->
  m (WebGLProgram attributes uniforms)

A naive approach is to add a phantom type to the program to denote if it was bound:

useProgram : MonadState WebGL2.WebGLRenderingContext m =>
  (1 _ : WebGLProgram  attributes uniforms NotInUse) ->
  m (WebGLProgram  attributes uniforms InUse)

(We could do something even fancier with dependent types that does not require changing our type definitions, but that's not particularly relevant here)

This would allow us to do something rather cool with erased implicit arguments:

uniform1fv : MonadState WebGL2.WebGLRenderingContext m =>
  WebGLUniformLocation uniformType ->
  {auto 0 prf : WebGLProgram attributes uniforms InUse} ->
  Float32Array ->
  m ()

which would check if a WebGLProgram that has been marked as InUse (by useProgam) exists at all in the current context.

The problem is that we can call useProgram twice, getting 2 programs that are InUse, even though only the last one actually is.

So, one way or another, useProgram must "consume" some form of program status when invoked.

What's even worse, I'm not trying to prevent the user from binding to non-existing inputs. That's actually fine, even useful when debugging, and can be ignored. The problem is not binding values that are used. So we also need to keep track of what inputs have been bound.

Because of that, I'm currently inclined to think some form of indexed monads are inevitable. I'm not very happy about that because it makes things a bit more complicated for the end-user. Indexed monads are not all that common after all.