OS of Interest: Hubris

 Hubris is a fledgling operations system by Oxide Computer Computer.  They are developing it de novo (as Bryan Cantrill would say, and probably has) for use in the control systems of their new server hardware.  It's an embedded OS suitable for MCU's with memory protection hardware.  To quote Bryan:

When we started Oxide, we knew we were going to take a fresh look at the entire system. We knew, for example, that we wanted to have a true hardware root of trust and that we wanted to revisit the traditional BMC. We knew, too, that we would have our own system software on each of these embedded systems, and assumed that we would use an existing open source operating system as a foundation. However, as we waded deeper into these embedded systems and especially their constraints of security and robustness we found that what we wanted out of the existing operating systems wasn't necessarily what they offered (or even wanted to offer).

Cliff Biffle seems to be the chief designer.

Electronics of Interest: LPC55S69 MCU with Transform Engine allowing for co-processor FFTs

 The NXP LPC55S69 includes a PowerQuad" feature that can be used to accelerate DSP functions, including FFTs

A variant of this chip is used in Great Scott Gadget's HackRF SDR, though apparently that uses a number of other chips to do signal processing work. 

Website of Interest: List of Foundational Haskell Papers

Description / Disclaimer: 

This repo is a collection of links to various papers, and as such, may go out of date intermittently as resources shuffle around the web. It would be greatly appreciated if people raise issues when these pdf's have dead links, as it helps us all maintain the most up to date set of resources. Additionally, you may find that the "set of links" approach is tedious. This is done to avoid any sort of licensing concerns. If anyone has a better idea of the implications (especially licensing) of hosting the actual papers, the end goal would ideally be to serve as a kind of library. Feel free to find me to discuss. Thanks, Emily. (Pillmore)

List of Haskell Papers

Person of Interest: Alexis King

Alexis King

About:
My name is Alexis King, and I write a lot of software. I live in Chicago.

I’m interested in functional programming, static types, and programming language research, and I try to spend as much time as I can writing Haskell and Racket. I mostly work on web applications and infrastructure, but I’m especially passionate about writing libraries, open-source software, and various kinds of tooling.

I write about some of the things I do on this blog, and I sometimes tweet about them and other things on Twitter. I work on a lot of open-source projects on GitHub, and you can email me at lexi.lambda@gmail.com.

Person of Interest: Chris Olah

Chris Olah

About

A wandering machine learning researcher, bouncing between groups. I want to understand things clearly, and explain them well

Programming Language of Interest: Idris

Idris

Overview

Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML, and include:

• Full dependent types with dependent pattern matching
• Simple foreign function interface (to C)
• Compiler-supported interactive editing: the compiler helps you write code using the types
• where clauses, with rule, simple case expressions, pattern matching let and lambda bindings
• Dependent records with projection and update
• Interfaces (similar to type classes in Haskell)
• Type-driven overloading resolution
• do notation and idiom brackets
• Indentation significant syntax
• Extensible syntax
• Cumulative universes
• Totality checking
• Hugs style interactive environment

Person of Interest: Edwin Brady

Edwin Brady

About

I am a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and domain specific languages (DSLs). I am currently working on the implementation of DSLs for stateful, resource-aware programming, especially for correct network protocol design and implementation, using Idris, a dependently typed functional programming language.

