114 research outputs found
Aspect−Oriented Programming with Type Classes
No full textWe consider the problem of adding aspects to a strongly typed language which supports type classes. We show that type classes as supported by the Glasgow Haskell Compiler can model an AOP style of programming via a simple syntax-directed transformation scheme where AOP programming idioms are mapped to type classes. The drawback of this approach is that we cannot easily advise functions in programs which carry type annotations. We sketch a more principled approach which is free of such problems by combining ideas from intentional type analysis with advanced overloading resolution strategies. Our results show that type-directed static weaving is closely related to type class resolution -- the process of typing and translating type class programs
Translating Generalized Algebraic Data Types to System F
No full textGeneralized algebraic data types (GADTs) extend ordinary
algebraic data types by refining the types of constructors with syntactic
equality constraints. This is highly useful and allows for novel applications
such as strongly-typed evaluators, typed LR parsing etc. To translate
GADTs we need to enrich the System F style typed intermediate
languages of modern language implementations to capture these equality
constraints. We show that GADTs can be translated to a minor extension
of System F where type equality proofs are compiled into System
F typable proof terms. At run-time proof terms evaluate to the identity.
Hence, they can be safely erased before execution of the program. We
provide evidence that our approach scales to deal with extensions where
equality is not anymore syntactic. The benefit of our method is that type
checking of target programs remains as simple as type checking in System
F. Thus, we can offer a light-weight approach to integrate GADTs
and extensions of it into existing implementations
Modular Generic Programming with Extensible Superclasses
No full text"Generics for the Masses" (GM) and "Scrap your Boilerplate" (SYB) are generic programming approaches based on some inenious applications of Haskell type classes. To achieve modularity, the GM and SYB approach have been extended by using some experimental language extensions such as abstraction over type classes and recursive instances. Hence, the type class encodings behind the GM and SYB approach become less practical and harder to understand.We show that none of these type class features are necessary if we use the single feature of extensible superclasses, the complement of subclass extension. We formalize type classes with extensible superclasses as the combination of a previously introduced type-passing translation scheme and a general type class framework. Our results shed some new light on the use of type classes to support generic programming
Foundations for structured programming with GADTs
No full textGADTs are at the cutting edge of functional programming and become more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of data types as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derive an initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools — analogous to the well-known and widely-used ones for algebraic and nested data types — for reasoning about, programming with, and improving the performance of programs involving, GADTs; we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can be derive
A functional perspective on machine learning via programmable induction and abduction
No full textWe present a programming language for machine learning based on the concepts of ‘induction’ and ‘abduction’ as encountered in Peirce’s logic of science. We consider the desirable features such a language must have, and we identify the ‘abductive decoupling’ of parameters as a key general enabler of these features. Both an idealised abductive calculus and its implementation as a PPX extension of OCaml are presented, along with several simple examples
Extracting programs from type class proofs
No full textPPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming200697-10
Special issue on FLOPS 2018
No full textSpecial Issue containing selected papers from the 14th International Symposium on Functional and Logic Programming (FLOPS 2018)
Functional and Logic Programming:14th International Symposium (FLOPS 2018), Nagoya, Japan, May 9-11, 2018
No full textThis volume contains the proceedings of the 14th International Symposium on Functional and Logic Programming - FLOPS 2018 - held in Nagoya, Japan, May 9 - 11, 2018. The 17 papers presented in this volume were carefully reviewed and selected from 41 submissions. They cover all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming focusing on topics such as functional-logic programming, re-writing systems, formal methods and model checking, program transformations and program refinements, developing programs with the help of theorem provers or SAT/SMT solvers, language design, and implementation issues
Join ordering for constraint handling rules
No full textJoin ordering is the problem of finding cost optimal execution plans for matching multi-headed rules. In the context of Constraint Handling Rules, this topic has received limited attention so far, even though it is of great importance for efficient CHR execution. We present a formal cost model for joins and investigate the possibility of join optimization at runtime. We propose some heuristic approximations of the parameters of this cost model, for both the static and dynamic case. We discuss an O(n log n) optimization algorithm for the special case of acyclic join graphs. However, in general, join order optimization is an NP-complete problem. Finally, we identify some classes of cyclic join graphs that can be reduced to acyclic ones.status: Publishe
- …
