- Haskell-Cafe - Haskell.org

runGet exits prematurely
by Quentin Liu 23 Feb '18

23 Feb '18

Hi, I am using Data.Binary to decode binary files and found that the `runGet` function would throw an exception “not enough bytes” even though it has not consumed all the input. Specifically, in the loop I am repeatedly trying to parse the binary file until it has consumed all the input parsePPackets xs = do empty <- isEmpty if empty then return xs else do p <- parseB6034 parsePPackets (p:xs) When I try to run this function with `runGet`, the exception “Data.Binary.Get.runGet at position 3293603: not enough bytes” would be thrown, while the total length of input is 5864230, a number significantly larger. The function `parseB6034` consumes no more than 250 bytes in each round. In addition, the `parsePPackets` works well when fed with a small amount of data. Is it the problem of my code or an error with the package binary? The ByteString fed into `runGet` is lazy ByteString, as required by `runGet` function. Best Regards, Qingbo Liu

1 0

Occurs check: cannot construct the infinite type - but it doesn't need to
by Tom Ellis 23 Feb '18

23 Feb '18

I have run into a similar problem to my last question which is not resolved with NoMonomorphismRestriction. 'foo2' has a partial type signature and I get an occurs check. 'foo3' is exactly the same except it has no signature, and it works! Why can't 'foo2' be inferred like 'foo3'? {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE NoMonomorphismRestriction #-} type family Quux a type family Corge a foo :: ( b ~ Quux a , a ~ Corge b ) => a -> b foo = undefined -- Occurs check: cannot construct the infinite type: -- t0 ~ Corge (Quux t0) -- arising from a use of ‘foo’ -- The type variable ‘t0’ is ambiguous -- foo2 :: _ foo2 = foo foo3 = foo

1 0

Re: [Haskell-cafe] [Haskell] ANN: Hackage Account Registration Changes
by Niklas Hambüchen 23 Feb '18

23 Feb '18

On 23/02/2018 00.27, Matthias Kilian wrote: > Does it > maen that one can't trust *any* package on hackage.haskell.org at > least a little bit (based on trust between acknowledging persons > and reputation) without reviewing the package's source code? Yes, in fact you cannot trust any random code you download from the Internet, Hackage is no exception. Anybody could register and upload a package that runs some `runIO` TemplateHaskell which deletes your entire home directory upon compilation, no matter if they are verified as a human or not. Other programming languages' ecosystems don't solve this problems either; if we want it solved, we should layer a trusted curated package repository on top where all code is reviewed by a set of trusted experts.

1 0

ThEdu'18: Call for Extended Abstracts & Demonstrations
by Achim D. Brucker 23 Feb '18

23 Feb '18

(Apologies for duplicates) Call for Extended Abstracts & Demonstrations ************************************************************************** ThEdu'18 Theorem proving components for Educational software 18 July 2018 http://www.uc.pt/en/congressos/thedu/thedu18 ************************************************************************** at FLoC 2018 Federated Logic Conference 2018 6-19 July 2018 Oxford, UK http://www.floc2018.org/ ************************************************************************** THedu'18 Scope: Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. Invited Talk Julien Narboux, University of Strasbourg, France Important Dates * Extended Abstracts: 15th April 2018 * Author Notification: 15th May 2018 * Workshop Day: 18 July 2018 Topics of interest include: * methods of automated deduction applied to checking students' input; * methods of automated deduction applied to prove post-conditions for particular problem solutions; * combinations of deduction and computation enabling systems to propose next steps; * automated provers specific for dynamic geometry systems; * proof and proving in mathematics education. Submission We welcome submission of extended abstracts and demonstration proposals presenting original unpublished work which is not been submitted for publication elsewhere. All accepted extended abstracts and demonstrations will be presented at the workshop. The extended abstracts will be made available online. Extended abstracts and demonstration proposals should be submitted via easychair, https://easychair.org/conferences/?conf=thedu18 formatted according to http://www.easychair.org/publications/easychair.zip Extended abstracts and demonstration proposals should be approximately 5 pages in length and are to be submitted in PDF format. At least one author of each accepted extended abstract/demonstration proposal is expected to attend THedu'18 and presents his/her extended abstract/demonstration. Program Committee Francisco Botana, University of Vigo at Pontevedra, Spain Roman Hašek, University of South Bohemia, Czech Republic Filip Maric, University of Belgrade, Serbia Walther Neuper, Graz University of Technology, Austria (co-chair) Pavel Pech, University of South Bohemia, Czech Republic Pedro Quaresma, University of Coimbra, Portugal (co-chair) Vanda Santos, CISUC, Portugal Wolfgang Schreiner, Johannes Kepler University, Austria Burkhart Wolff, University Paris-Sud, France Proceedings The extended abstracts and system descriptions will be available in ThEdu'18 Web-page. After presentation at the conference, selected authors will be invited to submit a substantially revised version, extended to 14--20 pages, for publication by the Electronic Proceedings in Theoretical Computer Science (EPTCS). -- Dr. Achim D. Brucker | Software Assurance & Security | University of Sheffield https://www.brucker.ch | https://logicalhacking.com/blog @adbrucker | @logicalhacking

