Re: On Eq, was Re: [Haskell-cafe] When to use fancy types [Re: NumberTheory library]
> Lennart Augustsson wrote (on Sat, 14 May 2005 at 16:01): > Why would a constructivist think that all functions are continuous? > It makes no sense. How would you define a non-continuous function (on reals, say) without (something like) definition by undecidable cases? Formal systems for constructive mathematics usually have models in which all functions |R -> |R are continuous. For a long time, constructive mathematics lacked an analogue of classical point-set topology. (Bishop et al dealt mainly with metric spaces.) Nowadays, this seems to have been (crudely speaking) "fixed". Basically, one starts with the structure of neighbourhoods (inclusion and covering), and analyses notions like point and continuous function in those terms. Some of the major contributions to the subject have been made by people working in Sweden, at least one in your own department. Peter Hancock ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Joy Combinators (Occurs check: infinite type)
> Greg Buchholz wrote (on Wed, 09 Mar 2005 at 20:08): > Can anyone recommend a nice dependently typed language to play with? > Cayenne, Epigram, other? http://www.cs.chalmers.se/~catarina/agda/ See also the sexy IDE alfa: http://www.cs.chalmers.se/~hallgren/Alfa/ Peter Hancock ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Point-free style
> Lennart Augustsson wrote (on Mon, 14 Feb 2005 at 14:55): > Any definition can be made point free if you have a > complete combinator base at your disposal, e.g., S and K. > Haskell has K (called const), but lacks S. S could be > defined as >spread f g x = f x (g x) > Given that large set of Haskell prelude functions I would > not be surprised if spread could already be defined point > free in Haskell. :) It sometimes surprises me the prelude doesn't have diag f x = f x x (aka W. It already has B, C, K and I: (.), flip, const and id.) Peter Hancock ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell programs in C
> Ben Rudiak-Gould wrote (on Tue, 25 Jan 2005 at 14:49): > Mark Carroll wrote: >> Wasn't there someone mentioning here a little while ago >> some project where they strip most of System.* from the libraries and get >> something that might be suitable for embedded applications? What was that >> called? Anyone remember? > hOp: > http://www.macs.hw.ac.uk/~sebc/hOp/ Something pretty impressive built on hOp: http://www.cse.ogi.edu/~hallgren/House/ Page fault handlers written in Haskell! Peter Hancock ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The difference between ($) and application
> Jon Cast wrote (on Tue, 14 Dec 2004 at 22:02): > No. All that is needed for ($) to work is impredicativity (or, more > precisely, for the foralls in ($)'s type to be impredicative). That is > something that could easily be implemented in a compiler. I'm not clear > on why it hasn't been, but the type system, in relation to an > arbitrary-rank predicative system, is no more of a jump that higher-rank > types were. This sounds interesting and I'd like to understand it. * The rank of a type is the nesting depth of quantifiers over types, isn't it? Nested quantifiers can be understood either predicatively (with ramified universe types) or impredicatively. * ($) is the identity function restricted to "functions-in-general" ie the type FIG = forall a, b . (a -> b) -> a -> b You are saying (?) * The type of ($) cannot be expressed predicatively. (It seems perfectly expressed by FIG. But you could say that FIG is really (forall a, b :: V_n . ...) which is not a type because it contains a parameter. But there is really no parameter, the subscripts are just a way of ensuring the formula is properly stratified. Or something to do with ($) being self applicable?? * ?? What we have in implemented type systems is arbitrary-rank predicative type quantification. (Strewth!) * It would have been easy instead to implement impredicative quantification over types. Sorry if this is hopelessly wrong. Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] closed classes
> At the moment I'm only thinking of parameter-less kind declarations but > one could easily imagine kind parameters, and soon we'll have kind > polymorphism but one step at a time. > Any thoughts? Apologies if it's widely known, but a system with "kind polymorphism" was first considered by Girard (in 1971!). It's mentioned in Appendix A of "The System F of Variable Types, Fifteen Years Later" by Girard in "Logical Foundations of Functional Programming", ed Huet, Addison-Wesley 1990, pp 87-126. There he calls it "system U". It is inconsistent, and non-normalising (as a logical system). The implications of this for type-checking "should be considered very cautiously" (to borrow Girard's words). Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Toy application advice wanted
Sound on linux tends to center around the "jack" sound architecture. This is a demon for connecting audio and midi gadgets as it were by jack-leads. From a brief look, it seems very callback oriented. It seems to be highly thought of by knowledgable audio types, and the bee's knees for low latency. It could be fun to figure out ways of writing jack-clients and plugins in Haskell. Would it be difficult, or stupid? Are callbacks to Haskell from C a problem? I suppose an interesting jackable component written in Haskell would of necessity something more midi than audio oriented. Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: .. Drowning in stateful, side-effect riddled, spaghetti code? We have the answer. fdps[]c.
What about (generic, of course) Has|http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Yet Another Monad Tutorial
> Jeff Newbern wrote (on Tue, 12 Aug 2003 at 17:20): (proposed revisions) > In the section "No Way Out": > -- > The IO monad is a familiar example of a one-way monad in Haskell. > Because you can't escape from the IO monad, it is impossible to write a > function that does a computation in the IO monad but returns a > non-monadic value. I wouldn't say that, as it is inaccurate. Of course you can return a value of _some_ monadic type eg. (Maybe ...). > Not only are functions of the type IO a -> a > impossible to create, You can quite easily write a function of type IO (IO a) -> IO a, which is a special case of that type. > but any function whose result type does not > contain the IO type constructor is guaranteed not to use the IO monad. That's rather vague: what does it mean for a function to use a monad? > Other monads, such as List and Maybe, do allow values out of the monad. > So it is possible to write non-monadic functions that internally do > computations in those monads. The one-way nature of the IO monad also > has consequences when combining monads, a topic that is discussed in > part III. > -- In summary, I've only a vague idea of what you are trying to say. If you can't reformulate it more precisely, don't add the above stuff. > and a little farther down: > -- > Some people argue that using monads to introduce non-pure features into > Haskell disqualifies it from claiming to be a pure functional language. > This subtle question not particularly relevant to the practical > programmer is revisited in the context of the I/O monad later in the > tutorial. > -- That's fair enough. I don't think the question is so much subtle as religious, as we might expect from the terminology of "purity". > Later, in the section on the I/O monad: > -- > In Haskell, the top-level main function must have type IO (), so that > programs are typically structured at the top level as an > imperative-style sequence of I/O actions and calls to functional-style > code. Revisiting the debate about the purity of Haskell (in a functional > sense), it is important to note that the IO monad only simulates > imperative-style I/O. That (about simulation) seems weak. A simulation isn't a vague syntactic resemblance. > The functions exported from the IO module do not > perform I/O themselves. They return I/O actions, which describe an I/O > operation to be performed. The I/O actions are combined within the IO > monad (in a purely functional manner) to create more complex I/O > actions, resulting in the final I/O action that is the main value of the > program. The result of the Haskell compiler is an executable function > incorporating the main I/O action. Executing the program "applies" this > ultimate I/O action to the outside world to produce a new state of the > world. That seems to me the wrong thing to say. There is no application. Whether or not the word is put in quotes, it is something involving a function and an argument. An IO action is not a function. > This occurs only once per execution of the program, and since the > state of the world changes for each execution, the issue of purity is > neatly side-stepped. > -- By "the program", I think you mean the IO action. I think it is right to speak of the action as something that is executed. Execution may involve (side-effect free) calculation; but execution is something essentially different from calculation, not an impure form of it. I'm sorry to sound negative -- it's just that you invited criticism. Your pages seem generally of a very high quality to me. Sorry not to be more constructive too. Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Another typing question
> Samuel E Moelius, wrote (on Wed, 06 Aug 2003 at 15:35): > On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote: >> This is why most sensible dependent type theories have a hierarchy of >> universes behind the scenes. You can think of * in Haskell as the lowest >> universe, inhabited by types. > Why wouldn't terms be the lowest universe? A universe is a type of types/set-like-things, modulo a pile of subtleties. (The first of which is that it is actually a type of codes for types.) I think the term "universe", which afaik was introduced into type theory by Martin-Lof, was chosen for its use in the foundations of category theory in dealing with questions of "size" (smallness/largeness). Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
comonads, io
I came across an interesting paper "Codata and comonads in Haskell" by Richard Kieburtz, and some other work by Alberto Pardo on comonads. Kieburtz proposes an OI comonad, as an alternative to (or something alongside?) the IO monad. Just for reasons of symmetry, it's natural to wonder if they aren't as pervasive in functional programs as monads. Frustratingly, I can't seem to grasp the intuition. I'm aware that the state-monad s->(s,a) has a dual state-in-context comonad (s,s->a). How does the side-effect manifest itself? The (ineffective) hints the authors give revolve around the idea that side-effects "derive" from the context of a program. Any other hints? Are comonads especially appropriate for programming systems that react to changes in their environment? Is an object of OI type something like a program to react to events? I can't make the slightest sense of Kieburtz's OI co-monad, with commands like coGetChar :: OI Handle -> Char. Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: converting capital letters into small letters
> Andy Moran wrote (on Fri, 26 Jul 2002 at 16:52): > As for removing vowels, instead of proposing a solution, I choose to dispute > that the problem needs solving and claim victory. Removing vowels from identifiers can be very important if you are writing in certain assemblers from the 1970's. Maybe this could be the killer application we are all looking for? Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Writing a counter function
> lmichele wrote (on Sun, 30 Jun 2002 at 09:26): > By the way, what's the purpose of this coding? (this is the type of > question: "ok, I have a hammer, now, for what kind of nail it is useful?") I would guess that something like the asked-for counter could be useful if one is allocating ranges of addresses to things, for example heap nodes when compiling a function body to instructions to build a graph. Why not have a monad m a = Int -> (a,Int) which is a state monad plus the operation bump : Int -> m Int bump k n = (n,n+k) Rgds, Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: partial application
Apropos of section notation, don't forget flip, alias the C combinator. It allows you to express partial applications "to the next argument but one" is in operator section notation. We can express (usually horribly) any affine lambda-abstraction with flip, (.), id and const. Peter Hancock ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
