Re: [Haskell-cafe] Generating random arguments for a function
In general you can't do this whether you use pats of QuickCheck or not - `randomEvalute` would need to inspect the supplied function to see how many input parameters it has so it can list them, but there is no such introspection in Haskell. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generating random arguments for a function
* Stephen Tetley stephen.tet...@gmail.com [2013-01-13 08:49:08+] In general you can't do this whether you use pats of QuickCheck or not - `randomEvalute` would need to inspect the supplied function to see how many input parameters it has so it can list them, but there is no such introspection in Haskell. This can be done with relatively simple type class hackery. In fact, QuickCheck already does that in order to generate arguments and print them in case of failure. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generating random arguments for a function
Yes - I was just checking the first QuickCheck paper to see how the authors did this. You would need a new type class that works like `Testable` and the versions of associated machinery `forAll` and `evaluate` to unroll function application. On 13 January 2013 09:28, Roman Cheplyaka r...@ro-che.info wrote: This can be done with relatively simple type class hackery. In fact, QuickCheck already does that in order to generate arguments and print them in case of failure. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generating random arguments for a function
I have a working code of this but for that I have to reimplement Arbitrary and Testable typeclasses which I don't want to do. I thought it might be possible to use parts of quickcheck without actually changing its code but still I am unable to find a suitable solution. -Satvik On Sun, Jan 13, 2013 at 2:58 PM, Roman Cheplyaka r...@ro-che.info wrote: * Stephen Tetley stephen.tet...@gmail.com [2013-01-13 08:49:08+] In general you can't do this whether you use pats of QuickCheck or not - `randomEvalute` would need to inspect the supplied function to see how many input parameters it has so it can list them, but there is no such introspection in Haskell. This can be done with relatively simple type class hackery. In fact, QuickCheck already does that in order to generate arguments and print them in case of failure. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Where is the convergence point between Category Theory and Haskell?
Morning Cafe, I'm planning to do a series of write-ups about Category Theory, to publish them on the company's blog I'm currently employed. I'm not a CT expert, but since the best way to learn something is to explain it to others, I want to take a shot :) In my mind I will structure the posts following Awodey's book, but I'm wondering how can I make my posts a little more real world. I always read about the Hask category, which seems to be the bootstrap of the whole logic behind Haskell. Can you please give my materials/papers/links/blogs to the Hask category and briefly explain me how it relates to Category Theory and Haskell itself? I hope my question is clear enough, in case is not, I'll restate :P Cheers, A. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Generating random arguments for a function
I think it's more complicated because he doesn't know what the return type or arity of the function is. In QuickCheck they know the return type of a property is Bool. In this case, we only know that the return type is an instance of Show. I don't think that's enough to simply implement this. On Sunday, January 13, 2013, Stephen Tetley wrote: Yes - I was just checking the first QuickCheck paper to see how the authors did this. You would need a new type class that works like `Testable` and the versions of associated machinery `forAll` and `evaluate` to unroll function application. On 13 January 2013 09:28, Roman Cheplyaka r...@ro-che.info javascript:; wrote: This can be done with relatively simple type class hackery. In fact, QuickCheck already does that in order to generate arguments and print them in case of failure. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org javascript:; 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] Generating random arguments for a function
Hi, Am Sonntag, den 13.01.2013, 07:34 -0800 schrieb Bob Ippolito: I think it's more complicated because he doesn't know what the return type or arity of the function is. In QuickCheck they know the return type of a property is Bool. In this case, we only know that the return type is an instance of Show. I don't think that's enough to simply implement this. I posted on SE an answer that tries to do it with OverlappingInstances: http://stackoverflow.com/questions/14294802/evaluating-function-at-random-arguments-using-quickcheck/14295179#14295179 Greetings, Joachim -- Joachim nomeata Breitner m...@joachim-breitner.de | nome...@debian.org | GPG: 0x4743206C xmpp: nome...@joachim-breitner.de | http://www.joachim-breitner.de/ signature.asc Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Where is the convergence point between Category Theory and Haskell?
There was a conversation on the cafe about this last month. Check out: https://groups.google.com/forum/#!topic/haskell-cafe/tBO2AowUvMY Category theory is a language of composition. In logical terms, different categories are models of different axioms. That said, a rich enough category is suitable for encoding the whole of category theory (as a language -- not necessarily as a model containing sub-models. Typing introduces some complications, since types meant to help us escape logical paradoxes like Russell's by introducing a notion of foundedness) Hask is the category whose objects are types and whose morphisms are Haskell functions. Hask is a very rich category, and is suitable for encoding a lot (but not all) of category theory. As far as I know, the actual boundary is as yet unknown. On Sun, Jan 13, 2013 at 4:15 AM, Alfredo Di Napoli alfredo.dinap...@gmail.com wrote: Morning Cafe, I'm planning to do a series of write-ups about Category Theory, to publish them on the company's blog I'm currently employed. I'm not a CT expert, but since the best way to learn something is to explain it to others, I want to take a shot :) In my mind I will structure the posts following Awodey's book, but I'm wondering how can I make my posts a little more real world. I always read about the Hask category, which seems to be the bootstrap of the whole logic behind Haskell. Can you please give my materials/papers/links/blogs to the Hask category and briefly explain me how it relates to Category Theory and Haskell itself? I hope my question is clear enough, in case is not, I'll restate :P Cheers, A. ___ 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] Where is the convergence point between Category Theory and Haskell?
Thank you Alexander for the reply. My wondering is: is Hask a category created by Haskell researchers or was something already present in literature? Cheers, A. On 13 January 2013 17:44, Alexander Solla alex.so...@gmail.com wrote: There was a conversation on the cafe about this last month. Check out: https://groups.google.com/forum/#!topic/haskell-cafe/tBO2AowUvMY Category theory is a language of composition. In logical terms, different categories are models of different axioms. That said, a rich enough category is suitable for encoding the whole of category theory (as a language -- not necessarily as a model containing sub-models. Typing introduces some complications, since types meant to help us escape logical paradoxes like Russell's by introducing a notion of foundedness) Hask is the category whose objects are types and whose morphisms are Haskell functions. Hask is a very rich category, and is suitable for encoding a lot (but not all) of category theory. As far as I know, the actual boundary is as yet unknown. On Sun, Jan 13, 2013 at 4:15 AM, Alfredo Di Napoli alfredo.dinap...@gmail.com wrote: Morning Cafe, I'm planning to do a series of write-ups about Category Theory, to publish them on the company's blog I'm currently employed. I'm not a CT expert, but since the best way to learn something is to explain it to others, I want to take a shot :) In my mind I will structure the posts following Awodey's book, but I'm wondering how can I make my posts a little more real world. I always read about the Hask category, which seems to be the bootstrap of the whole logic behind Haskell. Can you please give my materials/papers/links/blogs to the Hask category and briefly explain me how it relates to Category Theory and Haskell itself? I hope my question is clear enough, in case is not, I'll restate :P Cheers, A. ___ 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] Advice on type families and non-injectivity?
I sometimes run into trouble with lack of injectivity for type families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
Hello Conal,
The issue with your example is that it is ambiguous, so GHC can't figure
out how to instantiate the use of `foo`. It might be easier to see why
this is if you write it in this form:
foo :: (F a ~ b) = b
foo = ...
Now, we can see that only `b` appears on the RHS of the `=`, so there is
really no way for GHC to figure out what is the intended value for `a`.
Replacing `a` with a concrete type (such as `Bool`) eliminates the
problem, because now GHC does not need to come up with a value for `a`.
Another way to eliminate the ambiguity would be if `F` was injective---then
we'd know that `b` uniquely determines `a` so again there would be no
ambiguity.
If `F` is not injective, however, the only workaround would be to write the
type in such a way that the function arguments appear in the signature
directly (e.g., something like 'a - F a' would be ok).
-Iavor
On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott co...@conal.net wrote:
I sometimes run into trouble with lack of injectivity for type families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
glasgow-haskell-us...@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
Hi Iavor,
Thanks for the remarks.
so there is really no way for GHC to figure out what is the intended value
for `a`.
Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation `(forall a. F a) ==
(forall a'. F a')`?
-- Conal
On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki
iavor.diatc...@gmail.comwrote:
Hello Conal,
The issue with your example is that it is ambiguous, so GHC can't figure
out how to instantiate the use of `foo`. It might be easier to see why
this is if you write it in this form:
foo :: (F a ~ b) = b
foo = ...
Now, we can see that only `b` appears on the RHS of the `=`, so there is
really no way for GHC to figure out what is the intended value for `a`.
Replacing `a` with a concrete type (such as `Bool`) eliminates the
problem, because now GHC does not need to come up with a value for `a`.
Another way to eliminate the ambiguity would be if `F` was injective---then
we'd know that `b` uniquely determines `a` so again there would be no
ambiguity.
If `F` is not injective, however, the only workaround would be to write
the type in such a way that the function arguments appear in the signature
directly (e.g., something like 'a - F a' would be ok).
-Iavor
On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott co...@conal.net wrote:
I sometimes run into trouble with lack of injectivity for type
families. I'm trying to understand what's at the heart of these
difficulties and whether I can avoid them. Also, whether some of the
obstacles could be overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
glasgow-haskell-us...@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
Hi Christian,
Given bar :: Bool, I can't see how one could go from Bool to F a =
Bool and determine a uniquely.
The same question applies to foo :: Bool, right? Yet no error message
there.
Regards, - Conal
On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen
choe...@tbi.univie.ac.at wrote:
Hi,
How would you infer a from F a? Given bar :: Bool, I can't see how
one could go from Bool to F a = Bool and determine a uniquely.
My question is not completely retorical, if there is an answer I would
like to know it :-)
Gruss,
Christian
* Conal Elliott co...@conal.net [13.01.2013 20:13]:
I sometimes run into trouble with lack of injectivity for type
families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type
and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
Glasgow-haskell-users mailing list
glasgow-haskell-us...@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] cabal sdist warns about optimization levels
Hi all, I'm working on a library for fast sorting of MArrays. The library is primarily about speed, so I added ghc-options: -O2 to the cabal file. Now cabal sdist complains with: 'ghc-options: -O2' is rarely needed. Check that it is giving a real benefit and not just imposing longer compile times on your users. I wonder: (1) Is there a way how to disable the warning? As the main aim of the library is speed, I believe -O2 is appropriate here. And since the code is quite short, I'm quite sure the increased compile time won't be noticeable. (2) Why does cabal complain about it at the first place? I found a reference saying the warning is adequate: https://github.com/haskell/cabal/issues/808 but not saying why. Maybe for complex programs -O2 prolongs compile time too much, but libraries are usually compiled once and used many times, so using -O2 for them seems reasonable in many cases. Thanks for help, Petr Pudlak ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
Hello, On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net wrote: so there is really no way for GHC to figure out what is the intended value for `a`. Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`? Wouldn't that make `F` a constant type family, and so one could just skip the `a` parameter? Anyway, if there was a way to assert something like that about a type-function, than there would be no problem. When something like that happens (i.e., GHC figures out that it does not know how to instantiate a type variable, but it is sure that the actual instantiation does not matter), GHC instantiates the variable a special type called `Any`, which has a very polymorphic kind. By the way, Simon recently reworked the ambiguity checker in GHC, and now HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check uses exactly what's in your example: a value `f :: S` is ambiguous, if `g :: S; g = f` results in an error). -Iavor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Repa: traverse delayed array multiple times
Greetings to all! Currently I'm trying to do physical simulations using finite difference method. To accomplish this I need to repeat some manipulations on 2-dimensional grid several thousands or millions times, you know. Is it possible to do using repa? I wrote this rough sketch that shows what I am into. Apparently, program is severely slow. I think reason is: Every time an element is requested from a delayed array it is calculated anew, which means that delayed arrays are inefficient when the data is needed multiple times (http://www.haskell.org/haskellwiki/Numeric_Haskell:_A_Repa_Tutorial). I started diving into Guiding Parallel Array Fusion with Indexed Typeshttp://www.cse.unsw.edu.au/%7Ebenl/papers/guiding/guiding-Haskell2012-sub.pdfmentioned there. Is it a right place to find any answer to my question? To summarize, I want to apply my function to Array several thousand times as fast as possible (using multi-threading and GPGPU). It seems I need a lot of memory and throughput. Do I have to call iterate only once at a time or in some kind of batches. What are my possibilities? Thanks in advance! Example program: import System.Environment import Data.Array.Repa as Repa h = 50 w = 50 grid = fromListUnboxed (Z :. h :. w) $ take (h * w) [1, 1..] main = do args - getArgs let n = read $ head args g - computeP $ accumulate n grid :: IO (Array U DIM2 Int) putStrLn Ok accumulate :: Int - Array U DIM2 Int - Array D DIM2 Int accumulate n g = repaIterate step n $ delay g step :: (DIM2 - Int) - DIM2 - Int step f (Z :. i :. j) = center + right + left + top + bottom where left = f' j (i - 1) center = f' j i right = f' j (i + 1) top= f' (j + 1) i bottom = f' (j - 1) i f' j i = if j0 || i0 || i=h || j=w then 0 else f (Z :. j :. i) repaIterate :: ((DIM2 - Int) - DIM2 - Int) - Int - Array D DIM2 Int - Array D DIM2 Int repaIterate f n = (!! n) . iterate (\array - traverse array id f) Compilation: ghc -O2 -threaded -rtsopts --make repatest.hs time output: ./repatest 3 +RTS -N2 -H 0,02s user 0,02s system 109% cpu 0,033 total ./repatest 4 +RTS -N2 -H 0,09s user 0,02s system 126% cpu 0,089 total ./repatest 5 +RTS -N2 -H 0,30s user 0,02s system 155% cpu 0,200 total ./repatest 6 +RTS -N2 -H 1,16s user 0,06s system 185% cpu 0,663 total ./repatest 7 +RTS -N2 -H 5,63s user 0,24s system 191% cpu 3,071 total ./repatest 8 +RTS -N2 -H 27,72s user 0,89s system 191% cpu 14,960 total ./repatest 8 +RTS -N1 -H 26,23s user 0,19s system 100% cpu 26,388 total ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
I have a trick that loses a little convenience, but may still be more
convenient than data families.
{-# LANGUAGE TypeFamilies #-}
import Data.Tagged
type family F a
foo :: Tagged a (F a)
foo = Tagged undefined
bar :: Tagged a (F a)
bar = foo
This allows you to use the same newtype wrapper consistently, regardless of
what the type instance actually is; one of the inconveniences of data
families is the need to use different constructors for different types.
On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott co...@conal.net wrote:
I sometimes run into trouble with lack of injectivity for type families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE TypeFamilies #-}
type family F a
foo :: F a
foo = undefined
bar :: F a
bar = foo
The error message:
Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo
A terser (but perhaps subtler) example producing the same error:
baz :: F a
baz = baz
Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
Does the difficulty here have to do with trying to *infer* the type and
then compare with the given one? Or is there an issue even with type
*checking* in such cases?
Other insights welcome, as well as suggested work-arounds.
I know about (injective) data families but don't want to lose the
convenience of type synonym families.
Thanks, -- Conal
___
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] cabal sdist warns about optimization levels
On Sunday 13 January 2013, 21:27:44, Petr P wrote:
I wonder:
(1) Is there a way how to disable the warning? As the main aim of the
library is speed, I believe -O2 is appropriate here. And since the code is
quite short, I'm quite sure the increased compile time won't be noticeable.
(2) Why does cabal complain about it at the first place? I found a
reference saying the warning is adequate:
https://github.com/haskell/cabal/issues/808
but not saying why. Maybe for complex programs -O2 prolongs compile time
too much, but libraries are usually compiled once and used many times, so
using -O2 for them seems reasonable in many cases.
Sometimes compiling with -O2 instead of just -O takes significantly longer.
Not always is the produced result faster (often, the results are identical).
So if the code produced with -O performs equally to that produced with -O2,
and the -O2 compilation takes significantly longer, choosing -O2 imposes a
cost for no benefit.
That's, I think, why the warning is considered adequate.
You can specify -O2 on a per-module basis with an
{-# OPTIONS_GHC -O2 #-}
pragma where it matters, then cabal won't complain.
Or, if you're too lazy to check the consequences of -O2 vs. -O for each module
(like I usually am, if there are more than a handful), just verify that -O2
does indeed make a significant difference for the speed of the result in some
places without increasing compile time unduly, and henceforth ignore the
warning if it does. (Re-test every couple of compiler versions.)
After some time, you tend to not even notice it anymore ;)
Cheers,
Daniel
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] cabal sdist warns about optimization levels
On 13 January 2013 20:27, Petr P petr@gmail.com wrote: to the cabal file. Now cabal sdist complains with: 'ghc-options: -O2' is rarely needed. Check that it is giving a real benefit and not just imposing longer compile times on your users. I wonder: (1) Is there a way how to disable the warning? As the main aim of the library is speed, I believe -O2 is appropriate here. And since the code is quite short, I'm quite sure the increased compile time won't be noticeable. No, but you can just ignore it. You clearly have checked and you're satisfied it's the right thing to do, so it's fine. You don't need to hit 0 warnings, nobody is going to give you or your package black marks becuase of it! :-) (2) Why does cabal complain about it at the first place? There's lots of programs where it makes no measurable difference except to make compile times longer. To some extent it's to try to break the habbit of C programmers who always default to -O2. With gcc -O2 will almost always be significantly better than -O, but with ghc that's not the case: -O is the sensible default (almost by definition, to a first approximation, things that are always a win get put into -O, things that are sometimes a win and sometimes not go into -O2). Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Where is the convergence point between Category Theory and Haskell?
On 1/13/13 12:44 PM, Alexander Solla wrote: Hask is a very rich category, and is suitable for encoding a lot (but not all) of category theory. As far as I know, the actual boundary is as yet unknown. I'm not sure that's the most appropriate way to render things. In general, rich categories like CCCs and Toposes are good places to do mathematics. This means that we can translate the bulk of mathematics into those settings--- where mathematics means the study of particular structures like rings, groups, vector spaces, etc. These rich categories also provide a good place to do logic/lambda-calculi; from which we get the idea of categorifying Haskell and seeing where that leads us (i.e., asking what Hask looks like). However, standard category theory does not provide a good place for doing category theory. In order to provide a good place for doing category theory, people move on to enriched CT and higher CT[1]. HCT is about coming up with category theoretic definitions for things like co/limits, adjunctions, etc, while moving away from the set theoretic notions inherited from the original conceptions of these terms. In other words, HCT is a good place for doing *meta*mathematics (and metalogic). While there are apparent similarities, there are big differences between doing mathematics and doing metamathematics, and one should be careful not to get them confused. Asking what Haskell looks like when viewed from CT is very different than asking what portions of CT we can implement in Haskell. Haskell is a great place for doing mathematics, but I'm wary of how good it is for doing metamathematics; we conflate too many things which should be kept distinct (e.g., morphisms vs exponentials) and we fail to monitor the boundary between object and meta languages (e.g., a morphism in a category vs a mapping as described in the language of category theory). [1] For more discussion on this point, see n-Lab and n-Cafe: http://ncatlab.org/ http://golem.ph.utexas.edu/category/ -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Where is the convergence point between Category Theory and Haskell?
On 1/13/13 1:53 PM, Alfredo Di Napoli wrote: Thank you Alexander for the reply. My wondering is: is Hask a category created by Haskell researchers or was something already present in literature? Hask was created by Haskellers in discussions on blogs etc. If one is being particular about the details, it's not clear that Haskell types and functions actually do form a category of interest, let alone one with the properties commonly attributed to Hask (e.g., Cartesian closedness). One of the big problems is how laziness/bottoms are treated (e.g., eta-conversion does not hold in general). Thus, I'm not sure it's ever been discussed in the literature; it's more a helpful fiction than a legitimate mathematical object. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Where is the convergence point between Category Theory and Haskell?
On 01/13/2013 03:15 AM, Alfredo Di Napoli wrote: Morning Cafe, I'm planning to do a series of write-ups about Category Theory, to publish them on the company's blog I'm currently employed. I'm not a CT expert, but since the best way to learn something is to explain it to others, I want to take a shot :) In my mind I will structure the posts following Awodey's book, but I'm wondering how can I make my posts a little more real world. I always read about the Hask category, which seems to be the bootstrap of the whole logic behind Haskell. Can you please give my materials/papers/links/blogs to the Hask category and briefly explain me how it relates to Category Theory and Haskell itself? I hope my question is clear enough, in case is not, I'll restate :P Cheers, A. You want to give us the link to that blog? If you can keep your explanations reasonably illustrative and easy to understand, you'll get a regular reader out of me. -- frigidcode.com signature.asc Description: OpenPGP digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Advice on type families and non-injectivity?
On 1/13/13 3:52 PM, Iavor Diatchki wrote: On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net wrote: so there is really no way for GHC to figure out what is the intended value for `a`. Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`? Wouldn't that make `F` a constant type family, I don't see why. If we translate this to dependent type notation we get: ((a::*) - F a) == ((b::*) - F b) This equality should hold in virtue of alpha-conversion. What F is, is irrelevant; the only thing that matters is that it has kind *-*. In particular, it doesn't matter whether F is arbitrary, injective, parametric, constant, etc. The problem is that the above isn't the equation GHC sees. GHC sees: F a == F b and it can't infer any correlation between a and b, where one of those is universally quantified in the context (the definition of bar) and the other is something we need to fabricate to hand off to the polymorphic value (the call to foo). Of course, in this particular case it *ought* to be fine, by parametricity in the definition of foo. That is, since we merely need to come up with some b, any b, such that F b is the type we need (namely: F a), the a we have will suffice for that. So if we're explicit about type passing, the following is fine: foo :: forall b. F b bar :: forall a. F a bar = /\a - foo @a The problem is that while the a is sufficient it's not (in general) necessary. And that's the ambiguity GHC is complaining about. GHC can't see that foo is parametric in b, and therefore that a is as good as any other type. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Announce: Leksah 0.13.1.2 now 100% Gtk3 (still a bit experimental though)
I used the MinGW32 RPMs included in Fedora to get Gtk3 working on Windows. So no more Gtk2 unless you really want it (in which case use -f-gtk3 when building). Issue with Pane - HLint not working in the binary versions should be fixed with these too. OS X Choose the version that matches your installed GHC http://leksah.org/packages/leksah-0.13.1.2-ghc-7.0.3.dmg http://leksah.org/packages/leksah-0.13.1.2-ghc-7.0.4.dmg http://leksah.org/packages/leksah-0.13.1.2-ghc-7.4.1.dmg http://leksah.org/packages/leksah-0.13.1.2-ghc-7.4.2.dmg http://leksah.org/packages/leksah-0.13.1.2-ghc-7.6.1.dmg (probable needs OS X 10.7) Windows --- Choose the version that matches your installed GHC http://leksah.org/packages/leksah-0.13.1.2-ghc-7.0.3.exe http://leksah.org/packages/leksah-0.13.1.2-ghc-7.0.4.exe http://leksah.org/packages/leksah-0.13.1.2-ghc-7.4.1.exe http://leksah.org/packages/leksah-0.13.1.2-ghc-7.4.2.exe http://leksah.org/packages/leksah-0.13.1.2-ghc-7.6.1.exe Linux - Follow the steps in the .travis.yml file... https://github.com/leksah/leksah/blob/master/.travis.yml Should go something like this... https://travis-ci.org/leksah/leksah ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
