Numerical representation is a technique for modelling datastructures after number systems. Typically, the method has been used to derive one-dimensional datastructures. This paper explores utilizing the technique for modelling two-dimensional datastructures instead, with insights into multi-dimensional ones. The aim of this paper is to devise datastructures for modelling block matrices. We look into the different derivations and highlight some roadblocks that would otherwise not be an issue in the one-dimensional case. The points under consideration include dimensional bias, ease of defining functions and proving properties about them as well as the difficulty of understanding the derived datastructure.
A type- and control-flow analysis is a program analysis that yields both type-flow information, approximating the types that may instantiate type variables, and control-flow information, approximating the values (especially λ - and -expressions) that may be bound to variables. Moreover, each of the flows informs the other; control-flow establishes the types that may instantiate -bound type variables by determining the -expressions that flow to a type-application expression, while type-flow filters control-flow by rejecting the flow of values having static types that are incompatible (according to the type-flow information) with the static type of the receiving variable. In previous work [1, 13, 14], we introduced a (monovariant) type- and control-flow analysis for System F (with recursion). While System F has an expressive type system and has served as a useful core calculus in which to express interesting language features, it only allows abstraction over types and does not allow abstraction over type constructors. Increasingly, researchers are looking at System F _ω , with both term- and type-level abstraction over types of arbitrary kind, as a core calculus in which to explore advanced language features. Hence, we are motivated to define a type- and control-flow analysis for System F _ω that is able to analyze the rich structure of System F _ω types. In this work, we present a preliminary type- and control-flow analysis for System F _ω (with recursion). As in previous work, we give both a specification-based formulation of the analysis, used to prove soundness of the analysis, and a flow-graph-based formulation, used to guide the implementation of an algorithm. While the macro structure of the development for System F _ω follows that for System F, moving to System F _ω introduces subtle challenges that have left some unanswered questions about the meta-theory. In particular, the decidability of type compatibility defined in terms of System F _ω ’s definitional type equivalence remains an open question. In order to be computable, our flow-graph-based formulation uses a restricted form of definitional type equivalence and performs a 0CFA at the type-level, yielding an analysis result that is less precise than the “best” (but as of yet, uncomputable) analysis result accepted by the specification-based formulation. Our soundness results have been formalized in the Coq proof assistant. This work is based in part on the first author’s MS thesis [53].
Implementing communication between edge devices and their server in IoT systems is often a tedious and bug-prone task, since different programming languages with distinct underlying paradigms need to cooperate. The mTask system prevents this semantic friction by providing a single task-oriented framework for the whole system. Shared data sources provide flexible communication between tasks running on the server and tasks running on edge devices, however the current implementation has some drawbacks. We introduce an improved version of these shares with a clearer semantics. To improve the communication between edge devices and the server, we introduce the possibility to start parametrized server tasks from the edge device.
Functional Programming—–what is it good for? Programming is the writing of programs. Judging from the papers and most books on functional programming, functional programming excels as a tool for writing short programs—–up to a hundred lines maybe. We also know that there are large functional code bases at large companies, and folklore has it that this also works quite well. Yet there is precious little literature on how to go from a hundred lines to a million lines of functional code. This hinders the adoption of functional program by newcomers, who ask questions like: Successful practitioners rely on folklore and experience for the answers to these questions, but precious little is written down in findable places and accessible formats. This paper is a call to action: The functional programming community needs to do a better job at outreach—find the gaps in our published knowledge, write down what is undocumented and talk to other communities who deal with large-scale software development.
