Re: [Haskell-cafe] pure crisis :)
Hello Bulat! Sun, Feb 01, 2009 at 10:19:18PM +0300 you wrote: Hello haskell-cafe, pure functional denotation for crisis: (_|_) Thus, when people try to evaluate the amount of savings they have left, their behavior frequently becomes _undefined_ :) -- DoubleF pgpqVznaWBs7H.pgp Description: PGP signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parallel term reduction
I spent four hours investigating this problem! Thank you very much for the
excellent brainfood, and challenging Haskell's claim to be rawkin' at
parallelism. I think, though it took much experimentation, that I have
confirmed that it is :-)
On Sun, Feb 1, 2009 at 9:26 PM, John D. Ramsdell ramsde...@gmail.com
wrote:
I have a reduction system in which a rule takes a term and returns a
set of terms.
The reduction system creates a tree that originates at a starting
value called the root.
For most problems, the reduction system terminates, but a step count
limit protects
from non-termination.
That's typically a bad idea. Instead, use laziness to protect from
nontermination. For example, in this case, we can output a collection of
items lazily, and then take a finite amount of the output (or check whether
the output is longer than some length), without having to evaluate all of
it.
Here's my writeup of my solution, in literate Haskell. It doesn't output
the exact same structure as yours, but hopefully you can see how to tweak it
to do so.
{-# LANGUAGE RankNTypes #-}
*import* *qualified* Data.MemoCombinators *as* Memo
*import* *qualified* Data.Set *as* Set
*import* Control.Parallel (par)
*import* *qualified* Control.Parallel.Strategies *as* Par
*import* Data.Monoid (Monoid(..))
*import* Control.Monad.State
*import* *qualified* Data.DList *as* DList
*import* Debug.Trace
*import* Control.Concurrent
First, I want to capture the idea of a generative set like you're doing.
GenSet is like a set, with the constructor genset x xs which says if x is
in the set, then so are xs. I'll represent it as a stateful computation of
the list of things we've seen so far, returning the list of things we've
seen so far. It's redundant information, but sets can't be consumed lazily,
thus the list (the set will follow along lazily :-). Remember that State s a
is just the function (s - (s,a)). So we're taking the set of things we've
seen so far, and returning the new elements added and the set unioned with
those elements.
*newtype* GenSet a
= GenSet (State (Set.Set a) (DList.DList a))
genset :: (Ord a) = a - GenSet a - GenSet a
genset x (GenSet f) = GenSet $ *do*
seen - gets (x `Set.member`)
*if* seen
*then* return mempty
*else* fmap (DList.cons x) $
modify (Set.insert x) f
toList :: GenSet a - [a]
toList (GenSet f) = DList.toList $ evalState f Set.empty
GenSet is a monoid, where mappend is just union.
*instance* (Ord a) = Monoid (GenSet a) *where*
mempty = GenSet (return mempty)
mappend (GenSet a) (GenSet b) =
GenSet (liftM2 mappend a b)
Okay, so that's how we avoid exponential behavior when traversing the tree.
We can now just toss around GenSets like they're sets and everything will be
peachy. Here's the heart of the algorithm: the reduce function. To avoid
recomputation of rules, we could just memoize the rule function. But we'll
do something a little more clever. The function we'll memoize (parf) first
sparks a thread computing its *last* child. Because the search is
depth-first, it will typically be a while until we get to the last one, so
we benefit from the spark (you don't want to spark a thread computing
something you're about to compute anyway).
reduce :: (Ord a) = Memo.Memo a - (a - [a]) - a - [a]
reduce memo f x = toList (makeSet x)
*where*
makeSet x = genset x . mconcat . map makeSet . f' $ x
f' = memo parf
parf a = *let* ch = f a *in*
ch `seq` (f' (last ch) `par` ch)
The ch `seq` is there so that the evaluation of ch and last ch aren't
competing with each other. Your example had a few problems. You said the
rule was supposed to be expensive, but yours was cheap. Also, [x-1,x-2,x-3]
are all very near each other, so it's hard to go do unrelated stuff. I made
a fake expensive function before computing the neighbors, and tossed around
some prime numbers to scatter the space more.
rule :: Int - [Int]
rule n = expensive `seq`
[next 311 4, next 109 577, next 919 353]
*where*
next x y = (x * n + y) `mod` 5000
expensive = sum [1..50*n]
main :: IO ()
main = *do*
*let* r = reduce Memo.integral rule 1
print (length r)
The results are quite promising: % ghc --make -O2 rules2 -threaded % time
./rules2 5000 ./rules2 13.25s user 0.08s system 99% cpu 13.396 total % time
./rules2 +RTS -N2 5000 ./rules2 +RTS -N2 12.52s user 0.30s system 159% cpu
8.015 total That's 40% decrease in running time! Woot! I'd love to see what
it does on a machine with more than 2 cores.
Enjoy!
Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parallel term reduction
On Mon, Feb 2, 2009 at 2:15 AM, Luke Palmer lrpal...@gmail.com wrote: I spent four hours investigating this problem! Thank you very much for the excellent brainfood, and challenging Haskell's claim to be rawkin' at parallelism. I think, though it took much experimentation, that I have confirmed that it is :-) For those of you who don't like reading ugly gmail-mangled html, I posted my solution here: http://lukepalmer.wordpress.com/2009/02/02/parallel-rewrite-system/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell tutorial for pseudo users?
Hello, Are there any Haskell tutorials suitable for people who don't (and possibly don't want to) know Haskell, but just want to use an embedded language that happens to be in Haskell? Such a tutorial would focus on using libraries rather than defining them. For example, it might explain how to interpret a type signature involving type classes, but not how to write one's own type class. Thanks, / Emil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type metaphysics
Hi, The concept of type seems to be a little like porno: I know it when I see it, but I can't define it (apologies to Justice Stewart). I've picked through lots of documents that discuss types in various ways, but I have yet to find one that actually says what a type really is. For example, definitions of the typed lambda calculus usually define some type symbols and rules like a : T means a is of type T, and then reasoning ensues without discussion of what type means. The only discussion I've found that addresses this is at the Stanford Encyclopedia of Philosophy, article Types and Tokens [1]. It's all very philosophical, but there is one point there that I think has relevance to Haskell. It's in section 4.1, discussing the distinction between types and sets: Another closely related problem also stems from the fact that sets, or classes, are defined extensionally, in terms of their members. The set of natural numbers without the number 17 is a distinct set from the set of natural numbers. One way to put this is that classes have their members essentially. Not so the species homo sapiens, the word 'the', nor Beethoven's Symphony No. 9. The set of specimens of homo sapiens without George W. Bush is a different set from the set of specimens of homo sapiens with him, but the species would be the same even if George W. Bush did not exist. That is, it is false that had George W. Bush never existed, the species homo sapiens would not have existed. The same species might have had different members; it does not depend for its existence on the existence of all its members as sets do. So it appears that one can think of a type as a predicate; any token (value?) that satisfies the predicate is a token (member?) of that type. This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension. My hunch is that it /cannot/ be a set, although I'm not mathematician enough to prove it. My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type). To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially. (I suspect this leads to DeepThink about classical v. constructivist mathematics, but that's a subject for a different discussion.) I'm not sure that works technically, but it seems kinda cool. My question for the list: is the collection of e.g. Tcon Int values a set, or not? If it is, how big is it? Thanks, gregg [1] http://plato.stanford.edu/entries/types-tokens/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] circular dependencies in cabal
Hi Are you still in a not-able-to-do-a-cabal-install state? I had this problem as well and I solved it by simply deleting (or moving) my ~/.ghc directory and then re-installing ghc, as per this message: http://markmail.org/message/fraw3cw56squfeld Note: that this should only be used if you can't solve it the suggested way which is to look in your pkg database for packages registered in both user and global databases and unregister the user one. regards allan Valentyn Kamyshenko wrote: So, in practical terms, you suggest that no new version of the package that ghc package depends on (directly or indirectly) should ever be installed? For example, as soon as process-1.0.1.1 is installed on my computer, I'll have this problem with every package that depends on process? Another question: would not cabal-install automatically fetch the most recent version of the process package, as soon as I will try to install a package that depends on it (such as, for example, plugins)? -- Valentyn. On Feb 1, 2009, at 6:53 AM, Duncan Coutts wrote: On Sun, 2009-02-01 at 01:33 -0800, Valentyn Kamyshenko wrote: Hello all, when I tried to install plugins package with cabal, I've got the following error: # sudo cabal install plugins --global Resolving dependencies... cabal: dependencies conflict: ghc-6.10.1 requires process ==1.0.1.1 however process-1.0.1.1 was excluded because ghc-6.10.1 requires process ==1.0.1.0 For the most part I refer you to: http://haskell.org/pipermail/haskell-cafe/2009-January/054523.html However the difference is that you've got this problem only within the global package db rather than due to overlap in the global and user package db. It looks like both versions of process package are currently required: It looks like you installed process-1.0.1.1 and then rebuilt almost every other package against it. Of course you cannot rebuild the ghc package but you did rebuild some of its dependencies which is why it now depends on multiple versions of the process package. Generally rebuilding a package without also rebuilding the packages that depend on it is a bit dodgy (it can lead to linker errors or segfaults). Unfortunately cabal-install does not prevent you from shooting yourself in the foot in these circumstances. Any suggestions? Aim for a situation where you only have one version of the various core packages. If you do not need to install packages globally then installing them per-user means you at least cannot break the global packages. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Why binding to existing widget toolkits doesn't make any sense
Although efficient text rendering (or more generally, massive similar shape rendering) requires a lot of clever caching I guess :) On Mon, Feb 2, 2009 at 3:26 PM, Jeff Heard jefferson.r.he...@gmail.comwrote: That's my thought. On Mon, Feb 2, 2009 at 7:23 AM, Achim Schneider bars...@web.de wrote: Stephen Tetley stephen.tet...@gmail.com wrote: Also, Shiva-VG - http://sourceforge.net/projects/shivavg - the implementation of OpenVG that the Haskell binding works with supports OpenVG 1.0.1, so it doesn't handle text at all. You know, if the Haskell bindings are compositable enough, it shouldn't be a problem to simply load bezier shapes from freetype into other libraries. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited. ___ 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] Haskell tutorial for pseudo users?
2009/2/2 Emil Axelsson e...@chalmers.se: Hello, Are there any Haskell tutorials suitable for people who don't (and possibly don't want to) know Haskell, but just want to use an embedded language that happens to be in Haskell? Such a tutorial would focus on using libraries rather than defining them. For example, it might explain how to interpret a type signature involving type classes, but not how to write one's own type class. Thanks, / Emil Hi, Emil I don't think it's a good idea (or even possible) to use a Haskell library without knowing anything about Haskell or functional programming. However, it shouldn't take too long to learn the very basics needed to get going, but this of course depends on the complexity of the library you're trying to use. Take some the time to read the parts that are relevant to you in e.g. Learn You a Haskell for Great Good (http://learnyouahaskell.com/) or Real World Haskell which has been published in book form, but is also available at http://book.realworldhaskell.org. If you haven't already taken the course Introduction to Functional Programming given at Chalmers, you can take a look at the lecture slides and/or exercises/labs from the course at http://www.cs.chalmers.se/Cs/Grundutb/Kurser/funht/. I hope that helps. Deniz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Martijn van Steenbergen wrote: To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. Here you're probably thinking about the distinction between countable and uncountable sets. See also: http://en.wikipedia.org/wiki/Countable_set No - it's even bigger than those ! He is thinking of proper classes, not sets. http://en.wikipedia.org/wiki/Class_(set_theory) -- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Foundations and Methods Research Group Director. School of Computer Science and Statistics, Room F.13, O'Reilly Institute, Trinity College, University of Dublin http://www.cs.tcd.ie/Andrew.Butterfield/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
* Martijn van Steenbergen wrote: Int has 2^32 values, just like in Java. Haskell Report 6.4 (revised): The finite-precision integer type Int covers at least the range [ - 2^29, 2^29 - 1]. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell tutorial for pseudo users?
Hi Deniz, Deniz Dogan skrev: I don't think it's a good idea (or even possible) to use a Haskell library without knowing anything about Haskell or functional programming. However, it shouldn't take too long to learn the very Well, I guess I was asking for a tutorial which covers everything except the parts that are not normally relevant for a DSEL user. For example, I would expect the following to be left out: * Definition of data types and classes * Laziness * Monad internals * IO * etc. Things that I think should be covered: * Polymorphism * Higher-order functions * Lists * Recursion * Monadic combinators * etc. Of course, the requirements may vary from case to case, but you get the idea. Take some the time to read the parts that are relevant to you in e.g. Learn You a Haskell for Great Good (http://learnyouahaskell.com/) Seems like a nice and gentle tutorial, somewhat like what I imagined. However, it also seems a bit too high school-oriented for the audience I currently have in mind :) / Emil (who may try to write this tutorial himself at some point) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Hi Martijn, On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: There are many answers to the question what is a type?, depending on one's view. One that has been helpful to me when learning Haskell is a type is a set of values. That's the way I've always thought of types, never having had a good reason to think otherwise. But it seems it doesn't work - type theory goes beyond set theory. I've even found an online book[1] that uses type theory to construct set theory! At least I think that's what it does (not that I understand it.) This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. The tokens/values of Tcon Int may or may not constitute a set, but even if they, we have no way of describing the set's extension. Int has 2^32 values, just like in Java. You can verify this in GHCi: Ok, but that's an implementation detail. My question is what is the theoretical basis of types. Notice that the semantics of Haskell's built-in types are a matter of social convention. The symbols used - Int, 0, 1, 2, ... - are well-known, and we agree not to add data constructors. But we could if we wanted to. Say, Foo :: Int - Int. Then Foo 3 is an Int, distinct from all other Ints; in particular it is not equal to 3. I suspect a full definition of type would have to say something about operations. To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. Here you're probably thinking about the distinction between countable and uncountable sets. See also: It could be that values of a constructed type form an uncountably large set, rather than something too big to be a set at all. I'm afraid I don't know how to work with such critters. In any case, the more interesting thing (to me) is the notion that sets contain their members essentially, but data types don't, as far as I can see. Thanks much, gregg [1] http://www.cs.chalmers.se/Cs/Research/Logic/book/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Thinking of types as sets is not a bad approximation. You need to add
_|_ to your set of values, though.
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
2009/2/2 Gregg Reynolds d...@mobileink.com:
Hi Martijn,
On Mon, Feb 2, 2009 at 9:49 AM, Martijn van Steenbergen
mart...@van.steenbergen.nl wrote:
There are many answers to the question what is a type?, depending on
one's
view.
One that has been helpful to me when learning Haskell is a type is a set
of
values.
That's the way I've always thought of types, never having had a good reason
to think otherwise. But it seems it doesn't work - type theory goes beyond
set theory. I've even found an online book[1] that uses type theory to
construct set theory! At least I think that's what it does (not that I
understand it.)
This gives a very interesting way of looking at Haskell type
constructors: a value of (say) Tcon Int is anything that satisfies
isA Tcon Int. The tokens/values of Tcon Int may or may not
constitute a set, but even if they, we have no way of describing the
set's extension.
Int has 2^32 values, just like in Java. You can verify this in GHCi:
Ok, but that's an implementation detail. My question is what is the
theoretical basis of types.
Notice that the semantics of Haskell's built-in types are a matter of social
convention. The symbols used - Int, 0, 1, 2, ... - are well-known, and we
agree not to add data constructors. But we could if we wanted to. Say, Foo
:: Int - Int. Then Foo 3 is an Int, distinct from all other Ints; in
particular it is not equal to 3.
I suspect a full definition of type would have to say something about
operations.
To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
Here you're probably thinking about the distinction between countable and
uncountable sets. See also:
It could be that values of a constructed type form an uncountably large set,
rather than something too big to be a set at all. I'm afraid I don't know
how to work with such critters.
In any case, the more interesting thing (to me) is the notion that sets
contain their members essentially, but data types don't, as far as I can
see.
Thanks much,
gregg
[1] http://www.cs.chalmers.se/Cs/Research/Logic/book/
___
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] System.Posix.Files.isDirectory and System.Posix.Files.isSymbolicLink
On 2009 Feb 1, at 17:49, Erik de Castro Lopo wrote: The following code creates a symbolic link in the current directory and then uses System.Posix.Files.getFileStatus to get the status of the link. However, isDirectory returns True and isSymbolicLink returns False which is very different from what the stat() system call on a POSIX system would return. I consider this a bug. Have you actually tried it? stat() on a symlink returns information about the target of the link; lstat() returns information about the link itself. These functions correspond to getFileStatus and getSymbolicLinkStatus respectively. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allb...@kf8nh.com system administrator [openafs,heimdal,too many hats] allb...@ece.cmu.edu electrical and computer engineering, carnegie mellon universityKF8NH PGP.sig 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] type metaphysics
Hi and thanks for the response,
On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson
lenn...@augustsson.netwrote:
Thinking of types as sets is not a bad approximation. You need to add
_|_ to your set of values, though.
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
I'm afraid I haven't yet wrapped my head around _|_ qua member of a set. In
any case, I take it that sets being a reasonable /approximation/ of types
means there is a difference.
Back to metaphysics: you pointed out that the function space is countable,
and Christopher noted that there are countably many strings that could be
used to represent a function. So that answers my question about the size of
e.g. Tcon Int. But then again, that's only if we're working under the
assumption that the members of Tcon Int are those we can express with data
constructors and no others. If we drop that assumption,then it seems we
can't say much of anything about its size.
FWIW, what started me on this is the observation that we don't really know
anything about constructed types and values except that they are
constructed. I.e. we know that Foo 3 is the image of 3 under Foo, and
that's all we know. Any thing else (like operations) we must construct out
of stuff we do know (like Ints or Strings.) This might seem trivial, but to
me it seems pretty fundamental, since it leads to the realization that we
can use one thing (e.g. Ints) to talk about something we know nothing about,
which seems to be what category theory is about. (Amateur speaking here.)
Thanks,
gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 8:09 AM, Gregg Reynolds d...@mobileink.com wrote: Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it. It's too big for Set Theory if you insist on representing functions in type theory as functions in set theory - ie. set(A - B) = set(B)^set(A). But if you don't insist on such a constraint there's no problem with sets. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
If we're talking Haskell types here I think it's reasonable to talk
about the values of a type as those that we can actually express in
the Haskell program, any other values are really besides the point.
Well, if you have a more philosophical view of types then I guess
there is a point, but I thought you wanted to know about Haskell
types?
There's nothing mysterious about _|_ being a member of a set. Say
that you have a function (Int-Bool). What are the possible results
when you run this function? You can get False, you can get True, and
the function can fail to terminate (I'll include any kind of runtime
error in this).
So now we want to turn this bit of computing into mathematics, so we
say that the result must belong to the set {False,True,_|_} where
we've picked the name _|_ for the computation that doesn't terminate.
Note that is is mathematics, there's no notion of non-termination
here. The function simply maps to one of three values.
There's a natural ordering of the elements {False,True,_|_}. The _|_
is less than False and less than True, whereas False and True are
unordered with respect to each other. Think of this ordering as how
much information you get. Non-termination is less information than a
definite False or True.
Domain theory deals with this kind of ordered sets.
-- Lennart
On Mon, Feb 2, 2009 at 4:51 PM, Gregg Reynolds d...@mobileink.com wrote:
Hi and thanks for the response,
On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson lenn...@augustsson.net
wrote:
Thinking of types as sets is not a bad approximation. You need to add
_|_ to your set of values, though.
So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
I'm afraid I haven't yet wrapped my head around _|_ qua member of a set. In
any case, I take it that sets being a reasonable /approximation/ of types
means there is a difference.
Back to metaphysics: you pointed out that the function space is countable,
and Christopher noted that there are countably many strings that could be
used to represent a function. So that answers my question about the size of
e.g. Tcon Int. But then again, that's only if we're working under the
assumption that the members of Tcon Int are those we can express with data
constructors and no others. If we drop that assumption,then it seems we
can't say much of anything about its size.
FWIW, what started me on this is the observation that we don't really know
anything about constructed types and values except that they are
constructed. I.e. we know that Foo 3 is the image of 3 under Foo, and
that's all we know. Any thing else (like operations) we must construct out
of stuff we do know (like Ints or Strings.) This might seem trivial, but to
me it seems pretty fundamental, since it leads to the realization that we
can use one thing (e.g. Ints) to talk about something we know nothing about,
which seems to be what category theory is about. (Amateur speaking here.)
Thanks,
gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Lennart Augustsson wrote: The Haskell function space, A-B, is not uncountable. There is only a countable number of Haskell functions you can write, so how could there be more elements in the Haskell function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions. I was thinking about a fixed function type A - B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A - B. Is that what you meant? For example, fix the type to Integer - Bool. I can't enumeratate all possible implementations of this function. Right? Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
You can enumerate all possible implementations of functions of type (Integer - Bool). Just enumerate all strings, and give this to a Haskell compiler f :: Integer - Bool f = enumerated-string-goes-here if the compiler is happy you have an implementation. The enumerated functions do not include all mathematical functions of type (Integer - Bool), but it does include the ones we usually mean by the type (Integer - Bool) in Haskell. -- Lennart On Mon, Feb 2, 2009 at 4:47 PM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: Lennart Augustsson wrote: The Haskell function space, A-B, is not uncountable. There is only a countable number of Haskell functions you can write, so how could there be more elements in the Haskell function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions. I was thinking about a fixed function type A - B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A - B. Is that what you meant? For example, fix the type to Integer - Bool. I can't enumeratate all possible implementations of this function. Right? Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
I had the same idea, here's my implemention, running on an old Winhugs 2001 (and GHC 6.8). regards, Daniel import System import Directory chars = map chr [32..126] string 0 = return string n = do c - chars s - string (n-1) return (c:s) mkfun n = do s - string n return (f :: Integer - Bool; f = ++ s) test fundef = do system (del test.exe) writeFile test.hs (fundef ++ ; main = return ()) system (ghc --make test.hs) b - doesFileExist test.exe if b then putStrLn fundef else return () main = do let fundefs = [0..] = mkfun mapM_ test $ drop 1000 fundefs Lennart Augustsson schrieb: You can enumerate all possible implementations of functions of type (Integer - Bool). Just enumerate all strings, and give this to a Haskell compiler f :: Integer - Bool f = enumerated-string-goes-here if the compiler is happy you have an implementation. The enumerated functions do not include all mathematical functions of type (Integer - Bool), but it does include the ones we usually mean by the type (Integer - Bool) in Haskell. -- Lennart On Mon, Feb 2, 2009 at 4:47 PM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: Lennart Augustsson wrote: The Haskell function space, A-B, is not uncountable. There is only a countable number of Haskell functions you can write, so how could there be more elements in the Haskell function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions. I was thinking about a fixed function type A - B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A - B. Is that what you meant? For example, fix the type to Integer - Bool. I can't enumeratate all possible implementations of this function. Right? Martijn. ___ 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] Re: 1,000 packages, so let's build a few!
On Mon, 2009-02-02 at 13:49 +0900, Benjamin L.Russell wrote: On Sun, 01 Feb 2009 15:01:28 +, Duncan Coutts duncan.cou...@worc.ox.ac.uk wrote: On Sat, 2009-01-31 at 16:50 -0800, Don Stewart wrote: Windows people need to set up a wind...@haskell.org to sort out their packaging issues, like we have for debian, arch, gentoo, freebsd and other distros. Unless people take action to get things working well on their platform, it will be slow going. Actually instead of going off into another mailing list I would encourage them to volunteer on the cabal-devel mailing list to help out. There is lots we could do to improve the experience on Windows and half the problem is we do not have enough people working on it or testing things. That sounds like a great idea, but what specifically should Windows users do to help out? If we try to install a package on Windows and encounter a bug that we can't figure out, would it be sufficient to subscribe at http://www.haskell.org/mailman/listinfo/cabal-devel and to submit a bug report to cabal-de...@haskell.org ? So on cabal-devel we are concerned with bugs and missing features in Cabal that make life hard for windows users. We cannot directly fix individual packages, there are too many and that is the job of the package maintainers. We are interested in solving the more systemic problems however. So for example working out if we can replace many of the configure scripts: http://hackage.haskell.org/trac/hackage/ticket/482 Or just improving the error message when we fail to run configure http://hackage.haskell.org/trac/hackage/ticket/403 Or support in the cabal-install planner for non-Haskell dependencies (so we can track dependencies on sh.exe or libs that are not available on Windows.) The point is to make best use of the available information to work out which packages have no hope of building on Windows. We also have a collection of tickets that primarily affect Windows: http://hackage.haskell.org/trac/hackage/query?status=newstatus=assignedstatus=reopenedplatform=Windowsorder=priority many of these need help from windows users, either to decide what the solution should be or to test the solution. Having more Cabal volunteers who use Windows would be great. I've recently been trying to solve some permissions problems on Windows which is pretty hard without having proper access to a Windows system. There are also some important tickets that are just sitting around waiting for some policy decision to be made. The couple people who used to advise us on these questions (like what default install locations should be etc) have not had time recently so these things just sit around with no decisions made. So actually just having more Windows users subscribed to cabal-devel and commenting on tickets would be very useful, even if you do not have much time for hacking. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
oops, the '$ drop 1000' in the main function should not be there... Daniel van den Eijkel schrieb: I had the same idea, here's my implemention, running on an old Winhugs 2001 (and GHC 6.8). regards, Daniel import System import Directory chars = map chr [32..126] string 0 = return string n = do c - chars s - string (n-1) return (c:s) mkfun n = do s - string n return (f :: Integer - Bool; f = ++ s) test fundef = do system (del test.exe) writeFile test.hs (fundef ++ ; main = return ()) system (ghc --make test.hs) b - doesFileExist test.exe if b then putStrLn fundef else return () main = do let fundefs = [0..] = mkfun mapM_ test $ drop 1000 fundefs Lennart Augustsson schrieb: You can enumerate all possible implementations of functions of type (Integer - Bool). Just enumerate all strings, and give this to a Haskell compiler f :: Integer - Bool f = enumerated-string-goes-here if the compiler is happy you have an implementation. The enumerated functions do not include all mathematical functions of type (Integer - Bool), but it does include the ones we usually mean by the type (Integer - Bool) in Haskell. -- Lennart On Mon, Feb 2, 2009 at 4:47 PM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: Lennart Augustsson wrote: The Haskell function space, A-B, is not uncountable. There is only a countable number of Haskell functions you can write, so how could there be more elements in the Haskell function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions. I was thinking about a fixed function type A - B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A - B. Is that what you meant? For example, fix the type to Integer - Bool. I can't enumeratate all possible implementations of this function. Right? Martijn. ___ 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] type metaphysics
Gregg Reynolds d...@mobileink.com writes: This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. Reminiscent of arguments between dynamic and static typing camps - as far as I understand, a dynamic type is just a predicate. So division by zero is a type error, since the domain of division is the type of all numbers except zero. In contrast, I've always thought of (static) types as disjoint sets of values. My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type). I guess I don't quite understand what you mean by Tcon Int above. Could you give a concrete example of such a type? To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. I suspect that since types and values are separate domains, you avoid the complications caused by self reference. In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially. I don't follow this argument. Are you saying you can remove a data constructor from a type, and still have the same type? And because of this, the values of the type do not constitute a set? I guess it boils down to how Tcon Int does not depend on any particular constructor. -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson
lenn...@augustsson.netwrote:
If we're talking Haskell types here I think it's reasonable to talk
about the values of a type as those that we can actually express in
the Haskell program, any other values are really besides the point.
Well, if you have a more philosophical view of types then I guess
there is a point, but I thought you wanted to know about Haskell
types?
The metaphysics thereof. ;) I want to situate them in the larger
intellectual context to get a more precise answer to what is a type,
really?
There's nothing mysterious about _|_ being a member of a set. Say
that you have a function (Int-Bool). What are the possible results
when you run this function? You can get False, you can get True, and
the function can fail to terminate (I'll include any kind of runtime
error in this).
So now we want to turn this bit of computing into mathematics, so we
say that the result must belong to the set {False,True,_|_} where
we've picked the name _|_ for the computation that doesn't terminate.
Note that is is mathematics, there's no notion of non-termination
here. The function simply maps to one of three values.
I like that, thanks.
-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] FP simulators for real-time systems?
Hello, I'm interested to hear if anyone out there has used Haskell (or other functional languages for that matter) to build simulators for real- time systems. I'm somewhat familiar with Timber http://www.timber-lang.org/ and similar languages for actually constructing real-time systems. However, I'm more interested in documented uses of FP out-of-the- box to build simulators and associated test harnesses. Pointers to published papers are particularly appreciated. Thanks! Lee ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde ke...@malde.org wrote: Gregg Reynolds d...@mobileink.com writes: This gives a very interesting way of looking at Haskell type constructors: a value of (say) Tcon Int is anything that satisfies isA Tcon Int. Reminiscent of arguments between dynamic and static typing camps - as far as I understand, a dynamic type is just a predicate. So division by zero is a type error, since the domain of division is the type of all numbers except zero. In contrast, I've always thought of (static) types as disjoint sets of values. My reasoning is that we can define an infinite number of data constructors for it, including at least all possible polynomials (by which I mean data constructors of any arity taking args of any type). I guess I don't quite understand what you mean by Tcon Int above. Could you give a concrete example of such a type? Just shorthand for something like data Tcon a = Dcon a, applied to Int. Any data constructor expression using an Int will yield a value of type Tcon Int. To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. I suspect that since types and values are separate domains, you avoid the complications caused by self reference. In any case, Tcon Int does not depend on any particular constructor, just as homo sapiens does not depend on any particular man. So it can't be a set because it doesn't have its members essentially. I don't follow this argument. Are you saying you can remove a data constructor from a type, and still have the same type? And because of this, the values of the type do not constitute a set? Yep. Well, that is /if/ you start from the Open-World Assumption - see http://en.wikipedia.org/wiki/Open_World_Assumption (very important in ontologies e.g. OWL and Description Logics). Just because we know that e.g. expressions like Dcon 3 yield values of type Tcon Int does not mean that we know that those are the only such expressions. So we can't really say anything about how big it can be. Who knows, it might actually be a useful distinction for an OWL reasoner in Haskell. I guess it boils down to how Tcon Int does not depend on any particular constructor. That seems like a good way of putting it. -g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] FP simulators for real-time systems?
Opis is an ocaml library for implementing reactive systems where the same code can either be executed, run in a simulator or used as a specification in a formal model checker. The model checking is only possible because referential transparency massively reduces the state space of the program. http://perso.eleves.bretagne.ens-cachan.fr/~dagand/opis/ Flask is a similar haskell project which generates code for sensor networks. I don't know if they've gone as far down the testing/modelling route. http://www.eecs.harvard.edu/~mainland/flask/ The general theme is promising - reducing mutable state makes it much easier to automate reasoning about code. Jamie On Mon, Feb 2, 2009 at 6:43 PM, Lee Pike leep...@gmail.com wrote: Hello, I'm interested to hear if anyone out there has used Haskell (or other functional languages for that matter) to build simulators for real-time systems. I'm somewhat familiar with Timber http://www.timber-lang.org/ and similar languages for actually constructing real-time systems. However, I'm more interested in documented uses of FP out-of-the-box to build simulators and associated test harnesses. Pointers to published papers are particularly appreciated. Thanks! Lee ___ 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] Haskell tutorial for pseudo users?
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Emil Axelsson wrote: | Well, I guess I was asking for a tutorial which covers everything except | the parts that are not normally relevant for a DSEL user. For example, I | would expect the following to be left out: | | * Definition of data types and classes | * Laziness | * Monad internals | * IO | * etc. | | Things that I think should be covered: | | * Polymorphism | * Higher-order functions | * Lists | * Recursion | * Monadic combinators | * etc. | | Of course, the requirements may vary from case to case, but you get the | idea. I think that the contents of the two lists would vary so dramatically from case to case that writing a generic tutorial of this sort would likely be impossible. - - Jake -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkmHRm8ACgkQye5hVyvIUKk1+ACdF4b6m/+NWR56AqbTLhGWxb3b fFwAn3f6AHnbGionwlYsa47Vnz7ZW4VC =UTae -END PGP SIGNATURE- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Hi, Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer: That question has kind of a crazy answer. In mathematics, Nat - Bool is uncountable, i.e. there is no function Nat - (Nat - Bool) which has every function in its range. But we know we are dealing with computable functions, so we can just enumerate all implementations. So the computable functions Nat - Bool are countable. However! If we have a function f : Nat - Nat - Bool, we can construct the diagonalization g : Nat - Bool as: g n = not (f n n), with g not in the range of f. That makes Nat - Bool computably uncountable. That argument has a flaw. Just because we have a function in the mathematical sense that sends ℕ to (Nat - Bool) does not mean that we have Haskell function f of that type that we can use to construct g. Greetings, Joachim -- Joachim nomeata Breitner mail: m...@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nome...@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nome...@debian.org signature.asc Description: Dies ist ein digital signierter Nachrichtenteil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
The actual presentation and layout of widgets would be better handled by a DSL such as CSS (which is, in fact, declarative in nature), while event logic would be best handled purely in Haskell. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 12:39 PM, Creighton Hogg wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C ___ 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] why typeRepArgs (typeOf hello) is [Char] ?
Hello, With Data.Typeable : *Graph typeRepArgs (typeOf 1) [] *Graph typeRepArgs (typeOf 'a') [] *Graph typeRepArgs (typeOf True) [] *Graph typeRepArgs (typeOf hello) [Char] I don't understand why the latter is not []. Could someone explain it ? Thank you, Thu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, 2009-02-02 at 17:30 +0100, Krzysztof Skrzętnicki wrote: Do they? Haskell is a programing language. Therefore legal Haskell types has to be represented by some string. And there are countably many strings (of which only a subset is legal type representation, but that's not important). Haskell possesses models[1] in which the carriers of all types are countable. Haskell also possesses the models[2] which do assign uncountable carriers to several Haskell types --- a - b whenever a has an infinite carrier (and b is not a degenerate type of the form newtype B = B B ), [b] under the same conditions on b, etc. In many cases, these are the most insightful models, and I those models are what people mean when they talk about e.g. [Int] having an un-countable denotation. jcc [1] IIUC all models based on recursion theory have this property [2] IIUC most models based on domain theory have this property ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why typeRepArgs (typeOf hello) is [Char] ?
On Mon, 2009-02-02 at 21:09 +0100, minh thu wrote: Hello, With Data.Typeable : *Graph typeRepArgs (typeOf 1) [] *Graph typeRepArgs (typeOf 'a') [] *Graph typeRepArgs (typeOf True) [] *Graph typeRepArgs (typeOf hello) [Char] I don't understand why the latter is not []. Could someone explain it ? Because (hello :: [] Char)? Prelude :t hello hello :: [Char] jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why typeRepArgs (typeOf hello) is [Char] ?
The type of hello is String, which is [Char], which is really [] Char (that is, the list type of kind * - *, applied to Char). 1, 'a', and True are all simple types (I'm sure there's a more particular term, maybe monomorphic?) with no type arguments. [] has a type argument, Char. Consider: Prelude Data.Typeable typeRepArgs (typeOf (Just 1)) [Integer] and Prelude Data.Typeable typeRepArgs (typeOf (Left 'a' :: Either Char Int)) [Char,Int] -- typeRepArgs is giving you the arguments of the root type application, [] (list) in your case, Maybe and Either for the two examples I gave. Does this make sense? -Ross On Feb 2, 2009, at 3:09 PM, minh thu wrote: Hello, With Data.Typeable : *Graph typeRepArgs (typeOf 1) [] *Graph typeRepArgs (typeOf 'a') [] *Graph typeRepArgs (typeOf True) [] *Graph typeRepArgs (typeOf hello) [Char] I don't understand why the latter is not []. Could someone explain it ? Thank you, Thu ___ 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] type metaphysics
Gregg Reynolds d...@mobileink.com writes: Just shorthand for something like data Tcon a = Dcon a, applied to Int. Any data constructor expression using an Int will yield a value of type Tcon Int. Right. But then the set of values is isomorphic to the set of Ints, right? I don't follow this argument. Are you saying you can remove a data constructor from a type, and still have the same type? And because of this, the values of the type do not constitute a set? Yep. I don't see why you would consider it the same type. Since, given any two data types, I could remove all the data constructors, this would make them, and by extension, all types the same, wouldn't it? -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why typeRepArgs (typeOf hello) is [Char] ?
Thanks. Could you add to your explanation this one : *Graph typeRepArgs (typeOf (+)) [Integer,Integer - Integer] In fact, I tried to write a function that would give the types used by a function, for instance [Integer, Integer, Integer] for (+) (the last one would be the 'return' type). So I applied recursively typeRepArgs to the second element of the list (if any) (here, Integer - Integer). It worked well until I tried it on a function like :: Char - Int - [Char] where the last recursive call gives [Char] instead of []. Is it possible to write such a function ? Thank you, Thu 2009/2/2 Ross Mellgren rmm-hask...@z.odi.ac: The type of hello is String, which is [Char], which is really [] Char (that is, the list type of kind * - *, applied to Char). 1, 'a', and True are all simple types (I'm sure there's a more particular term, maybe monomorphic?) with no type arguments. [] has a type argument, Char. Consider: Prelude Data.Typeable typeRepArgs (typeOf (Just 1)) [Integer] and Prelude Data.Typeable typeRepArgs (typeOf (Left 'a' :: Either Char Int)) [Char,Int] -- typeRepArgs is giving you the arguments of the root type application, [] (list) in your case, Maybe and Either for the two examples I gave. Does this make sense? -Ross On Feb 2, 2009, at 3:09 PM, minh thu wrote: Hello, With Data.Typeable : *Graph typeRepArgs (typeOf 1) [] *Graph typeRepArgs (typeOf 'a') [] *Graph typeRepArgs (typeOf True) [] *Graph typeRepArgs (typeOf hello) [Char] I don't understand why the latter is not []. Could someone explain it ? Thank you, Thu ___ 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] ANN: regex-posix-unittest-1.0 AND regex-posix-0.94.1 AND regex-tdfa-0.97.1
I have three announcements to make about regex-* related packages. The regex-posix-0.94.1 package update provides better semantics for multiple matches. Below version 0.94, if any match was empty the matching would stop. Now the empty match is returned and the position is incremented and the searching continues. The regex-tdfa-0.71.1 package update provides the same new multiple match semantics. It also fixes a bug I found. I know of no outstanding bugs in regex-tdfa, and version 0.71.1 now passes all the tests used in regex-posix-unittest-1.0 announced below. We should care about the correctness of our operating system libraries. To help with this, I have a NEW package to announce: regex-posix-unittest-1.0 The accompanying wiki page is http://www.haskell.org/haskellwiki/Regex_Posix This new package provides an executable called regex-posix-unittest which you can install as --user or --global. The regex-posix-unittest executable with no arguments runs a suite of unit tests, all of which are described by text files in the package, the format is documented in the wiki page. By editing the text files in the package you can add to or delete from the unit tests being run. With two arguments the program expects the text first and the pattern second and will run just that match and print all the results. How does regex-posix-unittest help us care about the OS libraries? The regex-posix distributed in the GHC bundle uses the OS C library's regex.h API. The regex-posix-unittest package will quite likely show you that your OS C library regex.h API is full of bugs. If you are on Linux, it will show you a plethora of GLIBC bugs in Posix conformance. If you are on OS X, FreeBSD, or NetBSD, it will show you many bugs including a critical bug where it fail to find a match where one actually exists. These bugs in the OS library are inherited by your sed program as well as regex-posix and Haskell. If you are on Windows, or OpenBSD, or Solaris, or anything else, then please update the wiki page at http://www.haskell.org/haskellwiki/Regex_Posix or email me with your results so I can update the wiki. You may have evil and ingenious tests of Posix extended regular expressions to add to the test suite. Adding them is easy and if you send them to me I will put them in an updated version of regex-posix-unittest. Cheers, Chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why typeRepArgs (typeOf hello) is [Char] ?
Sure: (+) :: Integer - Integer - Integer (really Num a = a - a - a, but we'll use the defaulted one) Which is really (+) :: - Integer (- Integer Integer)(that is, the function type constructor is * - * - * and right associative) So when you say typeRepArgs (typeOf (+)) you get Integer and (- Integer Integer), which pretty-prints as (Integer - Integer) It is possible, but you have to check if the type constructor is really a function type, e.g.: import Data.Typeable funTyCon :: TyCon funTyCon = mkTyCon - argsOf :: TypeRep - [TypeRep] argsOf ty | typeRepTyCon ty == funTyCon = let (x:y:[]) = typeRepArgs ty in x : argsOf y | otherwise = [] *Main Data.Typeable let f = (undefined :: Int - Char - String - ()) *Main Data.Typeable argsOf (typeOf f) [Int,Char,[Char]] -Ross On Feb 2, 2009, at 3:27 PM, minh thu wrote: Thanks. Could you add to your explanation this one : *Graph typeRepArgs (typeOf (+)) [Integer,Integer - Integer] In fact, I tried to write a function that would give the types used by a function, for instance [Integer, Integer, Integer] for (+) (the last one would be the 'return' type). So I applied recursively typeRepArgs to the second element of the list (if any) (here, Integer - Integer). It worked well until I tried it on a function like :: Char - Int - [Char] where the last recursive call gives [Char] instead of []. Is it possible to write such a function ? Thank you, Thu 2009/2/2 Ross Mellgren rmm-hask...@z.odi.ac: The type of hello is String, which is [Char], which is really [] Char (that is, the list type of kind * - *, applied to Char). 1, 'a', and True are all simple types (I'm sure there's a more particular term, maybe monomorphic?) with no type arguments. [] has a type argument, Char. Consider: Prelude Data.Typeable typeRepArgs (typeOf (Just 1)) [Integer] and Prelude Data.Typeable typeRepArgs (typeOf (Left 'a' :: Either Char Int)) [Char,Int] -- typeRepArgs is giving you the arguments of the root type application, [] (list) in your case, Maybe and Either for the two examples I gave. Does this make sense? -Ross On Feb 2, 2009, at 3:09 PM, minh thu wrote: Hello, With Data.Typeable : *Graph typeRepArgs (typeOf 1) [] *Graph typeRepArgs (typeOf 'a') [] *Graph typeRepArgs (typeOf True) [] *Graph typeRepArgs (typeOf hello) [Char] I don't understand why the latter is not []. Could someone explain it ? Thank you, Thu ___ 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] Why binding to existing widget toolkits doesn't make any sense
Could CSS give us semantic clarity? - Conal On Mon, Feb 2, 2009 at 11:58 AM, John A. De Goes j...@n-brain.net wrote: The actual presentation and layout of widgets would be better handled by a DSL such as CSS (which is, in fact, declarative in nature), while event logic would be best handled purely in Haskell. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 12:39 PM, Creighton Hogg wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C ___ 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] type metaphysics
Hi Gregg,
Firsly: I'm not an expert on this, so if anyone thinks I'm writing
nonsense, do correct me.
There are many answers to the question what is a type?, depending on
one's view.
One that has been helpful to me when learning Haskell is a type is a
set of values. When seen like this it makes sense to write:
() = { () }
Bool = { True, False }
Maybe Bool = { Nothing, Just True, Just False }
Recursive data types have an infinite number of values. Almost all types
belong to this group. Here's one of the simplest examples:
data Peano = Zero | Suc Peano
There's nothing wrong with a set with an infinite number of members.
Gregg Reynolds wrote:
This gives a very interesting way of looking at Haskell type
constructors: a value of (say) Tcon Int is anything that satisfies
isA Tcon Int. The tokens/values of Tcon Int may or may not
constitute a set, but even if they, we have no way of describing the
set's extension.
Int has 2^32 values, just like in Java. You can verify this in GHCi:
Prelude (minBound, maxBound) :: (Int, Int)
(-2147483648,2147483647)
Integer, on the other hand, represents arbitrarily big integers and
therefore has an infinite number of elements.
To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
Here you're probably thinking about the distinction between countable
and uncountable sets. See also:
http://en.wikipedia.org/wiki/Countable_set
Haskell has types which have uncountably many values. They are all
functions of the form A - B, where A is an infinite type (either
countably or uncountably).
If a set is countable, you can enumerate the set in such a way that you
will reach each member eventually. For Haskell this means that if a type
a has a countable number of values, you can define a list :: [a] that
will contain all of them.
I hope this helps! Let us know if you have any other questions.
Martijn.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type and data constructors in CT
On Sun, Feb 1, 2009 at 12:36 PM, Gregg Reynolds d...@mobileink.com wrote: On Sat, Jan 31, 2009 at 3:14 PM, David Menendez d...@zednenem.com wrote: There's a paper about defining catamorphisms for GADTs and nested recursive types that models type constructors that way. If you recall a title or author I'll google it. I believe it was Foundations for Structural Programming with GADTs. http://crab.rutgers.edu/~pjohann/popl08.pdf So this gives us two functors, but they operate on different things, and I don't see how to get from one to the other in CT terms. Or rather, they're obviously related, but I don't see how to express that relation formally. Again, what sort of relationship are you thinking of? Data Ok, good question. I guess the problem I'm having is one of abstraction management. CT prefers to disregard the contents of its objects, imposing a kind of blood-brain barrier between the object and its internal structure. Typical definitions of functor, for example, make no reference to the elements of an object; a functor is just a pair of morphisms, one taking objects to objects, the other morphisms to morphisms. This leaves the naive reader (i.e. me) to wonder how it is that the internal stuff is related to the functor stuff. Right. The reason the definition of functor doesn't say anything about the internal stuff is that there are plenty of categories where there *is* no internal stuff. So for categories like Set or Mon, where the objects to have elements, category theory uses morphisms to describe their internal structure. For example, a set is an object in Set, and its elements are morphisms from the singleton set. So if I have some operation that creates a monoid from a set, and transforms set functions into monoid homomorphisms in a way that respects identity functions and composition, then I have a functor from Set to Mon. (For example, the free monoid that Wren mentioned.) Whatever internal stuff is going on will be reflected in the morphism part of the functor, because otherwise the functor can't map the morphisms correctly. For example: is it true that the object component of a functor necessarily has a bundle of specific functions relating the internal elements of the objects? If so, is the object component merely an abstraction of the bundle? Or is it ontologically a different thing? Let me try to give an illustrative example. Consider a category A with a single object and a bunch of morphisms from that object to itself. Now, the object itself isn't interesting, which is why I didn't give it a name. It's not any kind of set, and the morphisms aren't functions: composition just combines them in some unspecified manner. Because A is a category, we know that there's an identity morphism id, such that f . id = f = id . f, and we know that f . (g . h) = (f . g) . h. In other words, the morphisms in a single-object category form a monoid. What's more, since we don't care about what the morphisms are, we can take any monoid and create a single-object category. For example, we could define a category Plus where the morphisms are natural numbers, the identity morphism is 0, and morphism composition is addition. Now let's say we have to single-object categories, A and B, and a functor F : A - B. What do we know about F? We know that F maps the object in A to the object in B, and it maps the identity morphism in A to the identity morphism in B, and that for any morphisms f and g in A, F(f) . F(g) = F(f . g). In other words, F is a monoid homomorphism (that is, a mapping from one monoid to another that respects the identity and the monoid operation). We can define other functors, too. For example, a functor P : Plus - Set. We'll map the object in Plus to N (the set of natural numbers), and every morphism n in Plus to a function (\x - n + x) : N - N. You can prove for yourself that P(0) gives the identity morphism for N, and that P(m + n) = P(m) . P(n). So P is a functor whose object component doesn't have a bundle of specific functions relating the internal elements of the objects. All the interesting stuff in P takes place in the morphism map. Does that help at all? (A side note: As I said, for any monoid X, we can create a category C(X), and it's obvious that for any monoid homomorphism f : X - Y, we can create a functor C(f) : C(X) - C(Y). It turns out that for any monoids X, Y, and Z and homomorphisms f : Y - Z and g : X - Y, C(f) . C(g) = C(f . g). So C is a functor from the category of monads to the category of categories.) -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
On Mon, Feb 2, 2009 at 11:39 AM, Creighton Hogg wch...@gmail.com wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? Again, my goal would not be a purely functional library, because even IO is purely functional. My goal is a denotational library, i.e., one that has an elegant (denotational) semantics, and hence is powerfully compositional and good for reasoning. The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C The Fruit paper, Genuinely Functional User Interfaceshttp://www.apocalypse.org/pub/u/antony/work/pubs/genuinely-functional-guis.pdf, gives a semantic model, which could be a starting place for thinking about possibilities. At the very least, I'd like to take it to 3D. The idea there is that a UI is a function from flows (behaviors/signals) to flows, where the input includes mouse keyboard stuff and the output includes an image. An image is, as in Pan, a function from R^2 - Color, where color includes partial opacity. When UIs are transformed in time and/or space, they correspondingly see inversely-transformed input, thanks to a general principle of transforming functions. - Conal ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
The size, color, and layout of widgets has no effect on interaction semantics and is best pushed elsewhere, into a designer-friendly realm such as CSS. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 2:15 PM, Conal Elliott wrote: Could CSS give us semantic clarity? - Conal On Mon, Feb 2, 2009 at 11:58 AM, John A. De Goes j...@n-brain.net wrote: The actual presentation and layout of widgets would be better handled by a DSL such as CSS (which is, in fact, declarative in nature), while event logic would be best handled purely in Haskell. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 12:39 PM, Creighton Hogg wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C ___ 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] Cabal and more than one version
Hi, I'm bringing up an old thread, because it's very relevant to my problem. On Tue, Nov 18, 2008 at 22:30, Duncan Coutts wrote: On Tue, 2008-11-18 at 01:48 -0800, Jason Dusek wrote: I'd like to be able to do something like: if (template-haskell 2.3) cpp-options: -D TH_THE_YOUNGER else cpp-options: -D TH_THE_ELDER I guess this kind of thing is not possible at present? It is possible, in two different ways. The easiest way is that if you're using Cabal-1.6 then it provides cpp macros to test the version number of packages you're using. #if MIN_VERSION_template_haskell(2,3,0) ... #elseif ... #endif The alternative that works back to Cabal-1.2 is to use: flag newer-th ... if flag(newer-th) build-depends: template-haskell = 2.3 cpp-options: -D TH_THE_ELDER else build-depends: template-haskell 2.3 cpp-options: -D TH_THE_YOUNGER Either I'm doing something wrong or this doesn't work for cabal-install and GHC 6.8.3. I used the flag newer-th approach in EMGM: https://svn.cs.uu.nl:12443/viewvc/dgp-haskell/EMGM/tags/emgm-0.2/emgm.cabal?view=markup [...] flag th23 description: Define a CPP flag that enables conditional compilation for template-haskell package version 2.3 and newer. Library [...] build-depends: base = 3.0 4.0, template-haskell 2.4 -- Include deriveRep for Loc. This was introduced with -- template-haskell-2.3, included with GHC 6.10. if flag(th23) build-depends: template-haskell = 2.3 cpp-options: -DTH_LOC_DERIVEREP else build-depends: template-haskell 2.3 [...] When I run cabal install emgm (with GHC 6.8.3 and either Cabal 1.2 or 1.6), it tries (and fails) to install template-haskell-2.3. That's exactly what I don't want. Any suggestions? Thanks, Sean ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] cURL under Windows again
Hello cafe-subscribers, I saw some issues about installing haskell bindings for cURL under Windows, and now I'm trapped too. So, here is actions' log for everything (very detail; you can PgDn to the end with questions): 1. Windows Vista without UAC 2. ghc-6.10.1-i386-windows.exe is installed to C:\Program Files\Haskell C:\Program Files\Haskell\package.conf wasn't touched after installation (Cabal nor manually) 3. MinGW-5.1.4 installed to C:\temp\MinGW 4. MSys-1.0 installed to C:\temp\msys\1.0\ 5. curl-7.19.3.tar.bz2 had taken from http://curl.haxx.se/download/curl-7.19.3.tar.bz2 6. Under msys, curl-7.19.3.tar.bz2 is untared into /home/Kuznetsov/curl-7.19.3 7. cURL is made as: cd curl-7.19.3 $ ./configure configure: Configured to build curl/libcurl: ... curl version:7.19.3 Host setup: i686-pc-mingw32 Install prefix: /usr/local Compiler:gcc SSL support: no (--with-ssl / --with-gnutls) SSH support: no (--with-libssh2) zlib support:no (--with-zlib) krb4 support:no (--with-krb4*) GSSAPI support: no (--with-gssapi) SPNEGO support: no (--with-spnego) c-ares support: no (--enable-ares) ipv6 support:no (--enable-ipv6) IDN support: no (--with-libidn) Build libcurl: Shared=yes, Static=yes Built-in manual: no (--enable-manual) Verbose errors: enabled (--disable-verbose) SSPI support:no (--enable-sspi) ca cert bundle: no ca cert path:no LDAP support:enabled (winldap) LDAPS support: no (--enable-ldaps) $ make ... make[2]: Leaving directory `/home/Kuznetsov/curl-7.19.3/src' make[1]: Leaving directory `/home/Kuznetsov/curl-7.19.3/src' make[1]: Entering directory `/home/Kuznetsov/curl-7.19.3' make[1]: Nothing to be done for `all-am'. make[1]: Leaving directory `/home/Kuznetsov/curl-7.19.3' $ make install ... libtool: install: /bin/install -c .libs/libcurl.dll.a /usr/local/lib/libcurl.dll.a libtool: install: base_file=`basename libcurl.la` libtool: install: dlpath=`/bin/sh 21 -c '. .libs/'libcurl.la'i; echo libcurl-4.dll'` libtool: install: dldir=/usr/local/lib/`dirname ../bin/libcurl-4.dll` libtool: install: test -d /usr/local/lib/../bin || mkdir -p /usr/local/lib/../bin libtool: install: /bin/install -c .libs/libcurl-4.dll /usr/local/lib/../bin/libcurl-4.dll libtool: install: chmod a+x /usr/local/lib/../bin/libcurl-4.dll libtool: install: if test -n '' test -n 'strip --strip-unneeded'; then eval 'strip --strip-unneeded /usr/local/lib/../bin/libcurl-4.dll' || exit 0; fi libtool: install: /bin/install -c .libs/libcurl.lai /usr/local/lib/ libcurl.la libtool: install: /bin/install -c .libs/libcurl.a /usr/local/lib/libcurl.a libtool: install: chmod 644 /usr/local/lib/libcurl.a libtool: install: ranlib /usr/local/lib/libcurl.a -- Libraries have been installed in: /usr/local/lib If you ever happen to want to link against installed libraries in a given directory, LIBDIR, you must either use libtool, and specify the full pathname of the library, or use the `-LLIBDIR' flag during linking and do at least one of the following: - add LIBDIR to the `PATH' environment variable during execution - add LIBDIR to the `LD_RUN_PATH' environment variable during linking - use the `-LLIBDIR' linker flag ... /bin/install -c -m 644 'curl.h' '/usr/local/include/curl/curl.h' /bin/install -c -m 644 'curlver.h' '/usr/local/include/curl/curlver.h' /bin/install -c -m 644 'easy.h' '/usr/local/include/curl/easy.h' /bin/install -c -m 644 'mprintf.h' '/usr/local/include/curl/mprintf.h' /bin/install -c -m 644 'stdcheaders.h' '/usr/local/include/curl/stdcheaders.h' /bin/install -c -m 644 'types.h' '/usr/local/include/curl/types.h' /bin/install -c -m 644 'multi.h' '/usr/local/include/curl/multi.h' /bin/install -c -m 644 'typecheck-gcc.h' '/usr/local/include/curl/typecheck-gcc.h' /bin/install -c -m 644 'curlbuild.h' '/usr/local/include/curl/curlbuild.h' /bin/install -c -m 644 'curlrules.h' '/usr/local/include/curl/curlrules.h' ... 8. $ which curl curl /usr/local/bin/curl curl: try 'curl --help' for more information I have following files in C:\temp\msys\1.0\local\bin\ (/usr/local/bin in Unix-scheme): 02.02.2009 15:10 4 029 curl-config 02.02.2009 15:1098 591 curl.exe 02.02.2009 15:09 262 934 libcurl-4.dll In /usr/local/include/curl ten includes: 02.02.2009 15:1067 183 curl.h 02.02.2009 15:10 5 865 curlbuild.h 02.02.2009 15:10 7 478 curlrules.h 02.02.2009 15:10 2 799 curlver.h 02.02.2009 15:10 3 526 easy.h 02.02.2009 15:10 2 850 mprintf.h 02.02.2009 15:1013 039 multi.h 02.02.2009 15:10 1 383 stdcheaders.h 02.02.2009 15:1033 337 typecheck-gcc.h 02.02.2009 15:1015 types.h Sorry for many details, but now
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
On Mon, 2009-02-02 at 13:28 -0800, Conal Elliott wrote: On Mon, Feb 2, 2009 at 11:39 AM, Creighton Hogg wch...@gmail.com wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? Again, my goal would not be a purely functional library, because even IO is purely functional. My goal is a denotational library, i.e., one that has an elegant (denotational) semantics, and hence is powerfully compositional and good for reasoning. +1 jcc ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 3:25 PM, Ketil Malde ke...@malde.org wrote: Gregg Reynolds d...@mobileink.com writes: Just shorthand for something like data Tcon a = Dcon a, applied to Int. Any data constructor expression using an Int will yield a value of type Tcon Int. Right. But then the set of values is isomorphic to the set of Ints, right? Only if you're ignoring non-terminating values. Otherwise, you have to deal with the fact that Tcon Int contains _|_ and DCon _|_. -- Dave Menendez d...@zednenem.com http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the functions space in set theory. Most importantly Haskell functions
have to be monotonic (in the domain theoretic sense), so that limits
the number of possible functions.
http://en.wikipedia.org/wiki/Domain_theory
-- Lennart
On Mon, Feb 2, 2009 at 4:28 PM, Lennart Augustsson
lenn...@augustsson.net wrote:
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the functions space in set theory. Most importantly Haskell functions
have to be monotonic (in the domain theoretic sense), so that limits
the number of possible functions.
http://en.wikipedia.org/wiki/Domain_theory
-- Lennart
On Mon, Feb 2, 2009 at 3:49 PM, Martijn van Steenbergen
mart...@van.steenbergen.nl wrote:
Hi Gregg,
Firsly: I'm not an expert on this, so if anyone thinks I'm writing nonsense,
do correct me.
There are many answers to the question what is a type?, depending on one's
view.
One that has been helpful to me when learning Haskell is a type is a set of
values. When seen like this it makes sense to write:
() = { () }
Bool = { True, False }
Maybe Bool = { Nothing, Just True, Just False }
Recursive data types have an infinite number of values. Almost all types
belong to this group. Here's one of the simplest examples:
data Peano = Zero | Suc Peano
There's nothing wrong with a set with an infinite number of members.
Gregg Reynolds wrote:
This gives a very interesting way of looking at Haskell type
constructors: a value of (say) Tcon Int is anything that satisfies
isA Tcon Int. The tokens/values of Tcon Int may or may not
constitute a set, but even if they, we have no way of describing the
set's extension.
Int has 2^32 values, just like in Java. You can verify this in GHCi:
Prelude (minBound, maxBound) :: (Int, Int)
(-2147483648,2147483647)
Integer, on the other hand, represents arbitrarily big integers and
therefore has an infinite number of elements.
To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
Here you're probably thinking about the distinction between countable and
uncountable sets. See also:
http://en.wikipedia.org/wiki/Countable_set
Haskell has types which have uncountably many values. They are all functions
of the form A - B, where A is an infinite type (either countably or
uncountably).
If a set is countable, you can enumerate the set in such a way that you will
reach each member eventually. For Haskell this means that if a type a has
a countable number of values, you can define a list :: [a] that will contain
all of them.
I hope this helps! Let us know if you have any other questions.
Martijn.
___
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] Why binding to existing widget toolkits doesn't make any sense
On Mon, Feb 2, 2009 at 3:28 PM, Conal Elliott co...@conal.net wrote: On Mon, Feb 2, 2009 at 11:39 AM, Creighton Hogg wch...@gmail.com wrote: snip I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? Again, my goal would not be a purely functional library, because even IO is purely functional. My goal is a denotational library, i.e., one that has an elegant (denotational) semantics, and hence is powerfully compositional and good for reasoning. Well, that is essentially what I meant but your point about clarity is taken. A truly mathematical semantic model is above beyond what is meant by purely functional. The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C The Fruit paper, Genuinely Functional User Interfaces, gives a semantic model, which could be a starting place for thinking about possibilities. At the very least, I'd like to take it to 3D. The idea there is that a UI is a function from flows (behaviors/signals) to flows, where the input includes mouse keyboard stuff and the output includes an image. An image is, as in Pan, a function from R^2 - Color, where color includes partial opacity. When UIs are transformed in time and/or space, they correspondingly see inversely-transformed input, thanks to a general principle of transforming functions. Thanks. I'm reading it now. Cheers, C ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
ndmitchell: Hi So actually just having more Windows users subscribed to cabal-devel and commenting on tickets would be very useful, even if you do not have much time for hacking. I believe that as soon as a Windows user starts doing that you'll start asking them for patches :-) There are a number of reasons that we have fewer Windows developers: * Some of it comes down to social reasons - for some reason it seems to be socially acceptable to belittle Windows (and Windows users) on the Haskell mailing lists and #haskell. * Some of it comes down to technical issues - for example not having cabal.exe bundled with GHC 6.10.1 on Windows was a massive mistake (although I've heard everyone argue against me, I've not yet heard a Windows person argue against me). * Part of it comes down to most developers not being Windows people. * A little is because Windows is a second class citizen even in the libraries, my OS is NOT mingw32 - mingw32 is not even an OS, its a badly typed expression! How would you like it if your OS was listed as Wine? Things like this tell me that Haskell isn't Windows friendly, at best its windows tolerant. * Things like Gtk2hs, which Windows users need building for them, don't release in sync with GHC, which makes it hard to use. * Windows machines don't usually have a C compiler, and have a very different environment - while the rest of the world is starting to standardise. I gave up on fighting the fight when people decided not to bundle cabal.exe with Windows - and now I'm too busy with my day job... Now I'd say Duncan is the most vocal and practical Windows developer, even overlooking the fact he doesn't run Windows. GHC doesn't bundle with cabal-install on any system. What is needed is not for the GHC team to be doing Windows platform packages, but for the Windows Haskell devs to build their own system, as happens on all the Unices. Take GHC's release, wrap it up with native installers, throw in useful libraries and executables like cabal. Done. It's not the GHC compiler team's job to build distro-specific bundles. So, wind...@haskell.org anyone? Get the wiki going, get the set of tasks created. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Talking about the class of all Haskell types is a little tricky.
If one program has
data Foo x = Ick x | Ack x
and another program has
data Bar y = Ack y | Ick y
are {Program1}Foo and {Program2}Bar the same type or not?
They are certainly isomorphic.
Any Haskell program can be represented as a sequence of bytes.
(Proof: take your source tree, and use tar, pax, cpio, or whatever.)
There is therefore a countable infinity of Haskell programs.
In Haskell 98, a program can generate at most a countable infinity
of types (taking a 'type' here to be an element of the Herbrand
base generated by the type constructors, speaking somewhat loosely).
So surely there can be at most a countable infinity of Haskell types?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Verifying Haskell Programs
pocmatos: Hi all, Much is talked that Haskell, since it is purely functional is easier to be verified. However, most of the research I have seen in software verification (either through model checking or theorem proving) targets C/C++ or subsets of these. What's the state of the art of automatically verifying properties of programs written in Haskell? State of the art is translating subsets of Haskell to Isabelle, and verifying them. Using model checkers to verify subsets, or extracting Haskell from Agda or Coq. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
jwlato: Duncan Coutts wrote: Some are trivial and should be done away with. For example the ones that just check if a C header / lib is present are unnecessary (and typically do not work correctly). The next point release of Cabal can do these checks automatically, eg: Configuring foo-1.0... cabal: Missing dependencies on foreign libraries: * Missing header file: foo.h * Missing C libraries: foo, bar, baz This problem can usually be solved by installing the system packages that provide these libraries (you may need the -dev versions). If the libraries are already installed but in a non-standard location then you can use the flags --extra-include-dirs= and --extra-lib-dirs= to specify where they are. Thank you! Thank you! Thank you! For those of us who want to write cross-platform (i.e. Windows) bindings to C libraries, this is great news. It will be important now to report the lack of uses of these portability tests back to the authors of packages. A start would be to have hackage warn, I suppose. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Do they? Haskell is a programing language. Therefore legal Haskell types has to be represented by some string. And there are countably many strings (of which only a subset is legal type representation, but that's not important). All best Christopher Skrzętnicki On Mon, Feb 2, 2009 at 17:09, Gregg Reynolds d...@mobileink.com wrote: On Mon, Feb 2, 2009 at 10:05 AM, Andrew Butterfield andrew.butterfi...@cs.tcd.ie wrote: Martijn van Steenbergen wrote: To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. Here you're probably thinking about the distinction between countable and uncountable sets. See also: http://en.wikipedia.org/wiki/Countable_set No - it's even bigger than those ! He is thinking of proper classes, not sets. http://en.wikipedia.org/wiki/Class_(set_theory) Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it. Thanks, g ___ 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] ICFP09 Final CFP
Final Call for Papers ICFP 2009: International Conference on Functional Programming Edinburgh, Scotland, 31 August - 2 September 2009 http://www.cs.nott.ac.uk/~gmh/icfp09.html ** Submission deadline: 2 March 2009 ** Submission URL: https://www.softconf.com/a/icfp09/ ICFP 2009 seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects or concurrency. Particular topics of interest include * Language Design * Implementation * Software-Development Techniques * Foundations * Applications and Domain-Specific Languages * Functional Pearls The conference also solicits Experience Reports, which are short papers that provide evidence that functional programming really works or describe obstacles that have kept it from working in a particular application. Important Dates (at 20:00 UTC) ~~~ Submission: 2 March 2009 https://www.softconf.com/a/icfp09/ Author response: 21-23 April 2009 Notification: 5 May 2009 Final papers due: 8 June 2009 Call for Papers (full text) ~~~ http://web.cecs.pdx.edu/~apt/icfp09_cfp.html Call for Experience Reports (full text) ~~~ http://web.cecs.pdx.edu/~apt/icfp09_cfer.html Program Chair ~ Andrew Tolmach Department of Computer Science Portland State University P.O. Box 751, Portland, OR 97207 USA Email: a...@cs.pdx.edu Phone: +1 503 725 5492 Fax: +1 503 725 3211 Mail sent to the address above is filtered for spam. If you send mail and do not receive a prompt response, particularly if the deadline is looming, feel free to telephone. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
2009/2/2 Joachim Breitner m...@joachim-breitner.de
Hi,
Am Montag, den 02.02.2009, 11:06 -0700 schrieb Luke Palmer:
That question has kind of a crazy answer.
In mathematics, Nat - Bool is uncountable, i.e. there is no function
Nat - (Nat - Bool) which has every function in its range.
But we know we are dealing with computable functions, so we can just
enumerate all implementations. So the computable functions Nat -
Bool are countable.
However! If we have a function f : Nat - Nat - Bool, we can
construct the diagonalization g : Nat - Bool as: g n = not (f n n),
with g not in the range of f. That makes Nat - Bool computably
uncountable.
That argument has a flaw. Just because we have a function in the
mathematical sense that sends ℕ to (Nat - Bool) does not mean that we
have Haskell function f of that type that we can use to construct g.
What argument? What was I trying to prove?
But I admit that my notation is confusing; I am not distinguishing between
Haskell types and their denotations. I'll be more precise:
I will use N for the set of naturals, Nat for the Haskell type of (strict)
naturals, 2 for the set {0,1}, Bool for the Haskell type True|False, (-)
for a mathematical function, (~) for a *total* computable function in
Haskell.
N - 2 is uncountable, meaning there is no surjection N - (N - 2).
Nat ~ Bool is countable, meaning there is a surjection N - (Nat ~ Bool).
Enumerate all program source codes (which is countable, so N - SourceCode),
and pick out the ones which denote a total computable function Nat ~ Bool.
But Nat ~ Bool is *computably* uncountable, meaning there is no injective
function Nat ~ (Nat ~ Bool), by the diagonal argument above.
That's what I meant.
Luke
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
Hi So actually just having more Windows users subscribed to cabal-devel and commenting on tickets would be very useful, even if you do not have much time for hacking. I believe that as soon as a Windows user starts doing that you'll start asking them for patches :-) There are a number of reasons that we have fewer Windows developers: * Some of it comes down to social reasons - for some reason it seems to be socially acceptable to belittle Windows (and Windows users) on the Haskell mailing lists and #haskell. * Some of it comes down to technical issues - for example not having cabal.exe bundled with GHC 6.10.1 on Windows was a massive mistake (although I've heard everyone argue against me, I've not yet heard a Windows person argue against me). * Part of it comes down to most developers not being Windows people. * A little is because Windows is a second class citizen even in the libraries, my OS is NOT mingw32 - mingw32 is not even an OS, its a badly typed expression! How would you like it if your OS was listed as Wine? Things like this tell me that Haskell isn't Windows friendly, at best its windows tolerant. * Things like Gtk2hs, which Windows users need building for them, don't release in sync with GHC, which makes it hard to use. * Windows machines don't usually have a C compiler, and have a very different environment - while the rest of the world is starting to standardise. I gave up on fighting the fight when people decided not to bundle cabal.exe with Windows - and now I'm too busy with my day job... Now I'd say Duncan is the most vocal and practical Windows developer, even overlooking the fact he doesn't run Windows. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
Don Stewart wrote: GHC doesn't bundle with cabal-install on any system. What is needed is not for the GHC team to be doing Windows platform packages, but for the Windows Haskell devs to build their own system, as happens on all the Unices. Take GHC's release, wrap it up with native installers, throw in useful libraries and executables like cabal. Done. It's not the GHC compiler team's job to build distro-specific bundles. So, wind...@haskell.org anyone? Get the wiki going, get the set of tasks created. Isn't the Haskell Platform going to do all this? Shouldn't interested people just help out there? Ganesh == Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html == ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Hi, Am Montag, den 02.02.2009, 15:30 -0700 schrieb Luke Palmer: That's what I meant. thanks for the clarification, I indeed were confused by the notation and saw Haskell functions where you meant mathematical functions. Greetings, Joachim -- Joachim nomeata Breitner mail: m...@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nome...@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nome...@debian.org signature.asc Description: Dies ist ein digital signierter Nachrichtenteil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type and data constructors in CT
Gregg Reynolds wrote:
On Sat, Jan 31, 2009 at 4:26 PM, wren ng thornton w...@freegeek.org wrote:
But a data constructor Dcon a is an /element/ mapping taking elements
(values) of one type to elements of another type. So it too can be
construed as a functor, if each type itself is construed as a
category.
Actually no, it's not a functor. It's a (collection of) morphism(s). Let's
again assume a single-argument Dcon for simplicity. The Haskell type |Dcon
:: forall a. a - Tcon a| is represented by a collection of morphisms
|Dcon_{X} : X - Tcon X| for each X in Ob(Hask).
Ok, I see I elided that step. So my question is about the relation
between the individual (specialized) Dcon and the associated Tcon.
I.e. Dcon 3 is a value of type Tcon Int, inferred by the type system.
So it looks to me like the relation between the Tcon functor and the
Dcon functions is basically ad hoc.
Pretty much. Well, it's not ad hoc, it's algebraic. Data constructors,
by definition, don't perform any sort of introspection on the values
they're given. Looking at it sideways, they're 'polymorphic' in the
values of the type, and they preserve the structure of the value (namely
just storing it). This makes data constructors more well behaved than
arbitrary functions. The possible definitions of Haskell types are
formed by the algebra consisting of that id function, products of
algebras, coproducts of algebras, and equi-recursion (though removing
this and using iso-recursion is easier for CT treatment). This
well-behavedness is without even looking at polymorphic data constructors.
To take a different tactic, consider the free monoid. Like all free
things it is the monoid which consists of no more than what is necessary
to satisfy the monoid laws (that is, it doesn't cost or require anything
special; hence free). If you're familiar with Prolog, this is like the
idea of uninterpreted predicates. The value of foo(bar) is: foo(bar).
Since foo is uninterpreted, applying foo to bar means returning a value
that reifies the application of foo to bar. Uninterpreted predicates are
free application[1]. Data constructors in Haskell are just like this.
Applying (:) to x and xs results in the value (x:xs).
It is precisely because Dcons cannot inspect the values they are given
that makes it so easy for Tcons to be functors. Since the only thing
Dcons can do to values is id them up, this is definitionally structure
preserving. Note that it's possible to have functors which do inspect
the values but still preserve structure by transforming the values in
some consistent manner.
Because Dcons cannot do anything, this is why people often define
smart constructors for dealing with abstract types or for maintaining
invariants in types which have more structure than can be encoded in
ADTs (or GADTs). For example, the bytestring-trie package defines a Trie
type for patricia trees mapping ByteStrings to some value type. The
basic type for Trie a has Empty, Arc :: ByteString - Maybe a - Trie a,
and Branch :: Trie a - Trie a - Trie a. However, the actual abstract
type has a number of invariants which restrict the domain of the type to
be much smaller than what you would get with just that specification
(e.g. an Arc with no value can't recurse as an Arc, the arcs should be
collapsed into one).
Smart constructors are an important technique and they can capture many
interesting types which ADTs cannot, however when using smart
constructors you've stepped outside of the warm confines of what the
type system enforces for you. The Haskell type Trie a is not the same
thing as the abstract type it's used to represent. By stepping outside
of the type system, it's up to the programmer to prove that their
abstract type does adhere to the laws for functors, monoids, or
whatever. For ADTs, those proofs are already done for you (for functors
at least) due to their regular nature. And I do mean regular, ADTs are
coproducts, products, and recursion just like the choice, extension, and
Klene star of regular expressions.
[1] Easing off from the free monoid, the free associative operator is
free (binary) application extended by an equivalence relation for
associativity. Thus, values generated by the free assoc-op represent
equivalence classes over the application trees which could generate it.
The free monoid is the same thing but extended by equivalence relations
for the identity element (which is often written by writing nothing,
hence it's also an equivalence relation over all possible insertions of
the identity element).
It's important to remember that Tcon is the object half of an *endo*functor
|Tcon : Hask - Hask| and not just any functor. We can view the object half
of an endofunctor as a collection of morphisms on a category; not
necessarily real morphisms that exist within that category, but more like an
overlay on a graph. In some cases, this overlay forms a subcategory (that
is, they
Re: [Haskell-cafe] why typeRepArgs (typeOf hello) is [Char] ?
Thanks a lot ! 2009/2/2 Ross Mellgren rmm-hask...@z.odi.ac: Sure: (+) :: Integer - Integer - Integer (really Num a = a - a - a, but we'll use the defaulted one) Which is really (+) :: - Integer (- Integer Integer)(that is, the function type constructor is * - * - * and right associative) So when you say typeRepArgs (typeOf (+)) you get Integer and (- Integer Integer), which pretty-prints as (Integer - Integer) It is possible, but you have to check if the type constructor is really a function type, e.g.: import Data.Typeable funTyCon :: TyCon funTyCon = mkTyCon - argsOf :: TypeRep - [TypeRep] argsOf ty | typeRepTyCon ty == funTyCon = let (x:y:[]) = typeRepArgs ty in x : argsOf y | otherwise = [] *Main Data.Typeable let f = (undefined :: Int - Char - String - ()) *Main Data.Typeable argsOf (typeOf f) [Int,Char,[Char]] -Ross On Feb 2, 2009, at 3:27 PM, minh thu wrote: Thanks. Could you add to your explanation this one : *Graph typeRepArgs (typeOf (+)) [Integer,Integer - Integer] In fact, I tried to write a function that would give the types used by a function, for instance [Integer, Integer, Integer] for (+) (the last one would be the 'return' type). So I applied recursively typeRepArgs to the second element of the list (if any) (here, Integer - Integer). It worked well until I tried it on a function like :: Char - Int - [Char] where the last recursive call gives [Char] instead of []. Is it possible to write such a function ? Thank you, Thu 2009/2/2 Ross Mellgren rmm-hask...@z.odi.ac: The type of hello is String, which is [Char], which is really [] Char (that is, the list type of kind * - *, applied to Char). 1, 'a', and True are all simple types (I'm sure there's a more particular term, maybe monomorphic?) with no type arguments. [] has a type argument, Char. Consider: Prelude Data.Typeable typeRepArgs (typeOf (Just 1)) [Integer] and Prelude Data.Typeable typeRepArgs (typeOf (Left 'a' :: Either Char Int)) [Char,Int] -- typeRepArgs is giving you the arguments of the root type application, [] (list) in your case, Maybe and Either for the two examples I gave. Does this make sense? -Ross On Feb 2, 2009, at 3:09 PM, minh thu wrote: Hello, With Data.Typeable : *Graph typeRepArgs (typeOf 1) [] *Graph typeRepArgs (typeOf 'a') [] *Graph typeRepArgs (typeOf True) [] *Graph typeRepArgs (typeOf hello) [Char] I don't understand why the latter is not []. Could someone explain it ? Thank you, Thu ___ 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] type metaphysics
2009/2/2 Luke Palmer lrpal...@gmail.com: However! If we have a function f : Nat - Nat - Bool, we can construct the diagonalization g : Nat - Bool as: g n = not (f n n), with g not in the range of f. That makes Nat - Bool computably uncountable. This is making my head explode. How is g not in the range of f? In particular, f is a program, which I can easily implement; given: compiler :: String - Maybe (Nat - Bool) mkAllStrings :: () - [String] -- enumerates all possible strings I can write f as f n = validPrograms () !! n where validPrograms = map fromJust . filter isJust . map compiler . mkAllStrings Now, in particular, mkAllStrings will generate the following string at some index, call it stringIndexOfG: source code for compiler source code for mkAllStrings source code for f g n = not (f n n) This is a valid program, so the compiler will compile it successfully, and therefore there is some index validProgramIndexOfG less than or equal to stringIndexOfG which generates this program. But your argument seems to hold as well, so where is the contradiction? -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
Well, that is also the idea behind Microsoft's WPF/XAML: they provide a declarative approach to describe the widget tree (specifying what it is, not what is does), and a GUI toolkit (Expression Blend) for artists and designers so they can use a high level tool to build the GUI. You can even define limited behavior and animation in a declarative way. However, I believe those designer friendly tools are not designed by designers but by programmers who claim to think what designers want. I work everyday with artists and designers, and these people are frustrated by the limitations and erratic behavior (read side effects) of most designer friendly tools... Furthermore making even a simple GUI requires a lot of collaboration between the developer and the designer, and this screams for a language that both can understand and reason about :-) Also, this approach is nice for simple or (should I say mostly form-based GUIs), but as soon as you get into something more complicated, this design won't help you. For example, try to make a mathematical editor like that... or a diagram editor... IMO any GUI framework should work for complicated GUIs as well as easy form based one. I feel the model - presentation - view - reactivity - model' cycle is still the best approach today for building complex GUIs. Never start with widgets, these are just a possible representation of a model. Although this paradigm comes from Smalltalk, MVC is really functional in my opinion.. If you make that approach compositional *and* fast, you have a winner. Something like FRUIT on steroids (Grapefruit? ;-) but then of course you are stuck with the arrows syntax which feels like drawing graphical circuits with a text editor ;-) 2009/2/2 John A. De Goes j...@n-brain.net The size, color, and layout of widgets has no effect on interaction semantics and is best pushed elsewhere, into a designer-friendly realm such as CSS. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 2:15 PM, Conal Elliott wrote: Could CSS give us semantic clarity? - Conal On Mon, Feb 2, 2009 at 11:58 AM, John A. De Goes j...@n-brain.net wrote: The actual presentation and layout of widgets would be better handled by a DSL such as CSS (which is, in fact, declarative in nature), while event logic would be best handled purely in Haskell. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 12:39 PM, Creighton Hogg wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
2009/2/2 Luke Palmer lrpal...@gmail.com: But Nat ~ Bool is computably uncountable, meaning there is no injective (surjective?) function Nat ~ (Nat ~ Bool), by the diagonal argument above. Given that the Haskell functions Nat - Bool are computably uncountable, you'd expect that for any Haskell function (Nat - Bool) - Nat there'd always be two elements that get mapped to the same value. So here's a programming challenge: write a total function (expecting total arguments) toSame :: ((Nat - Bool) - Nat) - (Nat - Bool,Nat - Bool) that finds a pair that get mapped to the same Nat. Ie. f a==f b where (a,b) = toSame f -- Dan (PS I think this is hard. But my brain might be misfiring so it might be trivial.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
On Mon, Feb 02, 2009 at 10:07:57AM +, Neil Mitchell wrote: Hi The nix package manager (although beeing primarly a linux tool) can run on cygwin as well (at least it did some time ago).. I'd suggest trying that to package windows libraries. It dose generate tag files for you automatically as well. At least it can build dependencies such as C libraries and so on for you automatically as well. Unfortunately I don't have time to work on the windows port. The cool thing about nix is: You can always switch back to the previous generation if something breaks. It organizes the packages like a memory management system. You only reference the target and the deps in between will be build / removed automatically for you if they are no longer used when running the nix garbage collector. There is another drawback: It definitely only works on a ntfs partition. On the other hand it does also support binary distributions and install software by clicking on links. In the end this is perfect for developping (IMHO) even if you have to learn a lot at the beginning. My major problem hindering my starting to work on this is that cygwin doesn't run on Vista running in kvm/ qemu. sh.exe exits and that's it. So if you have a solution for that I'd consider resuming work on it Sincerly Marc Weber ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] pure crisis :)
On Sun, 01 Feb 2009 20:19:18 +0100, Bulat Ziganshin bulat.zigans...@gmail.com wrote: Hello haskell-cafe, pure functional denotation for crisis: (_|_) Well, some experts say, the crisis has reached it's bottom. -- Regards, Henk-Jan van Tuyl -- http://functor.bamikanarie.com http://Van.Tuyl.eu/ -- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Hi, Am Montag, den 02.02.2009, 14:41 -0800 schrieb Dan Piponi: 2009/2/2 Luke Palmer lrpal...@gmail.com: But Nat ~ Bool is computably uncountable, meaning there is no injective (surjective?) function Nat ~ (Nat ~ Bool), by the diagonal argument above. Given that the Haskell functions Nat - Bool are computably uncountable, you'd expect that for any Haskell function (Nat - Bool) - Nat there'd always be two elements that get mapped to the same value. So here's a programming challenge: write a total function (expecting total arguments) toSame :: ((Nat - Bool) - Nat) - (Nat - Bool,Nat - Bool) that finds a pair that get mapped to the same Nat. Ie. f a==f b where (a,b) = toSame f -- Dan (PS I think this is hard. But my brain might be misfiring so it might be trivial.) toSame _ = (const True, const True) ;-) Joachim -- Joachim nomeata Breitner mail: m...@joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nome...@joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nome...@debian.org signature.asc Description: Dies ist ein digital signierter Nachrichtenteil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Bytestrings vs String?
A lot of people are suggesting using Bytestrings for performance, strictness whatsoever reasons. However how well do they talk to other libraries? One I've in mind is hslogger right now. Should hslogger be implemented using Strings or Bytestrings ? Should there be two versions? hslogger-bytestring and hslogger-string? Or would it be better to implement one String class which can cope with everthing (performance will drop, won't it?) I feel it would make sense to talk about how to provide this? In the future I'd like to explore using haskell for web developement. So speed does matter. And I don't want my server to convert from Bytestrings to Strings and back multiple times.. So is the best we could do compile the same library twice using different flags ? One providing a Bytestring API, the other using Strings? Cluttering up code by from to Bytestring conversions doesn't look compelling to me. Thoughts? Marc Weber ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
ganesh.sittampalam: Don Stewart wrote: GHC doesn't bundle with cabal-install on any system. What is needed is not for the GHC team to be doing Windows platform packages, but for the Windows Haskell devs to build their own system, as happens on all the Unices. Take GHC's release, wrap it up with native installers, throw in useful libraries and executables like cabal. Done. It's not the GHC compiler team's job to build distro-specific bundles. So, wind...@haskell.org anyone? Get the wiki going, get the set of tasks created. Isn't the Haskell Platform going to do all this? Shouldn't interested people just help out there? The platform is a set of blessed libraries and tools. The distros will still need to package that. To do that for Windows, we're still going to need a windows packaging team, along side Debian, Arch, Gentoo, Mac etc. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] cabal list can't find Glob.cabal file?
On Mon, Feb 2, 2009 at 12:01 AM, Duncan Coutts duncan.cou...@worc.ox.ac.uk wrote: The solution is to upgrade: $ cabal install cabal-install $ cabal --version cabal-install version 0.6.0 using version 1.6.0.1 of the Cabal library Yes, this was the problem, despite me upgrading cabal-install before mailing the list. Alas, an old cabal binary was being picked up from /usr/local/bin. Cheers for the help, D ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] hslogger bugs or features - patches
== issue 1 That's not the most awkward thing: When logging to A.B.C hslogger does add 3 loggers to the global logger Map: A A.B A.B.C all three inheriting the default priority level of the default rootLogger A test application illustrating this (feature ?) module Main where -- packages: hslogger import System.Log.Logger as HL import System.Log.Handler.Simple as HL main = do -- the default logger logs to stderr level WARNING -- that's why the following message should be shown -- a) logM A.B.C HL.ALERT ALERT test, should be shown and should create the sublogger -- b) updateGlobalLogger rootLoggerName (setLevel EMERGENCY) logM A.B.C HL.ALERT ALERT test, should not be shown cause we have changed to EMERGENCY which prints: tmp %./test1 /tmp nixos ALERT test, should be shown and should create the sublogger ALERT test, should not be shown cause we have changed to EMERGENCY I've written some patches increasing speed by 30%. See the benchmark. You can get them by cloning git://mawercer.de/hslogger; (branch hslogger_updates) I've replaced the internal representation (Map name Logger) by a tree. Only logging to a logger does no longer add a new node (which cloned the priority level in the past causing issue 1) The basic interface updateLogger name (set priority or add handlers) and logM is still the same. The logM is based on MonadIO now. So you no longer have to call liftIO yourself.. Also I've removed the standard setup logging to stderr. There is a setupLogging function instead.. Why? I can think of some use cases where logging to stderr doesn't make sense and it took me too much time figuring out how to remve the old stderr logger (I didn't find a nice solution without changing the exposed API) I don't want to start using my personal copy of hslogger. That's why I'd like to ask you wether you consider these changes beeing improvements although they break existing code (You'll have do add that initialization line) I also wonder wether it's worth using Bytestrings instead of Strings? I've not spend to much time on updating all the documentation yet.. If you'd like to ensure that a use case sill works add another test case please. You can also push to that git repository. Sincerly Marc Weber ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Why binding to existing widget toolkits doesn't make any sense
Stephen Tetley stephen.tet...@gmail.com wrote: Also, Shiva-VG - http://sourceforge.net/projects/shivavg - the implementation of OpenVG that the Haskell binding works with supports OpenVG 1.0.1, so it doesn't handle text at all. You know, if the Haskell bindings are compositable enough, it shouldn't be a problem to simply load bezier shapes from freetype into other libraries. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Bytestrings vs String?
Marc Weber wrote: A lot of people are suggesting using Bytestrings for performance, strictness whatsoever reasons. However how well do they talk to other libraries? One I've in mind is hslogger right now. Should hslogger be implemented using Strings or Bytestrings ? Should there be two versions? hslogger-bytestring and hslogger-string? Or would it be better to implement one String class which can cope with everthing (performance will drop, won't it?) Not necessarily. hslogger could easily accept both, and deal with it appropriately under the hood. If whatever it prefers under the hood is supplied to it, I don't see any reason that performance would suffer. I very much suspect though that you would not likely see a measurable performance difference either way with hslogger in real-world situations. -- John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: hslogger bugs or features?
I haven't had the time to study your question in detail yet, but I would
start by directing you here:
http://www.python.org/doc/current/library/logging.html#module-logging
hslogger is heavily based upon an earlier version of the Python logging
module. I had some experience with it and found it to work well, and
thus based the hslogger design upon it.
-- John
Marc Weber wrote:
Following the advice on the hslogger wiki
(http://software.complete.org/software/wiki/hslogger)
I'm posting my thoughts about hslogger here:
What is wired?
This piece of code (src/System/Log/Logger.hs):
parentHandlers name =
let pname = (head . drop 1 . reverse . componentsOfName) name
in do
[...]
next - parentHandlers pname
return ((handlers parent) ++ next)
Why?
Because when logging to A.B.C it splits the String once to get
[A,B,C], then it drops the last part and runs the same again for
A.B and so on..
So A string is split 3 times for one logging action. I think this is a
waste of cpu cycles.. I'm going to improve this. While reading the code
i noticed two issues:
==
issue 1
That's not the most awkward thing:
When logging to A.B.C hslogger does add 3 loggers to the global
logger Map:
A
A.B
A.B.C
all three inheriting the default priority level of the default
rootLogger
A test application illustrating this (feature ?)
module Main where
-- packages: hslogger
import System.Log.Logger as HL
import System.Log.Handler.Simple as HL
main = do
-- the default logger logs to stderr level WARNING
-- that's why the following message should be shown
-- a)
logM A.B.C HL.ALERT ALERT test, should be shown and should create the
sublogger
-- b)
updateGlobalLogger rootLoggerName (setLevel EMERGENCY)
logM A.B.C HL.ALERT ALERT test, should not be shown cause we have
changed to EMERGENCY
which prints:
tmp %./test1
/tmp nixos
ALERT test, should be shown and should create the sublogger
ALERT test, should not be shown cause we have changed to EMERGENCY
which is quite confusing because I haven't told hslogger explicitely
to use a log level printing ALERTs on A.B.C. so I'd expect that only
the first message is shown. This behaviour is explained by the
inheritance of the loglevel when hslogger creates them (without
attaching handlers) automatically.
I don't want the logging behaviour depend on wether a log line has been
emitted before or not.
Do you agree? Have I missed something?
solution:
replacing
data Logger = Logger { level :: Priority,
handlers :: [HandlerT],
name :: String}
type LogTree = Map.Map String Logger
by a real log tree:
data LogTree = LogTree {
level :: Priority, -- level only applies to handlers, not to
subLoggers
handlers :: [HandlerT],
subLoggers :: Map.Map String LogTree
}
==
issue 2
The second ineresting point is (bug or feature?) that you can make the
root logger shut up by setting different log levels to sub loggers:
this sample does illustrate it:
module Main where
-- packages: hslogger
import System.Log.Logger as HL
import System.Log.Handler.Simple as HL
main = do
updateGlobalLogger (setLevel DEBUG)
updateGlobalLogger A (setLevel EMERGENCY)
logM A HL.ALERT ALERT test, should not be shown cause we have
changed to EMERGENCY
It doesn't print anything although the default log handler on root (=)
is set to loglever DEBUG. So there is no way to get all logmessages
without removing all all setLevel calls to subloggers?
Is this desirable?
==
my conclusion:
About issue 1 I think its a bug
About issue 2 I don't know. I think there should be a way to get all log
messages. So I feel this is a bug as well.
I neither have checkeg the logcxx nor log4j nor the reference
implementation in python.
Thoughts?
Sincerly
Marc Weber
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell tutorial for pseudo users?
It's not a tutorial but it covers all the relvant portions you asked about. Download the package, unzip it and you'll find my Haskell Cheat Sheet PDF inside: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/CheatSheet On Mon, Feb 2, 2009 at 6:35 AM, Emil Axelsson e...@chalmers.se wrote: Hello, Are there any Haskell tutorials suitable for people who don't (and possibly don't want to) know Haskell, but just want to use an embedded language that happens to be in Haskell? Such a tutorial would focus on using libraries rather than defining them. For example, it might explain how to interpret a type signature involving type classes, but not how to write one's own type class. Thanks, / Emil ___ 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] circular dependencies in cabal
On Sun, 2009-02-01 at 19:10 -0800, Valentyn Kamyshenko wrote: So, in practical terms, you suggest that no new version of the package that ghc package depends on (directly or indirectly) should ever be installed? For example, as soon as process-1.0.1.1 is installed on my computer, I'll have this problem with every package that depends on process? Installing process-1.0.1.1 is not itself a problem. It is a new version it does not clash with other versions. The problem is re-installing the same version as you already have installed. In particular re-installing the same version of a package as one that comes with ghc. It's generally not necessary to install new versions of the core packages however, so unless you really know that you need to it's probably simpler to avoid doing so. Another question: would not cabal-install automatically fetch the most recent version of the process package, as soon as I will try to install a package that depends on it (such as, for example, plugins)? No. That's the difference between cabal install and cabal upgrade. The install command installs the latest version of a package but tries to use as many of your existing installed packages as possible. The upgrade command installs the latest version of a package but also tries to install the latest version of all the packages it depends on. That is probably how people are getting into this mess. Using upgrade is not necessarily such a good idea. It does not distinguish between the interesting packages you might want to upgrade and the core packages that your probably do not want to touch. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] UDP
Andrew Coppin ha scritto: [...] Yeah, I just assumed that the bind step was only necessary for connection-oriented protocols. (Interestingly enough, the matching send program doesn't bind at all, yet seems to work fine...) For a client (that is, when you call connect), the kernel chooses the source IP address once the socket is connected. Of course, for a server this is not feasible, since the address *must* be know to external programs, if they want to connect to the server. For more details, I really suggest to read a good book like UNIX Network Programming, by W. Richard Stevens. Regards Manlio Perillo ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
The Haskell function space, A-B, is not uncountable.
There is only a countable number of Haskell functions you can write,
so how could there be more elements in the Haskell function space? :)
The explanation is that the Haskell function space is not the same as
the functions space in set theory. Most importantly Haskell functions
have to be monotonic (in the domain theoretic sense), so that limits
the number of possible functions.
http://en.wikipedia.org/wiki/Domain_theory
-- Lennart
On Mon, Feb 2, 2009 at 3:49 PM, Martijn van Steenbergen
mart...@van.steenbergen.nl wrote:
Hi Gregg,
Firsly: I'm not an expert on this, so if anyone thinks I'm writing nonsense,
do correct me.
There are many answers to the question what is a type?, depending on one's
view.
One that has been helpful to me when learning Haskell is a type is a set of
values. When seen like this it makes sense to write:
() = { () }
Bool = { True, False }
Maybe Bool = { Nothing, Just True, Just False }
Recursive data types have an infinite number of values. Almost all types
belong to this group. Here's one of the simplest examples:
data Peano = Zero | Suc Peano
There's nothing wrong with a set with an infinite number of members.
Gregg Reynolds wrote:
This gives a very interesting way of looking at Haskell type
constructors: a value of (say) Tcon Int is anything that satisfies
isA Tcon Int. The tokens/values of Tcon Int may or may not
constitute a set, but even if they, we have no way of describing the
set's extension.
Int has 2^32 values, just like in Java. You can verify this in GHCi:
Prelude (minBound, maxBound) :: (Int, Int)
(-2147483648,2147483647)
Integer, on the other hand, represents arbitrarily big integers and
therefore has an infinite number of elements.
To my naive mind this sounds
suspiciously like the set of all sets, so it's too big to be a set.
Here you're probably thinking about the distinction between countable and
uncountable sets. See also:
http://en.wikipedia.org/wiki/Countable_set
Haskell has types which have uncountably many values. They are all functions
of the form A - B, where A is an infinite type (either countably or
uncountably).
If a set is countable, you can enumerate the set in such a way that you will
reach each member eventually. For Haskell this means that if a type a has
a countable number of values, you can define a list :: [a] that will contain
all of them.
I hope this helps! Let us know if you have any other questions.
Martijn.
___
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] Re: Why binding to existing widget toolkits doesn't make any sense
That's my thought. On Mon, Feb 2, 2009 at 7:23 AM, Achim Schneider bars...@web.de wrote: Stephen Tetley stephen.tet...@gmail.com wrote: Also, Shiva-VG - http://sourceforge.net/projects/shivavg - the implementation of OpenVG that the Haskell binding works with supports OpenVG 1.0.1, so it doesn't handle text at all. You know, if the Haskell bindings are compositable enough, it shouldn't be a problem to simply load bezier shapes from freetype into other libraries. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited. ___ 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] Re: 1,000 packages, so let's build a few!
Duncan Coutts wrote: Some are trivial and should be done away with. For example the ones that just check if a C header / lib is present are unnecessary (and typically do not work correctly). The next point release of Cabal can do these checks automatically, eg: Configuring foo-1.0... cabal: Missing dependencies on foreign libraries: * Missing header file: foo.h * Missing C libraries: foo, bar, baz This problem can usually be solved by installing the system packages that provide these libraries (you may need the -dev versions). If the libraries are already installed but in a non-standard location then you can use the flags --extra-include-dirs= and --extra-lib-dirs= to specify where they are. Thank you! Thank you! Thank you! For those of us who want to write cross-platform (i.e. Windows) bindings to C libraries, this is great news. John Lato ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 9:47 AM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: Lennart Augustsson wrote: The Haskell function space, A-B, is not uncountable. There is only a countable number of Haskell functions you can write, so how could there be more elements in the Haskell function space? :) The explanation is that the Haskell function space is not the same as the functions space in set theory. Most importantly Haskell functions have to be monotonic (in the domain theoretic sense), so that limits the number of possible functions. I was thinking about a fixed function type A - B having uncountably many *values* (i.e. implementations). Not about the number of function types of the form A - B. Is that what you meant? For example, fix the type to Integer - Bool. I can't enumeratate all possible implementations of this function. Right? That question has kind of a crazy answer. In mathematics, Nat - Bool is uncountable, i.e. there is no function Nat - (Nat - Bool) which has every function in its range. But we know we are dealing with computable functions, so we can just enumerate all implementations. So the computable functions Nat - Bool are countable. However! If we have a function f : Nat - Nat - Bool, we can construct the diagonalization g : Nat - Bool as: g n = not (f n n), with g not in the range of f. That makes Nat - Bool computably uncountable. In summary, the set of total computable functions Nat - Bool is a countable set, but this fact is not observable by any algorithm. (so is it *really*countable after all? :-) Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 3:41 PM, Dan Piponi dpip...@gmail.com wrote: 2009/2/2 Luke Palmer lrpal...@gmail.com: But Nat ~ Bool is computably uncountable, meaning there is no injective (surjective?) function Nat ~ (Nat ~ Bool), by the diagonal argument above. Given that the Haskell functions Nat - Bool are computably uncountable, you'd expect that for any Haskell function (Nat - Bool) - Nat there'd always be two elements that get mapped to the same value. So here's a programming challenge: write a total function (expecting total arguments) toSame :: ((Nat - Bool) - Nat) - (Nat - Bool,Nat - Bool) that finds a pair that get mapped to the same Nat. Ie. f a==f b where (a,b) = toSame f Presumably under the condition that a /= b. It's unlikely that you can. At least you can't use Escardo's trick, because while the space of pairs of cantor spaces (cantor space = Nat - Bool) is compact, the space of pairs of *different* cantors spaces is not. This is witnessed by the following function: f (a,b) = length (takeWhile id (zipWith (==) a b)) This function finds the first index at which they differ. Since they are guaranteed to be different, this function is total. Thus, if the space of nonequal cantor spaces were compact, then so too would be Nat, which we know is not the case. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 02, 2009 at 02:41:36PM -0800, Dan Piponi wrote: 2009/2/2 Luke Palmer lrpal...@gmail.com: But Nat ~ Bool is computably uncountable, meaning there is no injective (surjective?) function Nat ~ (Nat ~ Bool), by the diagonal argument above. Given that the Haskell functions Nat - Bool are computably uncountable, you'd expect that for any Haskell function (Nat - Bool) - Nat there'd always be two elements that get mapped to the same value. So here's a programming challenge: write a total function (expecting total arguments) toSame :: ((Nat - Bool) - Nat) - (Nat - Bool,Nat - Bool) that finds a pair that get mapped to the same Nat. Ie. f a==f b where (a,b) = toSame f (Warning: sketchy argument ahead.) Let f :: (Nat - Bool) - Nat be a total function and let g0 = const True. The application f g0 can only evaluate g0 at finitely many values, so f g0 = f ( k) for any k larger than all these values. So we can write toSame f = (const True, head [ ( k) | k - [1..], f (const True) == f ( k) ]) and toSame is total on total inputs. Regards, Reid ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Parallel term reduction
On Sun, Feb 1, 2009 at 9:26 PM, John D. Ramsdell ramsde...@gmail.com wrote: I have a reduction system in which a rule takes a term and returns a set of terms. The reduction system creates a tree that originates at a starting value called the root. For most problems, the reduction system terminates, but a step count limit protects from non-termination. That's typically a bad idea. Instead, use laziness to protect from nontermination. For example, in this case, we can output a collection of items lazily, and then take a finite amount of the output (or check whether the output is longer than some length), without having to evaluate all of it. Very good suggestion. In my code, I should take limit on the generated list, and fail if the length of the list is limit. Sounds easy. I'll study your parallel solution tonight after work. Thank you. Here is an interesting fact about my term reduction system. The binary relation that defines reduction is slightly different from the usual. It's a relation between terms and sets of terms. Furthermore, some normal forms can be identified as answers, and some normal forms are dead ends. When applying a rule, it doesn't matter which set in the relation is used as the result. The answer normal forms will all be the same. If the rule produces the empty set for some choice, all other choices will lead only to normal forms that are dead ends. John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
Luke Palmer wrote: and pick out the ones which denote a total computable function [...] How important is totality to this argument? If it is important, how do you decide it? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 10:05 AM, Andrew Butterfield andrew.butterfi...@cs.tcd.ie wrote: Martijn van Steenbergen wrote: To my naive mind this sounds suspiciously like the set of all sets, so it's too big to be a set. Here you're probably thinking about the distinction between countable and uncountable sets. See also: http://en.wikipedia.org/wiki/Countable_set No - it's even bigger than those ! He is thinking of proper classes, not sets. http://en.wikipedia.org/wiki/Class_(set_theory) Yes, that's my hypothesis: type constructors take us outside of set theory (ZF set theory, at least). I just can't prove it. Thanks, g ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: HDBC v2.0 now available
Duncan Coutts wrote: So in the next cabal-install release (which should be pretty soon now) configure will do the same thing and pick base 3 unless you specify build-depends base = 4. Niklas Broberg wrote: I really really think this is the wrong way to go. Occasional destruction is desperately needed for progress, else things will invariably stagnate. I disagree. Having everything fail... would have been a disaster... during the lifespan of base 4 we need to encourage new releases to start working with it... Doing that with warnings hints etc is the way to go. No, that's not good enough either. Existing packages will just stay with old versions to avoid the work, and new packages will then also use old versions for maximum compatibility. The incentive is not strong enough. Those warnings and hints must have teeth. Comparing with what has happened in other languages, which have stagnated or not stagnated at various rates, it is clear that what we need is a well-defined deprecation process. The warnings should say something like: you had better upgrade this, otherwise it will stop working in the next version. Both maintainers and users should be aware of this threat. That way, code that is maintained will not stop working. There will be plenty of time to make the change. Code that is used but not maintained will generate a hue and cry among the users that will hopefully motivate someone to do something about it. Code that is not maintained and little used will eventually be destroyed, but that code is probably bitrotting in any case. The deprecation process can be as slow and fine-grained as we like. But there must be a well-defined point in the future when old unmaintained code will be allowed to stop working. Destruction is not such a friendly approach. We do not need to make the users suffer When done carefully, gradually, and with plenty of warning (at least one full version cycle), destruction is indeed friendly and helpful. It allows users to understand precisely what versions should be used, and when, in old, current, and future projects, while permitting Haskell to march steadily onward. -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 4:23 PM, Matthew Brecknell hask...@brecknell.orgwrote: Luke Palmer wrote: and pick out the ones which denote a total computable function [...] How important is totality to this argument? If it is important, how do you decide it? It is at the very essence of the argument; it is why there are countable sets which are computably uncountable: (nonconstructive) mathematics does not need to decide, only programs need to do that :-) Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why binding to existing widget toolkits doesn't make any sense
Hi John, I'm not sure how to interpret your remarks about has no effect and is best. I guess they're subjective opinions, but maybe I'm missing something objective in your intent. I can see, for instance, at least one way in which layout has a direct and enormous effect on interaction semantics. And while I can see some benefits in choosing CSS, I also see some significant drawbacks, and I wonder if you've factored these drawbacks into your is best. - Conal 2009/2/2 John A. De Goes j...@n-brain.net The size, color, and layout of widgets has no effect on interaction semantics and is best pushed elsewhere, into a designer-friendly realm such as CSS. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 2:15 PM, Conal Elliott wrote: Could CSS give us semantic clarity? - Conal On Mon, Feb 2, 2009 at 11:58 AM, John A. De Goes j...@n-brain.net wrote: The actual presentation and layout of widgets would be better handled by a DSL such as CSS (which is, in fact, declarative in nature), while event logic would be best handled purely in Haskell. Regards, John A. De Goes N-BRAIN, Inc. The Evolution of Collaboration http://www.n-brain.net|877-376-2724 x 101 On Feb 2, 2009, at 12:39 PM, Creighton Hogg wrote: 2009/1/29 Conal Elliott co...@conal.net: Hi Achim, I came to the same conclusion: I want to sweep aside these OO, imperative toolkits, and replace them with something genuinely functional, which for me means having a precise simple compositional (denotational) semantics. Something meaningful, formally tractable, and powefully compositional from the ground up. As long as we build on complex legacy libraries (Gtk, wxWidgets, Qt, OpenGL/GLUT, ...), we'll be struggling against (or worse yet, drawn into) their ad hoc mental models and system designs. As Meister Eckhart said, Only the hand that erases can write the true thing. I think working on a purely functional widget toolkit would actually be a really cool project. Do you have any ideas, though, on what should be the underlying primitives? The initial gut feeling I have is that one should just ignore any notion of actually displaying widgets instead focus on a clean algebra of how to 'add' widgets that relates the concepts of inheritance relative position. What I mean by inheritance, here, is how to direct a flow of 'events'. I don't necessarily mean events in the Reactive sense, because I think it'd be important to make the model completely independent of how time actual UI actions are handled. Any thoughts to throw in, here? Cheers, C ___ 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: 1,000 packages, so let's build a few!
Neil Mitchell wrote: * Part of it comes down to most developers not being Windows people. That certainly describes me. I find the platform annoying and stressful (all the worries about security). But another issue is: it's proprietary and expensive. The base OS isn't cheap, and doesn't even come with development tools. While GHC and friends do run on Windows for free, if you are trying to deal certain things (Windows GUIs, ODBC, etc.) it is difficult at best without shelling out the really big bucks for the Microsoft development environment. Having said that, I agree that good Windows support is a worthwhile goal for the community, and I very much appreciate patches and bug reports from Windows users. However, I am in somewhat of a difficult position when it comes to turning the latter into actual patches. Of course, MacOS X is also proprietary and expensive. But it has at least a bastardized POSIX core, and as such seems to never really need much porting from my Linux development environment. At least until Mac users start demanding resource fork and finder info support. ;-) -- John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell tutorial for pseudo users?
Ah, that's nice! I never actually looked at your Cheat Sheet before (thought it would be much shorter and not very useful :) ). I will definitely forward this to the people in our project. Still on the lookout for a DSEL tutorial though... / Emil Justin Bailey skrev: It's not a tutorial but it covers all the relvant portions you asked about. Download the package, unzip it and you'll find my Haskell Cheat Sheet PDF inside: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/CheatSheet On Mon, Feb 2, 2009 at 6:35 AM, Emil Axelsson e...@chalmers.se wrote: Hello, Are there any Haskell tutorials suitable for people who don't (and possibly don't want to) know Haskell, but just want to use an embedded language that happens to be in Haskell? Such a tutorial would focus on using libraries rather than defining them. For example, it might explain how to interpret a type signature involving type classes, but not how to write one's own type class. Thanks, / Emil ___ 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] Haskeline, pcre-light, iconv and Cabal on OSX
Thomas Davie wrote: This is caused by OS X's libiconv being entirely CPP macros, the FFI has nothing to get hold of. IIRC there's a ghc bug report open for it. Judah Jacobson wrote: The OS X system libiconv is actually OK; it's the MacPorts libiconv that has the CPP macros... Thanks for the report; I'm not sure of what the right solution is, but I opened a ticket on Haskeline's bug tracker Perhaps there should also be a ticket on MacPort's bug tracker? -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Why binding to existing widget toolkits doesn't make any sense
Hi Jeff Thanks. OpenVG is an interesting bit of kit, however... VGU - the higher level layer - would be hard pressed to be less like Haskell, you draw shapes and lines while passing a path handle around. Also, Shiva-VG - http://sourceforge.net/projects/shivavg - the implementation of OpenVG that the Haskell binding works with supports OpenVG 1.0.1, so it doesn't handle text at all. Text functions were added to the OpenVG at version 1.1. In the short term, this limits the usefulness of OpenVG, but if the implementations develop it does look like a good prospect. Stephen 2009/2/2 Jeff Heard jefferson.r.he...@gmail.com: I will happily check it on Linux. I'm only vaguely familiar with OpenVG... In theory it's a good API, and would support exactly what I'd need for a backend to Hieroglyph that isn't Cairo based, but we'd still need a good image API and probably to bind to Pango to get text and layout support. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 4:18 PM, Reid Barton rwbar...@math.harvard.eduwrote: So here's a programming challenge: write a total function (expecting total arguments) toSame :: ((Nat - Bool) - Nat) - (Nat - Bool,Nat - Bool) that finds a pair that get mapped to the same Nat. Ie. f a==f b where (a,b) = toSame f (Warning: sketchy argument ahead.) Let f :: (Nat - Bool) - Nat be a total function and let g0 = const True. The application f g0 can only evaluate g0 at finitely many values, so f g0 = f ( k) for any k larger than all these values. So we can write toSame f = (const True, head [ ( k) | k - [1..], f (const True) == f ( k) ]) and toSame is total on total inputs. Well done! That's not sketchy at all! There is always such a k (when the result type of f has decidable equality) and it is the modulus of uniform continuity of f. This is computable directly, but the implementation you've provided might come up with a smaller one that still works (since you only need to differentiate between const True, not all other streams). I guess I should hold off on conjecturing the impossibility of things... :-) Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: type metaphysics
Ryan Ingram schrieb: 2009/2/2 Luke Palmer lrpal...@gmail.com: However! If we have a function f : Nat - Nat - Bool, we can construct the diagonalization g : Nat - Bool as: g n = not (f n n), with g not in the range of f. That makes Nat - Bool computably uncountable. This is making my head explode. How is g not in the range of f? In particular, f is a program, which I can easily implement; given: f is 'easy to implement' if it enumerates all functions, not just total ones. Otherwise, f is hard to implement ;) In the first case, if we have (f n n) = _|_, then g n = not (f n n) = _|_ as well, so the diagonalization argument does not hold anymore. But I do agree that proofs by contradiction do not map well to haskell ... benedikt compiler :: String - Maybe (Nat - Bool) mkAllStrings :: () - [String] -- enumerates all possible strings I can write f as f n = validPrograms () !! n where validPrograms = map fromJust . filter isJust . map compiler . mkAllStrings Now, in particular, mkAllStrings will generate the following string at some index, call it stringIndexOfG: source code for compiler source code for mkAllStrings source code for f g n = not (f n n) This is a valid program, so the compiler will compile it successfully, and therefore there is some index validProgramIndexOfG less than or equal to stringIndexOfG which generates this program. But your argument seems to hold as well, so where is the contradiction? -- ryan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Verifying Haskell Programs
On Mon, Feb 2, 2009 at 15:04, Don Stewart d...@galois.com wrote: pocmatos: Hi all, Much is talked that Haskell, since it is purely functional is easier to be verified. However, most of the research I have seen in software verification (either through model checking or theorem proving) targets C/C++ or subsets of these. What's the state of the art of automatically verifying properties of programs written in Haskell? State of the art is translating subsets of Haskell to Isabelle, and verifying them. Using model checkers to verify subsets, or extracting Haskell from Agda or Coq. Don, can you give some pointers to literature on this, if any? That is, any documentation of a verification effort of Haskell code with Isabelle, model checkers, or Coq? (It's not that I don't believe you -- I'd be really interested to read it!) Denis ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Verifying Haskell Programs
dbueno: On Mon, Feb 2, 2009 at 15:04, Don Stewart d...@galois.com wrote: pocmatos: Hi all, Much is talked that Haskell, since it is purely functional is easier to be verified. However, most of the research I have seen in software verification (either through model checking or theorem proving) targets C/C++ or subsets of these. What's the state of the art of automatically verifying properties of programs written in Haskell? State of the art is translating subsets of Haskell to Isabelle, and verifying them. Using model checkers to verify subsets, or extracting Haskell from Agda or Coq. Don, can you give some pointers to literature on this, if any? That is, any documentation of a verification effort of Haskell code with Isabelle, model checkers, or Coq? (It's not that I don't believe you -- I'd be really interested to read it!) All on haskell.org, http://haskell.org/haskellwiki/Research_papers/Testing_and_correctness#Verifying_Haskell_programs And there's been work since I put that list together. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type metaphysics
On Mon, Feb 2, 2009 at 3:18 PM, Reid Barton rwbar...@math.harvard.edu wrote: toSame f = (const True, head [ ( k) | k - [1..], f (const True) == f ( k) ]) Nice! I like it because at first look it seems like there's no reason for this to terminate, but as you correctly argue, it always does. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: circular dependencies in cabal
Duncan Coutts duncan.cou...@worc.ox.ac.uk wrote: That is probably how people are getting into this mess. Using upgrade is not necessarily such a good idea. It does not distinguish between the interesting packages you might want to upgrade and the core packages that your probably do not want to touch. There's no need to use cabal upgrade to get into this kind of mess, I successfully pulled conflicting cabal versions just by using cabal install. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
