April 2016 - Haskell-Cafe

Are libraries expected to enforce safe usage of thread-unsafe functions?
by Thomas Koster 12 Apr '16

12 Apr '16

Hi friends, I am writing a library that has Handle-like values for resources that are not thread-safe (foreign state from a non-thread-safe C library). In other words, a resource can only be "used" by one Haskell thread at a time. Unless I take steps, if one shares the resource between concurrent Haskell threads, bad things will happen at runtime (even with a single-threaded runtime). Naturally, I want consumers to use my library safely, so I am considering making it safe for all by pessimistically enforcing safe usage with MVars. Is it common/expected that Haskell libraries enforce safe access like this? MVars are not free from cost, but are they cheap (i.e. almost as fast as no forced synchronization) as long as no blocking/rescheduling occurs? Thanks, -- Thomas Koster

2 2

Is it safe to postulate () has one inhabitant?
by David Feuer 12 Apr '16

12 Apr '16

The () kind has infinitely many inhabitants: the type '() and any stuck or looping types with appropriate kinds. However, I've not been able to find a way to break type safety with the postulate unitsEqual :: (a :: ()) :~: (b :: ()) in GHC 7.10.3 (it was possible using a now-rejected data family in 7.8.3). Is there some way I haven't found yet, or is this safe? If it's *not* safe, is the equivalent postulate using Void instead of () safe? For my purposes, () would be nicer, but it feels riskier.

4 4

Emacs (was stack and the Atom editor)
by Rustom Mody 12 Apr '16

12 Apr '16

On Sun, Apr 10, 2016 at 7:29 AM, Thomas Koster <tkoster(a)gmail.com> wrote: > > If I can't make Atom work for me, I will drop it just as fast as I > dropped Emacs. Spacemacs was suggested to me off-list; if it addresses > my complaints about Emacs, I might give it a chance. But Atom is the > topic of this thread, so lest this thread descend into a text editor > flame war, I suggest we stop talking about Emacs (or Vim, or Eclipse, > or anything else). > > [Note the changed subject line :-) ] Ive been having a great deal of confusion/trouble with emacs haskell-mode of late. No this is not a gripe about haskell-mode Just that I find myself confused over 1. The old comint interface and new λ one -- when does which kick in 2. Basic setups -- is it called haskell-mode/haskell-emacs or what? 3. I dont quite know when things stopped working/being comfortable/familiar but I remember it as having nothing to do with haskell -- updating org mode or some such Just that I am supposed to be (at least out here!!) an emacs and haskell expert and while showing others how to get started I am often finding my own setups embarrassingly broken Any tips for an old emacs-geezer?

4 14

Re: [Haskell-cafe] Emacs (was stack and the Atom editor)
by Johannes Waldmann 12 Apr '16

12 Apr '16

> ... failed experiments like code folding So, what *is* the recommended method for folding (in emacs)? Yes, ideally we don't need this, because we do not write deeply nested code. But then we have a lot of top-level declarations, which I still want to fold. Yes, if there are too many declarations in one module, then this should be split. But still, that whole mess of declarations needs to be navigated, no matter how it's mapped to files (modules). The question is how it's mapped to the screen real estate. - J.W.

1 0

[TFP 2016] extended deadline, april 25 2016, final call for papers
by Peter Achten 12 Apr '16

12 Apr '16

