User loginNavigation |
FunctionalObjects to Unify Type Classes and GADTsObjects to Unify Type Classes and GADTs, by Bruno C. d. S. Oliveira and Martin Sulzmann:
A very interesting paper on generalizing and unifying type classes and GADTs. Classes are now first-class values, resulting in a language that resembles a traditional, albeit more elegant, object-oriented language, and which supports a form of first-class "lightweight modules". The language supports the traditional use of implicit type class dispatch, but also supports explicit dispatch, unlike Haskell. The authors suggest this could eliminate much of the duplication in the Haskell standard library of functions that take a type class or an explicit function, eg. insert/insertBy and sort/sortBy, although some syntactic sugar is needed to make this more concise. Classes are open to extension by default, although a class can also be explicitly specified as "sealed", in which case extension is forbidden and you can pattern match on the cases. Furthermore, GADTs can now also carry methods, thus introducing dispatch to algebraic types. This fusion does not itself solve the expression problem, though it does ease the burden through the first-class support of both types of extension. You can see the Scala influences here. I found this paper via the Haskell sub-reddit, which also links to a set of slides. The authors acknowledge Scala as an influence, and as future work, suggest extensions like type families and to support more module-like features, such as nesting and opaque types. By naasking at 2010-02-22 21:51 | Functional | Object-Functional | OOP | Theory | Type Theory | 15 comments | other blogs | 4180 reads
A Lambda Calculus for Real AnalysisA Lambda Calculus for Real Analysis
Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated Jean-Yves Girard's regrettably out-of-print Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX. By Paul Snively at 2010-02-16 22:00 | Category Theory | Functional | Lambda Calculus | Logic/Declarative | Meta-Programming | Semantics | Type Theory | 8 comments | other blogs | 5432 reads
Computational Semantics with Functional Programming
The manuscript of the book Computational Semantics with Functional Programming by Jan van Eijck and Christina Unger, as well as related software, is available online.
The introductory chapters are probably going to be unnecessary for LtU readers, but once things get going there is a lot to learn here if you are interested in formal semantics of natural language, especially in the Montague-style. And if this doesn't ring a bell - just search for "continutation" in the manuscript, and be prepared to meet old friends (you know who you are) in a new context. If the contributing editors will neglect their duties, LtU will wither and die. Hint, hint. Delimited Control in OCaml, Abstractly and Concretely, System DescriptionDelimited Control in OCaml, Abstractly and Concretely, System Description
Oleg was kind enough to send me an e-mail letting me know of this paper's existence (it appears not yet to be linked from the "Computation" page under which it is stored) and to include me in the acknowledgements. Since the paper in its current form has been accepted for publication, he indicated that it can be made more widely available, so here it is. In typical Oleg fashion, it offers insights at both the theoretical and implementation levels. By Paul Snively at 2010-01-25 17:27 | Cross language runtimes | Functional | Implementation | Semantics | Type Theory | 3 comments | other blogs | 3183 reads
Syntactic Proofs of Compositional Compiler CorrectnessSyntactic Proofs of Compositional Compiler Correctness
A submitted draft of another paper from Adam, continuing to expand LambdaTamer's reach. By Paul Snively at 2010-01-09 17:10 | Functional | Implementation | Lambda Calculus | Semantics | Type Theory | 4 comments | other blogs | 3134 reads
A Verified Compiler for an Impure Functional LanguageA Verified Compiler for an Impure Functional Language
Further work on/with LambdaTamer for certified compiler development. By Paul Snively at 2010-01-09 17:03 | Functional | Implementation | Lambda Calculus | Semantics | Type Theory | 4 comments | other blogs | 3279 reads
Certified Programming With Dependent Types Goes BetaCertified Programming With Dependent Types From the introduction:
This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights. Please note that Adam is explicitly requesting feedback on this work. By Paul Snively at 2010-01-09 16:56 | Functional | Lambda Calculus | Logic/Declarative | Misc Books | Semantics | Teaching & Learning | Type Theory | 6 comments | other blogs | 3177 reads
John Hughes on Erlang and HaskellJohn Hughes talks about his experience with Erlang vs. Haskell in an InfoQ Interview. While the discussions about strict vs lazy, pure vs side effecting, and dynamic vs static typing are interesting he raises a good question for the LtU crowd at the end:
So, LtU, where is the next order of magnitude coming from? Causal Commutative Arrows and Their OptimizationCausal Commutative Arrows and Their Optimization, Hai Liu. Eric Cheng. Paul Hudak. ICFP 2009.
One way of understanding what is going on in this paper is that in terms of dataflow programming, FRP programs correspond to programs with single-entry, single-exit dataflow graphs. This means that none of the internal dataflow nodes in an FRP program are actually necessary -- you can coalesce all those nodes into a single node while preserving the observable behavior. (They briefly touch on this point when they mention that synchronous languages try to compile to "single loop code".) What's very slick is that they have a nice normal form procedure that (a) is defined entirely in terms of their high-level language, and (b) always yields code corresponding to the the coalesced dataflow graph. It's an elegant demonstration of the power of equational reasoning. SequenceL - declarative computation on nonscalarsI recently came across the language SequenceL, which it seems NASA is using in some of its human spaceflight programs. SequenceL is described as a high-level language for declarative computation on nonscalars. One of the key features of the language appears to be the avoidance of the need to explicitly specify recursive or iterative operations. For example, given the function definition
Search(scalar Target, tuple [Subscript, Word]) =
Subscript when Word = Target
which applies to tuples, the programmer can apply the function directly to lists of tuples without any need to specify how that application will be performed, e.g. search(fox,[[1,dog],[2,cat],[3,fox],[4,parrot]]) → 3 search(rabbit,[[1,dog],[2,cat],[3,fox],[4,parrot]]) → [] The language designers (Daniel Cooke and J. Nelson Rushton) claim that this kind of thing leads to more concise and readable code, and a more direct representation of a specification. Unfortunately, the SequenceL website appears to be inaccessible at the moment. However, Daniel Cooke's site includes links to a number of papers and talks that describe SequenceL. In particular, the paper Normalize, Transpose, and Distribute: An Automatic Approach for Handling Nonscalars provides a detailed description of the "Consume-Simplify-Produce/Normalize-Transpose" approach that is embodied by SequenceL. There's also an overview of SequenceL available through CiteSeer. By Allan McInnes at 2009-10-11 21:34 | Functional | Logic/Declarative | 13 comments | other blogs | 4921 reads
|
Browse archivesActive forum topics |