module T () ...
ghc-4.04 pathch level 1 understands module T () where f x = 'a' as module T exporting f. Probably, it confuses this withmodule Twhere f x = 'a' ? -- Sergey Mechveliani [EMAIL PROTECTED]
RE: Segmentation faults with ghc-4.02 code
I tried to compile the following program with both ghc-3.02 and ghc-4.02 (pathlevel 1), using the linux glibc binary releases. The 3.02 one works fine but the code produced by 4.02 segmentation faults when I try to run I can't repeat this one - the program compiles fine and pops up a button when I run it. This is with stock 4.02 on Linux. The commands I used were: $ gcc -c tclhaskell.c $ ghc-4.02 -c -O Meurig.hs -fglasgow-exts -'#include "tclhaskell.h"' $ ghc-4.02 Meurig.o tclhaskell.o -L/usr/X11R6/lib -ltcl -ltk -ldl -lX11 Perhaps it's picking up the wrong versions of libraries or something? Cheers, Simon
RE: fromInteger/hClose bugs in 4.03
Sven Panne [EMAIL PROTECTED] writes:
...
* hClose on a semi-closed handle fails (4.02 has this bug, too):
import IO
main = do
h - openFile "/etc/passwd" ReadMode
c - hGetContents h
putStr c
hClose h
Transcript:
root:x:0:0:root:/root:/bin/bash
bin:x:1:1:bin:/bin:/bin/bash
[...]
Fail: illegal operation
Action: hClose
Handle: {closed}
Reason: handle is closed
According to the library report, closing a semi-closed handle
should be allowed.
But that's not the case here. By the time you get around to doing
the 'hClose', you've read to the end of the file and the semi-closed
handle has been closed for you (cf. report.)
--Sigbjorn
RE: `deriving' cost
And the Simon's warning is for remembering that the effect is about as if one sets these instances manually. Do i understand correct? My point was merely that it's easy to forget how much code is needed for an instance of Show or Read, since it's easy (too easy :-) to stick 'deriving Show' on every datatype. This is partly why in Haskell 1.3 the Text class was split into Show and Read. GHC could do better, for instance by using interpretive Show and Eq methods like Hugs - it would involve less code, but probably be slower, so perhaps only when optimisation is turned off. Cheers, Simon
Re: Haskell 2 -- Dependent types?
On 21-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote: (i.e., you leave out the pivot [x]) Obviously the result of sort will no longer be a permutation of its argument. Will this then not type check? No, the proof (whereever it is) would no longer type check. As I understand it, this is not necessarily true: if the proof contains loops, it might type check, even though it is not really a valid proof. So even though the sort function itself doesn't loop, if its proof of correctness has loops, then the sort function might return the wrong answer. Do I understand this correctly? -- Fergus Henderson [EMAIL PROTECTED] | "Binaries may die WWW: http://www.cs.mu.oz.au/~fjh | but source code lives forever" PGP: finger [EMAIL PROTECTED]| -- leaked Microsoft memo.
Re: Haskell 2 -- Dependent types?
On 21-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote: F a * = member (map (F a) [0..]) // member [a] a - Bool I mave no clue what this means. What is `member'? Member is memq, in, etc. Checks for membership in a list. I'm still lost. What is // and how does it bind? I believe "//" here is a C++/Java/C9X-style comment. Just read it as if "//" were "--". Everything from the "//" until the end of line is a comment. -- Fergus Henderson [EMAIL PROTECTED] | "Binaries may die WWW: http://www.cs.mu.oz.au/~fjh | but source code lives forever" PGP: finger [EMAIL PROTECTED]| -- leaked Microsoft memo.
RE: Haskell 2 -- Dependent types?
If you return the same proof of correctness that you used for the earlier definition of sort, then no it won't type check. But if you return a proof defined as e.g. proof = proof then if I understand things correctly it will type check. On that note, since this has been of interest on comp.lang.functional: Howabout a way to tell the compiler: "don't allow general recursion"?
Re: Haskell 2 -- Dependent types?
No, the proof (whereever it is) would no longer type check. As I understand it, this is not necessarily true: if the proof contains loops, it might type check, even though it is not really a valid proof. You're right. If the proof is looping it will still pass as a proof. -- Lennart
RE: Haskell 2 -- Dependent types?
apply :: (F a *) [a] - (F a *)
apply f [] = a
apply f [a:as] = apply (f a) as
The type gets noisier.
(To correct a couple of minor typos, that should be
apply f [] = f
apply f (a:as) = apply (f a) as
)
Heh, thank you. :)
I agree it is in some sense six of one and half a dozen of the other.
But I think that when using dynamic types, with an appropriate coding
style, you should be able to separate out the dynamic type tests and
the conversions to dynamic types a bit more clearly than you have done
above. For example:
apply :: Dynamic - [a] - b
-- code goes here -- dynamic type tests
conversions go here
apply f [] = f' where (f' :: b) = f
apply f (a:as) =
apply' (f' a) aswhere (f' :: a - _) = f
apply' = apply . dynamic
*Personally,* I like the way I did it better. It might be silly to get into
style arguments, but I do think a discussion of which is a better style is
worthwhile: an official coding style wrt/ dynamics is a good thing, imo.
I also think that the notion of dynamic types is quite straightforward
to understand (particularly for programmers with experience in other
languages that support similar constructs, e.g. Java, C++, Eiffel, etc.)
whereas the notion of dependent types is a bit more complicated.
Hm. I don't care much for this argument. I think people familiar with Java,
C++, Eiffel, are already with a disadvantage with functional programming:
the whole style of programming with higher order functions is foreign to
them.
The introductory programming course is in Scheme (for (EE)CS majors) at my
university. Everybody in the class has had some programming experience
(there's an entrance exam)--99% of them with imperative languages. For most,
using higher order functions like map, and lambda abstractions took time to
get used to. They got used to it however.
When imperative programmers go from C++ or whatever to Scheme, they have to
now think of "functions as data." Now, we're asking them to think of "types
as data."
1) I don't think we're asking them to leap that much further.
2) Who cares about imperative programmers anyway: our goal is to write
*correct* software with optimum productivity (and secondarily, optimum
performance). If extra effort is required *initially* to use dependant
types, but they further that goal, then add 'em.
You're right that we may well want to have both. But if we could only
have one, I'd rather dynamic types, and once we have dynamic types,
then the need for dependent types is much reduced. So we need to weigh
up the benefits and drawbacks of dependent types very carefully.
Dynamic types are in my opinion a necessity. There may very well be a debate
about this, but I'll completely grant you this point. We need them.
There are two ways to look at Cayenne, fundamentally:
- As a programming language
- As a system for expressing proofs.
They're equivalent in Lof's system and amazingly, it's just as
elegant in
expressing both: they're the same thing!
I understand that, and I know about the Curry-Howard isomorphism,
and it is all certainly very conceptually elegant.
But from a programmer's perspective, the program and it's proof
of correctness are two different things. As a programmer, I want
the two to be clearly separated, so that I can tell at a glance
which part is the program and which part is the proof of correctness.
Using the same constructs for both could well make things easier, but
I still want some clear visual indication that distinguishes the two.
Hm. I don't care to see the proof. I only want to know that the function
satisfies its specification. But I'm also unsatisfied with Lennart's
"recording-up" of the proof.
I'm hoping one can express sort in a different way.
Lennart's:
sort :: (l :: [a]) - sig { r :: [a]; o :: Ordered r; p :: Permutation l r }
I want the range of sort to be list... Rather, I want the range of sort to
be a subtype of [a]. That way you can keep the specification with the
implementation and you don't have to extract values from a tuple or a
record. How do you do this Lennart?
I want to be able to say:
(foldr (-) 0) . sort
Without having some spurious "sortReallySorts."
I am I stupidly assuming this is possible when it isn't?
I can't think of a good way to do this... My first thought was my own list
ADT:
data myList a = MkMyList [a] [a-#]
e.g., egList = MkMyList [1, 2, 3, 4] [Ordered, Permutation [4, 3, 2, 1]]
This works if I define my foldr for MkMyList and such, but this is yucky.
...I thought about this pretty hard. Particularly I thought about using
classes; this was fruitless. So I decided I'd invent a new language feature
and a nice little syntax to handle it.
Sorted l r = Ordered r /\ Permutation l r
sort :: (l :: [a]) - (r :: [a]) = Sorted l r
= is the "magic operator". Basically it's equivalent to /\, except it
allows
Re: Haskell 2 -- Dependent types?
I consider even the second one to be mixing the proofs with the code, because there's no easy way that I can tell at a glance that `sortReallySorts' is a proof rather than a program. But I consider that a feature and not a bug. :-) -- Lennart
Re: Haskell 2 -- Dependent types?
[EMAIL PROTECTED] wrote: enabling types to express all properties you want is, IMO, the right way. Why do I feel that there must be another approach to programming? How many people do you expect to program in Haskell once you are done adding all it takes to "express all imaginable properties through types"? What kind of baroque monster will it be? I didn't say you had to use it. If you want to continue programming in the Haskell style you can. But if you feel the need to express properties, the power is there. It's like assertions; if you don't want them, don't use them. But if you are careful you'll use them where there is a need. But unlike assertions type properties will be checked at compile time. Is type really _the_ medium for everything? It's a good candidate, IMO. People are putting more and more into type systems, why not go all the way. -- Lennart
RE: Haskell-2
What is the general consensus on views and the extended pattern guards that are discussed at http://www.haskell.org/development/ ? I think views are really neat, but am not quite sure how I feel about pattern guards.
Re: Haskell 2 -- Dependent types?
...I thought about this pretty hard. Particularly I thought about using
classes; this was fruitless. So I decided I'd invent a new language feature
and a nice little syntax to handle it.
Sorted l r = Ordered r /\ Permutation l r
sort :: (l :: [a]) - (r :: [a]) = Sorted l r
You've reinvented subsets. :-)
In more ordinary mathematical notation I'd write
sort :: (l :: [a]) - { r :: [a] | Sorted l r }
i.e., the range of sort is a subset of the type [a] where
the list is a sorted version of l.
I have also been thinking about how to add this, but I've not
come up with a satisfactory solution yet. This trick is
to make this mesh nicely with type checking.
One solution, admittedly somewhat of a hack, is to be able
to mark one of the components of a record as being the
essential one. E.g.
sort :: (l :: [a]) - sig { *r :: [a]; s :: Sorted l r }
where the * marks the essential component. The idea being
that if you have something of type `sig { *x :: T; ... }',
but need a `T' you the selection would be implicit. But you
would still be able to access the other components with the
usual . notation. E.g.
let ys = sort l
a = foldr (+) 0 ys -- use it as a list
foo = ys.s -- access the proof
...
I have no idea if this work well in practice or if it is
reasonable to implement. I'm still hoping for a better
idea.
The problem with your = "magic operator" is that the proof
is no longer accessible, which I think will make further
proofs difficult.
-- Lennart
PS. Have we bored normal Haskell users to tears yet?
Re: Haskell 2 -- Dependent types?
On 20-Feb-1999, Nick Kallen [EMAIL PROTECTED] wrote: [Lennart wrote:] [Nick Kallen wrote:] To what extent will a program that type checks completely fail to follow its specification? Can someone give specific examples? It's trivial to construct examples. Take sorting sort :: (l :: [a]) - ComplicatedTypeToSpecifySorting l Well, here's an implementation: sort xs = sort xs It's type correct, but doesn't really do what you want. but if you say sort [] = [] sort (x:xs) = sort elts_lt_x ++ [x] ++ sort elts_greq_x where elts_lt_x = [y | y - xs, y x] elts_greq_x = [y | y - xs, y = x] will the type checker say "yes," and can you believe it? No, the type checker will say "no", because the "ComplicatedTypeToSpecifySorting" must contain a proof of correctness, and the value returned from your sort function doesn't include the proof of correctness. But if you do include a proof of correctness, then it will typecheck. What if you do this: sort (x:xs) = sort elts_lt_x ++ sort elts_greq_x where elts_lt_x = [y | y - xs, y x] elts_greq_x = [y | y - xs, y = x] (i.e., you leave out the pivot [x]) Obviously the result of sort will no longer be a permutation of its argument. Will this then not type check? If you return the same proof of correctness that you used for the earlier definition of sort, then no it won't type check. But if you return a proof defined as e.g. proof = proof then if I understand things correctly it will type check. -- Fergus Henderson [EMAIL PROTECTED] | "Binaries may die WWW: http://www.cs.mu.oz.au/~fjh | but source code lives forever" PGP: finger [EMAIL PROTECTED]| -- leaked Microsoft memo.
