- Haskell-Cafe - Haskell.org

[ANNOUNCE] sbvPlugin: Run SMT solvers over Haskell "theorems"
by Levent Erkok 22 Dec '15

22 Dec '15

Hello all, I'm happy to announce the first public release of sbvPlugin, a new GHC-core plugin based on the SBV library: http://hackage.haskell.org/package/sbvPlugin The plugin can be used to prove (or refute!) theorems in your Haskell code, using the SBV library as its backend. Here's a most simple example: {-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} module Test where import Data.SBV.Plugin {-# ANN test theorem #-} test :: Integer -> Integer -> Bool test x y = x + y >= x - y When compiled (or loaded into ghci), you'll see that the plugin will attempt to prove the given theorem, and will produce a counter-example since it is not valid! (This assumes, you've installed an SBV-supported SMT solver. Z3 from Microsoft is a good choice: http://github.com/Z3Prover/z3) <http://github.com/Z3Prover/z3> The plugin is still in its early days and the examples are rather sparse. But see the following for one worked out instance: (Thanks to Anthony Cowley for the original idea.) http://hackage.haskell.org/package/sbvPlugin/docs/Data-SBV-Plugin-Examples-… The sbvPlugin takes advantage of the SBV library ( http://hackage.haskell.org/package/sbv) to directly reason about Haskell programs at GHC's core level. However, the plugin is *not* a replacement for SBV. It only exposes a few features of SBV directly at the Haskell level; which hopefully makes it useful and more friendly than SBV; but it is neither intended nor possible for it to replace the SBV library itself. In particular, the plugin is limited to certain types (mostly numeric), and a few composite ones (lists and tuples.) If the plugin does not "understand" a Haskell type/expression, it'll use a technique called "uninterpretation" to black-box it. In those cases, the counter-examples produced might be bogus, though proofs will still be valid. Note that any definitions that are outside of the module being compiled will also go uninterpreted, including all the Prelude functions. The plugin is still in its early days, and there are a number of rough edges. Any feedback is most welcome! Happy hacking, -Levent.

1 0

Re: [Haskell-cafe] More disciplined alternative to rewrite rules?
by Johannes Waldmann 21 Dec '15

21 Dec '15

What graph(s) do you want to rewrite? How would this help with respect to A, B, and C? The program is a term (tree), the runtime data structure (heap) is a graph - you want rewriting at run-time then? But the purpose is to move work from run-time to compile-time. - J.W.

3 3

RFC: explicit support for GADTs in Template Haskell
by Jan Stolarek 21 Dec '15

21 Dec '15

GHC Users, I am working on adding proper support for GADTs in Template Haskell. By proper I mean that GADTs data constructors will no longer be encoded using H98 data constructors, but will be represented explicity. GADTs allow to declare several constructors with the same signature: data T where MkT1, MkT2 :: T The question is whether to represent such constructors in TH syntax as: (1) GadtC [Name] [StrictType] Name [Type] -- or: (2) GadtC Name [StrictType] Name [Type] Note the difference in first field. (1) is closer to the original syntax, as it stores the list of all names in a single declaration, as was originally written in the source code. (2) requires to have a separate `GadtC` for each constructor even if constructors were declared together, as in the example above. I would like to hear from TH users which of these two representations you prefer. At the moment I have implemented (1) as it directly represents source syntax. The downside of (1) is that information whether several data constructors were declared together is not recoverable during reification, and so reifying T will yield: data T where MkT1 :: T MkT2 :: T Janek --- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.

2 2

wondering on Haskell kickstarter project: VST plugin / mobile synthesizer
by Anton Kholomiov 21 Dec '15

21 Dec '15

I'm wondering if it's good idea to make crowd-founding project for a synthesizer written in Haskell. What's your opinion? Would you like to support such a project? I've made a prototype: https://github.com/anton-k/tiny-synth It's a desktop synthesizer, a collection of instruments. About 150 instruments written in Haskell. It works with midi keyboard. You can try it out with USB-midi device. The UI is written with Python and audio engine is written with Haskell. I use my library csound-expression to generate the code for Csound. The Csound is an audio programming language it can be used as C library. There are bindings to many languages and it can work on Android / iOS. Right now I've made a prototype for desktop. The big plan is to create VST/AU/Lv2 plugins and mobile versions for Android and iOS. [1] https://github.com/anton-k/tiny-synth [2] http://hackage.haskell.org/package/csound-expression [3] https://github.com/spell-music/csound-expression Cheers, Anton

2 3

More disciplined alternative to rewrite rules?
by Will Yager 21 Dec '15

21 Dec '15

Has there been any discussion of replacing rewrite rules with a more disciplined and robust system? Some problems I've noticed with rewrite rules are: A) It's highly syntactic. It isn't really capable of encapsulating intent; it just does restrictively simple term manipulation. B) As a result, many performance-oriented modules seem to have an ungainly number of rewrite rules so as to cover every likely case. C) There are many cases where rewrite rules fail to work as intended, either because the module author missed a rewrite case or because the rewrite fails to fire for some reason. Perhaps a good approach would be to implement a rewrite system in a domain more amenable to simplification rules. For example, there has been a great deal of (quite successful) work on circuit simplification in the form of operations on graphs. Haskell is quite amenable to graph representations, so this approach might work for Haskell as well. -Will

1 0

Imported rewrite rules are ignored
by Johannes Waldmann 21 Dec '15

21 Dec '15

Forgot to say: I confirm your observation for ghc-7.* and I checked that the imported rule *does* fire with ghc-6.10.4.

1 0

Imported rewrite rules are ignored
by Johannes Waldmann 21 Dec '15

21 Dec '15

Well, ghc --show-iface RuleModule.hi does show the rule: rewrite_me :: () -> () {- Strictness: b, Inline: NOINLINE -} "rewrite_me" [ALWAYS] forall input :: () rewrite_me input = ()

1 0

New Functional Programming Job Opportunities
by Functional Jobs 21 Dec '15

21 Dec '15

Here are some functional programming job opportunities that were posted recently: Software Engineer (Scala/Play/Scala.js/React) at AdAgility https://functionaljobs.com/jobs/8871-software-engineer-scala-play-scalajs-r… Cheers, Sean Murphy FunctionalJobs.com

1 0

Imported rewrite rules are ignored
by Alexander Vieth 21 Dec '15

21 Dec '15

Hi café, I observe that rewrite rules from imported modules are ignored by GHC. Given these two files, one module and one executable, the problem can be demonstrated by switching between `rewrite_me` and `rewrite_me_local`. If the rule fires, the program should run cleanly, as the `error` term should be rewritten to `()`. The imported function rewrite_me is not rewritten; but the same thing, rewrite_me_local, defined in the same program, will be rewritten. File RuleModule.hs module RuleModule where {-# NOINLINE rewrite_me #-} rewrite_me :: () -> () rewrite_me = error "Should rewrite" {-# RULES "rewrite_me" forall input . rewrite_me input = () #-} File Rule.hs import RuleModule {-# NOINLINE rewrite_me_local #-} rewrite_me_local :: () -> () rewrite_me_local = error "Should rewrite" {-# RULES "rewrite_local" forall input . rewrite_me_local input = () #-} -- Replace with rewrite_me_local and it's all good. main = case rewrite_me () of () -> return () This is GHC 7.10.2. I compile using -O -fenable-rewrite-rules. Using -dverbose-core2core, the "Desugar (after optimization)" section shows no rules when using rewrite_me, but shows the rule rewrite_local when using the local variant. Maybe this is expected, but I thought it important to mention. Thanks for any advice, Alex

1 0

Preventing sharing
by Oleg 21 Dec '15

21 Dec '15

The old article Preventing memoization in (AI) search problems http://okmij.org/ftp/Haskell/index.html#memo-off deals with the problem, explaining the trick to deliberately confuse GHC so that it won't perform memoization (sharing). Yes, I know how bad this confusing of GHC sounds: which is part of my argument that lazy evaluation by default was a mistake.

2 1