TFP 2016 has extended its deadline for draft papers by two weeks (now April 25). Although all draft papers accepted to TFP 2016 will be invited to submit to the post-symposium formal proceedings, authors are reminded that they are not obligated to do so; we welcome works in progress that may not be destined for the TFP proceedings. Thanks, David Van Horn ----------------------------- C A L L F O R P A P E R S ----------------------------- ======== TFP 2016 =========== 17th Symposium on Trends in Functional Programming June 8-10, 2016 University of Maryland, College Park Near Washington, DC http://tfp2016.org/ The symposium on Trends in Functional Programming (TFP) is an international forum for researchers with interests in all aspects of functional programming, taking a broad view of current and future trends in the area. It aspires to be a lively environment for presenting the latest research results, and other contributions (see below). Authors of draft papers will be invited to submit revised papers based on the feedback receive at the symposium. A post-symposium refereeing process will then select a subset of these articles for formal publication. TFP 2016 will be the main event of a pair of functional programming events. TFP 2016 will be accompanied by the International Workshop on Trends in Functional Programming in Education (TFPIE), which will take place on June 7nd. == INVITED SPEAKERS == TFP 2016 is pleased to announce keynote talks by the following two invited speakers: * Ronald Garcia, University of British Columbia: "Static and Dynamic Type Checking: A Synopsis" * Steve Zdancewic, University of Pennsylvania: "Type- and Example-Driven Program Synthesis" == HISTORY == The TFP symposium is the heir of the successful series of Scottish Functional Programming Workshops. Previous TFP symposia were held in * Edinburgh (Scotland) in 2003; * Munich (Germany) in 2004; * Tallinn (Estonia) in 2005; * Nottingham (UK) in 2006; * New York (USA) in 2007; * Nijmegen (The Netherlands) in 2008; * Komarno (Slovakia) in 2009; * Oklahoma (USA) in 2010; * Madrid (Spain) in 2011; * St. Andrews (UK) in 2012; * Provo (Utah, USA) in 2013; * Soesterberg (The Netherlands) in 2014; * and Inria Sophia-Antipolis (France) in 2015. For further general information about TFP please see the TFP homepage. (http://www.tifp.org/) == SCOPE == The symposium recognizes that new trends may arise through various routes. As part of the Symposium's focus on trends we therefore identify the following five article categories. High-quality articles are solicited in any of these categories: Research Articles: leading-edge, previously unpublished research work Position Articles: on what new trends should or should not be Project Articles: descriptions of recently started new projects Evaluation Articles: what lessons can be drawn from a finished project Overview Articles: summarizing work with respect to a trendy subject Articles must be original and not simultaneously submitted for publication to any other forum. They may consider any aspect of functional programming: theoretical, implementation-oriented, or experience-oriented. Applications of functional programming techniques to other languages are also within the scope of the symposium. Topics suitable for the symposium include, but are not limited to: Functional programming and multicore/manycore computing Functional programming in the cloud High performance functional computing Extra-functional (behavioural) properties of functional programs Dependently typed functional programming Validation and verification of functional programs Debugging and profiling for functional languages Functional programming in different application areas: security, mobility, telecommunications applications, embedded systems, global computing, grids, etc. Interoperability with imperative programming languages Novel memory management techniques Program analysis and transformation techniques Empirical performance studies Abstract/virtual machines and compilers for functional languages (Embedded) domain specific languages New implementation strategies Any new emerging trend in the functional programming area If you are in doubt on whether your article is within the scope of TFP, please contact the TFP 2016 program chair, David Van Horn. == BEST PAPER AWARDS == To reward excellent contributions, TFP awards a prize for the best paper accepted for the formal proceedings. TFP traditionally pays special attention to research students, acknowledging that students are almost by definition part of new subject trends. A student paper is one for which the authors state that the paper is mainly the work of students, the students are listed as first authors, and a student would present the paper. A prize for the best student paper is awarded each year. In both cases, it is the PC of TFP that awards the prize. In case the best paper happens to be a student paper, that paper will then receive both prizes. == SPONSORS == TFP is financially supported by CyberPoint, Galois, Trail of Bits, and the University of Maryland Computer Science Department. == PAPER SUBMISSIONS == Acceptance of articles for presentation at the symposium is based on a lightweight peer review process of extended abstracts (4 to 10 pages in length) or full papers (20 pages). The submission must clearly indicate which category it belongs to: research, position, project, evaluation, or overview paper. It should also indicate which authors are research students, and whether the main author(s) are students. A draft paper for which ALL authors are students will receive additional feedback by one of the PC members shortly after the symposium has taken place. We use EasyChair for the refereeing process. Papers must be submitted at: https://easychair.org/conferences/?conf=tfp2016 Papers must be written in English, and written using the LNCS style. For more information about formatting please consult the Springer LNCS web site: http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0 == IMPORTANT DATES == Submission of draft papers: April 25, 2016 Notification: May 2, 2016 Registration: May 13, 2016 TFP Symposium: June 8-10, 2016 Student papers feedback: June 14, 2016 Submission for formal review: July 14, 2016 Notification of acceptance: September 14, 2016 Camera ready paper: October 14, 2016 == PROGRAM COMMITTEE == Amal Ahmed Northeastern University (US) Nada Amin École Polytechnique Fédérale de Lausanne (CH) Kenichi Asai Ochanomizu University (JP) Małgorzata Biernacka University of Wroclaw (PL) Laura Castro University of A Coruña (ES) Ravi Chugh University of Chicago (US) Silvia Ghilezan University of Novi Sad (SR) Clemens Grelck University of Amsterdam (NL) John Hughes Chalmers University of Technology (SE) Suresh Jagannathan Purdue University (US) Pieter Koopman Radboud University Nijmegen (NL) Geoffrey Mainland Drexel University (US) Chris Martens University of California, Santa Cruz (US) Jay McCarthy University of Massachusetts, Lowell (US) Heather Miller École Polytechnique Fédérale de Lausanne (CH) Manuel Serrano INRIA, Sophia-Antipolis (FR) Scott Smith Johns Hopkins University (US) Éric Tanter University of Chile (CL) David Van Horn (Chair) University of Maryland (US) Niki Vazou University of California, San Diego (US) Stephanie Weirich University of Pennsylvania (US)