1 0

Re: [Haskell-cafe] [Haskell] ANN: Hackage Account Registration Changes
by Gershom B 23 Feb '18

23 Feb '18

(Replying just on -cafe. The other cc's shouldn't be included in the follow-on discussion to this announcement). A PR to augment links with nofollow tags would be welcome. Note that for completeness this would have to be done in the markdown engine, the package-description rendering engine, _and_ the haddock generation, which are three distinct codepaths. That said, I think that does not suffice, as I do not think the intent of the spam is _just_ to perform search engine optimization. And further, I have seen other cases as well where people are undeterred by SEO-prevention measures. For example, we require manual approval of wiki.haskell.org accounts despite the addition of nofollow tags, as those did not deter spammers in that case. The current policy is not a "direction" we are taking -- it is an interim measure until a better fix can be put in place. There is some discussion of what a "better fix" might look like on an issue on hackage-server: https://github.com/haskell/hackage-server/issues/685 -g On Thu, Feb 22, 2018 at 7:26 PM, Geoffrey Huntley <ghuntley(a)ghuntley.com> wrote: > I feel that this is the wrong direction to take and will add more burden on > people that we shouldn't be adding additional burden to. It's also the wrong > "optics". > > I just had a quick squizz at Hackage with a simple PR you'll be able to > remove the incentives for this behaviour. > > Add "nofollow" to any links supplied by the user or that are rendered as > part of parsing user input. > > https://support.google.com/webmasters/answer/96569?hl=en > > The .NET ecosystem recently went through these same notions for the same > reasons - here's the PR > > https://github.com/NuGet/NuGetGallery/pull/4841/files > > On Fri., 23 Feb. 2018, 10:38 am Matthias Kilian, <kili(a)outback.escape.de> > wrote: >> >> Hi, >> >> On Thu, Feb 22, 2018 at 05:54:33PM -0500, Gershom B wrote: >> > In the meantime, as a short term measure, we have changed new account >> > registration policies on hackage. >> > >> > Users can still register as before, but new users do _not_ have upload >> > rights until they explicitly request them and are granted them by a >> > human being. >> > >> > (This is actually how we had configured hackage to work on initial >> > deployment -- we loosened things up for some years as the extra step >> > seemed unnecessary). >> >> Does this mean that before the todays change, anyone (or anything) >> could register and upload packages without any review and without >> any acknowledgement for trustfulness by another person? Does it >> maen that one can't trust *any* package on hackage.haskell.org at >> least a little bit (based on trust between acknowledging persons >> and reputation) without reviewing the package's source code? >> >> Ciao, >> Kili >> _______________________________________________ >> Haskell mailing list >> Haskell(a)haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell

1 0

ANN: Hackage Account Registration Changes
by Gershom B 22 Feb '18

22 Feb '18

As some people have seen, a spammer has started to create accounts on hackage to upload fake packages, in order to use their package-descriptions for linkspam. We'll be working to clean-up the package-index from this spam, and the accounts have been disabled. Further, we'll need to decide on some long-term changes going forward to make this sort of abuse more difficult. In the meantime, as a short term measure, we have changed new account registration policies on hackage. Users can still register as before, but new users do _not_ have upload rights until they explicitly request them and are granted them by a human being. (This is actually how we had configured hackage to work on initial deployment -- we loosened things up for some years as the extra step seemed unnecessary). Apologies for the inconvenience, but this seemed the most direct way to stop the current influx of spam. Users with existing hackage accounts should encounter no differences in behavior. Best, Gershom

1 0

Re: [Haskell-cafe] Pointer equality for nullary constructors
by David Feuer 22 Feb '18

22 Feb '18

