CommunityNews

CommunityNews

A Typed Programming Language

ABSTRACT

In the rank-polymorphic programming model, all functions operate on aggregate data of arbitrarily high rank, or number of dimensions. During function application, an argument array is split into cells, the individual components the function expects to consume. For example, an RGB-to- greyscale pixel transform operates on each vector in an arbitrarily large array. The aggregate structure surrounding the cells, called the frame, serves as the iteration space for cell-wise function application. The programming model was first developed by Iverson with the language APL [43], but it struggled with a barrier to efficient compilation: Loop nesting structure is derived from data computed at run time.

This dissertation presents the design and formal semantics of Remora, a higher-order, rank-polymorphic programming language with a static type system which identifies the shape of run-time data. This overview is followed by formal semantics for a core language. Remora’s static semantics ascribes to each expression a type which describes the shape of the resulting array. Quantification over the shape of cells and the type of atoms within an array is explicit, but the polymorphism over frames is entirely implicit. That is, a function’s type only describes its cell-level behavior, while implicit iteration—which is common to all functions—is identified by typing rules. A type-driven dynamic semantics determines the iteration space for functions applied to computed array data, and a type soundness theorem ensures that the types—and shapes—ascribed to expressions match those of their eventual results.

While frame polymorphism is instantiated implicitly in Remora’s formal semantics, explicitly instantiating cell polymorphism is a severe annotation burden. For example, a vector-mean function can be used on a 3ˆ5ˆ4 array with no explanation that the array is a 3ˆ5 frame, but the function must be explicitly instantiated to operate on vectors of length 4. That burden is alleviated by a bidirectional typing system which uses a novel constraint solver for the theory of array shapes to identify implicit dimension and shape arguments. The vector-mean function can then be applied directly to the 3 ˆ 5 ˆ 4 array, with bidirectional rules elaborating to code which explicitly instantiates it for 4-vector cells.

Two translation steps link Remora’s formal semantics to conventional rank-monomorphic languages with explicit iteration. While Remora’s dy- namic semantics relies heavily on run-time type information, a type era- sure pass can change from carrying full type information in dynamically created closures and arrays to describing argument and iteration-space shapes statically at sites. With that shape information at each call site, the program can be translated from using rank-polymorphic function calls to rank-monomorphic explicit iteration.

Read in full here:

This thread was posted by one of our members via one of our news source trackers.

Most Liked

OvermindDL1

OvermindDL1

I still find it better to define the shape of your data first then write functions to transform between them rather than have the machine try to infer it (like how V8 does)…

Where Next?

Popular General Dev topics Top

First poster: bot
FUZIX FUZIX is a fusion of various elements from the assorted UZI forks and branches beaten together into some kind of semi-coherent pla...
New
First poster: bot
Site Fingerprinting google.com Yes youtube.com Yes Amazon.com Yes Yahoo.com Yes Zoom.us No Facebook.com Yes Reddit.com Ye...
New
First poster: wolf4earth
It’s official. Your private communications can (and will) be spied on - European Digital Rights (EDRi). On 6 July, the European Parliame...
New
First poster: Maartz
This Keyboard Lets People Type So Fast It’s Banned From Typing Competitions. A new peripheral lets you keep typing without ever lifting ...
New
First poster: dpritchett
It’s not what programming languages do, it’s what they shepherd you to. How many of you have listened, read or taken part in a discussio...
New
First poster: bot
API Gateway Trends behind Features: Apache APISIX 3.0 vs. Kong 3.0 - API7.ai. By comparing the open-source API Gateway Apache APISIX and...
New
First poster: bot
openai-python/chatml.md at main · openai/openai-python. The OpenAI Python library provides convenient access to the OpenAI API from appl...
New
First poster: joeb
GitHub - crablang/crab: A community fork of a language named after a plant fungus. All of the memory-safe features you love, now with 100...
New
First poster: jkdiaz
Dark mode isn’t as good for your eyes as you believe. The shadowy display mode has leagues of fans claiming it helps reduce eye strain, ...
New
First poster: alvinkatojr
There are countless articles why developers should not focus on Frameworks too much and instead learn to understand the underlying langua...
New

Other popular topics Top

Devtalk
Reading something? Working on something? Planning something? Changing jobs even!? If you’re up for sharing, please let us know what you’...
1033 17470 383
New
wolf4earth
@AstonJ prompted me to open this topic after I mentioned in the lockdown thread how I started to do a lot more for my fitness. https://f...
New
DevotionGeo
I know that these benchmarks might not be the exact picture of real-world scenario, but still I expect a Rust web framework performing a ...
New
axelson
I’ve been really enjoying obsidian.md: It is very snappy (even though it is based on Electron). I love that it is all local by defaul...
New
dimitarvp
Small essay with thoughts on macOS vs. Linux: I know @Exadra37 is just waiting around the corner to scream at me “I TOLD YOU SO!!!” but I...
New
mafinar
This is going to be a long an frequently posted thread. While talking to a friend of mine who has taken data structure and algorithm cou...
New
AstonJ
If you get Can't find emacs in your PATH when trying to install Doom Emacs on your Mac you… just… need to install Emacs first! :lol: bre...
New
New
CommunityNews
A Brief Review of the Minisforum V3 AMD Tablet. Update: I have created an awesome-minisforum-v3 GitHub repository to list information fo...
New
AnfaengerAlex
Hello, I’m a beginner in Android development and I’m facing an issue with my project setup. In my build.gradle.kts file, I have the foll...
New