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

Exadra37
As part of our continued goal of helping developers provide safer products for businesses and consumers, we here at McAfee Advanced Threa...
New
First poster: dwaynebradley
Maybe it’s just my experience, but Object-Oriented Programming seems like a default, most common paradigm of software engineering. The on...
New
First poster: bot
Last night I re-read this Steve Yegge article about learning to type as a programmer. I can touch type, but I don’t usually manage to bre...
New
First poster: AstonJ
:tada: Launching Fig I am excited to announce that, as of today, Fig is generally available to the public for download. With our public ...
New
OvermindDL1
Yet another rust-made text editor, though I’m really liking the looks of how this one works!
New
First poster: mindriot
LG 28-inch 16:18 DualUp Monitor with Ergo Stand and USB Type-C™ (28MQ780-B) | LG USA. Shop LG 28MQ780-B on the official LG.com website ...
New
First poster: bot
Hector Martin (@marcan@treehouse.systems). Attached: 1 image For those wondering why the hell we need all this safety system stuff for...
New
First poster: bot
When Zig is safer and faster than Rust. There are endless debates online about Rust vs. Zig, this post explores a side of the argument I...
New
First poster: bot
Declarative GNOME configuration with NixOS. I adore tinkering with my machine, trying new tools, extensions, themes, and ideas. When I w...
New
First poster: joeb
The new frameworks will continue until morale improves.
/js
New

Other popular topics Top

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
brentjanderson
Bought the Moonlander mechanical keyboard. Cherry Brown MX switches. Arms and wrists have been hurting enough that it’s time I did someth...
New
Exadra37
Oh just spent so much time on this to discover now that RancherOS is in end of life but Rancher is refusing to mark the Github repo as su...
New
PragmaticBookshelf
Learn different ways of writing concurrent code in Elixir and increase your application's performance, without sacrificing scalability or...
New
New
foxtrottwist
A few weeks ago I started using Warp a terminal written in rust. Though in it’s current state of development there are a few caveats (tab...
New
New
PragmaticBookshelf
Author Spotlight Rebecca Skinner @RebeccaSkinner Welcome to our latest author spotlight, where we sit down with Rebecca Skinner, auth...
New
AstonJ
If you want a quick and easy way to block any website on your Mac using Little Snitch simply… File > New Rule: And select Deny, O...
New
New