FISh(ID:3654/fis001)

for Functional = Imperative + Shape

FISh is a new array programming language that combines (and extends) the expressive power  of functional programming with the  efficient execution  of imperative, or procedural, programming by performing  static shape analysis  on all programs.

This shape computation reduces higher-order functional programs to simple imperative forms, i.e. F - Sh = I. Conversely, FISh works best when functions are constructed from imperative procedures and shape functions, as recommended by the slogan that gives the language its name.  Functional = Imperative + Shape  FISh execution speeds on typical array problems are several times faster than other higher-order, polymorphic languages.

People:
Structures:
References:
  • C B Jay "The FISh language definition" view details Abstract: FISh is a array-based programming language that combines imperative and functional programming styles. It supports a generous class of polymorphic, higher-order, array operations, such as mapping and folding (reduction) of arbitrary array functions, which are implemented using efficient array access. This report gives a formal definition of the types, terms and evaluation rules of the language, plus some additional guidance on implementation issues
  • C B Jay and P A Steckler "The Functional Imperative: Shape!" view details Abstract: FiSh is a new programming language for array computation that compiles its higher-order polymorphic programs into simple imperative programs, which can then be translated into, say, C. The resulting code is extremely fast: two orders of magnitude faster than Haskell, and two to four times faster than Objective CAML, one of the fastest ML variants for array programming. The compiler employs a partial evaluator which determines the shapes of all arrays, i.e. their size in each dimension, which are required for imperative storage allocation. In most functional languages, such sizes cannot be computed statically, since they are integers to be computed at run-time. FiSh is able to determine shapes by distinguishing sizes and integers in the type system.
  • C B Jay, D Clarke and J Edwards "Shape Analysis for Parallel Computing" view details Abstract: Shapes are also known as (data) structures, containers, or indexing systems. They are used extensively in parallel computing to determine communication strategies, load-balancing, evaluation strategies, etc. Although widely used, most applications of shape are ad hoc, and may occur either during compilation, optimisation or at run-time. A primary goal of shape theory is to organise these techniques under a single umbrella, supported by a simple semantics.

    This paper focuses on potential applications in parallel computing. Then I will present a schematic view of how we intend to exploit shape in a data-parallel language.
  • C B Jay "Costing parallel programs as a function of shapes" view details Abstract: Portable, efficient, parallel programming requires cost models to compare different possible implementations. In turn, these require knowledge of the shapes of the data structures being used, as well as knowledge of the hardware parameters. This paper shows how shape analysis techniques developed in the FISh programming language could be exploited to produce a data parallel language with an accurate, portable cost model.
  • C B Jay "A Semantics for Shape" view details Abstract: Shapely types separate data, represented by lists, from shape, or structure. This separation supports shape polymorphism, where operations are defined for arbitrary shapes, and shapely operations, for which the shape of the result is determined by that of the input, permitting static shape checking. The shapely types are closed under the formation of fixpoints, and hence include the usual algebraic types of lists, trees, etc. They also include other standard data structures such as arrays, graphs and records.
  • C B Jay "Separating Shape from Data" view details Abstract: Shape theory gives a precise categorical account of how data is stored within data structures, or shapes...
  • C B Jay and J Noble "Shaping object-oriented programs" view details Abstract: Object-oriented programming is valued for the clarity and maintainability of its programs. However, this success is mainly confined to small-scale phenomena, such as re-implementation of a single class: large-scale structures are as obscure and fragile as ever. We offer shape theory as a means of reasoning about program structure, and improving object-oriented design. In particular, shape analysis should improve debugging and compilation, and shape polymorphism should support greater re-use of programs, despite large-scale structural changes.
  • C B Jay and M Sekanina "Shape Checking of Array Programs" view details Abstract:
    Shape theory provides a framework for the study of data types in which shape and data can be manipulated separately. This paper is concerned with shape checking, i.e. the detection of shape errors, such as array bound errors, without handling the data. It can be seen as a form of partial evaluation in which data computations are ignored.

    We construct a simply-typed lambda-calculus that supports a vector type constructor, whose iteration yields types of arrays. It is expressive enough to construct all of the usual array operations. All shape errors in a term t can be detected by evaluating its shape #t which proceeds by first eliminating all the data, and then evaluating in the usual way. Evaluation of #t will terminate if that of t does.

  • C B Jay, E Moggi and G Belle "Functors, Types and Shapes" view details Abstract: Polytypic programming, as exemplified by PolyP, offers exciting new possibilities for generic programming, by supporting quantification over a class of functors. Shape polymorphic programming also supports functor quantification to obtain the same benefits, but arrived at from a different perspective. This position paper advocates the Functorial ML approach for both the immediate requirements of polytypism and the broader goals of generic programming.

    Resources