Re: [Haskell-cafe] Re: [Coq-Club] An encoding of parametricity in Agda
Hi Taral, Eugene, [Taral] Perhaps I don't understand Agda very well, but I don't see parametricity here. For one, there's no attempt to prove that: forall (P Q : forall a, a - a), P = Q. [Eugene] Under parametricity, I mean the Reynolds Abstraction Theorem, from which free theorems follow. Would it help to say that the Abstraction Theorem states that every *definable* function is parametric, whereas Taral's formula states that *every* function of that type is parametric? (Both concepts are useful; Agda presumably has models where Taral's formula does not hold (if it's consistent, i.e. has models at all), so that formula presumably isn't provable in Agda without additional axioms.) All the best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Use unsafePerformIO to catch Exception?
Hi Duncan and all,
On Wed, Mar 25, 2009 at 3:52 AM, Duncan Coutts
duncan.cou...@worc.ox.ac.uk wrote:
On Mon, 2009-03-23 at 08:11 -0400, Xiao-Yong Jin wrote:
tryArith :: a - Either ArithException a
tryArith = unsafePerformIO . try . evaluate
You must not do this. It breaks the semantics of the language.
Other people have given practical reasons why you should not but a
theoretical reason is that you've defined a non-continuous function.
That is impossible in the normal semantics of pure functional languages.
So you're breaking a promise which we rely on.
...
Of course your tryArith only tests for certain kinds of _|_ value, but
in principle the problem is the same.
That's not *quite* how the semantics of Haskell exceptions are
defined, actually, unless I'm misunderstanding something or the
thinking about it has changed since the original paper on the topic:
Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow, Fergus
Henderson: A semantics for imprecise exceptions. SIGPLAN Conference
on Programming Language Design and Implementation, 1999.
http://www.haskell.org/~simonmar/papers/except.ps.gz
In the semantics given by that paper, the value of an expression of type Int is
(a) an actual number, or
(b) a set of exceptions that the expression might raise when evaluated, or
(c) bottom, which means: when evaluated, the expression may not
terminate, or may terminate and raise some arbitrary exception.
(The semantic ordering is: everything is larger than bottom; a set of
expressions A is larger than a set of expressions B iff A is a proper
subset of B; numbers are not comparable to sets.)
tryArith is still noncontinuous, though, and nondeterministic, too. Consider:
divzero = 1/0
overflow = 2**1000
loop = loop - 1
* What is (tryArith (divzero + overflow))? The denotational value of
(divzero + overflow) is the set {DivideByZero, Overflow}, so tryArith
can return either (Left DivideByZero) or (Left Overflow) --
nondeterminism.
* What is (tryArith (overflow + loop))? The denotational value of
(overflow + loop) is bottom, so tryArith can theoretically return any
arithmetic exception, or propagate any non-arithmetic exception, or
loop forever. In practice, of course, it will either return (Left
Overflow), or loop forever, or error out if the compiler notices the
loop. However, this still means that it *may* return (Left Overflow)
even though the semantical value of (overflow + loop) is bottom, which
means that the function is not monotone and thus not continuous.
All the best,
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Use unsafePerformIO to catch Exception?
On Thu, Mar 26, 2009 at 2:40 AM, Duncan Coutts duncan.cou...@worc.ox.ac.uk wrote: I was not being precise when I said tests for _|_. As you point out, the semantics of imprecise exceptions distinguishes exceptions from bottom, however pure code cannot make that distinction and so that's why I was lumping them together and saying that tryArith tests for certain kinds of _|_ value. Right... I had this mental picture of exceptions being values denotationally smaller than any real value of the domain before I read the imprecise exceptions paper, so I interpreted your imprecise description that way =) Anyway, I hope this is enough to dissuade people from using unsafePerformIO to catch exceptions. Yes, unfortunately you can't even use it to return Nothing on errors (ie without returning the specific exception) because of the (overflow + loop) issue where you have nondeterminism between returning Nothing and looping forever. I have my own history of wondering why isn't there in Control.Exception a function that... for a while before figuring out why there isn't :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] about Haskell code written to be too smart
2009/3/24 Peter Verswyvelen bugf...@gmail.com: This strategy is doomed to failure, unfortunately. So it is the good strategy, because Haskell's slogan is avoid success at all cost :-) IN THE YEAR 1987, WAR WAS BEGINNING BIG, IMPERATIVE SOFTWARE BEHEMOTHS CLASHED IN A STATE OF IMPURITY UNDER THE SHADOW OF FEAR AND DOUBT, COLONY BY COLONY FELL INTO TYPELESS ANARCHY WHOLE PLANETS WERE SCROUNGED BY TERRIBLE SEGFAULTS THE HUNGER FOR A NEW PARADIGM WAS GNAWING AT THE ROOTS OF THE CIVILIZED UNIVERSE MEANWHILE, IN A GALAXY FAR, FAR AWAY, A SMALL GROUP OF LAZY FUNCTIONAL PROGRAMMERS CREATED A LANGUAGE IT WAS OUR LAST, BEST HOPE TO AVOID SUCCESS AT ALL COST... IT FAILED IT EVOLVED THERE ARE 8,581 IMPLEMENTATIONS SUPPORTING 935,842,712 EXTENSIONS THEY LOOK AND FEEL ... FUNCTIONAL SOME ARE PROGRAMMED TO THINK THAT THEY AREN'T IMPERATIVE AT ALL AT LEAST ONE IS ACTUALLY USED ONCE, IT HAD BEEN OUR LAST, BEST HOPE TO AVOID SUCCESS IN THE YEAR 2009, IT BECAME SOMETHING GREATER: OUR LAST, BEST HOPE FOR BLASTING THE INFERIOR LANGUAGES OUT OF THE SKY (WITH LAZY CLASS) YOU HAVE NO CHANCE TO SURVIVE MAP YOUR BIND ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Haskell] Google Summer of Code 2009
Hi all, On Tue, Feb 10, 2009 at 3:26 PM, Malcolm Wallace malcolm.wall...@cs.york.ac.uk wrote: If you have ideas for student projects that you think would benefit the Haskell community, now is the time to start discussing them on mailing lists of your choice. We especially encourage students to communicate with the wider community (...) I have a project that I've tinkered with doing for a while, but have never actually gotten around to, and I'm wondering whether there would be interest from the community in using it. Actually, two related projects: (1) A library for working with hashable data structures, including a hashable finger tree with sequence, map and set types based on it. Surprisingly, there does not seem to be much library support for working with hashes in Haskell beyond the bare-bones, imperative Data.HashTable, even though pure functional programming and hashes Go Well Together. I'm pulling these bounds out of my intuition, but hashable collections should give amortized O(1) comparison for equality and amortized O(log n) comparison for order, and you could use them as set values and map keys without efficiency blowing up in your face. The library should probably also include support for hashtables based on the various kinds of pure and monad-encapsulated arrays we have in Haskell, and maybe include support for interning values; unsafePerformIO, weak references and friends were originally introduced with the intention to support interned values in a way that programmers can tailor to their own needs, but it would be nice to have some default library support. (2) Based on this, a serialization library that would recognize if it has already written a particular value from memory to the same file, and write a pointer to the first occurrence of that value instead of serializing the actual value again, making it efficient to serialize versioned data structures. The idea is to make something similar to HAppS' MACID, but where MACID serializes the different kinds of updates that you can do for your data, this library would simply do the update in memory, then serialize the whole updated value to disk, but actually *writing* only the *new* parts of the data structure. (I think this could be simpler to use, and would be in a sense more elegant and 'haskelly' than the MACID approach. On the other hand, we already *have* MACID.) So, anybody out there who looks at these things and thinks this could be useful? :-) Thanks, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Laws and partial values
Hi Lennart, On Sat, Jan 24, 2009 at 10:47 PM, Lennart Augustsson lenn...@augustsson.net wrote: You can dream up any semantics you like about bottom, like it has to be () for the unit type. But it's simply not true. I suggest you do some cursory study of denotational semantics and domain theory. Umh. It's certainly not Haskell, but as far as I can tell, the semantics Bob likes are perfectly fine domain theory. (_|_, _|_) = _|_ is the *simpler* definition of domain-theoretical product (and inl(_|_) = inr(_|_) = _|_ is the simpler definition of domain-theoretical sum), and the unit of this product (and sum) is indeed the type containing only bottom. Lifting everything, as Haskell does, is extra. I suppose it's unusual that Bob wants to lift sums but not products, but there's nothing theoretically fishy about it that I can see. All the best, - Benja P.S. For anybody wanting to brush up: http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf -- Section 3.2. -B ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Improved documentation for Bool (Was: [Haskell-cafe] Comments from OCaml Hacker Brian Hurt)
On Sun, Jan 18, 2009 at 5:48 PM, rocon...@theorem.ca wrote:
I noticed the Bool datatype isn't well documented. Since Bool is not a
common English word, I figured it could use some haddock to help clarify it
for newcomers.
-- |The Bool datatype is named after George Boole (1815-1864).
-- The Bool type is the coproduct of the terminal object with itself.
Russell, this does seem like it might be very helpful, but it might be
useful to include a note about what category you are working in.
People may sometimes naively assume that one is working in the
category of Haskell/Hugs/GHC data types and Haskell functions, in
which there are no terminal -- or initial -- objects ('undefined' and
'const undefined' are distinct maps between any two objects X and Y),
or else in the similar category without lifted bottoms, in which the
empty type is terminal and the unit type isn't ('undefined' and 'const
()' are both maps from any object X to the unit type). These niceties
will not confuse the advanced reader, but it may help the beginner if
you are more explicit.
- Benja
P.S. :-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Stupid question #374: why is MaybeT not in the standard library?
On Tue, Dec 23, 2008 at 2:52 AM, Antoine Latter aslat...@gmail.com wrote: Although I still had to use my own because I wanted a MonadPlus instance. I would offer a patch, but since there's more than one useful MonadPlus instance for MaybeT it probably still wouldn't be right for everyone. Umh, there is a MonadPlus instance in the package? http://hackage.haskell.org/packages/archive/MaybeT/0.1.2/doc/html/Control-Monad-Maybe.html (It's the one based on the Maybes.) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Stupid question #374: why is MaybeT not in the standard library?
On Tue, Dec 23, 2008 at 8:05 PM, Benja Fallenstein benja.fallenst...@gmail.com wrote: Umh, there is a MonadPlus instance in the package? Ah: ...in the version Cale uploaded two days ago, not in the previous version. Sorrynevermindisee :) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof that Haskell is RT
Hi all, On Wed, Nov 12, 2008 at 2:09 PM, Lennart Augustsson [EMAIL PROTECTED]wrote: You can't write a straightforward dynamic semantics (in, say, denotational style) for Haskell. The problem is that with type classes you need to know the types compute the values. ... It's possible that there's some more direct approach that represents types as some kind of runtime values, but nobody (to my knowledge) has done that. It seems to me that if you don't need your semantics to do the work of type-*checking* (i.e., you don't care if the rules assign some strange denotation to an ill-typed term), there is a natural approach to giving semantics to 98-style type classes. I'm figuring out the details as I type, though; if anybody sees anything that does not work, please do tell! Let type mean a non-overloaded type expression (i.e., not containing variables). I'll suppose that you already know the set of types in the program and the domain associated with each type. (This is usual in denotational treatments, right?) Let the domains be such that all sets of elements have a join (i.e., complete lattices). Define the domain of overloaded values to be the domain of functions from types to values of these types or bottom (when I say bottom in the following, it is this bottom, which is below the domain's bottom), i.e., the product of the liftings of the domains of all possible types. The interpretation of bottom is, this overloaded value doesn't have an instance at this type (e.g., [7,9] is bottom at type Bool). An *environment* is a function from symbols to overloaded values. The denotation of an expression is a function from environments to overloaded values; the denotation of a definition list is a function from environments to environments; the denotation of a whole program is the least fixed point of the definition list that makes up the program. Expressions are interpreted as follows (update :: Symbol - OverloadedValue - Environment - Environment is defined in the natural way): [[x]] = \env type. env x type [[T :: TYPE]] = \env type. if type instance of TYPE then [[T]] env type else bottom [[F X]] = Join_type2. \env type1. [[F]] env (type1 - type2) $ [[X]] env type2 [[\x. T]] = \env type. case type of (type1 - type2) - \val. [[T]] (update x (mono type1 val) env) type2 otherwise - bottom where mono ty val = \ty'. if ty == ty' then val else bottom [[let x=S in T]] = \env type. [[T]] (fix $ \env'. update x ([[S]] env') env) type Simple definitions are interpreted in the obvious way: [[x = T]] = \env sym. if sym == x then ([[T]] env) else (env sym) [[x :: Ty; x = T]] = [[x = T :: Ty]] Finally, instance declarations are interpreted in a special way. To interpret the declaration instance C Ty1 .. Tyn where ...; xi = Ti; ... we need to know the set of possible types for xi. (No type inference should be necessary -- the class declaration + the Ty1 .. Tyn from the instance declaration should give us all the necessary information, right?) Call this set Types. Then, [[xi = Ti]] = \env sym type. if sym == xi type in Types then [[T]] env type else env sym type That is, an instance declaration sets the value of a symbol at some types, and leaves the values at the other types alone. Some notes: * If T is a well-typed term and type is *not* a type instance of that term, then ([[T]] env type) is bottom. * In particular, [[T :: TYPE]] env type = [[T]] env type, when type is an instance of TYPE; otherwise, [[T :: TYPE]] env type = bottom. * Application is supposed to be strict in bottom: bottom x = bottom; f bottom = bottom. * In interpreting [[F X]], we take the join over all possible types of X (type2). If X is monomorphic, then ([[X]] env type2) is bottom for all types except the correct one, so the join gives the correct denotation. If X is polymorphic, but the type of F together with the type forced by the context of (F X) together determine what type of X must be used, then either ([[F]] env (type1 - type2)) or ([[X]] env type2) will be bottom for every type2 exept for the one we want to use; so the application ([[F]] ... $ [[X]] ...) will be bottom except for the correct type; so again, the join will give the correct denotation. (Caveat lector: I haven't proved this, I'm running on intuition :)) * In the interpretation of expressions like (show (read 5)), the join is non-degenerate: it consists of the join of 5, 5.0 etc. But since such expressions are rejected by the type-checker, we don't care. * Lets containing multiple definitions can be translated as in the Haskell report, if we add an interpretation for a case construct (I'm too lazy to try): http://www.haskell.org/onlinereport/exps.html#sect3.12 * In the interpretation of the lambda expression, we need to interpret the body of the expression separately for every type of the lambda expression; the function 'mono' converts the monomorphic parameter value into an OverloadedValue that is bottom everywhere except at the
Re: [Haskell-cafe] Haskell symbol ~
Hi Maurício, I've got one thing to add to the replies so far: On Wed, Aug 27, 2008 at 8:23 PM, Maurício [EMAIL PROTECTED] wrote: What does '~' mean in Haskell? I read in haskell.org/haskellwiki/Keywords that (...) Matching the pattern ~pat against a value always suceeds, and matching will only diverge when one of the variables bound in the pattern is used. Isn't that true for any variable, due to lazyness? To any variable, yes. But you don't apply it to a variable, you apply it to a constructor pattern: not ~xs but ~(x:xs). Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Thinking about an unlistN
Hi,
On Sun, Aug 10, 2008 at 8:57 PM, Michael Feathers
[EMAIL PROTECTED] wrote:
If I have, say, a function f :: a - a - a - a - b it would be nice to be
able to just:
unlistN 4 f [1..4]
It indeed doesn't work like this; there's more than one way to do
something *like* this, if you really want to. The closest one is
probably to use type-level numbers:
{-# OPTIONS_GHC -fglasgow-exts #-}
data Zero
data Suc a
zero :: Zero; zero = undefined; suc :: a - Suc a; suc = undefined
one = suc zero; two = suc one; three = suc two; four = suc three
class Unlist n a b where
type UnlistFn n a b
unlist :: n - UnlistFn n a b - [a] - b
instance Unlist Zero a b where
type UnlistFn Zero a b = b
unlist _ r _ = r
instance Unlist n a b = Unlist (Suc n) a b where
type UnlistFn (Suc n) a b = a - UnlistFn n a b
unlist _ f (x:xs) = unlist (undefined :: n) (f x) xs
main = print (unlist four (,,,) abcd)
This prints ('a','b','c','d').
Hope this is fun[*],
- Benja
[*] I hesistate to say hope this helps in this case :-)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Stripping text of xml tags and special symbols
Hi Pieter, 2008/8/5 Pieter Laeremans [EMAIL PROTECTED]: But the sphinx indexer complains that the xml isn't valid. When I look at the errors this seems due to some documents containing not well formed html. If you need to cope with non-well-formed HTML, try HTML Tidy: http://tidy.sourceforge.net/ All the best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Precedence and associativity in a pretty-printer
Hi Edsko, On Jan 22, 2008 7:34 PM, Edsko de Vries [EMAIL PROTECTED] wrote: Is there a nice way to pretty-print such an expression with the minimal number of brackets? I can come up with something, but I'm sure somebody thought hard about this problem before and came up with a really nice solution :) Take a look at how Haskell's derived Show instances do it? :-) http://www.haskell.org/onlinereport/derived.html#sect10.4 - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] functional graphs
Hi Christian, On Jan 21, 2008 10:57 AM, Christian Maeder [EMAIL PROTECTED] wrote: Thanks for pointing out this proposal. The actual problem is mkGraph that needs all the many edges created beforehand (that's what I wanted to avoid). Well, uh, at the risk of being obvious, if you can avoid using fgl functions that call mkGraph, then there is nothing to say that mkGraph has ever to be called, and conversely, if you must use fgl functions that call mkGraph, then there is no way to avoid the fact that it gets the edge labels in a list... :-) A quick grep of the library shows that use of mkGraph is very rare. I haven't chased down the uses of functions that call mkGraph, though, so I don't really know whether many or few functions use mkGraph internally. Of course, you can use (mkGraph = error mkGraph) and see whether you trip over it at all. Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] functional graphs
Hi Christian, On Jan 18, 2008 1:55 PM, Christian Maeder [EMAIL PROTECTED] wrote: data CGraph a b = CGraph [a] (a - a - b) Can I define an instance for the fgl Graph class? I had no idea how to define empty (except using undefined). Well, presumably the function does not need to be defined on values not in the list, so returning an error is fair enough-- empty = CGraph [] (const $ error Node not in graph) I suppose you want to use the index in the list as the Node (= Int), which should be fine, but you'll run into problems with mkGraph, because you don't have an Eq constraint on a, so you can't implement the function to pass to CGraph. Since mkGraph is required to have the type mkGraph :: [LNode a] - [LEdge b] - CGraph a b for *all* a and b, you don't have a way to add an Eq constraint anywhere, either. So, no dice... However, if you'd be able to live with data CGraph a b = CGraph [LNode a] (Node - Node - b) then you should be able to write the instance like this-- instance Graph CGraph where empty = CGraph [] (const $ error Node not in graph) isEmpty (CGraph xs _) = null xs labNodes (CGraph xs _) = xs mkGraph nodes edges = CGraph nodes f where f x y = fromMaybe (error Edge not found) (lookup (x,y) edges') edges' = map (\(x,y,l) - ((x,y),l)) edges match x (CGraph nodes f) = case lookup x nodes of Nothing - (Nothing, CGraph nodes f) Just l - let nodes' = filter ((/= x) . fst) nodes left = map (\(y,_) - (f y x, y)) nodes' right = map (\(y,_) - (f x y, y)) nodes' in (Just (left, x, l, right), CGraph nodes' f) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] functional graphs
Hi, On Jan 19, 2008 6:05 PM, Thomas Hartman [EMAIL PROTECTED] wrote: Do you just assume that every two nodes have an edge between them [...]? Since that's what complete graph means, I assume so =-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 0/0 1 == False
Hi Mitar, On Jan 10, 2008 9:22 AM, Mitar [EMAIL PROTECTED] wrote: I understand that proper mathematical behavior would be that as 0/0 is mathematically undefined that 0/0 cannot be even compared to 1. My understanding is that common mathematical practice is that comparing an undefined value to anything (including itself) always yields false; x /= x is sometimes used to formalize x is undefined. If you have access to JSTOR, this article contains an overview of different fields' perspectives on dealing with undefinedness: http://links.jstor.org/sici?sici=0022-4812(199009)55%3A3%3C1269%3AAPFVOC%3E2.0.CO%3B2-T - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] \_ - not equivalent to const $
On Jan 10, 2008 11:54 PM, Luke Palmer [EMAIL PROTECTED] wrote: Can someone explain what the heck is going on here? Evaluating (const EXPR) creates a closure object with a pointer to 'const' and a pointer to the EXPR thunk. Call this closure object C. Evaluating (C undefined) calls 'const' with the EXPR and C thunks as its arguments, which returns the EXPR thunk. The EXPR thunk is then forced by your code. Evaluating (C undefined) again calls 'const' with the EXPR and C pointers as its arguments again, which again returns the *now forced* EXPR thunk. I.e., evaluating (const EXPR) creates a closure with a pointer to a single EXPR thunk, and then applying the same closure to some argument multiple times uses that same EXPR thunk every time. An unoptimized (\_ - EXPR) creates a new thunk each time the function is applied to an argument. Hope that helps with understanding what is going on? - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Basic question concerning data constructors
Hi Yitz, On Jan 2, 2008 10:34 AM, Yitzchak Gale [EMAIL PROTECTED] wrote: No, only countably many. By the type expression Integer - Integer we mean all Haskell functions mapping Integers to Integers. There are only countably many of those. ... But that was not the context in this thread. The category Hask that we often mention in discussions about Haskell the programming language is most certainly a small category. I don't know. My understanding has been that at least part of the benefit of denotational semantics is that you can define what an expression means without referring back to the syntactic construction or the operational semantics of that expression -- and thus use the denotational semantics to check whether the operational semantics are right. But if you start with all Haskell functions, you already have to know what a Haskell function *is*. I think it should be allowed to think of the semantics of Haskell as being defined independently of the (relatively operational) notion of computable function, and then define computable function to be that subset of the functions in the model that you can actually write in Haskell. And the only explicit non-syntactic constructions of models for Haskell-like languages that I'm familiar with aren't countable (they contain all continuous functions, which in the case of (Integer - Integer) comes out to all monotonous functions). So I disagree that the function types of Hask should automatically be taken to be countable. If you want to assume it for some given purpose, sure, fine, but IMO that's an additional assumption, not something inherent in the Haskell language. Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Basic question concerning data constructors
On Dec 31, 2007 7:17 AM, [EMAIL PROTECTED] wrote: This declaration states that there's a bijection between the elements of Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot be true for any set. That's because we only allow computable functions, Nit the nit: Or (more commonly, I think) all continuous functions. and Foo - Bool is actually an exponential object in the category Hask. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The semantics of constructor patterns
Hi Cristian,
On Dec 30, 2007 6:10 PM, Cristian Baboi [EMAIL PROTECTED] wrote:
What I don't get it :
(s a1 a2 ... at) must be the value of A in the semantic domain. Let call
that value a.
Then how can one know if a was built with (s a1 a2 ... at) and not with
(egg b1 b2) ?
Because the semantic domain is chosen so that (s a1 a2 ... at) and
(egg b1 b2) are distinct objects.
More precisely, the domain corresponding to (for example) the type
data T = C1 T11 T12 | C2 T21 T22
should be isomorphic to the domain
[[T]] = lift (([[T11]] * [[T12]]) + ([[T21]] * [[T22]]))
where * is cartesian product, + is disjoint sum (e.g., X+Y = {(1,x) |
x in X} union {(2,y) | y in Y}, and 'lift' adds the bottom element to
the domain.
So here, C1 and C2 correspond to the two sides of the disjoint sum,
meaning you can tell them apart.
Hope that helps?
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Empty instance declaration
On Dec 28, 2007 5:14 PM, Mike Haskel [EMAIL PROTECTED] wrote: You can define Show as a data type, rather than a type class: type Show a = Either (a - String) (Int - a - String - String) ... The constructors for Show make explicit the two ways to define an instance. This technique also has the advantage of allowing multiple, non-conflicting instance declarations, selectable at runtime. Using Show as an example, you might have instances representing both formatted and unformatted display. An obvious disadvantage is that the instance needs a name and gets passed explicitly. Seems to me that using Either is entirely orthogonal from type-vs-class :-) class Show a where show0 :: Either (a - String) (Int - a - String - String) show :: Show a = a - String show = case show0 of Left s - s Right sp - \x - sp 0 x etc. - Benja ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell-cafe] Missing join and split
Hi all, On Dec 28, 2007 12:38 PM, Andrew Coppin [EMAIL PROTECTED] wrote: For joining you probably want some combination of intersperse and concat, e.g. unlines = concat . intersperse \n And that's what we have :-) Data.List.intercalate :: [a] - [[a]] - [a] Data.List.intercalate x = concat . intersperse x For splitting, do we split on a given character? A predicate? Do we keep the splitting character or throw it away? Do we generate empty sublists or elide them? Apparently nobody can agree on these points, and writing a function with all possible options would be very messy... If you use intercalate to join, I would presume that you would want to use an inverse of it to split. I'd write it like this: split :: Eq a = [a] - [a] - [[a]] split at xs | Just xs' - stripPrefix at xs = [] : split at xs' split at (x:xs) = (x:r) : rs where (r:rs) = split at xs split at [] = [[]] --with, if your version of the libraries is as old as mine and doesn't have Data.List.stripPrefix, stripPrefix (p:ps) (x:xs) | p == x = stripPrefix ps xs stripPrefix [] xs = Just xs stripPrefix _ _ = Nothing - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Missing join and split
On Dec 28, 2007 3:55 PM, David Roundy [EMAIL PROTECTED] wrote: On Dec 28, 2007 9:51 AM, Benja Fallenstein [EMAIL PROTECTED] wrote: If you use intercalate to join, I would presume that you would want to use an inverse of it to split. I'd write it like this: Of course, there is no inverse to intercalate Right; I misspoke. What I meant was that you would want a split such that intercalate a (split a xs) = a for finite, total (a,xs) (and, since it's achievable, even for infinite xs). Of course, (split a xs = [xs]) satisfies that, but if we add the requirement that split is also supposed to do its job :-) then I think split is fully specified except for whether (split a [] = []) or (split a [] = [[]]). The latter seems better to me; e.g., it satisfies split a (x ++ a ++ y) = split a x ++ split a y so if you want to use a logical approach, perhaps you'd want to define split first, and then define your join as the inverse of split. If your join comes out as being intercalate, I suppose it's six of one, half a dozen of the other :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Missing join and split
On Dec 28, 2007 4:24 PM, Benja Fallenstein [EMAIL PROTECTED] wrote: Right; I misspoke. What I meant was that you would want a split such that intercalate a (split a xs) = a for finite, total (a,xs) (and, since it's achievable, even for infinite xs). Of course, (split a xs = [xs]) satisfies that, but if we add the requirement that split is also supposed to do its job :-) then I think split is fully specified except for whether (split a [] = []) or (split a [] = [[]]). I take that back; it doesn't specify whether (split xx xxx) should be [,x] or [x,]. I prefer the former, because working left-to-right seems natural, and because it makes split more lazy (it can yield (:_) before evaluating the input enough to see the third 'x'). The latter seems better to me; e.g., it satisfies split a (x ++ a ++ y) = split a x ++ split a y I take that back, too: split xx = [,,] split xx x ++ split xx xxx = [x] ++ [,x] (...but, still... :-)) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Comments on reading two ints off Bytestring
On Dec 23, 2007 1:44 PM, Isaac Dupree [EMAIL PROTECTED] wrote: parseHeader3 :: BS.ByteString - Maybe (Int, Int) parseHeader3 bs = do (x, rest) - BS.readInt $ BS.dropWhile (not . isDigit) bs (y, _) - BS.readInt $ BS.dropWhile (not . isDigit) rest return (x, y) But that version still itches! :-) This is what it sounds like to me: parseHeader :: BS.ByteString - Maybe (Int,Int) parseHeader = evalStateT $ liftM2 (,) parseInt parseInt where parseInt = StateT $ BS.readInt . BS.dropWhile (not . isDigit) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: CAF's in Haskell
Hi Neil, On Dec 26, 2007 7:16 PM, Neil Mitchell [EMAIL PROTECTED] wrote: Given the code: fred = 2 + 2 bob = fred + fred In a Haskell implementation fred would be evaluated once to 4, then used twice. The 2+2 would only happen once (ignore defaulting and overloaded numerics for now). Is this sharing mandated by the standard? (I don't think so) Is there some paper that describes why this is desirable, and gives any detail? I think if the report does not mandate it, it's for the same reason that Haskell-the-language is non-strict, not lazy-- it thinks that it's the compiler's business to decide things like this. (After all, there are situations where it might be better to evaluate Fred twice, and the compiler might recognize some of them.) But the Haskell design certainly anticipates that this is what compilers will normally do: the point of the dreaded monomorphism restriction is to make sure that 'fred' doesn't accidentally become (Num a = a), which would make it infeasible to evaluate it only once (because you would have to store the value for every instance of Num). It's a lot like you can expect Haskell implementations to be lazy, not call-by-name. (I don't know when this behavior originated.) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
Hi Cristian, On Dec 18, 2007 10:53 AM, Cristian Baboi [EMAIL PROTECTED] wrote: - the lambda expressions can be written (input) but cannot be printed (output) Yes, since two different lambda expressions can denote the same function. I just want the sistem to be able to print one of these expressions ! Its this too much to ask ? I find it very strange that I can write a lambda expresion, but the system cannot. It's a trade-off. Haskell has as a design goal that you can use equational reasoning everywhere -- that if you have two ways of writing the same function, you can substitute one for the other in any expression, without changing the result of that expression. For example, since you can prove sum = foldl (+) 0 = foldr (+) 0 = last . scanl (+) 0 you can, in any place you use 'sum,' substitute any of these expressions without changing the result. You couldn't do this if you could write (show sum) and (show $ foldl (+) 0) and they would return different values. You could design the language differently, of course, but the Haskell designers want you -- and the compiler -- to be able to use equational reasoning everywhere -- so they disallow printing functions. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
Hi Henning,
On Dec 18, 2007 3:53 PM, Henning Thielemann
[EMAIL PROTECTED] wrote:
Since this was discussed already here, I summed it up in:
http://www.haskell.org/haskellwiki/Show_instance_for_functions
I find the discussion under theoretical answer unsatisfying. The
property that a Show instance for functions would break is
extensionality, and while extensionality is a desirable trait and
matches the common mathematical intuitions, a system with intensional
functions certainly isn't unmathematical or impure.
Further, even with extensionality, we can (with compiler support) in
principle have Show instances other than enumerating the graph. At
least for simple non-recursive functions, showing the Böhm tree of the
function could be useful (except that you loop forever if you
encounter bottom somewhere, of course, instead of printing bottom as
you would if you could print the actual Böhm tree). For example, id
would be shown as \a - a, maybe would be shown as \a b c - case c
of { Just d - b d; Nothing - a }, and all would be shown as \a -
case a of { (b:c) - case b of { False - False; True - case c of {
(d:e) - case d of { False - False et cetera ad infinitum.
Of course, for functions on ints this would indeed reduce to
enumerating the graph, printed as an infinite case expression.
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
On Dec 18, 2007 4:50 PM, Benja Fallenstein [EMAIL PROTECTED] wrote: Further, even with extensionality, we can (with compiler support) in principle have Show instances other than enumerating the graph. Now that I said it, I'm starting to doubt we even need compiler support beyond what we have already. :-) I'm starting to think that a smattering of unsafePerformIO might be able to do the trick. I shall have to think on this :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
Hi Henning, On Dec 18, 2007 5:17 PM, Henning Thielemann [EMAIL PROTECTED] wrote: The mathematical definition of function I know of, says that functions are special relations, and relations are sets of pairs. Their is nothing about intension. That's the standard definition in set theory, but it's not the only mathematical definition of function. It also doesn't suffice for defining all Haskell functions-- consider data T = T (T - Int) fn :: T - Int fn _ = 7 We have (fn (T fn) == 7), so in the graph of 'fn' we must have a pair (T fn, 7). But if 'fn' is the same mathematical object as its graph, that would mean that the graph of 'fn' would have to contain a pair whose first element indirectly contains... the graph of fn! This sort of circularity is not allowed in standard ZFC set theory, so if we're going to be precise, we will have to choose a different representation for functions than their graphs. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
Hi Paul, On Dec 18, 2007 5:18 PM, Paul Hudak [EMAIL PROTECTED] wrote: If the semantics of a language says that a function f is equivalent to a function g, but there is a function h such that h(f) is not equivalent to h(g), then h cannot be a function. Sure. Therefore that language cannot be a (purely) functional language. That is the pure and simple reason why functions are not Showable in Haskell. Not so fast :-) Caveat one, there may be useful ways to for functions to implement Show that don't conflict with extensionality (i.e., the property that two functions are equal if they yield the same results for all inputs). Caveat two, we generally assume extensionality when reasoning about Haskell, but it's entirely possible to give a semantics for Haskell that doesn't assume extensionality. IMHO, a good answer to the question why functions aren't showable in Haskell needs to explain why we prefer our semantics to be extensional, not say that by god-given fiat, Haskell is extensional, so we can't show functions. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
On Dec 18, 2007 6:01 PM, Paul Hudak [EMAIL PROTECTED] wrote:
Well, my caveat was that the Haskell designers wanted it this way. So
you are essentially rejecting my caveat, rather than creating a new one.
:-)
I mean, I reject the answer They wanted it this way because I think
the answer should be, They wanted it this way because They looked at
substituting equals under a lambda, and They saw it was good ;-)
Caveat one, there may be useful ways to for functions to implement
Show that don't conflict with extensionality (i.e., the property that
two functions are equal if they yield the same results for all
inputs).
Sure, and I suppose one way to do this is to put the show function for
functions into the IO monad -- then you can't inspect the results. But
if you want to inspect the result, then I have no idea how to do this.
If you can show and enumerate the argument type and show the result
type of a function, one way is to enumerate the graph of the function.
The wiki page gives the example,
Prelude \x - x+x
functionFromGraph [(0,0), (1,2), (2,4), (3,6),
Interrupted.
If you have special compiler support, and consider a fragment of
Haskell that contains only functions -- i.e., no algebraic data types,
no Ints etc. (it's kind of a boring fragment!, but you can have Church
numbers) --, you can reduce the function to head normal form. Head
normal form looks like this:
\VAR1 VAR2 ... VARm - VARi EXPR1 ... EXPRn
and there is a reduction strategy that finds the head normal form of
an arbitrary expression if there is one; a proof that if there isn't
one, the expression denotes bottom; and a proof that if you have two
HNFs, and they differ in the part before EXPR1 or differ in the number
of EXPRjs, these HNFs denote different values.
Therefore, when you have reduced the function to HNF, you can print
\VAR1 VAR2 ... VARm - VARi
(or more precisely, you can write a lazy 'show' that yields the above
characters as soon as it has computed the HNF). Then, you go on to
recursively compute the HNF of EXPR1, and you show that inside
parantheses.
Some examples:
show (\x - x) == \a - a
show (.) == \a b c - a (b c)
(let fix f = f (fix f) in show fix)
== \a - a (a (a (a (a.
[Unless I'm making some stupid mistake] It's well-established that
this is computable and doesn't break extensionality (i.e., that
applying this show to two functions with the same extension will give
the same result -- or conversely, if show gives different results for
two functions, there are arguments for which these functions yield
different results).
By itself, this isn't very interesting, but I *think* you should be
able to add algebraic data types and case expressions to this fragment
of Haskell and still do essentially the same thing. Then, you could
show, for example,
show either == \a b c - case c of { Left d - a d; Right e - b e }
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A Show instance for simple functions
Hi all,
Below is a program that implements Show for functions whose type is
composed of only (-) and type variables (or, more precisely, of (-)
and (State Int Term), but any type composed of (-) and type variables
can obviously be specialized to that).
(-fglasgow-exts is needed only for the convenience of being able to
declare instance MkTerm (State Int Term) -- if we'd wrap the State
Int Term in a newtype, as far as I can see this would be H98.)
- Benja
{-# OPTIONS_GHC -fglasgow-exts #-}
import Control.Monad
import Control.Monad.State
import Data.Char
data Term = Var Int | App Term Term | Lam Int Term
showVar i = [chr (ord 'a' + i)]
showTerm :: Term - String
showTerm (Var i) = showVar i
showTerm (Lam i x) = \\ ++ showVar i ++ - ++ showTerm x
showTerm (App f x) = showTerm f ++ ++ showArg x where
showArg (Var i) = showVar i; showArg x = ( ++ showTerm x ++ )
class MkTerm a where
argument :: State Int Term - a
mkTerm :: a - State Int Term
instance MkTerm (State Int Term) where
argument = id
mkTerm = id
instance (MkTerm a, MkTerm b) = MkTerm (a - b) where
argument f x = argument $ liftM2 App f (mkTerm x)
mkTerm f = do i - get; modify (+1)
body - mkTerm (f (argument (return (Var i
return $ Lam i body
instance (MkTerm a, MkTerm b) = Show (a - b) where
show f = showTerm $ evalState (mkTerm f) 0
type X = State Int Term
main = do print (id :: X - X)
print (id :: (X - X) - (X - X))
print ((.) :: (X - X) - (X - X) - (X - X))
print ((\x y - y x) :: X - (X - X) - X)
print ((\f x - f x x) :: (X - X - X) - X - X)
print ((\f - f id id) :: ((X - X) - (X - X) - X) - X)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] New to Haskell
Hi Paul, On Dec 19, 2007 6:54 AM, Paul Hudak [EMAIL PROTECTED] wrote: Your version of the answer is in fact correct, but is just an elaboration of the original one. So, I don't see what your point is... Ok, sorry, I'll try again... I'm trying to say that in my opinion, it's important to include the elaboration if you want to give a *useful* answer to why can't I print functions. :) If you can show and enumerate the argument type and show the result type of a function, one way is to enumerate the graph of the function. Yes, but this requires a STANDARD way to do this -- meaning that the underlying domains are enumerable in a standard way. I don't think that is always possible. It isn't always, no; in Haskell, there's no way to enumerate the instances of (IO Int), for example. But of course, you can't show (IO Int) in the first place, so I guess there's no expectation that you should be able to show functions with (IO Int) arguments, either. Function domains also aren't enumerable in general, although you could simply enumerate all functions writable in Haskell, and not care about duplicates. But it seems very unlikely anyway that printing higher-order functions in this way would be *practical*. And of course you may have an infinite graph, whereas the function itself is finite. (you mean that the function term is finite, I suppose) Yes, but you can show infinite lists, too -- resulting in an infinite String being returned by 'show.' Regarding the rest of your message: I don't see how this helps, since some terms do not have head-normal forms. But these terms denote bottom. Compare (show (1:2:_|_)); the behavior would be similar. Even in the pure lambda calculus there are terms that denote the same value but that are not convertible to one another. Such terms would return the same *infinite* String in this approach. You couldn't write a program to test whether they're equal; but you can't write a program that tests whether two arbitrary infinite lists are equal, either. It seems that at best this approach would yield only partial success. Oh, that's certainly true, in the sense that showing functions in this way would often not be as practical as one might hope for -- the worst problem being that recursive functions will often have infinite representations. Still, in my opinion, there is a difference between the theory says you can't show functions and from the theoretical perspective, there is an elegant way to show functions, but it would be a lot of work to implement and the result wouldn't be as practical as you're hoping for. Although I admit it's more of a theoretical difference than a practical one. :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
Hi Corey, On Dec 14, 2007 8:44 PM, Corey O'Connor [EMAIL PROTECTED] wrote: The reason I find all this odd is because I'm not sure how the type class Functor relates to the category theory concept of a functor. How does declaring a type constructor to be an instance of the Functor class relate to a functor? Is the type constructor considered a functor? Recall the definition of functor. From Wikipedia: A functor F from C to D is a mapping that * associates to each object X in C an object F(X) in D, * associates to each morphism f:X - Y in C a morphism F(f):F(X) - F(Y) in D such that the following two properties hold: * F(idX) = idF(X) for every object X in C * F(g . f) = F(g) . F(f) for all morphisms f:X - Y and g:Y - Z. http://en.wikipedia.org/wiki/Functor We consider C = D = the category of types. Note that any type constructor is a mapping from types to types -- thus it associates to each object (type) X an object (type) F(X). Declaring a type constructor to be an instance of Functor means that you have to provide 'fmap :: (a - b) - (f a - f b) -- that is, a mapping that associates to each morphism (function) fn :: a - b a morphism fmap fn :: f a - f b. Making sure that the two laws are fulfilled is the responsibility of the programmer writing the instance of Functor. (I.e., you're not supposed to do this: instance Functor Val where fmap f (Val x) = Val (x+1).) Hope this helps with seeing the correspondence? :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Questions about the Functor class and it's use in Data types à la carte
On Dec 15, 2007 3:44 AM, Benja Fallenstein [EMAIL PROTECTED] wrote: Hmmm. Something about that ticks off my don't play fast and loose with bottom detector. I should add that I do think you're correct if you ignore the existence of bottom, and I'm pretty sure that you're correct if you allow bottom but consider seq to be only slightly better than unsafePerformIO. But I couldn't turn your proof sketch into something that would completely convince me, myself :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re[2]: [Haskell-cafe] Execution of external command
On Dec 14, 2007 10:38 AM, Bulat Ziganshin [EMAIL PROTECTED] wrote: hUnsafeGetContentsDontUseThisUnlessYouHaveSpentThreeMonthsLearningGHCsExecutionSemanticsOrYouWillRegretIt i have more advanced proposal - we should include in its name whole paper on its semantics so anyone using it will be clearly warned. moreover, any suggestion to use this function will automatically include exact description of its caveats that is again The Right Thing To Do :) Until, that is, the first library appears on Hackage that aliases the name to ohBugger :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Software Tools in Haskell
On Dec 14, 2007 9:29 AM, Henning Thielemann [EMAIL PROTECTED] wrote: I remember there was a discussion about how to implement full 'wc' in an elegant but maximally lazy form, that is counting bytes, words and lines in one go. Did someone have a nice idea of how to compose the three counters from implementations of each counter? I'm afraid one cannot simply use the split and count fragments trick then. Could you turn the folds into scans and use zip3 and last? I.e., something like this: data Triple a b c = Triple !a !b !c deriving Show countChars :: String - [Int] countChars = scanl (\n _ - n+1) 0 countChar :: Char - String - [Int] countChar c = scanl (\n c' - if c == c' then n+1 else n) 0 countLines = countChar '\n' countWords = countChar ' ' last' [x] = x last' (x:xs) = x `seq` last' xs zip3' (x:xs) (y:ys) (z:zs) = Triple x y z : zip3' xs ys zs zip3' _ _ _ = [] wc :: String - Triple Int Int Int wc xs = last' $ zip3' (countChars xs) (countWords xs) (countLines xs) main = print . wc = getContents (or use Data.Strict.Tuple -- but that only has pairs and no zip...) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] eager/strict eval katas
Hi Thomas, On Dec 12, 2007 5:31 PM, Thomas Hartman [EMAIL PROTECTED] wrote: (solution involves building an accum list of (average,listLength) tuples. again you can't do a naive fold due to stack overflow, but in this case even strict foldl' from data.list isn't strict enough, I had to define my own custom fold to be strict on the tuples.) Might it be worthwhile considering the use of a custom strict pair type instead of rewriting the strict fold functions? I.e., define data Pair a b = Pair !a !b and then use ordinary foldl' and foldr' on that. Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] eager/strict eval katas
On Dec 12, 2007 9:58 PM, Don Stewart [EMAIL PROTECTED] wrote: And no need to even use custom ones, just use the library strict pairs, http://hackage.haskell.org/packages/archive/strict/0.2/doc/html/Data-Strict-Tuple.html Oh, good! :) 'nother Haskell lesson learned. Thanks, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Software Tools in Haskell
Another version of detab: main = interact $ perLine $ concat . snd. mapAccumL f 0 where f tab '\t' = (0, replicate (4-tab) ' ') f tab char = ((tab+1) `mod` 4, [char]) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Software Tools in Haskell
On Dec 13, 2007 2:20 AM, Benja Fallenstein [EMAIL PROTECTED] wrote:
Another version of detab:
main = interact $ perLine $ concat . snd. mapAccumL f 0 where
f tab '\t' = (0, replicate (4-tab) ' ')
f tab char = ((tab+1) `mod` 4, [char])
Although on reflection, I think I might like the following compromise
with Tillmann's version best:
main = interact $ perLine $ detab 0 where
detab tab ('\t':cs) = replicate (4-tab) ' ' ++ detab 0 cs
detab tab (char:cs) = char : detab ((tab+1) `mod` 4) cs
detab tab =
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Software Tools in Haskell
On Dec 13, 2007 2:28 AM, Benja Fallenstein [EMAIL PROTECTED] wrote:
Although on reflection, I think I might like the following compromise
with Tillmann's version best:
main = interact $ perLine $ detab 0 where
detab tab ('\t':cs) = replicate (4-tab) ' ' ++ detab 0 cs
detab tab (char:cs) = char : detab ((tab+1) `mod` 4) cs
detab tab =
On more reflection, I wonder whether it would be worthwhile to have a
library function for folds that work from both left *and* right:
foldlr :: (a - b - c - (a,c)) - a - c - [b] - (a,c)
foldlr f l r [] = (l,r)
foldlr f l r (x:xs) = let (l',r') = f l x r''; (l'',r'') = foldlr f l' r xs
in (l'',r')
main = interact $ perLine $ snd . foldlr detab 0 where
detab tab '\t' cs = (0, replicate (4-tab) ' ' ++ cs)
detab tab char cs = ((tab+1) `mod` 4, char : cs)
It's a fun function, anyway :-)
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: [Haskell] IVars
Hi Conal, On Dec 9, 2007 6:09 PM, Conal Elliott [EMAIL PROTECTED] wrote: readIVar' :: IVar a - a readIVar' = unsafePerformIO . readIVar so, we do not need readIVar'. it could be a nice addition to the libraries, maybe as unsafeReadIVar or unsafeReadMVar. The same argument applies any to pure function, doesn't it? For instance, a non-IO version of succ is unnecessary. My question is why make readIVar a blocking IO action rather than a blocking pure value, considering that it always returns the same value? From the rest of Marc's post, I understood the point to be that readIVar lets you do something that readIVar' does not let you do: block until the IVar is written, then continue *without* first evaluating the thunk in the IVar to WHNF. I haven't used IVars myself, so this isn't informed by hands-on experience, but it does sound sensible to me that block until the IVar has been written and evaluate the thunk to WHNF should be separable. All the best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Re: type class question
On Dec 7, 2007 6:57 PM, Peter Padawitz [EMAIL PROTECTED] wrote: Jules Bean wrote: Peter Padawitz wrote: Cause I don't see why the instantiation conflicts pointed out by others would vanish then. They would. If it's really true that there is only one possible choice of b,c,d for any particular a, then there are no conflicts, so you'd get no errors. How can ghci know this even if no instance has been defined? Because there is only one possible choice of b,c,d for any particular a is what the fundep means :-) If I omit the comp functions (see below), everything works. If I add them, all proposed solutions fail with error messages of the form Could not deduce (Java block1 ) from the context (Java block ) arising from use of `prod' at ... (see also Ben Franksen's comment from yesterday). If you add the cyclic functional dependencies to your code, it compiles just fine: type Block = [Command] data Command = Skip | Assign String IntE | Cond BoolE Block Block | Loop BoolE Block data IntE= IntE Int | Var String | Sub IntE IntE | Sum [IntE] | Prod [IntE] data BoolE = BoolE Bool | Greater IntE IntE | Not BoolE class Java block command intE boolE | block - command, command - intE, intE - boolE, boolE - block where block_ :: [command] - block skip :: command assign :: String - intE - command cond :: boolE - block - block - command loop :: boolE - block - command intE_ :: Int - intE var :: String - intE sub :: intE - intE - intE sum_ :: [intE] - intE prod :: [intE] - intE boolE_ :: Bool - boolE greater :: intE - intE - boolE not_ :: boolE - boolE compBlock :: Block - block compBlock = block_ . map compCommand compCommand :: Command - command compCommand Skip = skip compCommand (Assign x e) = assign x (compIntE e) compCommand (Cond be cs cs') = cond (compBoolE be) (compBlock cs) (compBlock cs') compCommand (Loop be cs)= loop (compBoolE be) (compBlock cs) compIntE :: IntE - intE compIntE (IntE i) = intE_ i compIntE (Var x)= var x compIntE (Sub e e') = sub (compIntE e) (compIntE e') compIntE (Sum es) = sum_ (map compIntE es) compIntE (Prod es) = prod (map compIntE es) compBoolE :: BoolE - boolE compBoolE (BoolE b) = boolE_ b compBoolE (Greater e e') = greater (compIntE e) (compIntE e') compBoolE (Not be) = not_ (compBoolE be) Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Why is this strict in its arguments?
Hi Paolo, On Dec 5, 2007 2:09 PM, Paulo J. Matos [EMAIL PROTECTED] wrote: I'm glad that my initial post generated such an interesting discussion but I'm still not understanding why the first version of findAllPath seems to be computing the whole list even when I just request the head, while the second one doesn't. Because the function starts its work with if isNothing lfpaths isNothing rtpaths then Nothing else ... which forces the evaluation of 'lfpaths' and 'rtpaths' to see whether they are Just or Nothing, which recursively forces the evaluation of findAllPath for the whole tree. Hope this helps, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Why is this strict in its arguments?
On Dec 5, 2007 5:40 PM, Paulo J. Matos [EMAIL PROTECTED] wrote: Oh, but lfpaths is not nothing so that means that isNothing rtpaths shouldn't be evaluated, right? You're right, and I was stupid not to think about that case. Since Luke already gave an in-depth analysis I'll be quiet now :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Properties of monads
Hi Radosław, You should be able to write this with MaybeT as follows: getStrip :: IO ( Maybe String ) getStrip = runMaybeT $ do pageContent - liftIO $ downloadFile mainPageAddress let x = patternForStrip pageContent print x z - x liftIO $ downloadFile $ mainPageAddress ++ z If you can do without the 'print', you should be able to write it as: getStrip :: IO ( Maybe String ) getStrip = runMaybeT $ do pageContent - liftIO $ downloadFile mainPageAddress z - patternForStrip pageContent liftIO $ downloadFile $ mainPageAddress ++ z You can find MaybeT here: http://www.haskell.org/haskellwiki/New_monads/MaybeT Best, - Benja On 11/18/07, Radosław Grzanka [EMAIL PROTECTED] wrote: Hello, I am writing some toys programs to learn and try to apply Monads properties (without success, I must say). Although I spent half a day on this code: http://hpaste.org/3957 I couldn't simplify (shorten) getStrip function. After reading Doing it with class ( http://www.haskell.org/all_about_monads/html/class.html ) I had an impression that I could collapse cases using some Monads properties. But maybe I misunderstood something. Can anyone look at it and give me a pointers?? (I don't mind if the code becomes unreadable a bit.) Thank you, Radek. ___ 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] Properties of monads
On 11/18/07, Benja Fallenstein [EMAIL PROTECTED] wrote: Hi Radosław, You should be able to write this with MaybeT as follows: Correction, sorry. The code in my original mail doesn't take care of converting the 'Maybe's returned by the functions you're calling into 'MaybeT's. The following should work, but is a little annoying: getStrip :: IO ( Maybe String ) getStrip = runMaybeT $ do pageContent - MaybeT $ downloadFile mainPageAddress z - MaybeT $ return $ patternForStrip pageContent MaybeT $ downloadFile $ mainPageAddress ++ z Something like the following might feel cleaner, though: maybeT :: Maybe a - MaybeT m a maybeT = MaybeT . return downloadFile :: String - MaybeT IO String downloadFile s = maybeT (parseURI s) = liftIO . httpGet getStrip :: MaybeT IO String getStrip = do pageContent - downloadFile mainPageAddress z - maybeT $ patternForStrip pageContent downloadFile $ mainPageAddress ++ z Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Producing MinimumValue
2007/7/19, Jason Dagit [EMAIL PROTECTED]: I prefer, allEqual [] = True allEqual xs = foldl1 (==) xs But, unfortunately, it's not a one liner like yours (unless you allow allEqual [] = undefined). Oh and silly me, that only works for [Bool]. My natural instinct is, allEqual [] = True allEqual (x:xs) = all (== x) xs with the same caveat about allEqual [] as in your case. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Re[2]: [Haskell-cafe] Producing MinimumValue
2007/7/20, Bulat Ziganshin [EMAIL PROTECTED]: allEqual [] = True allEqual (x:xs) = all (== x) xs with the same caveat about allEqual [] as in your case. allEqual xs = all (== head xs) xs Rght. Not evaluated in the edge case, because xs is empty. Didn't think of that, nice :-) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Newbie question about tuples
Hi Peter, 2007/7/12, peterv [EMAIL PROTECTED]: Q1) Is it possible to treat a tuple of N elements in a generic way? So instead of writing functions like lift1 e1, lift2 (e1,e2), lift3 (e1,e2,e3) just one function liftN that works on tuples of any length? Q2) (Maybe related to Q1) Can I convert a tuple of length N to a heterogeneous list (using forall aka existentially quantified types) and vice versa? Not in the standard libraries. I've been using a home-grown module for this sort of thing: http://antti-juhani.kaijanaho.fi/darcs/fenserve/fendata/TupleUtils.hs Q3) Suppose I want to declare an instance of Num on all tuple types having (Num instances) as elements; is this possible? I tried instance Num a = Num (a,a) where . but this fails This is illegal in Haskell 98, but should work in GHC if you use -fglasgow-exts. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Functional dependencies *not* part of the next Haskell standard?
2007/7/12, peterv [EMAIL PROTECTED]: Amazing, so simple it is, Yoda would say ;) I did not realize one could perform partial application on types when declaring instances (I mean not specifying the type of Vector2 in instance Vector Vector2). You ought to meditate on the type class 'Monad,' then, which was the motivating example for allowing these kinds of classes in standard Haskell ;-) All the best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Trying to make a Typeable instance
Hi Adrian, 2007/7/8, Adrian Hey [EMAIL PROTECTED]: So it seems ghc doesn't like kinds (* - *) either :-( Actually, AFAICT the problem seems to be with Data.Typeable itself rather than ghc. There is no proper TypeRep for (ListGT map k a) because map is not a type. Have you tried using (Typeable1 map) as the constraint? - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] sha1 implementation thats only 12 times slower then C
Hi, 2007/7/1, Bulat Ziganshin [EMAIL PROTECTED]: aa - unsafeRead a5 0 return $! aa bb - unsafeRead a5 1 return $! bb If this is a useful pattern, would it make sense to have a function to encapsulate it? mseq :: Monad m = m a - m a mseq m = m = (return $!) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Read-only functions in State Monad
Hi Ken, 2007/7/1, Ken Takusagawa [EMAIL PROTECTED]: I'd like to have a state monad with the feature that I can somehow annotate using the type system that some functions are only going to read the state and not modify it. I would suggest declaring a MonadReader instance for State, and writing your read-only functions as f :: MonadReader s m = Param - m Result Would that solve your problem? Best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Constructing a datatype given just its constructor as a string?
Hi Hugh, 2007/6/25, Donald Bruce Stewart [EMAIL PROTECTED]: hughperkins: Just noticed that all my responses have been going only to Neil, not to the group. Anyway, the jist of our conversation was that it's not possible to create arbitrary datatypes/constructors from strings in Haskell. Can anyone deny/confirm? Anyway there was a thread on this last week. That thread starting here: http://www.haskell.org/pipermail/haskell-cafe/2007-June/026777.html The takeaway was Stefan O'Rear's suggestion that if you don't want to create a table of datatypes manually, you can use hs-plugins -- something along the lines of data Foo = forall a. MyClass a = Foo a read' typeName s = eval (Foo (gread \ ++ s ++ \ :: ++ typeName ++ )) :: Foo - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Practical Haskell question.
Hi Peter, 2007/6/25, peterv [EMAIL PROTECTED]: I'm baffled. So using the Arrow abstraction (which I don't know yet) would solve this problem? How can (perfectActionB x) be checked with without ever executing performActionA which evaluates to x? This can only be done when x is a constant expression no? Arrows separate the action -- 'performActionB' -- from the argument -- 'x', so you can look at the action before you have to compute the argument to it. Of course, this means that you can no longer compute the action from the argument -- that is, 'if x then performActionB else performActionC' is something you can't directly do; you have to use a choice primitive instead, which explicitly says use one of these two arrows depending on what value this argument is, which then lets the library check these two arrows before actually applying them to an argument. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] SYB with class, simplified
Hi all,
The scrap your boilerplate with class sytstem [1] has two big
advantages over the plain SYB system from Data.Generics, IMHO: One, it
lets you declare an 'open' generic function as a type class, to which
new cases can be added by adding new instances (emphasized in the
paper); and two, it lets you write recursive functions that require
other type class constraints in addition to Data (not emphasized in
the paper, but something I've frequently found myself wanting with
Data.Generics).
[1] http://homepages.cwi.nl/~ralf/syb3/
However, when trying to convert the codebase I'm working on to
SYB-with-class, I've found that the type proxies and explicit
dictionaries used to simulate type class abstraction over type classes
are... annoying. Today, I've hit on an alternative approach to
implementing SYB-with-class (YAGS, yet another generics scheme...),
with less boilerplate per generic function. The approach may or may
not be new (I haven't studied *all* of the generics proposals out
there yet); in any case, it shares the use of type-level functions
with Smash Your Boilerplate, and it uses the same underlying gfoldl
operator as SYB, but implements it in a quite different way.
I believe that the equivalent of everywhere, mkT and friends can be
implemented as type-level functions in this framework, but I haven't
actually tried it yet.
This mail is a literate script demonstrating the approach. I'm hoping
to get some feedback on the idea. :)
On to the code:
{-# OPTIONS_GHC -fglasgow-exts -fallow-overlapping-instances
-fallow-undecidable-instances #-}
Yup, we need it all...
I'll start with three example generic functions.
* 'size' calculates the number of constructors in a term, except
for lists, for which it returns one plus sum of the element sizes.
* 'inc' increases all Ints in a term by one.
* 'prints' prints out each subterm of a term on its own line,
except for strings, for which it prints the string,
but not its subterms.
Thus, the following code:
test = (Hello, 7::Int, [2,3::Int])
main = do print (size test); print (inc test)
putStrLn ; prints test; return ()
prints this:
--
11
(Hello,8,[3,4])
(Hello,7,[2,3])
Hello
7
[2,3]
2
[3]
3
[]
--
Here is the 'size' function:
class Size a where size :: a - Int
data SizeF = SizeF
instance Size a = Apply SizeF a Int where apply _ = size
instance Size a = Size [a] where size xs = 1 + sum (map size xs)
instance Apply (GMapQ SizeF) a [Int] = Size a where
size x = 1 + sum (gmapQ SizeF x)
The constraint (Apply f x r) means that 'f' is a type-level function
that, when applied to 'x,' returns 'r':
class Apply f x r | f x - r where apply :: f - x - r
Here is the 'inc' function:
class Inc a where inc :: a - a
data IncF = IncF
instance Inc a = Apply IncF a a where apply _ = inc
instance Inc Int where inc = (+1)
instance Apply (GMapT IncF) a a = Inc a where inc = gmapT IncF
And here is the 'prints' function; for illustration, the
implementation is in a slightly different style, which does without
the declaration of a new type class:
data PrintsF = PrintsF; prints x = apply PrintsF x
instance Apply PrintsF String (IO String) where
apply _ x = print x return x
instance (Show a, Apply (GMapM PrintsF) a (IO a)) =
Apply PrintsF a (IO a) where
apply f x = print x gmapM f x
Note the 'Show' constraint: 'prints' can only be applied to values all
of whose subterms implement 'Show.' This is the kind of constraint you
can't have with the standard, not-with-class SYB code.
So much for the demo code; now, onwards to the actual library. The
core consists of the following three type classes:
class Constr x f where constr :: x - a - f a
class Param x p f where param :: x - f (p - a) - p - f a
class GFoldl x a f where gfoldl :: x - a - f a
Together, these classes form the equivalent of the standard SYB's
'gfoldl' method. (I'm ignoring the rest of the Data class at this
time, but I believe that it could be implemented in a similar
fashion.)
* 'Constr' and 'Param' correspond to the first and second argument
of the standard SYB's gfoldl.
* The parameter 'x' specifies the type of fold to perform
(GMapQ, GMapT and GMapM in the present module).
* We give an instance 'Constr' and 'Param' for each type of fold.
We give an instance of 'GFoldl' for each type we want to fold over.
Here are the instances of GFoldl:
instance Constr x f = GFoldl x () f where gfoldl = constr
instance Constr x f = GFoldl x Char f where gfoldl = constr
instance Constr x f = GFoldl x Int f where gfoldl = constr
instance (Constr x f, Param x a f, Param x [a] f) = GFoldl x [a] f where
gfoldl x [] = constr x []
gfoldl x (y:ys) = constr x (:) `p` y `p` ys where
p a b = param x a b
instance (Constr x f, Param x a f, Param x b f, Param x c f) =
GFoldl x (a,b,c) f where
Re: [Haskell-cafe] Practical Haskell question.
2007/6/25, Michael T. Richter [EMAIL PROTECTED]: OK, just to prevent this getting side-tracked: I'm absolutely uninterested in the results of performActionA before determining if performActionB is permitted/possible/whatever. Think more in terms of security permissions or resource availability/claiming than in terms of chaining results. I want to know before I begin to collect the results of performAction* that I will actually stand a chance at getting results at all. Uh, the posts you quote were precisely about how to do that. No side-tracking going on. :-) All the best, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell] Class type constraining?
2007/6/22, Hugo Pacheco [EMAIL PROTECTED]: class Functor f = C f a b | f a - b where ftest :: f a - b I want to write some function test :: (C f a b) = (a - b) test = ftest . undefined I'm not sure whether this is what you want, but the obvious way to make this type-check would seem to be to add a functional dependency and a type signature for 'undefined,' like this: class Functor f = C f a b | f a - b, a b - f where ftest :: f a - b test :: (C f a b) = (a - b) test = ftest . (undefined :: a - f a) - Benja ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell-cafe] Recursive instance dictionaries in GHC
Hi,
I can't figure out why the following program compiles with this
instance declaration
instance Size (Maybe [a]) = Size [a] where size x = size (foo x)
but has GHC loop forever with this one:
instance (Foo a b, Size b) = Size a where size x = size (foo x)
Anybody here know?
Thanks,
- Benja
{-# OPTIONS_GHC -fglasgow-exts -fallow-overlapping-instances
-fallow-undecidable-instances #-}
class Foo a b | a - b where foo :: a - b
instance Foo [a] (Maybe [a]) where foo (x:xs) = Just xs; foo [] = Nothing
class Size a where size :: a - Int
instance Size a = Size (Maybe a) where
size (Just x) = 1 + size x; size Nothing = 0
--instance (Foo a b, Size b) = Size a where size x = size (foo x)
-- OR
--instance Size (Maybe [a]) = Size [a] where size x = size (foo x)
main = print $ size foo
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Memo + IORef
Hi Tony, 2007/6/16, Tony Morris [EMAIL PROTECTED]: I was told on #haskell (IRC) the other day that it is possible to write a general memoisation table using IORef and unsafePerformIO. I can't think of how this can be achieved without writing to a file, since a function cannot hold state between invocations. What am I missing? You create a single IORef for the function (via unsafePerformIO), for example like this: memoTable :: Map Int Int memoTable = unsafePerformIO $ newIORef Map.empty memoizedFactorial n = unsafePerformIO $ do tbl - readIORef memoTable if (n `Map.member` tbl) then return (tbl Map.! n) else do let r = if n == 0 then 1 else n * memoizedFactorial (n-1) writeIORef memoTable $ Map.insert n r tbl return r - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Reading open data types
Hi all,
We've had a discussion on #haskell about how we can make a function
that reads in serialized values of an open data type, such as
class (Show a, Read a) = MyClass a where
typeTag :: a - String
... operations on the open data type...
data Obj = forall a. MyClass a = Obj { unObj :: a }
We would like to write a function like,
oread :: String - Obj
The problem here is that unlike with 'read,' the calling context of
'oread' does not fix the implementation of Read that we want to use.
The best we've been able to come up with was to build a table that
maps type names to types:
type TypeTable = Map String Obj
oread :: TypeTable - String - Obj
oread types s = Obj $ read repr `asTypeOf` unObj (types ! tag) where
tag = takeWhile (/= ' ') s
repr = drop 1 $ dropWhile (/= ' ') s
instance Show Obj where
show (Obj x) = typeTag x ++ ++ show x
As far as we can see, we'll have to create this table manually,
without support from the compiler. My suggestion would be to put the
code constructing the table for each module at the top of that module,
to keep it together with the exports and imports, like this:
module Foo.Foo (export1, export2, fooFooTypes) where
import Foo.Bar
import Foo.Baz
import Data.Map
fooFooTypes = fooBarTypes `union` fooBazTypes `union` fromList
[ (Foo.Foo.Ty1, Obj (undefined :: Ty1))
, (Foo.Foo.Ty2, Obj (undefined :: Ty2)) ]
However, this is still kind of boring. Is there a better way? If not,
would it be a good idea to have compiler support for building this
kind of type table?
Thanks,
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reading open data types
Hi Isaac, 2007/6/13, Isaac Dupree [EMAIL PROTECTED]: Since Show instances can overlap (e.g. (show (1::Int)) == (show (1::Integer))), we need to tag with the type. Indeed. But that's the easy part :-) Reminds me of Typeable. Since GHC lets us derive Typeable with a guarantee of different types being distinct (at least for a single compile-and-run session...), maybe that can be leveraged somehow? We can perhaps use it to go from the type to the type tag, but as far as I understand we can not, unfortunately, use it to go from the type tag to the type. (We *may* be able to use the TypeRep as the key of the map I proposed in my earlier mail, but we can't use it to replace the map, afaiu.) The problem is that, in the type system, a TypeRep is not actually associated with the type that it represents, nor is there (afaik) an internal table that associates TypeReps with the types they represent. In Data.Generics, there are some functions that let you take a DataTypeRep and use it to create a value of the corresponding type. However, the code doesn't use the DataTypeRep to get the type. The relevant function looks like this: fromConstr :: Data a = Constr - a Like 'read' gets the 'Read' instance, this gets the 'Data' instance from its return type (you have to call it in a context that constrains the return type). So, you can *not* use it to write a function like this: data D = forall a. Data a = D a fromConstrD :: Constr - D because, in the type system, you wouldn't be able to use the Constr to get the Data instance corresponding to the Constr's TypeRep. Hope that makes sense ... I'm not explaining it too well :-/ Thanks, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reading open data types
Hi Bulat, 2007/6/13, Bulat Ziganshin [EMAIL PROTECTED]: We've had a discussion on #haskell about how we can make a function that reads in serialized values of an open data type, such as look at Data.Generics.Text which may be implements exactly what you need Unfortunately not. Data.Generics.Text provides gread :: Data a = ReadS a That is, you have to constrain its return type to the particular type you want to read. What I'm looking for is a way to read any type implementing a certain class (deciding the type to use based on a type tag) and returning the result in an existential wrapper. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reading open data types
2007/6/14, Stefan O'Rear [EMAIL PROTECTED]: On Wed, Jun 13, 2007 at 05:12:25PM +0300, Benja Fallenstein wrote: However, this is still kind of boring. Is there a better way? If not, would it be a good idea to have compiler support for building this kind of type table? The compiler does build exactly such a table - it's called a symbol table. If you aren't afraid of massive overkill, you can use hs-plugins to write String - exists a. Read a = a . Now *there* is an idea. :-) Hah. Massive overkill, indeed, but you'd call 'eval' only once for every type tag, of course, and cache the result, so the overhead would be O(1) per run of the application. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
2007/5/12, Derek Elkins [EMAIL PROTECTED]:
In Haskell codata and data coincide, but if you want consistency, that cannot be
the case.
For fun and to see what you have to avoid, here's the proof of Curry's
paradox, using weird infinite data types. We'll construct an
expression that inhabits any type a. (Of course, you could just write
(let x=x in x). If you want consistency, you have to outlaw that one,
too. :-))
I'll follow the proof on Wikipedia: http://en.wikipedia.org/wiki/Curry's_paradox
data Curry a = Curry { unCurry :: Curry a - a }
id :: Curry a - Curry a
f :: Curry a - (Curry a - a)
f = unCurry . id
g :: Curry a - a
g x = f x x
c :: Curry a
c = Curry g
paradox :: a
paradox = g c
Modulo the constructor and destructor invocation, this is just the
familiar non-terminating ((\x - x x) (\x - x x)), of course.
- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
2007/5/13, Benja Fallenstein [EMAIL PROTECTED]: Modulo the constructor and destructor invocation, this is just the familiar non-terminating ((\x - x x) (\x - x x)), of course. The same technique also gives us data Y a = Y (Y a - a) y :: (a - a) - a y f = (\(Y x) - f $ x $ Y x) $ Y $ (\(Y x) - f $ x $ Y x) or y :: (a - a) - a y f = g (Y g) where g (Y x) = f $ x $ Y x as well as these formulations, which make GHC loop forever on my system: y :: (a - a) - a y f = (\(Y x) - f (x (Y x))) (Y (\(Y x) - f (x (Y x y :: (a - a) - a y f = g (Y g) where g (Y x) = f (x (Y x)) (Aaah, the power of the almighty dollar. Even type inference isn't safe from it.) - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
Adding some thoughts to what David said (although I don't understand the issues deeply enough to be sure that these ideas don't lead to ugly things like paradoxes)-- 2007/5/10, Gaal Yahas [EMAIL PROTECTED]: Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead: data Stream a = SHead a (Stream a) sMap :: (a - b) - Stream a - Stream b What is the object Stream a in logic? It's not that much more interesting than list. The 'data' declaration can be read as, To prove the proposition (Stream a), you must prove the proposition 'a' and the proposition 'Stream a.' In ordinary logic this would mean that you couldn't prove (Stream a), of course, but that just corresponds to strict languages in which you couldn't construct an object of type Stream a (because it would have to be infinite). To make sense of this, we need to assume a logic in which we can have similar 'infinite proofs.' (This is the part where I'm not sure it's really possible to do. I haven't read the Pierce chapter David refers to.) With that reading, (Stream a) is basically the same proposition as (a) -- as evidenced by f x = SHead x (f x) -- f :: a - Stream a g (SHead x) = x -- g :: Stream a - a We can find more interesting propositions, though. Here's an example (perhaps not useful, but I find it interesting :-)): data Foo a b = A a | Fn (Foo a b - b) We can prove this proposition if we can prove one of these propositions: a a - b (a - b) - b ((a - b) - b) - b ... Each of these is weaker than the previous one; if x is a proof of proposition n, then (\f - f x) is a proof of proposition n+1. The fourth one is a tautology in classical logic, but not in intuitionistic logic. - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Soft references
Hi all, Is there a way to achieve the effect of soft references in GHC? Or if not, is there any hope that they will be implemented in the future? (Soft references are like weak references, except that they are only reclaimed by the garbage collector if memory is short.) I'm building a memoization table of visualizations of a data set, but I can't store *all* visualizations of that set in memory at the same time. My current solution is to use a least-recently-used cache, but this is unsatisfying because I have to specify the maximum number of objects in the cache; if I make that too large, I run out of memory, so I have to make it so small that I can't possibly run out, meaning that I have to make it a lot smaller than it *could* be. With soft references, the program could memoize the optimal number of items, with the user being able to influence the behavior through the 'maximum heap size' RTS option. Any ideas? Thanks, - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why the Prelude must die
Hi, (new here) 2007/3/25, Jacques Carette [EMAIL PROTECTED]: Some classes would become even more important: monoid, groupoid, semi-group, loop (semi-group with identity), etc. But all of those are, to the average programmer (and many a mathematician), just as scary as Monad. Of course, when you get that general, you start having the problem that many types can be made into these structures in more than one way. Even the current Monoid class has that problem, even though it has some ties to a particular application (the Writer monad and stuff similar to it -- as reflected in the 'mappend' and 'mconcat' names). You can have newtype wrappers, but that's at least somewhat annoying :-) I'd like to see these classes in the standard library, but I'm not sure at this point whether they are useful enough to have in the prelude, as long as they're not at least losely to a specific application (Field - numbers; Monoid - collecting results; Monad - imperative computations). - Benja ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
