scholarly journals Oblivious algebraic data types

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-29
Author(s):  
Qianchuan Ye ◽  
Benjamin Delaware

Secure computation allows multiple parties to compute joint functions over private data without leaking any sensitive data, typically using powerful cryptographic techniques. Writing secure applications using these techniques directly can be challenging, resulting in the development of several programming languages and compilers that aim to make secure computation accessible. Unfortunately, many of these languages either lack or have limited support for rich recursive data structures, like trees. In this paper, we propose a novel representation of structured data types, which we call oblivious algebraic data types, and a language for writing secure computations using them. This language combines dependent types with constructs for oblivious computation, and provides a security-type system which ensures that adversaries can learn nothing more than the result of a computation. Using this language, authors can write a single function over private data, and then easily build an equivalent secure computation according to a desired public view of their data.

1995 ◽  
Vol 5 (1) ◽  
pp. 81-110 ◽  
Author(s):  
Peter Achten ◽  
Rinus Plasmeijer

AbstractFunctional programming languages have banned assignment because of its undesirable properties. The reward of this rigorous decision is that functional programming languages are side-effect free. There is another side to the coin: because assignment plays a crucial role in Input/Output (I/O), functional languages have a hard time dealing with I/O. Functional programming languages have therefore often been stigmatised as inferior to imperative programming languages because they cannot deal with I/O very well. In this paper, we show that I/O can be incorporated in a functional programming language without loss of any of the generally accepted advantages of functional programming languages. This discussion is supported by an extensive account of the I/O system offered by the lazy, purely functional programming language Clean. Two aspects that are paramount in its I/O system make the approach novel with respect to other approaches. These aspects are the technique of explicit multiple environment passing, and the Event I/O framework to program Graphical User I/O in a highly structured and high-level way. Clean file I/O is as powerful and flexible as it is in common imperative languages (one can read, write, and seek directly in a file). Clean Event I/O provides programmers with a high-level framework to specify complex Graphical User I/O. It has been used to write applications such as a window-based text editor, an object based drawing program, a relational database, and a spreadsheet program. These graphical interactive programs are completely machine independent, but still obey the look-and-feel of the concrete window environment being used. The specifications are completely functional and make extensive use of uniqueness typing, higher-order functions, and algebraic data types. Efficient implementations are present on the Macintosh, Sun (X Windows under Open Look) and PC (OS/2).


1996 ◽  
Vol 3 (56) ◽  
Author(s):  
Zine-El-Abidine Benaissa ◽  
Pierre Lescanne ◽  
Kristoffer H. Rose

<p>We present the lambda sigma^a_w calculus, a formal synthesis of the concepts of<br />sharing and explicit substitution for weak reduction. We show how<br />lambda sigma^a_w can be used as a foundation of implementations of functional<br />programming languages by modelling the essential ingredients of such<br />implementations, namely weak reduction strategies, recursion, space<br />leaks, recursive data structures, and parallel evaluation, in a uniform way.<br />First, we give a precise account of the major reduction strategies<br />used in functional programming and the consequences of choosing <br /> lambda-graph-reduction vs. environment-based evaluation. Second, we show<br />how to add constructors and explicit recursion to give a precise account<br />of recursive functions and data structures even with respect to<br />space complexity. Third, we formalize the notion of space leaks in lambda sigma^a_w<br />and use this to define a space leak free calculus; this suggests optimisations<br />for call-by-need reduction that prevent space leaking and enables<br />us to prove that the "trimming" performed by the STG machine does<br />not leak space.<br />In summary we give a formal account of several implementation<br />techniques used by state of the art implementations of functional programming<br />languages.</p><p>Keywords. Implementation of functional programming, lambda<br />calculus, weak reduction, explicit substitution, sharing, recursion, space<br />leaks.</p>


1993 ◽  
Vol 3 (2) ◽  
pp. 171-190 ◽  
Author(s):  
F. Warren Burton ◽  
Robert D Cameron

AbstractPattern matching in modern functional programming languages is tied to the representation of data. Unfortunately, this is incompatible with the philosophy of abstract data types.Two proposals have been made to generalize pattern matching to a broader class of types. The laws mechanism of Miranda allows pattern matching with non-free algebraic data types. More recently, Wadler proposed the concept of views as a more general solution, making it possible to define arbitrary mappings between a physical implementation and a view supporting pattern matching. Originally, it was intended to include views in the new standard lazy functional programming language Haskell.Laws and views each offer important advantages, particularly with respect to data abstraction. However, if not used with great care, they also introduce serious problems in equational reasoning. As a result, laws have been removed from Miranda and views were not included in the final version of Haskell.We propose a third approach which unifies the laws and views mechanisms while avoiding their problems. Philosophically, we view pattern matching as a bundling of case recognition and component selection functions instead of a method for inverting data construction. This can be achieved by removing the implied equivalence between data constructors and pattern constructors. In practice, we allow automatic mapping into a view but not out of the view. We show that equational reasoning can still be used with the resulting system. In fact, equational reasoning is easier, since there are fewer hidden traps.


