[Haskell-cafe] %==%, :==: and type equality in the singletons library
Hello, from the output of -ddump-splices I dont think it is the case but I'm asking anyway: is there any way to deduce a ~ b from a :==: b? Given data T = C1 | ... | Cn I can easily derive data EqT :: T - T - * where EqT :: a ~ b = EqT a b eqT :: ST a - ST b - Maybe (EqT a b) eqT SC1 SC1 = Just EqT ... eqT SCn SCn = Just EqT eqT _ _ = Nothing but this kind of replicates the boilerplate generated by the singletons library for %==%. However I can't see how to leverage %==% to inhabit eqT since I can't deduce a ~ b from a %==% b == STrue. Any idea? If there's no way to write eqT using what singletons generates, wouldn't it make sense for it to generate something that relates :==: and ~ ? Cheers, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] %==%, :==: and type equality in the singletons library
On Mon, Apr 8, 2013 at 9:59 PM, Richard Eisenberg e...@cis.upenn.edu wrote: On Apr 8, 2013, at 3:12 PM, Paul Brauner polux2...@gmail.com wrote: from the output of -ddump-splices I dont think it is the case but I'm asking anyway: is there any way to deduce a ~ b from a :==: b? Not easily. You would have to write a (potentially recursive) function that explicitly matches singleton constructors, similarly to what you wrote. (You could say that this function is a (potentially inductive) proof that the generated definition of :==: is correct.) Ok. I agree that this is boilerplate and could easily be generated. I've added it to the list of features to be included in the next version of singletons. I'm surprised myself that it hasn't occurred to me to include this before. Great! Paul Richard ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pattern matching with singletons
Very helpful, thanks! I may come back with more singleton/type families
questions :)
On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg e...@cis.upenn.eduwrote:
Hello Paul,
- Forwarded message from Paul Brauner polux2...@gmail.com -
snip
- is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
SLeft, ... (in which case GHC could infer it but for some reason can't)
- or are these pattern + definitions not sufficient to prove that a
~ ('CC ('Left 'CA)) no matter what?
The first one. GHC can deduce that (a ~ ('CC ('Left b))), for some fresh
variable (b :: TA), but it can't yet take the next step and decide that,
because TA has only one constructor, b must in fact be 'CA. In type-theory
lingo, this deduction is called eta-expansion. There have been on-and-off
debates about how best to add this sort of eta-expansion into GHC, but all
seem to agree that it's not totally straightforward. For example, see GHC
bug #7259. There's a non-negligible chance I will be taking a closer look
into this at some point, but not for a few months, so don't hold your
breath. I'm not aware of anyone else currently focusing on this problem
either, I'm afraid.
I'm glad you're finding use in the singletons package! Let me know if I
can be of further help.
Richard
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Pattern matching with singletons
Hello,
the following programs seems to hit either some limitation of GHC or maybe
I'm just missing something and it behaves the intended way.
{-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds, GADTs #-}
module Test where
import Data.Singletons
data TA = CA
data TB = CB
data TC = CC (Either TA TB)
$(genSingletons [''TA, ''TB, ''TC])
type family Output (x :: TC) :: *
type instance Output ('CC ('Left 'CA)) = Int
type instance Output ('CC ('Right 'CB)) = String
f :: Sing (a :: TC) - Output a
f (SCC (SLeft SCA)) = 1
g :: Sing (a :: TC) - Output a
g (SCC (SLeft _)) = 1
Function f typechecks as expected. Function g fails to typecheck with the
following error.
Could not deduce (Num (Output ('CC ('Left TA TB n0
arising from the literal `1'
from the context (a ~ 'CC n, SingRep (Either TA TB) n)
bound by a pattern with constructor
SCC :: forall (a_a37R :: TC) (n_a37S :: Either TA TB).
(a_a37R ~ 'CC n_a37S, SingRep (Either TA TB)
n_a37S) =
Sing (Either TA TB) n_a37S - Sing TC a_a37R,
in an equation for `g'
at Test.hs:21:4-16
or from (n ~ 'Left TA TB n0,
SingRep TA n0,
SingKind TA ('KindParam TA))
bound by a pattern with constructor
SLeft :: forall (a0 :: BOX)
(b0 :: BOX)
(a1 :: Either a0 b0)
(n0 :: a0).
(a1 ~ 'Left a0 b0 n0, SingRep a0 n0,
SingKind a0 ('KindParam a0)) =
Sing a0 n0 - Sing (Either a0 b0) a1,
in an equation for `g'
at Test.hs:21:9-15
Possible fix:
add an instance declaration for
(Num (Output ('CC ('Left TA TB n0
In the expression: 1
In an equation for `g': g (SCC (SLeft _)) = 1
I would expect that a ~ ('CC ('Left 'CA)) in the right hand-side of g (SCC
(SLeft _)) = 1 since SLeft's argument is necessarily of type STA, whose
sole inhabitant is SA.
Now I understand (looking at -ddump-slices, the singletons' library paper
and the error message) that the definition of SCC and SLeft
don't immediately imply what I just wrote above. So my question is: in the
right hand-side of g (SCC (SLeft _)) = 1,
- is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
SLeft, ... (in which case GHC could infer it but for some reason can't)
- or are these pattern + definitions not sufficient to prove that a
~ ('CC ('Left 'CA)) no matter what?
Cheers,
Paul
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Fwd: second call for papers: LDTA 2011 / ETAPS
-- Forwarded message -- From: Emilie Balland emilie.ball...@inria.fr Date: Tue, Dec 7, 2010 at 10:35 PM Subject: second call for papers: LDTA 2011 / ETAPS To: Paul.Brauner paul.brau...@loria.fr LDTA 2011 Call for Papers and Tool Challenge Submissions 11th International Workshop on Language Descriptions, Tools, and Applications www.ldta.info Saarbrucken, Germany March 26 27, 2011 an ETAPS workshop LDTA is an application and tool-oriented workshop focused on grammarware - software based on grammars in some form. Grammarware applications are typically language processing applications and traditional examples include parsers, program analyzers, optimizers and translators. A primary focus of LDTA is grammarware that is generated from high-level grammar-centric specifications and thus submissions on parser generation, attribute grammar systems, term/graph rewriting systems, and other grammar-related meta-programming tools, techniques, and formalisms are encouraged. LDTA is also a forum in which theory is put to the test, in many cases on real-world software engineering challenges. Thus, LDTA also solicits papers on the application of grammarware to areas including, but not limited to, the following: - program analysis, transformation, generation, and verification, - implementation of Domain-Specific Languages, - reverse engineering and re-engineering, - refactoring and other source-to-source transformations, - language definition and language prototyping, and - debugging, profiling, IDE support, and testing. This year LDTA will also be putting theory, as well as techniques and tools, to the test in a new way - in the LDTA Tool Challenge. Tool developers are invited to participate in the Challenge by developing solutions to a range of language processing tasks over a simple but evolving set of imperative programming languages. Tool challenge participants will present highlights of their solution during a special session of the workshop and contribute to a joint paper on the Tool Challenge and proposed solutions to be co-authored by all participants after the workshop. Note that LDTA is a well-established workshop similar to other conferences on (programming) language engineering topics such as SLE and GPCE, but is solely focused on grammarware. Paper Submission LDTA solicits papers in the following categories. - research papers: original research results within the scope of LDTA with a clear motivation, description, analysis, and evaluation. - short research papers: new innovative ideas that have not been completely fleshed out. As a workshop, LDTA strongly encourages these types of submissions. - experience report papers: description of the use of a grammarware tool or technique to solve a non-trivial applied problem with an emphasis on the advantages and disadvantages of the chosen approach to the problem. - tool demo papers: discussion of a tool or technique that explains the contributions of the tool and what specifically will be demonstrated. These papers should describe tools and applications that do not fit neatly into the specific problems in the Tool Challenge. Each submission must clearly state in which of these categories it falls and not be published or submitted elsewhere. Papers are to use the standard LaTeX article style and the authblk style for affiliations; a sample of which is provided at www.ldta.info. Research and experience papers are limited to 15 pages, tool demonstration papers are limited to 10 pages, and short papers are limited to 6 pages. The final version of the accepted papers will, pending approval, be published in the ACM Digital Library and will also be made available during the workshop. Please submit your abstract and paper using EasyChair at http://www.easychair.org/conferences/?conf=ldta2011. The authors of each submission are required to give a presentation at LDTA 2011 and tool demonstration paper presentations are intended to include a significant live, interactive demonstration. The authors of the best papers will be invited to write a journal version of their paper which will be separately reviewed and, assuming acceptance, be published in journal form. As in past years this will be done in a special issue of the journal Science of Computer Programming (Elsevier Science). Invited Speaker --- Rinus Plasmeijer, Radboud University Nijmegen, The Netherlands Important Dates --- Abstract submission: Dec. 15, 2010 Full paper submission: Dec. 22, 2010 Author notification: Feb. 01, 2011 Camera-ready papers due: TBD LDTA Workshop: March 26-27, 2011 LDTA Tool Challenge --- The aim of the LDTA Tool Challenge is to foster a better understanding, among tool developers and tool users, of relative strengths and weaknesses of different
Re: [Haskell-cafe] Haskellers design
Looks perfect to me. Go for it! PS: I'm reading your book, I have never tried web dev before but Yesod feels very right On Sat, Oct 23, 2010 at 08:09:25PM +0200, Michael Snoyman wrote: It looks good to me. Are there any objections to using this for Haskellers? On Sat, Oct 23, 2010 at 3:31 AM, Nubis nu...@woobiz.com.ar wrote: Hi guys, It's me again, I made a new proposal for the website with the standard colors. I've put my pretentions of content being grouped by color, and just used what I thought looked better for each part of the site. Here's the link: http://previasports.com/haskellers_website_standard/ Let me know what you think cheers! nubis :) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] haltavista - look for functions by example
Hi, i'ts on hackage now. Thanks to Jun Inoue, stack overflows are now catched. Paul On Sat, Sep 18, 2010 at 11:47:07AM +0200, Paul Brauner wrote: Hello, I just hacked together something I've been talking about a while ago on that mailing list. It's a program that looks for functions given a set of input/outputs. Example session 1: brau...@worf:~$ haltavista 2 2 4 EOF Prelude (*) Prelude (+) Prelude (^) Example session 2 (refining previous search): brau...@worf:~$ haltavista 2 2 4 1 2 3 EOF Prelude (+) Example session 3 (higher-order functions): brau...@worf:~$ haltavista (+1) (+2) (1,1) (2,3) EOF Data.Graph.Inductive.Query.Monad () Under the hood, uses: - hint for type inference; - hoogle to get a list of candidate functions; - hint for testing. Hoogle calling facility has been copy-pasted (and later modified) from the Yi project. It's availaible on github (http://github.com/polux/haltavista) and I plan to release it on hackage as soon as I catch stack overflows that occur during testing using hint. So far I didn't manage to do it, even by catching asynchronous exceptions. Every suggestion/help is welcome. Also, if I got something wrong with the licences (Yi uses GPL-2 and code is copy-pasted, Hint BSD3 and is linked, Hoogle is called as an external process, haltavista is GPL-3 for now) please tell me. Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] haltavista - look for functions by example
That's a great idea! In the same vein, have you had a look at quickspec by Koen Claessen, Nicholas Smallbone and John Hughes? www.cse.chalmers.se/~nicsma/quickspec.pdf This reminds me of another idea, suggested by Jun inoue: look for functions by specification instead of examples. I will try your idea ASAP. As you say, I think that might be helpful for beginners, as you suggest, or even when you're not a beginner anymore but you start using a new library. Paul On Sun, Sep 19, 2010 at 07:41:21PM +0200, Roel van Dijk wrote: Very interesting! It got me thinking: if you combine this with the Arbitrary class [1] of QuickCheck you can use it check if you have defined a function that is equal to an already defined function. Let's say I write the following function: intMul ∷ Integer → Integer → Integer intMul x 0 = 0 intMul x n = x + intMul x (n - 1) No you can automatically apply this function to a list of 100 generated inputs to get a list of input output pairs. Feed this into haltavista and it should tell you that you can replace your definition with Prelude (*). While such an observation is certainly not a proof it is still useful. It would be a nice addition to a Haskell editor. Especially for those new to the language. Regards, Roel 1 - http://hackage.haskell.org/packages/archive/QuickCheck/2.3/doc/html/Test-QuickCheck-Arbitrary.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] haltavista - look for functions by example
It works: brau...@worf:/tmp$ cat test.hs import Test.QuickCheck import Test.QuickCheck.Arbitrary import Control.Monad(forM_) intMul :: Integer - Integer - Integer intMul x n | n 0 = -(intMul x $ abs n) | n == 0 = 0 | n 0 = x + intMul x (n - 1) main = do xs - sample' arbitrary ys - sample' arbitrary zip xs ys `forM_` \(x,y) - putStrLn (show x ++ ++ show y ++ ++ (show $ intMul x y)) brau...@worf:/tmp$ runghc test.hs | haltavista Prelude (*) I will include this functionality in the next version. Thank you for this nice idea. Paul On Sun, Sep 19, 2010 at 08:16:08PM +0200, Paul Brauner wrote: That's a great idea! In the same vein, have you had a look at quickspec by Koen Claessen, Nicholas Smallbone and John Hughes? www.cse.chalmers.se/~nicsma/quickspec.pdf This reminds me of another idea, suggested by Jun inoue: look for functions by specification instead of examples. I will try your idea ASAP. As you say, I think that might be helpful for beginners, as you suggest, or even when you're not a beginner anymore but you start using a new library. Paul On Sun, Sep 19, 2010 at 07:41:21PM +0200, Roel van Dijk wrote: Very interesting! It got me thinking: if you combine this with the Arbitrary class [1] of QuickCheck you can use it check if you have defined a function that is equal to an already defined function. Let's say I write the following function: intMul ∷ Integer → Integer → Integer intMul x 0 = 0 intMul x n = x + intMul x (n - 1) No you can automatically apply this function to a list of 100 generated inputs to get a list of input output pairs. Feed this into haltavista and it should tell you that you can replace your definition with Prelude (*). While such an observation is certainly not a proof it is still useful. It would be a nice addition to a Haskell editor. Especially for those new to the language. Regards, Roel 1 - http://hackage.haskell.org/packages/archive/QuickCheck/2.3/doc/html/Test-QuickCheck-Arbitrary.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] haltavista - look for functions by example
There's a timeout of 1.5 second right now.. On Sun, Sep 19, 2010 at 07:46:54PM +0200, Roel van Dijk wrote: In my haste to reply I made an error in my 'newby' multiplication function. Pesky negative numbers... intMul ∷ Integer → Integer → Integer intMul x n | n 0 = -(intMul x $ abs n) | n == 0 = 0 | n 0 = x + intMul x (n - 1) I do wonder what happens when haltavista encounters a function that diverges. Like my original intMul applied to a negative number: intMul 2 (-1). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] haltavista - look for functions by example
Hello, I just hacked together something I've been talking about a while ago on that mailing list. It's a program that looks for functions given a set of input/outputs. Example session 1: brau...@worf:~$ haltavista 2 2 4 EOF Prelude (*) Prelude (+) Prelude (^) Example session 2 (refining previous search): brau...@worf:~$ haltavista 2 2 4 1 2 3 EOF Prelude (+) Example session 3 (higher-order functions): brau...@worf:~$ haltavista (+1) (+2) (1,1) (2,3) EOF Data.Graph.Inductive.Query.Monad () Under the hood, uses: - hint for type inference; - hoogle to get a list of candidate functions; - hint for testing. Hoogle calling facility has been copy-pasted (and later modified) from the Yi project. It's availaible on github (http://github.com/polux/haltavista) and I plan to release it on hackage as soon as I catch stack overflows that occur during testing using hint. So far I didn't manage to do it, even by catching asynchronous exceptions. Every suggestion/help is welcome. Also, if I got something wrong with the licences (Yi uses GPL-2 and code is copy-pasted, Hint BSD3 and is linked, Hoogle is called as an external process, haltavista is GPL-3 for now) please tell me. Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] benchmarking pure code
Ok, thank you for all your answers. I'm going to use NFData as advised by everyone. Paul On Wed, Mar 31, 2010 at 10:38:50AM -0700, Bryan O'Sullivan wrote: On Wed, Mar 31, 2010 at 4:12 AM, Paul Brauner paul.brau...@loria.fr wrote: Thank you, I will look at that. But it seems that criterion uses NFData no? I do not know of anything wrong with NFData. What you're seeing is much more likely to be a bug in either the benchmarking library you're using, or in your use of it. Most of the benchmarking frameworks on Hackage are extremely dodgy, which was why I wrote criterion. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] benchmarking pure code
Hello, I'm writing a library for dealing with binders and I want to benchmark it against DeBruijn, Locally Nameless, HOAS, etc. One on my benchmark consists in 1. generating a big term \x.t 2. substituting u fox in t The part I want to benchmark is 2. In particular I would like that: a. \x.t is already evaluated when I run 2 (I don't want to measure the performances of the generator) b. the action of substituting u for x in t were measured as if I had to fully evaluate the result (by printing the resulting term for instance). After looking at what was available on hackage, i set my mind on strictbench, which basically calls (rnf x `seq` print ) and then uses benchpress to measure the pure computation x. Since I wanted (a), my strategy was (schematically): let t = genterm rnf t `seq` print bench (subst u t) I got numbers I didn't expect so I ran the following program: let t = genterm print t bench (subst u t) and then I got other numbers! Which were closer to what I think they should be, so I may be happy with them, but all of this seems to indicate that rnf doesn't behave as intended. Then I did something different: I wrote two programs. One that prints the result of (subst u t): let t = genterm let x = (subst u t) print x bench (print x) recorded the numbers of that one and then ran the program: let t = genterm bench (print (subst u t)) got the numbers, and substracted the first ones to them. By doing so, I'm sure that I get realistic numbers at least: since I print the whole resulting term, I've got a visual proof that it's been evaluated. But this is not very satisfactory. Does anyone have an idea why calling rnf before the bench doesn't seem to cache the result as calling show does? (my instances of NFData follow the scheme described in strictbench documentation). If not, do you think that measuring (computation + pretty printing time - pretty printing time) is ok? Regards, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] benchmarking pure code
Hello, actually I don't know if I can. I totally wouldn't mind but this is mainly my co-author work and I don't know if he would (I suppose not but since he is sleeping right now I can't check). However let's assume it's a deBruijn representation for instance, I can tell you the scheme I used: data Term = Lam Term | App Term Term | Var Int instance NFData where rnf (Lam t) = rnf t rnf (App t1 t2) = rnf t1 `seq` rnf t2 rnf (Var x) = rnf x the actual datatype doesn't have fancy stuff like higher-order types for constructors, it's really similar. The only difference is that it is a GADT, but this souldn't change anything right? Did I make some mistake in instancing NFData ? Regards, Paul On Wed, Mar 31, 2010 at 09:32:29AM +0200, Bas van Dijk wrote: On Wed, Mar 31, 2010 at 9:17 AM, Paul Brauner paul.brau...@loria.fr wrote: Does anyone have an idea why calling rnf before the bench doesn't seem to cache the result as calling show does? (my instances of NFData follow the scheme described in strictbench documentation). Is it possible you could show us your term type and your NFData instance? regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] benchmarking pure code
Thank you, I will look at that. But it seems that criterion uses NFData
no?
Paul
On Wed, Mar 31, 2010 at 12:57:20PM +0200, Bas van Dijk wrote:
On Wed, Mar 31, 2010 at 11:06 AM, Paul Brauner paul.brau...@loria.fr wrote:
data Term = Lam Term | App Term Term | Var Int
instance NFData where
rnf (Lam t) = rnf t
rnf (App t1 t2) = rnf t1 `seq` rnf t2
rnf (Var x) = rnf x
the actual datatype doesn't have fancy stuff like higher-order
types for constructors, it's really similar. The only difference
is that it is a GADT, but this souldn't change anything right?
Did I make some mistake in instancing NFData ?
No, your NFData instance is correct. You first pattern match on the
term followed by recursively calling rnf on the sub-terms. This will
correctly force the entire term.
Maybe you could try using criterion[1] for your benchmark and see if
that makes any difference. Something like:
{-# LANGUAGE BangPatterns #-}
import Criterion.Main
main :: IO ()
main = let !t = genterm in defaultMain [bench subst $ nf (subst u) t]
regards,
Bas
[1] http://hackage.haskell.org/package/criterion
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] phonetic dictionnary
You should have a looks at soundexes: http://en.wikipedia.org/wiki/Soundex the algorithm is really simple and you can process a whole dictionnary in no time to obtain what you're looking for. Paul On Thu, Mar 25, 2010 at 01:59:28PM +0100, Dupont Corentin wrote: Hello, sorry if i ask a lot of questions these days! Do you know of a phonetic dictionnary? i'm very fond of enigmas. To solve certain enigmas, i've made a little program that search into a french dictionnary. But it would be much better if i could search into a phonetic dictionnary... The goal is to answer questions like Wich word would rhyme with aligator? Corentin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] explicit big lambdas
Thanks to all! Paul On Fri, Mar 19, 2010 at 04:24:17PM +0100, Bas van Dijk wrote: On Fri, Mar 19, 2010 at 4:03 AM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Alternatively: let f :: some type involving a f = ... f' :: a - some type involving a f' _ = f in f' (undefined :: Int) normal f arguments Or use Edward Kmett's tagged library: http://hackage.haskell.org/packages/archive/tagged/0.0/doc/html/Data-Tagged.html so you don't have to use bottom values: let f :: some type involving a f = ... f' :: Tagged a some type involving a f' = Tagged f regards, Bas ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] libraries and executables in cabal
Hi, i'm working on a project made of - lots of modules - one excutable importing these modules - another excutable importing these same modules I don't especially want to expose those modules as libraries, especially on hackage, since they are meaningless without the executables. But, if I declare two executables in my .cabal file, cabal will compile all those modules two times each time I want to compile the executables. Is there a way to tell cabal that those modules should be considered part of a private library ? Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] searching a function by providing examples of input/ouput pairs
Hi, I was looking at hoogle documentation when I remembered that there is some nice, but quite unusable, feature of squeak (smalltalk) which allows you to search function in the library by giving a list of pairs of inputs/ouputs. When I'm saying that it is quite unusable, I mean that squeak has to try _every_ function, some of which may be very slow to deliver a result, or require some side effects. But, piggibacking such a feature on top of hoogle would surely be more efficient: 1. infer types for arguments and outout 2. look for matching functions using google 3. test them Has anyone tried that before? If not I would be glad to. Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: searching a function by providing examples of input/ouput pairs
On Thu, Mar 18, 2010 at 01:49:20PM +0100, Janis Voigtländer wrote: Paul Brauner schrieb: Hi, I was looking at hoogle documentation when I remembered that there is some nice, but quite unusable, feature of squeak (smalltalk) which allows you to search function in the library by giving a list of pairs of inputs/ouputs. When I'm saying that it is quite unusable, I mean that squeak has to try _every_ function, some of which may be very slow to deliver a result, or require some side effects. But, piggibacking such a feature on top of hoogle would surely be more efficient: 1. infer types for arguments and outout 2. look for matching functions using google 3. test them Has anyone tried that before? If not I would be glad to. Sounds like something useful to have. And you could even have the system use a list of pairs of inputs/outputs to give you functions that are *not* yet in any library. :-) http://www.haskell.org/communities/11-2009/html/report.html#sect6.11.1 Yeah that would be nice to have hoogle + not_yet_existing_matcher + igor to wor together :) Put it on my todo list. Paul -- Jun.-Prof. Dr. Janis Voigtländer http://www.iai.uni-bonn.de/~jv/ mailto:j...@iai.uni-bonn.de ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] explicit big lambdas
Hi again, is there a way in some haskell extension to explicit (system F's) big lambdas and (term Type) applications in order to help type inference? If not: is there a way to provide ghc directly with core code before the type checking phase? Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] datakind declaration
Hello, I remember seeing something like typedata T = A | B somewhere, where A and B are type constructors, but I can't find it in the ghc doc. Have I been dreaming or is it some hidden feature ? Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] telling ghc to run several jobs in parallel
Hi, I have to processors but ghc --make only uses one of them, even if some files could be compiled in parallel. Is there some option similar to the -j one of the make tool ? (I read the manual but didn't find it) Regards, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] lawless instances of Functor
Hi, I'm trying to get a deep feeling of Functors (and then pointed Functors, Applicative Functors, etc.). To this end, I try to find lawless instances of Functor that satisfy one law but not the other. I've found one instance that satisfies fmap (f.g) = fmap f . fmap g but not fmap id = id: data Foo a = A | B instance Functor Foo where fmap f A = B fmap f B = B -- violates law 1 fmap id A = B -- respects law 2 fmap (f . g) A = (fmap f . fmap g) A = B fmap (f . g) B = (fmap f . fmap g) B = B But I can't come up with an example that satifies law 1 and not law 2. I'm beginning to think this isn't possible but I didn't read anything saying so, neither do I manage to prove it. I'm sure someone knows :) Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lawless instances of Functor
Thanks. I was wondering if the free theorem of fmap entailed that implication, but I'm not used enough to decipher the output of the tool, neither am I able to generate it by hand. However, if this holds (law1 = law2), I wonder why this isn't some classic category theory result (maybe it is ?). I don't know much about category theory, but it seems to me that functors are pretty central to it. Maybe i'm confusing haskell's notion of Functor and category theory functors. Paul On Tue, Jan 05, 2010 at 08:01:46AM +0900, Derek Elkins wrote: On Tue, Jan 5, 2010 at 7:14 AM, Paul Brauner paul.brau...@loria.fr wrote: Hi, I'm trying to get a deep feeling of Functors (and then pointed Functors, Applicative Functors, etc.). To this end, I try to find lawless instances of Functor that satisfy one law but not the other. I've found one instance that satisfies fmap (f.g) = fmap f . fmap g but not fmap id = id: data Foo a = A | B instance Functor Foo where fmap f A = B fmap f B = B -- violates law 1 fmap id A = B -- respects law 2 fmap (f . g) A = (fmap f . fmap g) A = B fmap (f . g) B = (fmap f . fmap g) B = B But I can't come up with an example that satifies law 1 and not law 2. I'm beginning to think this isn't possible but I didn't read anything saying so, neither do I manage to prove it. I'm sure someone knows :) Ignoring bottoms the free theorem for fmap can be written: If h . p = q . g then fmap h . fmap p = fmap q . fmap g Setting p = id gives h . id = h = q . g fmap h . fmap id = fmap q . fmap g Using fmap id = id and h = q . g we get, fmap h . fmap id = fmap h . id = fmap h = fmap (q . g) = fmap q . fmap g So without doing funky stuff involving bottoms and/or seq, I believe that fmap id = id implies the other functor law (in this case, not in the case of the general categorical notion of functor.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Control.Parallel and the Reader monad
Hi, I'm facing the following problem. I've got come computation c :: a - Reader e b that i'm running on several as: mapM c xs A natural optimisation of this program would to be to take advantage of Control.Parallel to run these computation in parallel, which seems sound since the Reader monad is commutative. Unfortunately, I didn't manage to do so. Has this situation been tackled with before ? Is there some library or function I've missed involving commutative monads and Control.Parallel ? Regards, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] convert a list of booleans into Word*
Hello, I haven't found a function in hackage or in the standard library that takes a list of booleans (or a list of 0s and 1s, or a tuple of booleans or 0s and 1s) and outputs a Word8 or Word32. I have written one which seems very inefficient : toWord8 :: [Bool] - Word8 toWord8 bs = go 0 0 bs where go n r [] = r go n r (b:bs) = go (n+1) (if b then setBit r n else clearBit r n) bs Is there a better way to do this out there ? (If it helps, i'm writting a toy compression algorithm, which outputs binary as lists of booleans, and I'd like to output that in a file). Cheers Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] convert a list of booleans into Word*
Thanks for the answers. I already had a look at Binary but, as said above, it doesn't support bit manipulation, only bytes. On Wed, Sep 30, 2009 at 11:18:03AM +0200, paul.brau...@loria.fr wrote: Hello, I haven't found a function in hackage or in the standard library that takes a list of booleans (or a list of 0s and 1s, or a tuple of booleans or 0s and 1s) and outputs a Word8 or Word32. I have written one which seems very inefficient : toWord8 :: [Bool] - Word8 toWord8 bs = go 0 0 bs where go n r [] = r go n r (b:bs) = go (n+1) (if b then setBit r n else clearBit r n) bs Is there a better way to do this out there ? (If it helps, i'm writting a toy compression algorithm, which outputs binary as lists of booleans, and I'd like to output that in a file). Cheers Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] haskell code pretty printer ?
Hello, is there a pretty printer for haskell code somewhere ? I've googled and caballisted for this without success. I've written some small script using Language.Haskell.Pretty and Language.Haskell.Parser but the result isn't that 'pretty'. I mean, it outputs readable code but supercombinator's definitions aren't separated by a blank line for instance (despite having put 'spacing' to 'True'). Do you know of such a tool ? Regards, Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