When I’m not doing that, you might find me playing Go (I’m about 1 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train.

I’m afraid I also perpetrated the whitespace programming language.

Manuscript of Interest: Write You a Haskell

Write You a Haskell
Building a modern functional compiler from first principles.

Author: Stephen Diehl

Abstract:
In 2014 I wrote a short tutorial about building a small imperative language in Haskell that compiled into LLVM. I was extremely happy with the effect the tutorial seemed to have, and the warm response I got from so many people was very encouraging.

I've done a great bit of thinking about what the most impactful topic I could write about in 2015 could be; and decided throughout this year I will follow up with a large endeavor for another project-based tutorial on building a simple functional programming language from first principles.

This is a nontrivial topic and is unfortunately very much underserved, the knowledge to build such a modern functional language is not widely disseminated among many programmers. The available resources most often discuss language theory in depth while completely glossing over the engineering details. I wished to write a project-based tutorial that included the engineering details and left the reader with a fully functional toy language at the end that could be extended for further projects.

We will build a small functional language called Fun which is a partial Haskell 2010 toy language; complete with a parser, type inference, datatypes, pattern matching, desugaring, typeclasses, higher-kinded types, monadic IO, arbitrary-rank polymorphism, records, Core language, STG intermediate language, lazy evaluation, interpreter, native code generator, a runtime, and several optimization passes.

As with most of my writing, this is the pre-edited rough cut version, which I will refine over time.

Project of Interest: Aweigh (Offline Navigation System)

Aweigh

Aweigh is an open navigation system that does not rely on satellites: it is inspired by the mapping of celestial bodies and the polarized vision of insects. Ancient seafarers and desert ants alike use universally accessible skylight to organize, orient, and place themselves in the world. Aweigh is a project that learns from the past and from the microscopic to re-position individuals in the contemporary technological landscape. 

Networked technolgies that we increasingly rely on undergo changes that are often beyond our control. Most smartphone users require government-run satellites to get around day by day, while consequences of Brexit are calling into question the UK’s access to the EU’s new satellite system, Project Galileo. Aweigh is a set of tools and blueprints that aims to open modern technologies to means of democratization, dissemination, and self-determination.

These tools were designed to depend only on publicly available materials and resources: digital fabrication machines, open-source code, packaged instructions, and universally accessible sky light. Aweigh is inspired by ancient navigation devices that use the process of taking angular measurements between the earth and various celestial bodies as reference points to find one’s position. Combining this process with the polarization of sunlight observed in insect eyes, the group developed a technology that calculates longitude and latitude in urban as well as off-grid areas. 

All of Aweigh’s development resources are made public via free online distribution, in conjunction with a downloadable manual, schematics for a custom PCB, templates, and several device variations. These variations provide multiple methods of implementation at each step of construction for a spectrum of user skill levels. Aweigh is a project that shows a future where individuals have a voice in the power structures driving their technologies.

Paper of Interest:

Paper of Interest: "Seven Sketches in Compositionality: An Invitation to Applied Category Theory"

Authors: Brendan Fong, David I. Spivak

The purpose of this book is to offer a self-contained tour of applied category theory. It is an invitation to discover advanced topics in category theory through concrete real-world examples. Rather than try to give a comprehensive treatment of these topics—which include adjoint functors, enriched categories, proarrow equipments, toposes, and much more—we merely provide a taste. We want to give readers some insight into how it feels to work with these structures as well as some ideas about how they might show up in practice. The audience for this book is quite diverse: anyone who finds the above description intriguing. This could include a motivated high school student who hasn’t seen calculus yet but has loved reading a weird book on mathematical logic they found at the library. Or a machine learning researcher who wants to understand what vector spaces, design theory, and dynamical systems could possibly have in common. Or a pure mathematician who wants to imagine what sorts of applications their work might have. Or a recently-retired programmer who’s always had an eerie feeling that category theory is what they’ve been looking for to tie it all together, but who’s found the usual books on the subject impenetrable.

Paper of Interest: Asymptotically Efficient Quantum Karatsuba Multiplication

Asymptotically Efficient Quantum Karatsuba Multiplication

Craig Gidney

(Submitted on 15 Apr 2019)

We improve the space complexity of Karatsuba multiplication on a quantum computer from O(n1.427) to O(n) while maintaining O(nlg3) gate complexity. We achieve this by ensuring recursive calls can add their outputs directly into subsections of the output register. This avoids the need to store, and uncompute, intermediate results. This optimization, which is analogous to classical tail-call optimization, should be applicable to a wide range of recursive quantum algorithms.

Explanatory Article:

A New Approach to Multiplication Opens the Door to Better Quantum Computers

Book of Interest: Structure and Interpretation of Classical Mechanics

Structure and Interpretation of Classical Mechanics


From Chapter 1:

The subject of this book is motion and the mathematical tools used to describe it.

Centuries of careful observations of the motions of the planets revealed regularities in those motions, allowing accurate predictions of phenomena such as eclipses and conjunctions. The effort to formulate these regularities and ultimately to understand them led to the development of mathematics and to the discovery that mathematics could be effectively used to describe aspects of the physical world. That mathematics can be used to describe natural phenomena is a remarkable fact.

Classical mechanics describes the motion of a system of particles, subject to forces describing their interactions. Complex physical objects, such as juggling pins, can be modeled as myriad particles with fixed spatial relationships maintained by stiff forces of interaction.

The motion of a system can be described by giving the position of every piece of the system at each moment. Such a description of the motion of the system is called a configuration path; the configuration path specifies the configuration as a function of time. The juggling pin rotates as it flies through the air; the configuration of the juggling pin is specified by giving the position and orientation of the pin. The motion of the juggling pin is specified by giving the position and orientation of the pin as a function of time.

The path-distinguishing function that we seek takes a configuration path as an input and produces some output. We want this function to have some characteristic behavior when its input is a realizable path. For example, the output could be a number, and we could try to arrange that this number be zero only on realizable paths. Newton’s equations of motion are of this form; at each moment Newton’s differential equations must be satisfied.

However, there is an alternate strategy that provides more insight and power: we could look for a path-distinguishing function that has a minimum on the realizable paths—on nearby unrealizable paths the value of the function is higher than it is on the realizable path. This is the variational strategy: for each physical system we invent a path-distinguishing function that distinguishes realizable motions of the system by having a stationary point for each realizable path.1 For a great variety of systems realizable motions of the system can be formulated in terms of a variational principle.2

Mechanics, as invented by Newton and others of his era, describes the motion of a system in terms of the positions, velocities, and accelerations of each of the particles in the system. In contrast to the Newtonian formulation of mechanics, the variational formulation of mechanics describes the motion of a system in terms of aggregate quantities that are associated with the motion of the system as a whole.

Paper of Interest: QuaterNet: A Quaternion-based Recurrent Model for Human Motion

QuaterNet: A Quaternion-based Recurrent Model for Human Motion

Dario Pavllo, David Grangier, Michael Auli

(Submitted on 16 May 2018 (v1), last revised 31 Jul 2018 (this version, v2))

Deep learning for predicting or generating 3D human pose sequences is an active research area. Previous work regresses either joint rotations or joint positions. The former strategy is prone to error accumulation along the kinematic chain, as well as discontinuities when using Euler angle or exponential map parameterizations. The latter requires re-projection onto skeleton constraints to avoid bone stretching and invalid configurations. This work addresses both limitations. Our recurrent network, QuaterNet, represents rotations with quaternions and our loss function performs forward kinematics on a skeleton to penalize absolute position errors instead of angle errors. On short-term predictions, QuaterNet improves the state-of-the-art quantitatively. For long-term generation, our approach is qualitatively judged as realistic as recent neural strategies from the graphics literature

Implementation