- Haskell-Cafe - Haskell.org

using scoped type variables in proofs...
by Nicholls, Mark 11 May '15

11 May '15

Hello, I have written the below proof as an exercise. I want to explicitly annotate the proof with type variables.....but I cant get a line to work... > {-# LANGUAGE DataKinds #-} > {-# LANGUAGE ExplicitForAll #-} > {-# LANGUAGE FlexibleContexts #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE GADTs #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE PolyKinds #-} > {-# LANGUAGE StandaloneDeriving #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE UndecidableInstances #-} > {-# LANGUAGE ScopedTypeVariables #-} > import Prelude hiding (head, tail, (++), (+), replicate) > import qualified Prelude as P > data Nat where > Z :: Nat > S :: Nat -> Nat > data SNat (a :: Nat) where > SZ :: SNat 'Z > SS :: SNat a -> SNat ('S a) here a nice plus > type family (n :: Nat) :+ (m :: Nat) :: Nat > type instance Z :+ m = m > type instance (S n) :+ m = S (n :+ m) lets try to do > data val1 :== val2 where > Refl :: val :== val If I prove its abelian then we get it... the "proof" works if we remove the type annotation but I want the annotation to convince myself I know whats going on. > theoremPlusAbelian :: SNat a -> SNat b -> (a :+ b) :== (b :+ a) > theoremPlusAbelian (SZ :: SNat a) (SZ :: SNat b) = > -- forall 0 and 0 > (Refl :: (a :+ b) :== (b :+ a)) > theoremPlusAbelian ((SS a) :: SNat a) (SZ :: SNat b) = > -- forall a + 1 and 0 > case theoremPlusAbelian (a :: (a ~ 'S a1) => SNat a1) (SZ :: SNat b) of > (Refl :: (a1 :+ b) :== (b :+ a1)) -> > (Refl :: (a :+ b) :== (b :+ a)) > theoremPlusAbelian (SZ :: SNat a) ((SS a) :: SNat b) = > -- forall 0 and a + 1 > case theoremPlusAbelian (SZ :: SNat a) (a :: (b ~ 'S b1) => SNat b1) of > (Refl :: (a :+ b1) :== (b1 :+ a)) -> > (Refl :: (a :+ b) :== (b :+ a)) > -- cant seem to prove this... > theoremPlusAbelian ((SS a) :: (SNat a)) ((SS b) :: (SNat b)) = > -- forall a+1 and b+1 > -- 1st prove (a + 1) + b = b + (a + 1)...from above > case theoremPlusAbelian ((SS a) :: (SNat a)) (b :: (b ~ 'S b1) => SNat b1) of THE COMMENTED LINE FAILS. Could not deduce ((b1 :+ 'S a1) ~ (a2 :+ 'S a1)) from the context (a ~ 'S a1) bound by a pattern with constructor SS :: forall (a :: Nat). SNat a -> SNat ('S a), in an equation for 'theoremPlusAbelian' at Cafe2.lhs:57:24-27 or from (b ~ 'S a2) bound by a pattern with constructor SS :: forall (a :: Nat). SNat a -> SNat ('S a), in an equation for 'theoremPlusAbelian' at Cafe2.lhs:57:45-48 NB: ':+' is a type function, and may not be injective The type variable 'b1' is ambiguous Expected type: (a :+ a2) :== (a2 :+ a) Actual type: (a :+ b1) :== (b1 :+ a) Relevant bindings include b :: SNat a2 (bound at Cafe2.lhs:57:48) a :: SNat a1 (bound at Cafe2.lhs:57:27) In the pattern: Refl :: (a :+ b1) :== (b1 :+ a) In a case alternative: (Refl :: (a :+ b1) :== (b1 :+ a)) -> case theoremPlusAbelian a (SS b) of { Refl -> case theoremPlusAbelian a b of { Refl -> Refl } } In the expression: case theoremPlusAbelian ((SS a) :: SNat a) (b :: b ~ S b1 => SNat b1) of { (Refl :: (a :+ b1) :== (b1 :+ a)) -> case theoremPlusAbelian a (SS b) of { Refl -> case theoremPlusAbelian a b of { Refl -> ... } } } > -- (Refl :: (a :+ b1) :== (b1 :+ a)) -> > Refl -> > -- now prove a + (b + 1) = (b + 1) + a...from above > case theoremPlusAbelian a (SS b) of > Refl -> > -- now prove a + b = b + a > case theoremPlusAbelian a b of > -- which seems to have proved a + b = b + a > Refl -> Refl CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.

3 4

New Functional Programming Job Opportunities
by Functional Jobs 11 May '15

11 May '15

Here are some functional programming job opportunities that were posted recently: Haskell Web Engineer at Front Row Education http://functionaljobs.com/jobs/8823-haskell-web-engineer-at-front-row-educa… Sr. Software Engineer at McGraw-Hill Education http://functionaljobs.com/jobs/8822-sr-software-engineer-at-mcgraw-hill-edu… Cheers, Sean Murphy FunctionalJobs.com

1 0

FFI nested structs - malloc - free
by Proclivis 11 May '15

11 May '15

FFI Gurus, I created a c2hs FFI of a nested C structure, where struct A has a pointer to a struct B. To do so, I used a malloc, but I am unsure if the memory will be freed when the resulting Ptr is freed. The example at this link uses the same technique, so it will serve as an example. https://github.com/ifesdjeen/haskell-ffi-tutorial/blob/master/src/Example.h… Line 48 and 51 do the malloc and assign the pointer in the struct, from inside a Storable poke implementation. But, there is no explicit free, nor a finalizer. Will the memory be freed when the Ptr of the Storable is freed? If it is, it implies that some magic keeps track of mallocs inside a poke, and creates finalizers. Or, this example leaks. If it leaks, how do I create a finalizer from inside a poke implementation? Mike

5 8

First Call for Papers for IFL 2015
by publicityifl＠gmail.com 10 May '15

10 May '15

Hello, Please, find below the first call for papers for IFL 2015. Please forward these to anyone you think may be interested. Apologies for any duplicates you may receive. best regards, Jurriaan Hage Publicity Chair of IFL --- IFL 2015 - Call for papers 27th SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES - IFL 2015 University of Koblenz-Landau, Koblenz, Germany In cooperation with ACM SIGPLAN September 14-16, 2015 http://ifl2015.wikidot.com/ Scope The goal of the IFL symposia is to bring together researchers actively engaged in the implementation and application of functional and function-based programming languages. IFL 2015 will be a venue for researchers to present and discuss new ideas and concepts, work in progress, and publication-ripe results related to the implementation and application of functional languages and function-based programming. Peer-review Following the IFL tradition, IFL 2015 will use a post-symposium review process to produce the formal proceedings. All participants of IFL2015 are invited to submit either a draft paper or an extended abstract describing work to be presented at the symposium. At no time may work submitted to IFL be simultaneously submitted to other venues; submissions must adhere to ACM SIGPLAN's republication policy: http://www.sigplan.org/Resources/Policies/Republication The submissions will be screened by the program committee chair to make sure they are within the scope of IFL, and will appear in the draft proceedings distributed at the symposium. Submissions appearing in the draft proceedings are not peer-reviewed publications. Hence, publications that appear only in the draft proceedings do not count as publication for the ACM SIGPLAN republication policy. After the symposium, authors will be given the opportunity to incorporate the feedback from discussions at the symposium and will be invited to submit a revised full article for the formal review process. From the revised submissions, the program committee will select papers for the formal proceedings considering their correctness, novelty, originality, relevance, significance, and clarity. Important dates August 10: Submission deadline draft papers August 12: Notification of acceptance for presentation August 14: Early registration deadline August 21: Late registration deadline September 7: Submission deadline for pre-symposium proceedings September 14-16: IFL Symposium December 1: Submission deadline for post-symposium proceedings January 15, 2016: Notification of acceptance for post-symposium proceedings March 1, 2016: Camera-ready version for post-symposium proceedings Submission details Prospective authors are encouraged to submit papers or extended abstracts to be published in the draft proceedings and to present them at the symposium. All contributions must be written in English. Papers must adhere to the standard ACM two columns conference format. For the pre-symposium proceedings we adopt a 'weak' page limit of 12 pages. For the post-symposium proceedings the page limit of 12 pages is firm. A suitable document template for LaTeX can be found at: http://www.acm.org/sigs/sigplan/authorInformation.htm Authors submit through EasyChair: https://easychair.org/conferences/?conf=ifl2015 Topics IFL welcomes submissions describing practical and theoretical work as well as submissions describing applications and tools in the context of functional programming. If you are not sure whether your work is appropriate for IFL 2015, please contact the PC chair at rlaemmel(a)acm.org. Topics of interest include, but are not limited to: - language concepts - type systems, type checking, type inferencing - compilation techniques - staged compilation - run-time function specialization - run-time code generation - partial evaluation - (abstract) interpretation - metaprogramming - generic programming - automatic program generation - array processing - concurrent/parallel programming - concurrent/parallel program execution - embedded systems - web applications - (embedded) domain specific languages - security - novel memory management techniques - run-time profiling performance measurements - debugging and tracing - virtual/abstract machine architectures - validation, verification of functional programs - tools and programming techniques - (industrial) applications Peter Landin Prize The Peter Landin Prize is awarded to the best paper presented at the symposium every year. The honored article is selected by the program committee based on the submissions received for the formal review process. The prize carries a cash award equivalent to 150 Euros. Programme committee Chair: Ralf Lämmel, University of Koblenz-Landau, Germany - Malgorzata Biernacka, University of Wroclaw, Poland - Laura M. Castro, University of A Coruña, Spain - Martin Erwig, Oregon State University, USA - Dan Ghica, University of Birmingham, UK - Andrew Gill, University of Kansas, USA - Stephan Herhut, Google, USA - Zhenjiang Hu, National Institute of Informatics (NII), Japan - Mauro Jaskelioff, CIFASIS/Universidad Nacional de Rosario, Argentina - Frédéric Jouault, ESEO, France - Oleg Kiselyov, Tohoku University, Japan - Lindsey Kuper, Indiana University, USA - Rita Loogen, Philipps-Universität Marburg, Germany - Akimasa Morihata, University of Tokyo, Japan - Atsushi Ohori, Tohoku University, Japan - Bruno C. D. S. Oliveira, The University of Hong Kong, Hong Kong - Frank Piessens, Katholieke Universiteit Leuven, Belgium - Norman Ramsey, Tufts University, USA - Matthew Roberts, Macquarie University, Australia - Manfred Schmidt-Schauss, Goethe-University Frankfurt, Germany - Simon Thompson, University of Kent, UK - Stephanie Weirich, University of Pennsylvania, USA - Steve Zdancewic, University of Pennsylvania , USA Venue The 27th IFL will be held in association with the Faculty of Computer Science, University of Koblenz-Landau, Campus Koblenz. Koblenz is well connected by train to several international airports. For instance, Koblenz can be reached from Frankfurt by high-speed train ICE within an hour. The modern Koblenz campus is close to the city center and can be reached by foot, bus, or cab. See the website for more information on the venue.

1 0

Automatic liftIO or how to write this shorter?
by Gleb Popov 10 May '15

10 May '15

Hello haskell-cafe@ I'm writing a GUI app in Haskell and bindings to the widget toolkit i'm using in parallel. These bindings are very simple and all its functions have return type (IO something). So far so good, i wrote the following code to create an config window: createConfigUI root = do box <- Box.add root -- first field addToPackEnd box =<< do f <- Fr.add box setPartText f Nothing "E-mail" setPartContent f Nothing =<< do box <- Box.add box addToPackEnd box =<< do e <- Ent.add box Ent.singleLineSet e True -- Here onEvent "changed,user" e $ do reactOnUserInput e objectShow e return e objectShow box return box objectShow f return f -- next field addToPackEnd box =<< do ... Initially, i was quite satisfied with flipped bind use for creating UI elements and arranging them. Nested do scopes allow copypasting code without renaming variables and also provide some visual representation on widget hierarchy. But at some point i need to return some stuff from some inner do block into outmost. For example, at the line with comment "Here" i defined let setText t = entrySet e t and wanted to return it from whole createConfigUI action. Moreover, createConfigUI have much more fields, for each of them i want to do the same. My initial thought was to wrap everything with runWriter and just call tell setText wherever i want to gather all setter functions into a list, but i can't do this because i would need to put liftIO before every IO action all over the place. If only there was i way to turn an (IO a) into (MonadIO m => m a), it would be easy. Another solution is to make my bindings return (MonadIO m => m a). This would be equal effort of plugging liftIO's everywhere, but at least it would be hidden from user of bindings. I'd gone this way, but looked at gtk bindings first and found that (IO a) is used there. So, my questions are: 1. What would you recommend in my situation? Is it possible yield values from inner do blocks into outer without much hassle? 2. If there is nothing wrong with switching bindings from (IO a) to MonadIO typeclass, why not to do this for gtk, wxWidgets and nearly every FFI binding? Thanks in advance.

2 3

[ANN] servant 0.4.0 released (+new website)
by Alp Mestanogullari 10 May '15

10 May '15

Hello everyone, We're happy to announce the releases of: - servant 0.4.0 - servant-server 0.4.0 - servant-client 0.4.0 - servant-jquery 0.4.0 - servant-docs 0.4.0 - servant-blaze 0.4.0 - servant-lucid 0.4.0 to Hackage. As well as a new website, same URL as before: http://haskell-servant.github.io/ -- which features a tutorial that's much more informative than the getting started we had for the previous version. The tutorial is available at http://haskell-servant.github.io/tutorial The highlights for this release are: - Multiple content-types support (with servant-blaze and servant-lucid offering a way to encode data for the HTML content type) - Handlers in other monads than `EitherT` - Response headers support - Safe links to endpoints - Saner types for aborting early in request handlers (the `Left` branch in `EitherT`) For more details about the new features, please read the release post: http://haskell-servant.github.io/posts/2015-05-10-servant-0.4-released.html Cheers -- Alp Mestanogullari

1 0

How to estimate number of downloads of GHC or Haskell Platform?
by nr＠cs.tufts.edu 09 May '15

09 May '15

For a review, I'm trying to get a rough estimate of how many times GHC or the Haskell Platform have been downloaded. Although I'm sure I've seen this information graphed over time at workshops, my web-search skills are not turning up anything. I'd be quite happy to get an estimate to within a factor of ten. Can anyone suggest any sources, or a good way to estimate this number? Norman

3 2

Using ClassyPrelude to handle either Text or ByteString
by Mike Meyer 08 May '15

08 May '15

Ok, I can't seem to figure out how to make this work, and since I'm using ClassyPrelude (from classy-prelude, latest version on hackage as of yesterday), I think cafe is a better place to ask than beginners. Sorry if this should have gone there. I want to read in a list of files, concatenate them, and then run the resulting data through a "process" function. So far, no problem. Given an opts record that contains the list of files and some control for the process function, this expression works: hPut stdout =<< process opts . concat <$> mapM (readFile . fpFromString) (files opts) (BTW, recommendations on cleaning that up gratefully accepted) However, I'd like to be able to read them all as either Text or ByteString, depending on options being passed to me. This doesn't work so well. If I give process a type of Text -> Text or ByteString->ByteString, everything works fine with no other changes. However, any attempt to make it polymorphic fails with ambiguous type warnings. I've tried a slew of things, and found a few that work. But none of them are what I'd call good, much less elegant. Is there a good way to do this?

2 1

Re: [Haskell-cafe] RFC: "Native -XCPP" Proposal
by Herbert Valerio Riedel 08 May '15

08 May '15

Hello Christian, (I've re-CC'ed haskell-cafe, assuming this wasn't deliberate) On 2015-05-08 at 09:50:46 +0200, Christian Maeder wrote: > using cpphs is the right way to go! > > Rewriting it from scratch may be a good exercise but is (essentially) a > waste of time. > > However, always asking Malcolm to get source changes into cpphs would > be annoying. > > Therefore it would be great if the sources were just part of the ghc > sources (under git). > > Another "problem" might be the dependency "polyparse" that is currently > not part of the core libraries. A scheme was actually discussed privately to address this: We certainly don't want to expose cpphs/polyparse (and text!) as new packages in GHC's global pkg-db. Which we'd end up, if we handled cpphs as the other exposed boot libraries. Therefore we'd only use the few relevant modules from cpphs/polyparse as "other-modules" (i.e. internal hidden dependencies -- i.e. we wouldn't use cpphs/polyparse's .cabal files) compiled into GHC, but not exposed. We'd either create a new Git submodule to hold our "fork" of cpphs/polyparse, or just add it somewhere inside ghc.git > (I guess that replacing polyparse by something else would also be a nice > exercise.) > > So (for me) the only question is, if Malcolm is willing to transfer > control over cpphs to the haskell-community (or ghc head) - of course > with due acknowledgements! I don't think this will be necessary, as we don't need the cpphs-upstream to mirror each modifications immediately. The benefit of the scheme described above is that we'd be somewhat decoupled from cpphs' upstream, and can freely experiment in our "fork", and can sync up with Malcolm from time to time to merge improvements in both directions. -- hvr

4 5

status of deb.haskell.org?
by Jeremy 08 May '15

08 May '15

The haskell status page says that deb.haskell.org has been down since mid-February. Are there any plans to bring it back up? -- View this message in context: http://haskell.1045720.n5.nabble.com/status-of-deb-haskell-org-tp5768430.ht… Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

3 3