1 0

Haskell DockerHub Official Repository: Needs Maintainer TLC
by Peter Salvatore 12 Apr '16

12 Apr '16

Greetings, I have a confession to make: I've been a neglectful maintainer of the "haskell" Official Repository on DockerHub. I'm hoping to find a proper maintainer who is both a Docker nerd and a Haskell enthusiast to ensure that it is kept up to date and improved over time. Bonus points for someone involved in GHC development, or at an organization that is heavily involved in the Haskell community. I'm happy to help you get up to speed with where the image is at today and how to effectively submit future iterations after you've had a chance to review the DockerHub Official Repositories documentation at https://docs.docker.com/docker-hub/official_repos/. The current Dockerfiles are located at https://github.com/freebroccolo/docker-haskell and there are two other maintainers who also contribute occasionally. Thanks,

2 1

Re: [Haskell-cafe] Is it safe to postulate () has one inhabitant?
by David Feuer 11 Apr '16

11 Apr '16

Great. My aim is to convert a poly-kinded implementation, s, of type-aligned sequences into an implementation of regular sequences by using newtype AsUnitLoop a (x :: ()) (y :: ()) = UL a newtype Lower s a = Lower' (s (AsUnitLoop a) '() '()) Using the postulate, I can "prove" that s (AsUnitLoop a) x y ~ s (AsUnitLoop a) '() '() So when I take the tail/init of a sequence I will again get a sequence, and two sequences holding values of the same type can be concatenated. The original reflection-without-remorse code uses data AsUnitLoop a (x :: *) (y :: *) where UL : a -> AsUnitLoop a () () which adds an extra constructor to each cell. With the postulate, I get what I want for free. I'm *hoping* it's possible to use a pattern synonym, Lower, that converts s (AsUnitLoop a) '() '() (requiring '()) to Lower s a but that provides only exists x y . s (AsUnitLoop a) x y when matching. This way, the postulate won't "leak" to other code unless it imports a Postulate module. Unfortunately, the pattern synonym documentation is a bit vague on types. On Apr 11, 2016 8:49 PM, "Richard Eisenberg" <eir(a)cis.upenn.edu> wrote: I believe this is safe, yes. Saying the kind () has infinitely many types in it is somewhat like saying the type () has infinitely many terms in it, like (), undefined, undefined 1, undefined False, ... With the change to type families in the past few years, it should be impossible to match on any inhabitant of the kind () except the type '(). That makes the postulate you postulate quite sensible. Richard On Apr 11, 2016, at 4:07 PM, David Feuer <david.feuer(a)gmail.com> wrote: The () kind has infinitely many inhabitants: the type '() and any stuck or looping types with appropriate kinds. However, I've not been able to find a way to break type safety with the postulate unitsEqual :: (a :: ()) :~: (b :: ()) in GHC 7.10.3 (it was possible using a now-rejected data family in 7.8.3). Is there some way I haven't found yet, or is this safe? If it's *not* safe, is the equivalent postulate using Void instead of () safe? For my purposes, () would be nicer, but it feels riskier. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe(a)haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

