1,066 papers · page 48 of 54
We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type τ1 Λ τ2 to be used in some places at type τ1 …
Based on our experience with modelling and verifying microarchitectural designs within Haskell, this paper examines our use of Haskell as host for an embedded language. In particular, we highlight our use of Haskell's lazy lists, type classes, lazy state monad, and unsafe Perform…
We propose a conservative extension of the polymorphic lambda calculus (Fω) as an intermediate language for compiling languages with name-based class and interface hierarchies. Our extension enriches standard Fω with recursive types, existential types, and row polymorphism, but o…
In an impure functional language, there are programs whose behaviour is completely functional (in that they behave extensionally on inputs), but the functions they compute cannot be written in the purely functional fragment of the language. That is, the class of programs with fun…
The advantage of lazy functional languages is that programs may be written declaratively without specifying the exact evaluation order. The ensuing order of evaluation can however be quite involved which makes it difficult to debug such programs using traditional, operational tec…
This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different frdm the conventional ML type discipline, the proposed type system allows full rank 1 polymorphism, where polymorphic…
Square matrices serve as an interesting case study in functional programming. Common representations, such as lists of lists, are both inefficient---at least for access to individual elements---and error-prone, because the compiler cannot enforce "squareness". Switching to a typi…
In a programming language with procedures and assignments, it is often important
ML-style modules are valuable in the development and maintenance of large software systems, unfortunately, none of the existing languages support them in a fully satisfactory manner. The Official SML'97 Definition does not allow higher-order functors, so a module that refers to e…
Languages such as Java, ML, Scheme, and Haskell provide automatic storage management, that is, garbage collection. The two fundamental operations performed on a garbage-collected heap are "allocate" and "collect." Because the heap is in an inconsistent state during these operatio…
Positive recursive (fixpoint) types can be added to the polymorphic (Church-style) lambda calculus λ2 (System F) in several different ways, depending on the choice of the elimination operator. We compare several such definitions and we show that they fall into two equivalence cla…
We present two complementary approaches to writing XML document-processing applications in a functional language.In the first approach, the generic tree structure of XML documents is used as the basis for the design of a library of combinators for generic processing: selection, g…
Programs are often structured around the idea that di#erent pieces of code comprise distinct principals, each with a view of its environment. Typical examples include the modules of a large program, a host and its clients, or a collection of interactive agents. In this paper, we …
No abstract available.
Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) may depend on other compone…
MLJ compiles SML'97 into verifier-compliant Java bytecodes. Its features include type-checked interlanguage working extensions which allow ML and Java code to call each other, automatic recompilation management, compact compiled code and runtime performance which, using a `just i…
Lava is a tool to assist circuit designers in specifying, designing, verifying and implementing hardware. It is a collection of Haskell modules. The system design exploits functional programming language features, such as monads and type classes, to provide multiple interpretatio…
Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and f…
We provide a semantical framework for exact real arithmetic using linear fractional transformations on the extended real line. We present an extension of PCF with a real type which introduces an eventually breadth-first strategy for lazy evaluation of exact real numbers. In this …
No abstract available.