Programmers make assumptions about the order of memory operations, which are not captured in the operations' types and therefore cannot be enforced statically by a compiler. This can lead programmers to accidental...
详细信息
ISBN:
(纸本)9781450386159
Programmers make assumptions about the order of memory operations, which are not captured in the operations' types and therefore cannot be enforced statically by a compiler. This can lead programmers to accidentally violate those assumptions if they are not careful. To address this issue, we encode the memory locations that are accessed by a given computation using a graded monad. We use the data flow dependencies which arise from this to construct a type-level graph that we analyse to automatically order the computations so that no dependencies are violated. This also allows for computations which have no dependencies on each other to be run concurrently.
AspectAG is a domain specific language embedded in Haskell to represent modular attribute grammars. In AspectAG attribute grammar fragments can be defined independently (even in separate modules) and then combined in ...
详细信息
ISBN:
(纸本)9781450375627
AspectAG is a domain specific language embedded in Haskell to represent modular attribute grammars. In AspectAG attribute grammar fragments can be defined independently (even in separate modules) and then combined in a safe way. This flexibility is achieved through the use of extensible records, which are implemented using type-level programming ***-levelprogramming support has remarkably evolved in Haskell since the first version of AspectAG was designed; having incorporated new features like data promotion and kind polymorphism, among others, which allows to program in a "strongly typed" way at the level of types in a similar way as when programming at the level of *** this paper we redefine AspectAG applying the new type-level programming techniques. As a consequence, we obtain a more robust system with better error messages.
type family applications in Haskell must be fully saturated. This means that all type-level functions have to be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension to ...
详细信息
type family applications in Haskell must be fully saturated. This means that all type-level functions have to be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension to GHC that removes this restriction. We augment Haskell's existing type arrow, ->, with an unmatchable arrow, ->, that supports partial application of type families without compromising soundness. A soundness proof is provided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) in the type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.
Logic programming allows structuring code in terms of predicates or relations, rather than functions. Although logic programming languages present advantages in terms of declarativeness and conciseness, the introducti...
详细信息
Logic programming allows structuring code in terms of predicates or relations, rather than functions. Although logic programming languages present advantages in terms of declarativeness and conciseness, the introduction of static types has not become part of most popular logic programming languages, increasing the difficulty of testing and debugging of logic programming code. This paper demonstrates how to implement logic programming in Haskell, thus empowering logic programs with types, and functional programs with relations or predicates. We do so by combining threeideas. First, we use extensible types to generalize a type by a parameter type function. Second, we use a sum type as an argument to introduce optional variables in extensible types. Third, we implement a unification algorithm capable of working with any data structure, provided that certain operations are implemented for the given type. We demonstrate our proposal via a series of increasingly complex examples inspired by educational texts in logic programming, and leverage the host language's features to make new notation convenient for users, showing that the proposed approach is not just technically possible but also practical.
This paper presents TensorSafe, a Haskell library that makes possible the definition and structural validation of deep neural network architectures. Nowadays, the development process of deep learning models has been n...
详细信息
This paper presents TensorSafe, a Haskell library that makes possible the definition and structural validation of deep neural network architectures. Nowadays, the development process of deep learning models has been notably simplified due to the availability of sophisticated tools in the industry. However, most of these tools do not provide any security controls at compilation time, making the developers deal with unexpected run-time errors and uncertainties. In particular, validating the structure of deep neural networks at compilation time is a complex subject that involves the mathematical validation of all operations that a deep learning model will perform. Moreover, this structural checking requires an advanced usage of types systems theories to manipulate abstract type definitions capable of modeling neural network constructions. Many different programming techniques were involved in the specification of TensorSafe. Primarily, the application of the functional programming paradigm and the use of type-level programming were of great importance for the development process and to probe the correctness of the neural network models. The experimental evaluation showed that by using TensorSafe it is possible to correctly create well-known deep neural network architectures, such as AlexNet or ResNet50.
Generating good random values described by algebraic data types is often quite intricate. State-of-the-art tools for synthesizing random generators serve the valuable purpose of helping with this task, while providing...
详细信息
ISBN:
(纸本)9781450375627
Generating good random values described by algebraic data types is often quite intricate. State-of-the-art tools for synthesizing random generators serve the valuable purpose of helping with this task, while providing different levels of invariants imposed over the generated values. However, they are often not built for composability nor extensibility, a useful feature when the shape of our random data needs to be adapted while testing different properties or *** this work, we develop an extensible framework for deriving compositional generators, which can be easily combined in different ways in order to fit developers' demands using a simple type-level description language. Our framework relies on familiar ideas from the à la Carte technique for writing composable interpreters in Haskell. In particular, we adapt this technique with the machinery required in the scope of random generation, showing how concepts like generation frequency or terminal constructions can also be expressed in the same type-level fashion. We provide an implementation of our ideas, and evaluate its performance using real-world examples.
Generating good random values described by algebraic data types is often quite intricate. State-of-the-art tools for synthesizing random generators serve the valuable purpose of helping with this task, while providing...
详细信息
ISBN:
(纸本)9781450375627
Generating good random values described by algebraic data types is often quite intricate. State-of-the-art tools for synthesizing random generators serve the valuable purpose of helping with this task, while providing different levels of invariants imposed over the generated values. However, they are often not built for composability nor extensibility, a useful feature when the shape of our random data needs to be adapted while testing different properties or sub-systems. In this work, we develop an extensible framework for deriving compositional generators, which can be easily combined in different ways in order to fit developers' demands using a simple typelevel description language. Our framework relies on familiar ideas from the a la Carte technique for writing composable interpreters in Haskell. In particular, we adapt this technique with the machinery required in the scope of random generation, showing how concepts like generation frequency or terminal constructions can also be expressed in the same type-level fashion. We provide an implementation of our ideas, and evaluate its performance using realworld examples.
Haskell, as implemented by the Glasgow Haskell Compiler (GHC), allows expressive type-level programming. The most popular typelevelprogramming extension is typeFamilies, which allows users to write functions on types...
详细信息
Haskell, as implemented by the Glasgow Haskell Compiler (GHC), allows expressive type-level programming. The most popular typelevelprogramming extension is typeFamilies, which allows users to write functions on types. Yet, using type functions can cripple type inference in certain situations. In particular, lack of injectivity in type functions means that GHC can never infer an instantiation of a type variable appearing only under type functions. In this paper, we describe a small modification to GHC that allows type functions to be annotated as injective. GHC naturally must check validity of the injectivity annotations. The algorithm to do so is surprisingly subtle. We prove soundness for a simplification of our algorithm, and state and prove a completeness property, though the algorithm is not fully complete. As much of our reasoning surrounds functions defined by a simple pattern-matching structure, we believe our results extend beyond just Haskell. We have implemented our solution on a branch of GHC and plan to make it available to regular users with the next stable release of the compiler.
Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiv...
详细信息
Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including case expressions, anonymous functions, partially-applied functions, and let expressions. In this paper, we present an algorithm with a proof of correctness - to encode these term-level constructs at the typelevel. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement. We believe that delineating the mismatch between GHC's term level and its typelevel is a key step toward supporting dependently typed programming. We have implemented our approach as part of the singletons package, available online.
Monads provide a greatly useful capability to pure languages in simulating side-effects, but implementations such as the Monad Transformer Library [1] in Haskell prohibit reuse of those side-effects such as threading ...
详细信息
ISBN:
(纸本)9783642229404
Monads provide a greatly useful capability to pure languages in simulating side-effects, but implementations such as the Monad Transformer Library [1] in Haskell prohibit reuse of those side-effects such as threading through two different states without some explicit work-around. Monad Factory provides a straightforward solution for opening the non-proper morphisms by indexing monads at both the type-level and term-level, allowing 'copies' of the monads to be created and simultaneously used within even the same monadic transformer stack. This expands monads' applicability and mitigates the amount of boilerplate code we need for monads to work together, and yet we use them nearly identically to non-indexed monads.
暂无评论