1 0

Differences between QuasiQuotes and TemplateHaskell
by Dominik Bollmann 11 Apr '16

11 Apr '16

Hi, Originally, I thought that QuasiQuotes build on top of TemplateHaskell, since they just provide a way of parsing a string into a Template Haskell AST. That is, a quasi-quoter is defined by four parsers of types String -> Q Exp String -> Q Pat String -> Q Type String -> Q Dec that parse EDSLs into corresponding Haskell (abstract) syntax. However, while playing around with the Shakespeare package's quasiquoter hamlet, I noticed that (e.g.) a snippet html = [hamlet| <html> <body> <h1>Hello World |] () has type Html and not (as I would expect) Q Exp. Hence, it seems as if quasiquotes are spliced in implicitly? This confuses me since in Template Haskell in general a quote (e.g.,) [e| \x -> x |] has type Q Exp, which then needs to be explicitly spliced in order to produce the id function \x -> x. So why do quasiquotes not have types Q Exp, but rather concrete types? If anyone could clarify my confusion, this would be great! Dominik.

2 1

MPTC and quantification in GADTs vs. regular ADTs
by Kosyrev Serge 11 Apr '16

11 Apr '16

Good day folks! What is the explanation for the difference in GHC reaction towards the two variants of the following piece of code: > {-# LANGUAGE GADTs #-} > {-# LANGUAGE RankNTypes #-} > {-# LANGUAGE RecordWildCards #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE UnicodeSyntax #-} > > import Prelude.Unicode > > class MPTC row col where > class TC a where > method ∷ a → a > 1 data T row col where 1 T ∷ ∀ row col. MPTC row col ⇒ 1 { col ∷ col 1 , row ∷ row } → T row col 2 data T row col 2 = ∀ row col. MPTC row col ⇒ 2 T { col ∷ col 2 , row ∷ row } > > instance MPTC row col ⇒ TC (T row col) where > method w@T{..} = > seq (recover (toCol w) row) w > > toCol ∷ MPTC row col ⇒ T row col → col > toCol = (⊥) > > recover ∷ MPTC row col ⇒ col → row → T row col > recover = T Note the missing > instance MPTC row col Nevertheless, the former typechecks, while the latter is rejected with: > mptc-data-vs-gadt.hs:23:14-34: error: … > • Could not deduce (MPTC row1 col) arising from a use of ‘recover’ > from the context: MPTC row col > bound by the instance declaration > at mptc-data-vs-gadt.hs:21:10-38 > or from: MPTC row1 col1 > bound by a pattern with constructor: > T :: forall row col row col. > MPTC row col => > col -> row -> T row col, > in an equation for ‘method’ > at mptc-data-vs-gadt.hs:22:14-18 > Possible fix: > add (MPTC row1 col) to the context of the data constructor ‘T’ > • In the expression: (recover (toCol w) row) > In the expression: seq (recover (toCol w) row) w > In an equation for ‘method’: > method w@(T {..}) = seq (recover (toCol w) row) w I'm sure this must have something to do with GADTs carrying type equality constraints, but still I don't quite understand the difference in interpretation of the forall quantification. To my understanding, a value bound by the pattern 'w@T{..}' ought to be treated as sufficient evidence for 'MPTC row col', no matter whether it is a GADT or not. ..but it isn't. -- с уважениeм / respectfully, Косырев Сергей

2 1

C2HS - marchalling arrays
by Alexey Raga 10 Apr '16

10 Apr '16

Hi, I am using c2hs and I want to create bindings for a C function with the following signature: my_function(my_struct_t*, int* values, size_t num_values); Ideally I'd like to have a function that accepts [CInt], not a pair (pointer, size). What is the easiest way to do it? Can c2hs help me with this or I need to do it manually? Regards, Alexey.

1 0