News aggregator

Hi all, I was creating "bigger" uncurries which I am simply extending from an existing uncurry I found some where, e.g. uncurry4 :: (a -> b -> c -> d -> e) -> ((a, b, c, d) -> e) uncurry4 f ~(a,b,c,d) = f a b c d when I realized, what's the "~" for ? I've only been able to find a partial explanation that it involves preserving laziness, or something, maybe ? I was hoping someone could enlighten me. Thanks Brian

Hi all, also if there's not that much to see and only a few minutes of gameplay, but after spending quite a few hours writing it, getting a feeling for Haskell and it's usage, perhaps it's in some way useful for someone, even if just for a few minutes of distraction. https://github.com/dan-t/layers Greetings, Daniel

*************************************************************** ICTAC 2013 10th International Colloquium on Theoretical Aspects of Computing *** Call For Papers *** September 4-6, 2013 Shanghai, China http://ictac2013.ecnu.edu.cn/ *************************************************************** ICTAC 2013 is the 10th International Colloquium on Theoretical Aspects of Computing, the latest in a series founded by the International Institute for Software Technology of the United Nations University (UNU-IIST). ICTAC 2013 will bring together practitioners and researchers from academia, industry and government to present research and to exchange ideas and experience addressing challenges in both theoretical aspects of computing and in the exploitation of theory through methods and tools for system development. The other main purpose is to promote cooperation in research and education between participants an

