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] Unexported functions are evil
Peter Simons [EMAIL PROTECTED] writes: The only reason I could think of is that a function is considered to be internal, meaning: You don't want users of the module to rely on the function still being there (or still working the same way) in any of the next revisions. Right. (I guess you could sometimes have name clashes as well?) You could also view if from the opposite angle: when I work on a module, it is nice to check the export list to see what parts I need to maintain consistently, and what parts I am at liberty to change. On those occasions, however, why not put the function into a module, say Foo.Bar.Private and import it into Foo.Bar from there? So you don't want to automatically re-export imports, I take it? :-) Then those people who enjoy playing with fire _can_ use it, and everybody else will not. Is there something I missed? An opportunity to ignore export restrictions would be very useful for testing. It is nice to put tests into a separate module, but sometimes you really need access to internals as well. -kzm -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type system extension
Hi, I'd just been writing some code and an interesting idea for an extension to Haskell's type system sprang into my head. I have no idea if people have played with it, but it looked vaguely useful to me, so I thought I'd see what everyone else thought. Supposing you have these types: type Export = String data SCode = SModule String [Export] | SUnknown It would be useful to specify a function as so: doSomethingToAModule :: SCode(SModule) - SomeRandomOtherType which would specify, not only that the first argument was of type SCode, but more specifically, that it used the SModule constructor. This would then allow you to safely only write a case for the SModule constructor, and not worry about a runtime error when pattern matching failed on an SUnknown (as this would be checked at compile time). I hope this makes sense What does anyone think of the idea, and is there an obvious flaw in the plan? Thanks Tom Davie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system extension
Hi, Yes, sounds like a good idea. I'm not sure the right approach is to make the user give this information though - the code will very likely be something like doSomethingToAModule (SModule a b) = f a b from which you can derive the type SCode(SModule) very easily. As the expressions get more complex, you will want more substantial annotations - i.e. SCode(SModule(_,[])|SUnknown) for something which either exports nothing, or is unknown. At this point getting the programmer to type in essentially the same information twice is likely to become annoying. My current work on my PhD is all related to checking that a Haskell program cannot raise a pattern match error, and it is accomplished in a similar sort of method to what you are suggesting, and achieves similar goals. This work is still ongoing, but a first order checker exists for a subset of Haskell already - so progress is being made. Thanks Neil www.cs.york.ac.uk/~ndm/ On 5/15/05, Thomas Davie [EMAIL PROTECTED] wrote: Hi, I'd just been writing some code and an interesting idea for an extension to Haskell's type system sprang into my head. I have no idea if people have played with it, but it looked vaguely useful to me, so I thought I'd see what everyone else thought. Supposing you have these types: type Export = String data SCode = SModule String [Export] | SUnknown It would be useful to specify a function as so: doSomethingToAModule :: SCode(SModule) - SomeRandomOtherType which would specify, not only that the first argument was of type SCode, but more specifically, that it used the SModule constructor. This would then allow you to safely only write a case for the SModule constructor, and not worry about a runtime error when pattern matching failed on an SUnknown (as this would be checked at compile time). I hope this makes sense What does anyone think of the idea, and is there an obvious flaw in the plan? Thanks Tom Davie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system extension
On May 16, 2005, at 12:46 AM, Neil Mitchell wrote: Hi, Yes, sounds like a good idea. I'm not sure the right approach is to make the user give this information though - the code will very likely be something like doSomethingToAModule (SModule a b) = f a b from which you can derive the type SCode(SModule) very easily. As the expressions get more complex, you will want more substantial annotations - i.e. SCode(SModule(_,[])|SUnknown) for something which either exports nothing, or is unknown. At this point getting the programmer to type in essentially the same information twice is likely to become annoying. I'm not certain I agree with you. Where I do agree is that the types are liable to get very complex fairly quickly, and this may well be the flaw in the plan, however, I think Haskell benefits greatly from asking the programmer to provide the same information twice in slightly different forms. The type system after all is essentially a method of providing a sanity check -- does the code actually match up with what the programmer specified as a type. My current work on my PhD is all related to checking that a Haskell program cannot raise a pattern match error, and it is accomplished in a similar sort of method to what you are suggesting, and achieves similar goals. This work is still ongoing, but a first order checker exists for a subset of Haskell already - so progress is being made. I haven't thought about this for more than half a day when the idea popped into my head, so obviously you've dealt with it a bit more, but I wonder if this is only half the problem. By the sounds of it you are doing type inferencing from the program (as you explained above), which allows for a certain level of checks. However, type errors are not only thrown when the type inference system can't generate types to fit the program, but also when the programmer has specified types that are different to that the inference worked out. Thanks for a very interesting reply Tom Davie ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Unexported functions are evil
G'day all. Quoting Peter Simons [EMAIL PROTECTED]: I was wondering: Is there any reason why you would have a function in one of your modules and _not_ export it? The short answer: Because that function is nobody else's business. The long answer: The reason why programming is hard is that programs are complex. The art of software design and construction is the art of controlling that complexity so that it doesn't get out of hand. Paraphrasing what David Roundy said, every piece of code (with the possible exception of main) that you write is an API for some other part. Controlling the complexity means that I ask because I have _never_ had problems with a module exporting too much, but I have had problems with modules exporting too little quite frequently. Continuing on from the previous thought, part of the problem here is that we teach people to write code (e.g. how to implement a sort), but we don't teach people to write APIs. APIs are both trickier to get right AND are more important in larger programs. So while I think you've identified a real problem (the modules that you want to use expose insufficient APIs), I think your solution is wrong. The right solution is to complain to the module writer, and ask them to export a functionally complete API. The reason why I like purely functional languages like Haskell is that it is virtually impossible to write code that cannot be reused. I'd disagree with that. Strongly. Very strongly. It's _easier_ to write reusable code, for sure. But reusable code is tricky no matter what you do. And according to Alan Perlis, you never know if it's truly reusable until you've reused it at least three times. The only reason I could think of is that a function is considered to be internal, meaning: You don't want users of the module to rely on the function still being there (or still working the same way) in any of the next revisions. Right. And I agree with David: This is reason enough. With my business hat on: Every time you expose something for use, you must at the very least document it. At most, you are implicitly supporting it. If you have customers that have spent money or other resources on your code, then you owe it to them. On those occasions, however, why not put the function into a module, say Foo.Bar.Private and import it into Foo.Bar from there? Then those people who enjoy playing with fire _can_ use it, and everybody else will not. Taking this to an illogcial extreme, why don't we allow pointer arithmetic in Haskell, but require people to import Prelude.C first, so that people who enjoy playing with fire can do it? After all, we use it under the covers... Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