1996 ◽  
Vol 6 (3) ◽  
pp. 485-518 ◽  
Author(s):  
Konstantin Läufer

AbstractWe argue that the novel combination of type classes and existential types in a single language yields significant expressive power. We explore this combination in the context of higher-order functional languages with static typing, parametric polymorphism, algebraic data types and Hindley–Milner type inference. Adding existential types to an existing functional language that already features type classes requires only a minor syntactic extension. We first demonstrate how to provide existential quantification over type classes by extending the syntax of algebraic data type definitions, and give examples of possible uses. We then develop a type system and a type inference algorithm for the resulting language. Finally, we present a formal semantics by translation to an implicitly-typed second-order λ-calculus and show that the type system is semantically sound. Our extension has been implemented in the Chalmers Haskell B. system, and all examples from this paper have been developed using this system.


2008 ◽  
Vol 18 (5-6) ◽  
pp. 567-598 ◽  
Author(s):  
BJÖRN BRINGERT ◽  
AARNE RANTA

AbstractThis paper introduces a pattern for almost compositional functions over recursive data types, and over families of mutually recursive data types. Here “almost compositional” means that for all of the constructors in the type(s), except a limited number of them, the result of the function depends only on the constructor and the results of calling the function on the constructor's arguments. The pattern consists of a generic part constructed once for each data type or family of data types, and a task-specific part. The generic part contains the code for the predictable compositional cases, leaving the interesting work to the task-specific part. Examples of the pattern are given, implemented in dependent type theory with inductive families, in Haskell with generalized algebraic data types and rank-2 polymorphism, and in Java using a variant of the Visitor design pattern. The relationships to the “Scrap Your Boilerplate” approach to generic programming, and to general tree types in dependent type theory, are investigated by reimplementing our operations using those frameworks.


2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-32
Author(s):  
Vikraman Choudhury ◽  
Jacek Karwowski ◽  
Amr Sabry

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections. Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.


2021 ◽  
Vol 4 ◽  
pp. 72-77
Author(s):  
Volodymyr Protsenko

When creating a programming language, it is necessary to determine its syntax and semantics. The main task of syntax is to describe all constructions that are elements of the language. For this purpose, a specific syntax highlights syntactically correct sequences of characters of the language alphabet. Most often it is a finite set of rules that generate an infinite set of all construction languages, such as the extended Backus-Naur (BNF) form.To describe the semantics of the language, the preference is given to the abstract syntax, which in real programming languages is shorter and more obvious than specific. The relationship between abstract syntax objects and the syntax of the program in compilers solves the parsing phase.Denotational semantics is used to describe semantics. Initially, it records the denotations of the simplest syntactic objects. Then, with each compound syntactic construction, a semantic function is associated, which by denotations of components of a design calculates its value – denotation. Since the program is a specific syntactic construction, its denotation is possible to determine using the appropriate semantic function. Note that the program itself is not executed when calculating its denotation.The denotative description of a programming language includes the abstract syntax of its constructions, denotations – the meanings of constructions and semantic functions that reflect elements of abstract syntax (language constructions) in their denotations (meanings).The use of the functional programming language Haskell as a metalanguage is considered. The Haskell type system is a good tool for constructing abstract syntax. The various possibilities for describing pure functions, which are often the denotations of programming language constructs, are the basis for the effective use of Haskell to describe denotational semantics.The paper provides a formal specification of a simple imperative programming language with integer data, block structure, and the traditional set of operators: assignment, input, output, loop and conditional. The ability of Haskell to effectively implement parsing, which solves the problem of linking a particular syntax with the abstract, allows to expand the formal specification of the language to its implementation: a pure function — the interpreter.The work contains all the functions and data types that make up the interpreter of a simple imperative programming language.


Author(s):  
David J. Lobina

Recursion, or the capacity of ‘self-reference’, has played a central role within mathematical approaches to understanding the nature of computation, from the general recursive functions of Alonzo Church to the partial recursive functions of Stephen C. Kleene and the production systems of Emil Post. Recursion has also played a significant role in the analysis and running of certain computational processes within computer science (viz., those with self-calls and deferred operations). Yet the relationship between the mathematical and computer versions of recursion is subtle and intricate. A recursively specified algorithm, for example, may well proceed iteratively if time and space constraints permit; but the nature of specific data structures—viz., recursive data structures—will also return a recursive solution as the most optimal process. In other words, the correspondence between recursive structures and recursive processes is not automatic; it needs to be demonstrated on a case-by-case basis.


Sign in / Sign up

Export Citation Format

Share Document