fromInteger/hClose bugs in 4.03
The current ghc-4.03 from the repository contains two bugs:
* In the modules Int and Word: The fromInteger methods handle
the J# cases only, but not the S# cases. Example:
import Word
main = print ((fromInteger 42)::Word32)
yields
Fail: Word.lhs:573: Non-exhaustive patterns in function fromInteger
* 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.
Cheers,
Sven
--
Sven PanneTel.: +49/89/2178-2235
LMU, Institut fuer Informatik FAX : +49/89/2178-2211
LFE Programmier- und Modellierungssprachen Oettingenstr. 67
mailto:[EMAIL PROTECTED]D-80538 Muenchen
http://www.pms.informatik.uni-muenchen.de/mitarbeiter/panne
Re: Do Existential Types make Algebraic Types obsolete? (was Re: how to exploit existential types)
On 19-Feb-1999, S. Alexander Jacobson [EMAIL PROTECTED] wrote:
Do existential types makes algebraic types obsolete?
I mean there seems to be a large semantic overlap between the two
concepts.
For example, once you can implement lists with just the product type (,),
why bother with algebraic types?
Algebraic types model a fixed set of alternatives.
Type classes (which is what you use in conjunction with
existential types) model an unbounded set of alternatives.
If, as is the case with lists, you know in advance the
fixed set of alternatives, then algebraic types work
much better. If, on the other hand, you don't know
the alternatives in advance, then using type classes
(and, where appropriate, existential types) makes more sense.
Arguably Boolean is a natural algebraic type, but if we pattern
match on typenames then we don't need the algebraic types here. e.g.
--Booleans w/o algebraic types
data True = True
data False = False
class Boolean where -- no methods required
instance Boolean True where -- trivial implentation
instance Boolean False where --trivial implementation
--(There is probably much better syntax for this)
Pattern matching on type names would not be a violation of the type
system, it would just be syntactic sugar...e.g. for booleans it would be
equivalent to:
--Hack because there is no built in pattern matching on type names
instance TypeName True where
typeName x = "True"
instance TypeName False where
typeName x = "False"
--definition of if' in this framework
if' x y z = case (typeName x) of
"True" - y
"False" - z
The problem with this is that there is nothing to stop
someone defining `instance Boolean Int'. So this
doesn't really capture the programmer's intent as
well as the algebraic type does.
It's also going to be less efficient than algebraic types.
Languages like C and Java do not seem to have an equivalent to algebraic
types
True. Such alternatives have been proposed, however.
For C++, John Skaller proposed "variants", which were
algebraic types; you may be able to pull up the old
debates on comp.std.c++ using DejaNews.
And for Java, the designers of Pizza extended Java
with algebraic types.
because they allow heterogenous lists.
I don't think that follows. Pizza for example certainly has an equivalent
to algebraic types but also allows heterogenous lists.
Are there contexts where you need algebraic types because existential
types won't do the job? Wouldn't everybody be happier if you could just
pattern match on type names (someone else requested this in a recent
thread)?
That might work OK *if* you had union types.
You can use type classes (such as `Boolean' in your example above)
as a poor man's version of union types, but they're really not
ideal in that role.
For an example of a language which explores this, see TEL,
which is the language that Gert Smolka designed for his PhD thesis.
(Gert Smolka is more widely known for the language Oz.)
Or the most extreme version of this question, once you abandon algebraic
types, do you need constructor names at all or can you just use
position e.g.
data MyType a b = Int a b
myFunc (MyType x y z) = MyType (x+1) y z
data MyType2 a b = {field1::Int,field2::a,field3::b}
myFunc2 x = (field1 x+1,field2 x)
You sometimes need the constructor names to avoid ambiguity.
Consider what happens if you have two different
types that have the same fields:
data PolarCoord = MkPolar Float Float
data RectCoord = MkRect Float Float
class Coord t where ...
instance Coord PolarCoord where ...
instance Coord RectCoord where ...
--
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?
The basic problem that I have with this is that although dependent types do allow you to specify a lot of things in the type system, I'm not sure that using the type system is really the best way to specify these things. Well, I think types are just the place for these things. People already use types as a partial specification, enabling types to express all properties you want is, IMO, the right way. But I don't think we have found the right formalism for it yet. E.g., equational reasoning doesn't look pretty in Cayenne. But when it comes to things like proving that `==' is reflexive, symmetric, and transitive, I think it may well be much clearer if these kinds of properties are expressed more directly, rather than by cleverly encoding them in the type system. I don't see how these properties can be expressed in a different way even if they were outside the types. You may object to the notation used, but give me a font with quantifiers and I'll make it look pretty. :-) -- Lennart
Re: Haskell 2 -- Dependent types?
On 19-Feb-1999, Nick Kallen [EMAIL PROTECTED] wrote: I'll admit to not having yet written something in Cayenne, but I'm an adamant supporter of adding dependant types to the language. I remember a year ago, I was writing a small (trivial) program. One of the essential ways I was structuring the program was with a function "apply" similar to Lisp/scheme's apply. Needless to say, you can't express apply in Haskell although you can in Cayenne. In the context of this problem, I could easily get around this by restructuring my program, but this was obviously not ideal. We should be able to express trivial functions like apply in the type system. If your language supports optional dynamic type checking, as it should, then expressing functions like apply shouldn't be too hard. I'm an adamant supporter of adding optional dynamic types to the language. But I remain very cautious about the merits of dependent types. I think it is quite possible that the additional complexity of dependent types may outweigh their benefits. Foremost is that dependant types allow us to type more things than before. Yes, but not as many as optional dynamic types allow. For example with dynamic types you would not need to change the order of the arguments for `apply'. It is also clear, however, that dependant types are no trivial thing. Expressing the most general type of apply--that's not a super-type--is a complicated process. It is clear that a large library of type functions will likely be necessary, I think. This can be used as an argument both for and against dependant types. Indeed. It is, however, also clear that when in using dependant types, much more type information and documentation are provided. If, in fact, the example from above can be type checked (question [2]), then it is clear that dependant types are a *huge* bonus to more formally developing programs. Since essentially anything (well, minus partial functions and some other good things) can be specified in Lof's type theory, it becomes possible for the programmer to use formal methods to any extent he desires, with theorem proving being equivalent to the program type checking. The basic problem that I have with this is that although dependent types do allow you to specify a lot of things in the type system, I'm not sure that using the type system is really the best way to specify these things. When you only have a hammer, everything looks like a nail. If type checking is the only form of compile-time checking, then the only way of checking something at compile time is to make it part of the type system. And so the desire for better compile-time checking may lead us to create very complicated type systems. But when it comes to things like proving that `==' is reflexive, symmetric, and transitive, I think it may well be much clearer if these kinds of properties are expressed more directly, rather than by cleverly encoding them in the type system. -- 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?
[EMAIL PROTECTED] writes: 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? Is type really _the_ medium for everything? -- O.L.
Re: Haskell 2 -- Dependent types?
Well if the ComplicatedTypeToSpecifySorting is correct (I don't know if
this is possible, but I suspect it isn't) it will of course not type check.
Of course it is possible. The types in Cayenne have the same power
as predicate logic, so you can specify most anything you like.
Here's a possible type of sort (again assuming we have some = available):
[I'm writing this from the top of my head so there might be some
buglets.]
-- sort returns a record with the sorted list and two proofs
sort :: (l :: [a]) - sig { r :: [a]; o :: Ordered r; p :: Permutation l r }
-- Predicate to test if a list is ordered
Ordered :: [a] - #
Ordered [] = Truth
Ordered [x] = Truth
Ordered (x:x':xs) = IsTrue (x = x') /\ Ordered (x':xs)
-- Predicate to test if a list is a permutation of another
Permutation :: [a] - [a] - #
Permutation [] [] = Truth
Permutation (x:xs) ys = IsTrue (elem x ys) /\ Permutation xs (ys \\ [x])
IsTrue (True) = Truth
IsTrue (False) = Absurd
data Absurd = -- empty type
data Truth = truth-- one element type
data (/\) a b = () a b -- Conjunction, i.e. pairs
-- Lennart
Re: Haskell 2 -- Dependent types?
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? This is how I parse it: (member (map (F a) [0..])) // ( (member [a] a) - Bool ) Why does the first occurence of member only have one argument and the second two? I'd like to make an argument against that. Like Fergus I am an advocate of a dynamic types. (I've never met a type system I didn't like ;). I like dynamic types too. But I don't want to pay the price for them if I don't use them. Because they do carry a runtime cost. You can add dependant types to Cayenne (theoretically) just by allowing the run-time type inspection that you intentionally disallowed. In my mind, you'd kill two birds with one stone. Yes, and I've been thinking about adding runtime type tests. Perhaps by adding a function of type `encode :: # - Type', where Type is a normal data type used to capture the types in Cayenne. But before adding that I'd like to play with what I've already got. :-) type yourself. I guess it would be possible to do a little type inference, but for a function like apply it would be difficult (and impossible in general). The obvious question: does "in general" equal "in practice"? What I think would work in practice is to have type inference for those functions where it works today in e.g. Haskell. But if you use more powerful types you have to add signatures. Which I think is a good idea anyway. :-) (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. -- Lennart
Re: Haskell 2 -- Dependent types?
Well, yes, up to a point, but it may be clearer if the simple regular types part is kept separate from the undecidable part, as was done in NU-Prolog, or as is done in Eiffel. I'm not necesssarily advocating that the properties and proofs of these properties should be mixed with the regular code. That's just one way of doing it. Take sort as an example, we can do this (ignoring the compare function): sort :: (xs :: [a]) - ListTypeWithProofOfCorrectnes xs sort xs = ... sort code with integrate proof or this sort :: [a] - [a] sort xs = ... normal sort code sortReallySorts :: IsASortingFunction sort sortReallySorts = ... proof that sort really sorts Both of these styles are perfectly feasible to express in Cayenne. Which one to use depends on the situation (and your taste :-). I guess you prefer the latter. BTW, has Eiffel changed? Last time I looked you could only have assertions checked at runtime, and no correctness proofs. If you were talking about assertions, you might as well have said C. :-) I don't see how these properties can be expressed in a different way even if they were outside the types. You may object to the notation used, but give me a font with quantifiers and I'll make it look pretty. :-) You may be right, but I won't believe it until I see it ;-) Well, I won't believe that you can make it any easier by moving the proof out of the instance declarations. Defining what an equivalence relation is will look similar in other notations. BTW, don't get me wrong -- I think Cayenne is a very interesting language, and it's a very promising line of research. I'm just saying that I think we should be very cautious about adopting this kind of thing into Haskell-2. I've not been advocating that either. I'm advocating some form of dependent types. I would like to see dependent records, but you could limit the dependency to be on types (just as Haskell already has for the function tupe). That way records can replace modules (if you add some other little goo). Let me just point out that my main interest in dependent types is NOT to do specifications and proofs (like sort above), but to make the type system more expressible. This way we can make more programs typeable, and also give more accurate types to programs. The latter is well illustrated in a paper by Hongwei Xi and Frank Pfenning in POPL99. -- Lennart
Re: Haskell 2 -- Dependent types?
On 21-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote: [Fergus wrote:] The basic problem that I have with this is that although dependent types do allow you to specify a lot of things in the type system, I'm not sure that using the type system is really the best way to specify these things. Well, I think types are just the place for these things. People already use types as a partial specification, enabling types to express all properties you want is, IMO, the right way. Well, yes, up to a point, but it may be clearer if the simple regular types part is kept separate from the undecidable part, as was done in NU-Prolog, or as is done in Eiffel. [...] I don't see how these properties can be expressed in a different way even if they were outside the types. You may object to the notation used, but give me a font with quantifiers and I'll make it look pretty. :-) You may be right, but I won't believe it until I see it ;-) I don't think it's just the font that is the issue. For example, I find the use of instance declarations for expressing proofs of correctness to be rather unintuitive. I don't think a different font will fix that. BTW, don't get me wrong -- I think Cayenne is a very interesting language, and it's a very promising line of research. I'm just saying that I think we should be very cautious about adopting this kind of thing into Haskell-2. -- 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.
