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: 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
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