Double-barreled continuations don't seem to work well when you want to abort construction of a recursive structure. Think about Data.HashMap.Strict.insert. We don't really want to have to walk all the way back up to the top if we discover that the value pointer we're inserting is the same as the I've already in the map. On Feb 22, 2018 2:55 PM, "Carter Schonwald" <carter.schonwald(a)gmail.com> wrote: David: i'm inclined to agree with Doug here. Phrased differently: what is the example change in overheads in micro or milliseconds? what is an example tiny program where those overheads are a significant part of program overhead? why woulnd't they use something like https://www.microsoft. com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscont inued.pdf aka the so called "double barrelled cps" transform? On Wed, Feb 21, 2018 at 11:21 PM, David Feuer <david.feuer(a)gmail.com> wrote: > Because sometimes the sanctioned way is inefficient. throwIO always > wraps its exception argument in a SomeException constructor before > calling raiseIO# on the result. That extra baggage is likely enough to > make the implementation I'm considering too slow to bother with, so I > care right now in 2018. I'd very much prefer to get an > officially-approved way to do what I want, but barring that I'll take > one that works. > > On Wed, Feb 21, 2018 at 9:33 AM, Doug McIlroy <doug(a)cs.dartmouth.edu> > wrote: > > > >> > Can I use reallyUnsafePtrEquality# reliably to identify whether a > value is > >> a nullary constructor of a particular type? > > > > Can this "optimization" possibly save enough time to justify > > nonstandard trickery? > > This kind of obscure brittle coding may have been OK 50 years > > ago. But why do it now? > > > > Doug > > _______________________________________________ > > Haskell-Cafe mailing list > > To (un)subscribe, modify options or view archives go to: > > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > > Only members subscribed via the mailman list are allowed to post. > _______________________________________________ > Haskell-Cafe mailing list > To (un)subscribe, modify options or view archives go to: > http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe > Only members subscribed via the mailman list are allowed to post. >

1 1

Pointer equality for nullary constructors
by David Feuer 22 Feb '18

22 Feb '18

Can I use reallyUnsafePtrEquality# reliably to identify whether a value is a nullary constructor of a particular type? For example, if I have data Foo = Foo Can I write isFoo :: a -> Bool isFoo !a = isTrue# (reallyUnsafePtrEquality# a Foo) instead of isFoo :: forall a. Typeable a => a -> Bool isFoo a | Just Refl <- eqTypeRep (typeRep @a) (typeRep @Foo) , Foo <- a = True | otherwise = False The reason I'm asking is because this would let me (potentially) raiseIO# a nullary constructor and then catch# it and see if it was what I was looking for rather than having to open a SomeException to get to an Exception dictionary, open that to get a TypeRep, and then peer inside that to check a Fingerprint. That is, I'd get lighter-weight exceptions that only carry the information I actually need. Thanks, David

4 6

Re: [Haskell-cafe] Pointer equality for nullary constructors
by Doug McIlroy 22 Feb '18

22 Feb '18

> > Can I use reallyUnsafePtrEquality# reliably to identify whether a value is > a nullary constructor of a particular type? Can this "optimization" possibly save enough time to justify nonstandard trickery? This kind of obscure brittle coding may have been OK 50 years ago. But why do it now? Doug

5 5

VerifyThis 2018: Call for Problems and First Announcement
by Andrei Paskevich 21 Feb '18

21 Feb '18

******************************************************************************* VerifyThis Verification Competition 2018 FIRST ANNOUNCEMENT AND CALL FOR PROBLEMS Competition to be held at ETAPS 2018 http://verifythis.ethz.ch ******************************************************************************** Get involved, even if you cannot participate in the competition: provide a challenge. IMPORTANT DATES Submission deadline: March 9, 2018 Competition: April 14 and 15, 2018 CALL FOR PROBLEMS To extend the problem pool, we are now soliciting algorithms and data structures which could contribute interesting verification challenges for the VerifyThis program verification competition (itself introduced below). We encourage suggestions at any level of detail, in particular submissions without a fully worked out verification task. - a problem may contain an informal statement of the algorithm to be implemented (optionally with complete or partial pseudocode) and the requirement(s) to be verified - a problem should be suitable for a 60-90 minute time slot - submission of reference solutions is welcome but not mandatory - problems with an inherent language- or tool-specific bias should be clearly identified as such - problems that contain several subproblems or other means of difficulty scaling are especially welcome - the organizers reserve the right (but no obligation) to use the problems in the competition, either as submitted or with modifications - submissions from (potential) competition participants are allowed Problems from previous competitions can be seen at http://verifythis.ethz.ch Submissions are to be sent by email to verifythis(a)cs.nuim.ie by the date indicated above. PRIZES The most suitable submission for competition will receive a prize. ABOUT VerifyThis 2018 will take place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2018) on April 14 and 15, 2018. It is the 7th event in the VerifyThis competition series. Information on previous events and participants can be found at http://verifythis.ethz.ch The aims of the competition are: - to bring together those interested in formal verification, and to provide an engaging, hands-on, and fun opportunity for discussion - to evaluate the usability of logic-based program verification tools in a controlled experiment that could be easily repeated by others. The competition will offer a number of challenges presented in natural language. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification. There are no restrictions on the programming language and verification technology used. The correctness properties posed in problems will have the input-output behaviour of programs in focus. Solutions will be judged for correctness, completeness and elegance. ORGANIZERS * Marieke Huisman, University of Twente, the Netherlands * Rosemary Monahan, Maynooth University, Ireland * Peter Müller, ETH Zürich, Switzerland * Andrei Paskevich, Paris-Sud University, France * Gidon Ernst, National Institute of Informatics Tokyo, Japan CONTACT Email: verifythis(a)cs.nuim.ie Web: http://verifythis.ethz.ch

1 0