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
Neovim nightly, v0.5.0 and v0.4.4 has been released. Link: Release Nvim development (prerelease) build · neovim/neovim · GitHub Link:...
New
First poster: OvermindDL1
You can now buy a 100W USB-C cable with a built-in power meter. They’re just $20 on Amazon, and they work!
New
First poster: peterchancc
Why I like Clojure as a solo developer | Biff. Most of the reasons fall into a few categories: data orientation, the JVM, and the REPL.
New
CommunityNews
9 fintech engineering mistakes. Read this list unless you want to build a money dissappearing system
New
CommunityNews
Apple Patents Suggest Future AirPods Could Monitor Biosignals & Brain Activity - AppleMagazine. The US Patent & Trademark Office...
New
First poster: joni
My experience trying to write original, full-length human-sounding articles using Claude AI. You can use AI tools like Claude to help yo...
New
New
First poster: chris.johan
Skype’s days appear to be numbered, as a hidden string in the latest Skype for Windows preview suggests Microsoft will shutter the servic...
New
First poster: AstonJ
Truly independent web browser. Contribute to LadybirdBrowser/ladybird development by creating an account on GitHub.
New

Other popular topics Top

Devtalk
Hello Devtalk World! Please let us know a little about who you are and where you’re from :nerd_face:
New
DevotionGeo
I know that -t flag is used along with -i flag for getting an interactive shell. But I cannot digest what the man page for docker run com...
New
AstonJ
You might be thinking we should just ask who’s not using VSCode :joy: however there are some new additions in the space that might give V...
New
AstonJ
Inspired by this post from @Carter, which languages, frameworks or other tech or tools do you think is killing it right now? :upside_down...
New
AstonJ
Do the test and post your score :nerd_face: :keyboard: If possible, please add info such as the keyboard you’re using, the layout (Qw...
New
Exadra37
I am asking for any distro that only has the bare-bones to be able to get a shell in the server and then just install the packages as we ...
New
AstonJ
Biggest jackpot ever apparently! :upside_down_face: I don’t (usually) gamble/play the lottery, but working on a program to predict the...
New
New
sir.laksmana_wenk
I’m able to do the “artistic” part of game-development; character designing/modeling, music, environment modeling, etc. However, I don’t...
New
AstonJ
This is cool! DEEPSEEK-V3 ON M4 MAC: BLAZING FAST INFERENCE ON APPLE SILICON We just witnessed something incredible: the largest open-s...
New