the proceedings contain 8 papers. the topics discussed include: histo- and dynamorphisms revisited;generic datatypes á la carte;dependent type providers;N queens problem: a metaprogramming stress test for the com...
ISBN:
(纸本)9781450323895
the proceedings contain 8 papers. the topics discussed include: histo- and dynamorphisms revisited;generic datatypes á la carte;dependent type providers;N queens problem: a metaprogramming stress test for the compiler;usage of generic programming on hackage - experience report;multi-polymorphic programming in bondi;programming macro tree transducers;and generic representations of tree transformations.
I explore programming withthe dependently typed functional language, AGDA. I present the progress which AGDA has made, demonstrate its usage in a small development, reflect critically on the state of the art, and spe...
详细信息
I explore programming withthe dependently typed functional language, AGDA. I present the progress which AGDA has made, demonstrate its usage in a small development, reflect critically on the state of the art, and speculate about the way ahead. I do not seek to persuade you to adopt AGDA as your primary tool for systems development, but argue that AGDA stimulates new useful ways to think about programming problems and deserves not just curiosity but interest, support and contribution.
We explore how two different mechanisms for reasoning about state, linear typing and the type, region and effect discipline, complement one another in the design of a strongly typed functionalprogramming language. th...
详细信息
ISBN:
(纸本)9781581134155
We explore how two different mechanisms for reasoning about state, linear typing and the type, region and effect discipline, complement one another in the design of a strongly typed functionalprogramming language. the basis for our language is a simple lambda calculus containing first-class memory regions, which are explicitly passed as arguments to functions, returned as results and stored in user-defined data structures. In order to ensure appropriate memory safety properties, we draw upon the literature on linear type systems to help control access to and deallocation of regions. In fact, we use two different interpretations of linear types, one in which multiple-use values are freely copied and discarded and one in which multiple-use values are explicitly reference-counted, and show that both interpretations give rise to interesting invariants for manipulating regions. We also explore new programming paradigms that arise by mixing first-class regions and conventional linear data structures.
We investigate the use of functionalprogramming to develop a numerical linear algebra run-time;i.e. a framework where the solvers can be adapted easily to different contexts and task parallelism can be attained (semi...
详细信息
We describe a new and simpler implementation in Haskell of CML's events, which encode reactions by a thread to combinations of messages from other threads. We add a new type of Guarded Events, by which recipients ...
详细信息
ISBN:
(纸本)9781581134155
We describe a new and simpler implementation in Haskell of CML's events, which encode reactions by a thread to combinations of messages from other threads. We add a new type of Guarded Events, by which recipients can filter messages with conditions on their value known as Guards. We implement guarded channels. the guard type and the indexing algorithm are not part of the channel definition, so that the user can trade off what guards are required against the cost of indexing. As an example we sketch the encapsulation of a graphical user interface toolkit. this can be done concisely not only because of guarded events, but also because we construct events monadically. Monadic events are especially helpful for representing concurrent processes which transform themselves in reaction to external communications.
We demonstrate a natural mapping from XML element types to ML module expressions. the mapping is inductive and definitions of common XML operations can be derived as the module expressions are composed. We show how to...
详细信息
We demonstrate a natural mapping from XML element types to ML module expressions. the mapping is inductive and definitions of common XML operations can be derived as the module expressions are composed. We show how to derive, in a generic way, the validation function, which checks an XML document for conformance to its DTD (Document Type Definition). One can view validation as assigning ML types to XML elements and the validation procedure a prerequisite for typeful XML programming in ML. Our mapping uses the parametric module facility of ML in some contrived way. For example, in validating WML (WAP Markup Language) documents, we need to use 36-ary type constructors, as well as higher-order modules that take in as many as 17 modules as input. that one can systematically model XML DTDs at the module level suggests ML-like languages are suitable for type-safe prototyping of DTD-aware XML applications.
Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, the...
详细信息
Generic Haskell is an extension of Haskell that supports the construction of generic programs. During the development of several applications, such as an XML editor and compressor, we encountered a number of limitatio...
详细信息
ISBN:
(纸本)9781581137569
Generic Haskell is an extension of Haskell that supports the construction of generic programs. During the development of several applications, such as an XML editor and compressor, we encountered a number of limitations withthe existing (Classic) Generic Haskell language, as implemented by the current Generic Haskell compiler. Specifically, generic definitions become disproportionately more difficult to write as their complexity increases, such as when one generic function uses another, because recursion is implicit in generic definitions. In the current implementation, writing such functions suffers the burden of a large administrative overhead and is at times counter- intuitive. Furthermore, the absence of type checking in the current implementation can make Generic Haskell hard to use. In this paper we develop the foundations of Dependency-style Generic Haskell which addresses the above problems, shifting the burden from the programmer to the compiler. these foundations consist of a full type system for Dependency-style Generic Haskell's core language and appropriate reduction rules. the type system enables the programmer to write generic functions in a more natural style, taking care of dependency details which were previously the programmer's responsibility.
Programs written using a deterministic-by-construction model of parallel computation are guaranteed to always produce the same observable results, offering programmers freedom from subtle, hard-to-reproduce nondetermi...
详细信息
Music theory has been essential in composing and performing music for centuries. Within Western tonal music, from the early Baroque on to modern-day jazz and pop music, the function of chords within a chord sequence c...
详细信息
ISBN:
(纸本)9781450308656
Music theory has been essential in composing and performing music for centuries. Within Western tonal music, from the early Baroque on to modern-day jazz and pop music, the function of chords within a chord sequence can be explained by harmony theory. Although Western tonal harmony theory is a thoroughly studied area, formalising this theory is a hard problem. We present a formalisation of the rules of tonal harmony as a Haskell (generalized) algebraic datatype. Given a sequence of chord labels, the harmonic function of a chord in its tonal context is automatically derived. For this, we use several advanced functionalprogramming techniques, such as type-level computations, datatype-generic programming, and error-correcting parsers. As a detailed example, we show how our model can be used to improve content-based retrieval of jazz songs. We explain why Haskell is the perfect match for these tasks, and compare our implementation to an earlier solution in Java. We also point out shortcomings of the language and libraries that limit our work, and discuss future developments which may ameliorate our solution.
暂无评论