Dear Haskellers, while playing with folds and trying to implement `!!` by folding, I came to the conclusion that: - `foldr` is unsuitable because it counts the elements from the end, while `!!` needs counting from the start (and it's not tail recursive). - `foldl` is also unsuitable, because it always traverses the whole list. I came up with the following tail-recursive generalization of `foldl` that allows exiting the computation prematurely: foldlE :: (a -> c) -> (a -> b -> Either c a) -> Either c a -> [b] -> c foldlE f g = fld where fld (Left c) _ = c fld (Right a) [] = f a fld (Right a) (x:xs) = fld (g a x) xs `foldl` can be defined from it as foldl'' :: (a -> b -> a) -> a -> [b] -> a foldl'' f z = foldlE id ((Right .) . f) (Right z) and `!!` as: -- Checks for a negative index omitted for brevity. index :: Int -> [a] -> a index i = foldlE (error $ "No such index") f (Right i) where f 0 x = Left x f

Dear Haskellers, while playing with folds and trying to implement `!!` by folding, I came to the conclusion that: - `foldr` is unsuitable because it counts the elements from the end, while `!!` needs counting from the start (and it's not tail recursive). - `foldl` is also unsuitable, because it always traverses the whole list. I came up with the following tail-recursive generalization of `foldl` that allows exiting the computation prematurely: foldlE :: (a -> c) -> (a -> b -> Either c a) -> Either c a -> [b] -> c foldlE f g = fld where fld (Left c) _ = c fld (Right a) [] = f a fld (Right a) (x:xs) = fld (g a x) xs `foldl` can be defined from it as foldl'' :: (a -> b -> a) -> a -> [b] -> a foldl'' f z = foldlE id ((Right .) . f) (Right z) and `!!` as: -- Checks for a negative index omitted for brevity. index :: Int -> [a] -> a index i = foldlE (error $ "No such index") f (Right i) where f 0 x = Left x f

I am glad to announce a new major release of SmallCheck (hackage).

What is SmallCheck?

SmallCheck is a property-based testing library for Haskell.

If you are familiar with QuickCheck, you can think of SmallCheck as a better QuickCheck. The main way in which it is better is that it is non-random: whether your tests pass does not depend on the roll of the dice.

If you are not familiar with QuickCheck, the idea of SmallCheck is to check certain properties of your functions, as opposed to unit testing, where you just check the expected outcome of some particular tests.

For an introduction to property-based testing, check out Chapter 11 of Real World Haskell. It should be straightforward to translate all the examples there to SmallCheck.

What’s new in 1.0 Monadic properties

Properties are now parameterised on the monad they work in.

The two main ways a property can use the monad are:

1. generating test cases monadically
2. verifying the condition monadically

Monadic test cases generation can be used to read test cases from files. A well-known problem when testing compilers is that it is hard to enumerate or randomly generate valid programs. So here you go — just put some examples in the file system, and use them to verify some properties of your compiler.

An example of monadic verification is when you want to verify your code against an external (or otherwise impure) reference implementation.

Quantifiers

The semantics of quantifiers has changed. Previously, all variables were quantified universally by default, and a quantifier (like exists) changed the quantification of the next variable.

So, for example, exists $ \x y -> p x y was interpreted as \(\exists x: \forall y. p\ x\ y\), which is probably not what one would expect.

Now the quantification operators (forAll, exists and existsUnique) set the quantification context for all subsequent variables, so the above property means \(\exists x, y: p\ x\ y\).

Uniqueness quantification

There’s an interesting effect related to the uniqueness quantifier existsUnique (which was previously called exists1).

There are two ways to interpret existsUnique $ \x y -> p x y, “curried” and “uncurried”:

• \(\exists ! x: \exists ! y: p\ x\ y\)
• \(\exists ! (x,y): p\ x\ y\)

These two actually have different meaning. Suppose that \(p\ x\ y=(|x|=|y|)\), where \(|x|\) denotes the absolute value of an integer \(x\). Then the first property above is true, and the second is false (be sure to check this yourself).

When mathematicians write \(\exists ! x,y:p\ x\ y\), they really mean the second interpretation, so this is what SmallCheck implements (although the first interpretation would be much easier to implement).

Higher-order properties

Both SmallCheck and QuickCheck have a ==> operator, which tests an implication. The left argument of ==> has type Bool, and it’s usually a statement that the generated arguments satisfy some side condition (e.g. generated programs are valid).

In this new version of SmallCheck, the left argument of ==> can be an arbitrary property, with its own quantifiers etc. Here’s how we could test an isPrime function:

import Test.SmallCheck import Test.SmallCheck.Series isPrime :: Integer -> Bool isPrime _ = True main = smallCheck 5 {- 5 is the testing depth -} $ \(Positive n) -> (exists $ \(Positive d) -> d /= 1 && d /= n && n `mod` d == 0) ==> not (isPrime n)

Unsurprisingly, the result will be

Failed test no. 4. there exists 4 such that condition is false Ordered testing

SmallCheck has just got more efficient and less annoying!

Previously, if you wanted to get the minimal counterexample, you used the function smallCheck which tested the property first with depth 0, then with depth 1 and so on — up to the limit that you told it.

The reason was that the Serial instance of e.g. Integer generated the following integers for depth 3:

[-3,-2,-1,0,1,2,3]

They are tried in exactly this order, and, if all of them were counterexamples, the user would be presented with -3 as the first one.

Now the instances generate examples in the order of increasing depth, e.g.

[0,1,-1,2,-2,3,-3]

so there’s no need to try multiple depths.

Better reporting

The way SmallCheck reports its findings is now greatly improved, especially in some complex cases.

For example, consider the following property:

smallCheck 5 $ existsUnique $ \x -> (forAll $ \y -> x * y >= 0) ==> (forAll $ \y -> x * y == (0 :: Integer))

Here’s what SmallCheck 0.6.2 reports (or, to be precise, would report if it supported higher-order properties):

Depth 0: Completed 1 test(s) without failure. Depth 1: Failed test no. 12. Test values follow. non-uniqueness -1 0

And this is the output of SmallCheck 1.0:

Failed test no. 12. there are at least two arguments satisfying the property: for 0 condition is true for 1 property is vacuously true because there exists -1 such that condition is false Required type annotations

Because the Testable class is now multi-parameter (parameterised on the type and the monad), ambiguous types that involve this class do not get defaulted. To put it simply, most non-trivial properties now require some type annotations.

This turned out to be a very good thing for SmallCheck (which I couldn’t envision). Defaulting for properties often works in an unexpected way. For example, here’s what an older SmallCheck would tell you if you asked it whether all things are the equal:

> depthCheck 5 $ \x y -> x == y Depth 5: Completed 1 test(s) without failure.

The result is unexpected, but at least we get some clue from the fact that there was just one test: the type of the variables got defaulted to ()!

Alas, QuickCheck doesn’t give us even this hint:

> quickCheck $ \x y -> x == y +++ OK, passed 100 tests.

Luckily, with the new SmallCheck you actually get a type error:

<interactive>:10:26: No instance for (Eq a0) arising from a use of `==' The type variable `a0' is ambiguous Possible fix: add a type signature that fixes these type variable(s)

And indeed, the problem is easy to fix once you know it’s there:

> smallCheck 5 $ \x y -> x == (y :: Integer) Failed test no. 2. there exist 0 1 such that condition is false Simpler interface

I took this chance to clean the API and make it more orthogonal.

Previously SmallCheck had functions like

forAllElem :: (Show a, Testable b) => [a] -> (a -> b) -> Property

which did three things at once:

• made the variable universally quantified
• converted the list to a depth-independent series
• quantified the variable over that series

No wonder the API suffered from the combinatorial explosion. Now these things are all done separately:

generate :: (Depth -> [a]) -> Series m a

can be used to turn a list into a series;

over :: (Monad m, Show a, Testable m b) => Series m a -> (a -> b) -> Property m

sets the domain of quantification; and

forAll :: Testable m a => a -> Property m

sets the quantification context.

Hello, In the haskell-src-exts quasi quoter there is some code to convert all names in `dataToQa` to global names. The reasoning is according to the source:

I'm happy to announce a new major release of the grid package: http://hackage.haskell.org/package/grid https://github.com/mhwombat/grid/wiki (wiki) WHAT'S NEW: Functions for reporting the boundary and centre of bounded grid have been added, along with some miscellaneous new utility functions. IMPORTANT: The order of parameters for some functions has changed to make it easier to use them with map and fold operations. ABOUT GRID: Grid provides tools for working with regular arrangements of tiles, such as might be used in a board game or self-organising map (SOM). Grid currently supports triangular, square, and hexagonal tiles, with various 2D and toroidal layouts. If you need a tile shape or layout that isn't currently provided, please let me know. See Math.Geometry.Grid for an example of how to use the package. Suggestions for improvement are welcome.

Summary: Management of finite resources is an important part of any modern build system, only properly available in Shake and Ninja.

I've just released Shake 0.9, a build system library, with a few bug fixes and a bunch of new features (the change log has a complete list). This release contains an incompatible change which makes the Resource feature easier to use, so I thought I'd describe the motivation and use of Resources in Shake. A full upgrade guide is at the bottom of this post.

What are Resources for?

When you run -j10 (shakeThreads=10) you are asking the build system to limit computation so it uses no more than ten CPU resources at a time. The CPU is certainly a precious resource, but there are other resource limitations a build system may need to obey:

• Some APIs are global in nature, if you run two programs that access the Excel API at the same time things start to fail.
• Many people have large numbers of CPUs, but only one slow rotating hard drive. If you run ten hard-drive thrashing linkers simultaneously the computer is likely to grind to a halt.
• Some proprietary software requires licenses, a fixed number of which can be purchased and managed using a license manager. As an example, the Kansas Lava team only have access to 48 licenses for modelsim.

Resources in other build systems

I know of two approaches used by other build systems to obey resource constraints:

• Limit the number of CPUs to hit your target - for example, the Lava build system could cap the number of CPUs to the number of licenses. People with 24 CPUs might ask the build system to use only 8, so the linkers do not make their machines unusable (and even then, a link heavy rebuild may still harm interactive performance). This solution wastes CPU resources, leaving CPUs that could be building your code idling.
• Add locks to suspend jobs that are competing for the shared resource. For example any rule using Excel could take the Excel lock, either a mutex/MVar in some build systems, or creating a file to serve as the lock in make based build systems. Locking can be made to work, but is tricky if you have to fake locks using the file system, and still squanders CPU resources - instead of blocking the CPU should be running another rule.

The one exception is the Ninja build system which has a concept of "pools", which properly model finite resources.

Resources in Shake

In Shake the Resource type represents a finite resource, which multiple build rules can use. Resource values are created with newResource and used with withResource. As an example, only one set of calls to the Excel API can occur at one time, therefore Excel is a finite resource of quantity 1. You can write:

shake shakeOptions{shakeThreads=2} $ do
want ["a.xls","b.xls"]
excel <- newResource "Excel" 1
"*.xls" *> \out ->
withResource excel 1 $
system' "excel" [out,...]

Now we will never run two copies of excel simultaneously. Moreover, it will never block waiting for excel if there are other rules that could be run.

For most programming languages the compiler is CPU bound but the linker is disk bound. Running 8 linkers will often cause an 8 CPU system to grid to a halt. We can limit ourselves to 4 linkers with:

disk <- newResource "Disk" 4
want [show i <.> "exe" | i <- [1..100]]
"*.exe" *> \out ->
withResource disk 1 $
system' "ld" ["-o",out,...]
"*.o" *> \out ->
system' "cl" ["-o",out,...]

Now we can use 7 or 8 CPUs while still leaving the computer responsive enough to browse the web.

Software licenses are another finite resource and can be managed in the same way. For a complete example see the Kansas Lava test program, which uses Shake.

Porting from Shake 0.8

In Shake 0.9 the newResource function has been renamed to newResourceIO - rename newResource to newResourceIO everywhere and your code will work again.

However, you may have noticed that newResourceIO (as it is now called) forces you to create the resource before calling the shake function, meaning that often the creation and use of the resource are far apart. I have introduced a function newResource which runs in the Rules monad, allowing you to create a resource and then use it nearby. Moving the creation and use of resources closer together makes it much easier to check your resource constraints are met.

The only other breaking change is that shakeVersion has become a String rather than an Int, allowing you to store more precise information about the version (for example, your build system might want to encode the GHC version and the version of the build system in the string).

Updated 18 Feb 2013: Ninja also supports finite resources.

submitted by CKoenig
[link] [50 comments]

In a previous post I discussed the status of Church’s Law in type theory, showing that it fails to hold internally to extensional type theory, even though one may see externally that the definable numeric functions in ETT are λ-definable, and hence Turing computable.  The distinction between internal and external is quite important in logic, mainly because a logical formalism may be unable to express precisely an externally meaningful concept.  The classical example is the Löwenheim-Skolem Theorem of first-order logic, which says that any theory with an infinite model has a countable model.  In particular the theory of sets has a countable model, which would seem to imply that the set of real numbers, for example, is countable.  But internally one can prove that the reals are uncountable (Cantor’s proof is readily expressed in the theory), which seems to be a paradox of some kind.  But no, all it says is that the function witnessing the countability of the term model cannot be expressed internally, and hence there is no contradiction at all.

A similar situation obtains with Church’s Law.  One may observe empirically, so to say, that Church’s Law holds externally of ETT, but this fact cannot be internalized.  There is a function given by Church’s Law that “decompiles” any (extensional) function of type N→N by providing the index for a Turing machine that computes it.  But this function cannot be definable internally to extensional type theory, because it may be used to obtain a decision procedure for halting of Turing machines, which is internally refutable by formalizing the standard undecidability proof.  In both of these examples it is the undefinability of a function that is important to the expressive power of a formalism, contrary to naïve analyses that would suggest that, when it comes to definability of functions, the more the merrier.  This is a general phenomenon in type theory.  The power of type theory arises from its strictures, not its affordances, in direct opposition to the ever-popular language design principle “first-class x” for all imaginable values of x.

Another perspective on the same issue is provided by Martin-Löf’s meaning explanation of type theory, which is closely related to the theory of realizability for constructive logic.  The high-level idea is that a justification for type theory may be obtained by starting with an untyped concept of computability (i.e., a programming language given by an operational semantics for closed terms), and then giving the meaning of the judgments of type theory in terms of such computations.  So, for example, the judgment A type, where A is a closed expression means that A evaluates to a canonical type, where the canonical types include, say, Nat, and all terms of the form A’→A”, where A’ and A” are types.  Similarly, if A is a type, the judgment a:A means that A evaluates to a canonical type A’ and that a evaluates to a canonical term a’ such that a’ is a canonical element of A’, where, say, any numeral for a natural number is a canonical member of Nat.  To give the canonical members of the function type A’→A” requires the further notion of equality of elements of a type, a=b:A, which all functions are required to respect.  A meaning explanation of this sort was suggested by Martin-Löf in his landmark paper Constructive Mathematics and Computer Programming, and is used as the basis for the NuPRL type theory, which extends that account in a number of interesting directions, including inductive and coinductive types, subset and quotient types, and partial types.

The relation to realizability emerges from applying the meaning explanation of types to the semantics of propositions given by the propositions-as-types principle (which, as I’ve previously argued, should not be called “the Curry-Howard isomorphism”).  According to this view a proposition P is identified with a type, the type of its proofs, and we say that P true iff P evaluates to a canonical proposition that has a canonical member.  In particular, for implication we say that P→Q true if and only if P true implies Q true (and, in addition, the proof respects equality, a condition that I will suppress here for the sake of simplicity).  More explicitly, the implication is true exactly when the truth of the antecedent implies the truth of the consequent, which is to say that there is a constructive transformation of proofs of P into proofs of Q.

In recursive realizability one accepts Church’s Law and demands that the constructive transformation be given by the index of a Turing machine (i.e., by a program written in a fixed programming language).  This means, in particular, that if P expresses, say, the decidability of the halting problem, for which there is no recursive realizer, then the implication P→Q is vacuously true!  By taking Q to be falsehood, we obtain a realizer for the statement that the halting problem is undecidable.  More generally, any statement that is not realized is automatically false  in the recursive realizability interpretation, precisely because the realizers are identified with Turing machine indices.  Pressing a bit further, there are statements, such as the statement that every Turing machine either halts or diverges on its own input, that are true in classical logic, yet have no recursive realizer, and hence are false in the realizability interpretation.

In contrast in the meaning explanation for NuPRL Church’s Law is not assumed.  Although one may show that there is no Turing machine to decide halting for Turing machines, it is impossible to show that there is no constructive transformation that may do so.  For example, an oracle machine would be able to make the required decision.  This is entirely compatible with intuitionistic principles, because although intuitionism does not affirm LEM, neither does it deny it.  This point is often missed in some accounts, leading to endless confusions.  Intuitionistic logic, properly conceived, is compatible with classical logic in that classical logic may be seen as an idealization of intuitionistic logic in which we heuristically postulate that all propositions are decidable (all instances of LEM hold).

The crucial point distinguishing the meaning explanation from recursive realizability is precisely the refusal to accept Church’s Law, a kind of comprehension principle for functions as discussed earlier.  This refusal is often called computational open-endedness because it amounts to avoiding a commitment to the blasphemy of limiting God’s programming language to Turing machines (using an apt metaphor of Andrej Bauer’s).  Rather, we piously accept that richer notions of computation are possible, and avoid commitment to a ”final theory” of computation in which Church’s Law is postulated outright.  By avoiding the witnessing function provided by Church’s Law we gain expressive power, rather than losing it, resulting in an elegant theory of constructive mathematics that enriches, rather than diminishes, classical mathematics.    In short, contrary to “common sense” (i.e., uninformed supposition), more is not always better.

Update: corrected minor technical error and some typographical errors.

Update: clarified point about incompatibility of recursive realizability with classical logic.

Filed under: Research Tagged: semantics, type theory

The last week and a half I've been working on this plotter. We use google protocol buffers for telemetry for our UAVs/simulations/etc, and we were sorely missing the ability to view this data in real time.

The essence of it is you make channels with:

newChannel : String -> PbTree a -> IO (Channel, Chan a)

and you start the gui with

runPlotter :: [Channel] -> IO ()

You just forkIO a thread to write to (Chan a) and it will be available for viewing! The tricky part was automatically creating (PbTree a) which is sort of like Tree (String, Maybe (a -> Double)). I use template haskell for this in makeAccessors :: Name -> ExpQ. It doesn't work for every possible ADT but I think it works for everything that a protobuf can represent *fingers crossed*.

It's not on hackage yet but here's the github if you're interested.

submitted by bigstumpy
[link] [3 comments]

Hi all, as some of you may have noticed Lambdabot doesn't build on GHC 7.6.1 due to OldException being removed (and a few other changes). I updated the code so that it builds on latest GHC release. The updated code is available here: https://github.com/killy9999/lambdabot/tree/upstream It builds on Linux, but I am not 100% certain that it will build on Windows. If it doesn't I will be grateful for reporting this (and any other) issues on the bug tracker: https://github.com/killy9999/lambdabot/issues The changes required to make the code run weren't as small as I initially thought they will be. In some places this resulted in a bit ugly code, but aside from that I think that everything should work correctly. Now I would like to do a bit of maintanance on the project, since the code is a bit of a mess and it could use some cleanup. My plans are: - clean up the package namespace by placing existing modules in Lambdabot module - integrate lambdabot-utils into lambdabot (already done) - reformat the

I have a tiny DSL that actually works quite well. When I say import language.CWMWL main = runCWMWL $ do out (matrixMult, A, 1, row, matrix-row) then runCWMWL is a function that is exported by language.CWMWL. This parses the experession and takes some action. Now, A is the name of the matrix and the third tuple element would represent the numbe of the row. For example 1 to 10000. I want to achieve some sort of "elegant" (means readable code, a good representation) recursion that would let me do something like sequence [ out (matrixMult, A, n, row, matrix-row) | n <- [1..1000] ] but in a nicer manner an without expending this to 10000 lines of code at compile time. How can I best introduce recursion into my DSL or borrow this from the host language Haskell "effectively"? --Joerg

Preface: I'm a beginner with Haskell.

I'm trying to represent a gamestate. The game contains objects which can have abilities that arbitrarily modify the gamestate. I want to have something like this:

data GameObject = GameObject { name :: String , attributes :: [ Int ] , specialWorldModifyingAbility :: GameWorld -> GameWorld } data GameWorld = GameWorld { components :: [ GameObject ] }

however, I can't get this to compile, because GameObject references GameWorld, and GameWorld references GameObject.

I feel as though this is a mis-design. Is there a recommended approach to this type of situation? Note that each type of GameObject (and its accompanying WorldModifyingAbility) will be predetermined and hardcoded in - there's no need to generate either during runtime. Perhaps I should be using a typeclass here rather than a data declaration, and each object should be an instance? I don't really know.

EDIT: thanks for taking a look, nandemo and etrepum. After your comments, I went back and looked for what I left out. The important detail I omitted was apparently Template Haskell. I actually had

{-# LANGUAGE TemplateHaskell #-} module Foo where import Control.Lens data GameObject = GameObject { _name :: String , _attributes :: [ Int ] , _specialWorldModifyingAbility :: GameWorld -> GameWorld } $( makeLenses ''GameObject ) data GameWorld = GameWorld { _components :: [ GameObject ] }

which doesn't compile unless I move the call to makeLenses after the declaration of GameWorld. Thankfully an easy fix.

submitted by mazeofmice
[link] [3 comments]