Re: [Haskell-cafe] The Riddle of the Buddhist Monk
Sameer, I think that my Maude to Haskell translation was a bit too literal and naive. But your reply helped me gain further insight to both languages, which is essentially my current research task. Thanks, Pat On 12/23/11, Sameer Sundresh sam...@sundresh.org wrote:On Wed, Dec 21, 2011 at 10:12 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote: On 21/12/11, Richard O'Keefe o...@cs.otago.ac.nz o...@cs.otago.ac.nz wrote: So what exactly is the program supposed to do? I am trying to see whether Haskell modules can be used for blending[1]. The original MAUDE [2,3] program just sets up an arbitrary meeting point, which is assumed to be time-2 and location-2. Then in MONK_MEETS_HIMSELF the up and down versions of these are made match. To do this I wish to declare the function location in MONK_ON_MOVE. Then I require different equations for that same location function in MONK_ON_MOVE_DOWN and MONK_ON_MOVE_UP both of which import MONK_ON_MOVE. Finally, I wish to import MONK_ON_MOVE_DOWN and MONK_ON_MOVE_UP into MONK_MEETS_HIMSELF and use the combined set of equations to check locations.You can't do that in Haskell. All equations defining a function must occur contiguously in the same Haskell module. You've actually defined two separate functions, MONK_ON_MOVE_DOWN.location and MONK_ON_MOVE_UP.location. If you want to define a single function that blends their behaviors, you need to do that explicitly. For example, you might define these as partial functions, returning type Maybe LocationOnPath, and then try each implementation (in your case, 2 tries), until one of them returns a non-Nothing result. You could use type classes with overlapping instances to try to merge two different definitions of location, but it wouldn't work the way you want. The compiler would statically choose one implementation of location that would be used for a given type, rather than trying equations from both (as you desire, and as would happen in Maude). So far I cannot figure out how the location function and the constructors can be shared in this way using Haskell modules. I have tried various combination import/export options, type classes, and newtype. I have also tried to use Strings instead of constructors. I had trouble using Haskell equations with pure constructors. Due to my ignorance of Haskell semantics I am not sure what Constructor1 = Constructor2 means. But in the original Maude there are constructor only equations such as Timed2 = Timeu2 which in Maude means that the constructor Timed2 could be replaced with Timeu2. I wrote Haskell functions to try to achieve a similar effect e.g. timed2 :: TimeOfDay - TimeOfDay timed2 Timed2 = Timeu2I'm not sure why top-level equations like Timed2 = Timeu2 (or even Just () = Nothing) aren't an error in GHC (or even a -Wall warning), but, as you've observed, this won't cause Timed2 to rewrite to Timeu2. Constructors in Haskell truly are constructors, they don't rewrite to something else (similar to the intention of the [ctor] annotation in Maude). To make it work, you'd have to manually separate out which of your terms are truly constructors and which ones are functions. Then write equations defining the functions. Be sure that all equations for a given function are in a given place. You could of course implement a rewrite system on top of Haskell, and the syntax probably wouldn't be that bad (someone's probably already done it). But you can't directly write Maude-style rewrite systems in Haskell; the two languages just work differently. [1] http://cseweb.ucsd.edu/~goguen/pps/taspm.pdf [2] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000456.html [3] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000462.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On Tue, Dec 20, 2011 at 3:10 PM, Chris Wong
chrisyco+haskell-c...@gmail.com wrote:
On Wed, Dec 21, 2011 at 10:53 AM, Matthew Farkas-Dyck
strake...@gmail.com wrote:
With GHC 7.0.3:
$ cat test.hs
class ℝ a where {
test :: a;
};
(∈) :: Eq a = a - [a] - Bool;
x ∈ (y:ys) = x == y || x ∈ ys;
main = putStrLn Two of three ain't bad (^_~);
$ runhaskell test.hs
Two of three ain't bad (^_~)
$
Why not expand it even further?
My experience with Agda makes me think that extending it further can
make it painful to program in. Initially I thought that using unicode
symbols would just make input a bit slower and that editor support
could address that. You know, like writing about math using latex.
My actual experience with Agda was different than that.
I was using Emacs and I found that I needed to make my font size very
large to see all the detail of the unicode symbols clearly enough to
distinguish between them fully. The alternative was using the support
in emacs for displaying the codepoint, as a number, for any glyph I
wanted to distinguish. Perhaps it's still just an issue of editor
support but it left a sour taste in my mouth.
Jason
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 23 Dec 2011, at 02:11, Conor McBride wrote: So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)? The plan is to make a clearer distinction between being and doing by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [list of effects]value type is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. Oh, so it's not an arbitrary monad, but a single one. That's a bit disappointing. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 23 Dec 2011, at 02:11, Conor McBride wrote: So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)? The plan is to make a clearer distinction between being and doing by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [list of effects]value type is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. Oh, so it's not an arbitrary monad, but a single one. That's a bit disappointing. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 23 Dec 2011, at 16:16, MigMit wrote: On 23 Dec 2011, at 02:11, Conor McBride wrote: So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)? The plan is to make a clearer distinction between being and doing by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [list of effects]value type is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. Oh, so it's not an arbitrary monad, but a single one. That's a bit disappointing. The list of effects is arbitrary, and localizable, by means of defining handlers. So it's not a single monad. It's probably still disappointing. Cheers Conor ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
I'd like to make special syntax for folds, so that fold is built in the type definition. Maybe it can be some special braces or just fold(..). So we can write the same function in place of foldr, maybe, either and so on and don't have to define them by hand. Inside special fold-braces one can write functions (separated with | as inside of type declaration) that have apropriate types. Constructors define the order of functions inside fold-braces. Handful of examples: data List a = Nil | Cons a (List a) length :: List a - List a length = fold( 0 | const (+1) ) (++) :: List a - List a - List a a ++ b = fold( b | Cons ) a head :: List a - a head = fold( undefined | const ) data Maybe a = Nothing | Just a fromJust :: Maybe a - a fromJust = fold (undefined | id) data Nat = Zero | Succ Nat add :: Nat - Nat - Nat add a = fold (a | Succ) mul :: Nat - Nat - Nat mul a = fold (Zero | add a) Maybe something similiar for unfolds but I have no syntax here. -- I'd like to invent some type-system that can allow me to say that (.), (), (=) are the same things just as id and pure I'd like to have in place of Monad-class special case of Category class We can express return and (=) with id and (.) in Monad's typing. return = id ma = mf = (mf . const ma) () where id and (.) are class Kleisli m where id :: a - m a (.) :: (b - m c) - (a - m b) - (a - m c) I'd like to parametrise it over m so Kleisli can become a special case of Category. And we ?can? define ($) in terms of id, (.), const and (), ($) :: Category cat = cat a b - ?dom cat a?- ?cod cat b? f $ a = (f . const a) () so (=) becomes just ($) Anton ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Composing Enumeratees in enumerator
I've been looking for a way to compose enumeratees in the enumerator package, but I've come up with nothing so far. I want this function (=$=) :: Monad m = Enumeratee a0 a1 m b - Enumeratee a1 a2 m b - Enumeratee a0 a2 m b I'm building a modular library on top of enumerator that facilitates reading time series data from a DB, applying any number of transformations to it, and then writing it back / doing something else with it. I'd like to be able to write simple transformations (enumeratees) and compose them without binding them to either a db reader (enumerator) or db writer (iteratee). I've been looking at the iterIO package as a possible alternative, because it seems to allow easy composition of Inums (enumeratees). I'm a little skittish of it because it seems unpopular next to enumerator. Thoughts on these issues? Cheers, Mike S Craig ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?
On 2011-12-23 13:46, Conor McBride wrote: The plan is to make a clearer distinction between being and doing by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation [list of effects]value type is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type. The list of effects is arbitrary, and localizable, by means of defining handlers. So it's not a single monad. It's probably still disappointing. On the contrary! Haskell doesn't draw a clear line in types between the effect part and the value part, or support easy fluidity of shifting roles between the two. Rather we have two modes: (1) the implicit partiality mode, where the value part is the whole of the type and the notation is applicative; (2) the explicit side-effect mode, where the type is an effect operator applied to the value type and the notation is imperative. I was drawn to call-by-push-value a few years ago while attempting to create a language which would support both call-by-value and call-by-name. I haven't had the skill to express what I have felt to be the shortcoming of Haskell, but I believe you've put your finger right on it. it's an attempt to re-rationalise techniques that emerged from Haskell programming. Exactly. Haskell has grown a wealth of features/libraries/techniques for combining monads, yet the fundamental monad, evaluation, has a separate place in the language. -- Scott Turner ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] On stream processing, and a new release of timeplot coming
Hi Cafe,
In the last couple of days I completed my quest of making my graphing
utility timeplot ( http://jkff.info/software/timeplotters ) not load the
whole input dataset into memory and consequently be able to deal with
datasets of any size, provided however that the amount of data to *draw* is
not so large. On the go it also got a huge speedup - previously visualizing
a cluster activity dataset with a million events took around 15 minutes and
a gig of memory, now it takes 20 seconds and 6 Mb max residence.
(I haven't yet uploaded to hackage as I have to give it a bit more testing)
The refactoring involved a number of interesting programming patterns that
I'd like to share with you and ask for feedback - perhaps something can be
simplified.
The source is at http://github.com/jkff/timeplot
The datatype of incremental computations is at
https://github.com/jkff/timeplot/blob/master/Tools/TimePlot/Incremental.hs .
Strictness is extremely important here - the last memory leak I eliminated
was lack of bang patterns in teeSummary.
There's an interesting function statefulSummary that shows how closures
allow you to achieve encapsulation over an unknown piece of state -
curiously enough, you can't define StreamSummary a r as StreamSummary {
init :: s, insert :: a-s-s, finalize :: s-r } (existentially qualified
over s), as then you can't define summaryByKey - you don't know what type
to store in the states map.
It is used to incrementally build all plots simultaneously, shown by the
main loop in makeChart at
https://github.com/jkff/timeplot/blob/master/Tools/TimePlot.hs
Incremental building of plots of different types is at
https://github.com/jkff/timeplot/blob/master/Tools/TimePlot/Plots.hs
There are also a few interesting functions in that file - e.g.
edges2eventsSummary, which applies a summary over a stream of long events
to a stream of rise/fall edges.
This means that you can define a stream transformer (Stream a - Stream
b) as a function (StreamSummary b - StreamSummary a), which can be much
easier. I have to think more about this idea.
--
Eugene Kirpichov
Principal Engineer, Mirantis Inc. http://www.mirantis.com/
Editor, http://fprog.ru/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] strict, lazy, non-strict, eager
Most individuals of the Haskell community have long been maintaining a cognitive dissonance; some cases turn into plain hypocrisy. You might excuse it for its ancient and prominent origin: Richard Bird and/or Philip Wadler themselves wrote like it is too lazy, make it more strict 13 years ago and surely more. But perpetuating it is not helping. I have not written this complaint until now because I have been waiting for unmistakable evidence, a smoking gun, a red hand so caught that you cannot explain away, for example you cannot explain that one sentence is from one person, the other sentence is from a different person. So, on IRC in #haskell, from the same person, speaking on the same topic in the same context, in the same interval of 3 minutes (the first two sentences in the same minute): 1. a function f is strict if f ⊥ = ⊥ 2. ⊥ represents any computation which does not terminate, i.e. an exception or an infinite loop 3. strict describes the denotational semantics People, could you please make up your mind already? It has been more than 13 years. Denotational semantics: A. There are no computational steps. There is no termination, and there is no non-termination, since there are no steps to finish, and no steps to keep going. B. ⊥ represents no information, not non-termination. There is no non-termination to represent. C. fix id = ⊥ because ⊥ is the least fixed point of id, not because fix id non-terminates. There is nothing to terminate or non-terminate. D. You say strict, more strict, less strict; non-strict, more non-strict, less non-strict. You don't say eager, and you don't say lazy. Operational semantics: A. There is no ⊥; it does not appear in any sequence of computational steps, finitely long or infinitely long. B. You say eager, more eager, less eager; lazy, more lazy, less lazy; or speculative, more speculative, less speculative; or any other adjectives for evaluation strategies. You don't say strict, and you don't say non-strict. Semantics, semantically speaking: A. Which semantics, which semantically? There are two. B. Actually there are more, but apparently two is already enough to cause all kinds of incoherent statements. If I draw your attention to algebraic semantics, will you start saying it is too lazy, need to make it more idempotent? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] strict, lazy, non-strict, eager
See that's typically the speech that scares people away from Haskell... -- The ⊥ is a lie. 2011/12/24 Albert Y. C. Lai tre...@vex.net Most individuals of the Haskell community have long been maintaining a cognitive dissonance; some cases turn into plain hypocrisy. You might excuse it for its ancient and prominent origin: Richard Bird and/or Philip Wadler themselves wrote like it is too lazy, make it more strict 13 years ago and surely more. But perpetuating it is not helping. I have not written this complaint until now because I have been waiting for unmistakable evidence, a smoking gun, a red hand so caught that you cannot explain away, for example you cannot explain that one sentence is from one person, the other sentence is from a different person. So, on IRC in #haskell, from the same person, speaking on the same topic in the same context, in the same interval of 3 minutes (the first two sentences in the same minute): 1. a function f is strict if f ⊥ = ⊥ 2. ⊥ represents any computation which does not terminate, i.e. an exception or an infinite loop 3. strict describes the denotational semantics People, could you please make up your mind already? It has been more than 13 years. Denotational semantics: A. There are no computational steps. There is no termination, and there is no non-termination, since there are no steps to finish, and no steps to keep going. B. ⊥ represents no information, not non-termination. There is no non-termination to represent. C. fix id = ⊥ because ⊥ is the least fixed point of id, not because fix id non-terminates. There is nothing to terminate or non-terminate. D. You say strict, more strict, less strict; non-strict, more non-strict, less non-strict. You don't say eager, and you don't say lazy. Operational semantics: A. There is no ⊥; it does not appear in any sequence of computational steps, finitely long or infinitely long. B. You say eager, more eager, less eager; lazy, more lazy, less lazy; or speculative, more speculative, less speculative; or any other adjectives for evaluation strategies. You don't say strict, and you don't say non-strict. Semantics, semantically speaking: A. Which semantics, which semantically? There are two. B. Actually there are more, but apparently two is already enough to cause all kinds of incoherent statements. If I draw your attention to algebraic semantics, will you start saying it is too lazy, need to make it more idempotent? __**_ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
