Re: Haskell 2 -- Dependent types?
On 28-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote: I downloaded the NU-Prolog manual and skimmed it, but I didn't see the features you're describing (probably because I haven't "done" Prolog since my learn-5-languages-in-a-quarter class 12 years ago). Could you give me a pointer to which section of the manual I should read? I'm not sure if it is documented in the NU-Prolog manual. It's probably documented somewhere, but off-hand I don't know where. Anyway the relevant feature is `where' annotations on `:- pred' declarations and `:- type' declarations. For example: :- pred append(list(T), list(T), list(T)) where (X, Y, Z : length(X, XL), length(Y, YL), length(Z, ZL), plus(XL, YL, ZL)). This gives a partial specification for `append'; it states that append(X, Y, Z) should succeed only if the length of X plus the length of Y is equal to the length of Z. You can also attach conditions to types, e.g. :- type sorted_list(T) == list(T) where X : sorted(X). Then when you write :- pred merge(sorted_list(T), sorted_list(T), sorted_list(T)). it is equivalent to :- pred merge(list(T), list(T), list(T)) where (X, Y, Z : sorted(X), sorted(Y), sorted(Z)). For Eiffel, as far as I can tell, what you get are assertions in function declarations (pre- and post-conditions on the functions). You also get class invariants. Consider the Haskell function sortBy: sortBy :: (a - a - Ordering) - [a] - [a] Suppose you wanted to verify that the output of sortBy was sorted according to the supplied comparison function. [...] It must be a precondition on sortBy that the comparison function satisfies this constraint. This can be expressed as a precondition, if preconditions can have universally quantified formulas (so preconditions can no longer be executable). Now, when you define a sorting function, you want to state and verify the above property. Where does it go? Eiffel doesn't have higher-order functions, so the first argument of sortBy would be a class with a sort method. The requirement that the sort method be an ordering would be a class invariant of this class. To me, the set of "acceptable comparison functions" feels like a type, so "encoding" this requirement in the type system is natural. It's certainly reasonable to consider class invariants in Eiffel or `where' annotations in NU-Prolog to be a part of the type. The point is that they are a _clearly separated_ part of the type. -- 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?
Lennart Augustsson [EMAIL PROTECTED] writes: (I believe that there are type theories with dependent types, such as the one in Thompson's _Type Theory and Functional Programming_, where each term has at most one type; so it can't just be dependent types that disallow principal types.) The more I think about this, the less I believe it. :-) I don't think each term can have a at most one type (unless all terms have a type annotation, in which case it is trivial). Sorry; I wasn't thinking clearly. You're quite right; Thompson's theory does achieve its at-most-one type property by putting lots of type information in the terms (although not quite as bad as an annotation on each subterm). Carl Witty [EMAIL PROTECTED]
Re: Haskell 2 -- Dependent types?
Fergus Henderson [EMAIL PROTECTED] writes: Could you give an example of language syntax that you feel would be better than putting these properties in the type system, while still allowing similar compile-time checking? I already gave NU-Prolog and Eiffel as examples. Those languages don't provide the same kind of static checking as Cayenne, because they don't provide a place for the user to put proofs. But extending them with some kind of syntax for proofs shouldn't be too hard, I think. Once you've got the proofs in there, I believe checking them at compile-time should be straight-forward. I downloaded the NU-Prolog manual and skimmed it, but I didn't see the features you're describing (probably because I haven't "done" Prolog since my learn-5-languages-in-a-quarter class 12 years ago). Could you give me a pointer to which section of the manual I should read? For Eiffel, as far as I can tell, what you get are assertions in function declarations (pre- and post-conditions on the functions). I believe that the compile-time checking possible in Cayenne or other hypothetical dependently-typed languages is significantly more expressive. Consider the Haskell function sortBy: sortBy :: (a - a - Ordering) - [a] - [a] Suppose you wanted to verify that the output of sortBy was sorted according to the supplied comparison function. (This is half the specification of a sorting function; the other half would be that the output is a permutation of the input.) In other words, suppose we want to verify that the comparison function, when applied to every successive pair of values in the output, returns either LT or EQ (never GT). This can be easily expressed as a postcondition on sortBy. Unfortunately, it cannot be proven; you need constraints on the comparison function. (For example, with the comparison function compare x y = GT no list with two or more elements could ever be sorted.) At a minimum, for any x and y, it must not be the case that x `cmp` y == GT and y `cmp` x == GT It must be a precondition on sortBy that the comparison function satisfies this constraint. This can be expressed as a precondition, if preconditions can have universally quantified formulas (so preconditions can no longer be executable). Now, when you define a sorting function, you want to state and verify the above property. Where does it go? It's not a postcondition of the comparison function, because it relates multiple different calls of the comparator. What syntax would you use to state that only some functions of type (a - a - Ordering) are acceptable as arguments to sortBy? How does the compiler verify that calls to sortBy use only acceptable comparison functions? To me, the set of "acceptable comparison functions" feels like a type, so "encoding" this requirement in the type system is natural. It also means that you don't have to think about a separate verification compiler pass to perform the compile-time checking; it's part of type checking, which I find conceptually clear and simple. Carl Witty [EMAIL PROTECTED]
Re: Haskell 2 -- Dependent types?
On 26-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote: This occurs because in the absense of type declarations, Haskell assumes that any recursion will be monomorphic, which is in general not necessarily the case. As I'm sure you know, type inference is in general impossible for polymorphic recursion, and since Haskell insists on decidable type checking this was an easy solution. Yep, there is a drawback to the Mercury approach, you lose decidability. But as we've been discussing losing decidability isn't necessarily such a bad thing ;-) Interestingly, the Mercury typechecker behaves differently for the equivalent example: it infers the more general type. Are you sure Mercury doesn't suffer from the same problem if you just complicate the example? Well, I'm fairly sure it doesn't, but I'm not completely 100% sure. -- 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 25-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote: [someone wrote:] I've lost track of what we're talking about here. In what system can we not hope for principal types? [...] Cayenne doesn't have that property. Again, I think this is a feature, not a bug. I'll include a small example below. ... struct abstract type Stack a = List a push :: a - Stack a - Stack a push x xs = x : xs ... This has type sig type Stack a push :: a - Stack a - Stack a ... Outside the defining struct Stack is abstract and cannot be interchanged for List. But here's another type we could give push push :: a - List a - Stack which (outside the defining struct) would look like a totally different creature. So what does Cayenne do if you don't declare the type for `push'? Does it report an error? I agree that allowing this kind of thing is a feature, not a bug, so long as the compiler reports an error rather than inferring some (non-principle) type for cases like that where there is no principle type. The same issue with regard to principle types arises in Mercury with regard to the module system, since the Mercury module system allows synonym types to be exported as abstract types. Mercury sidesteps this by requiring explicit type declarations for any exported procedures. The original rationale for this requirement was that using explicit type declarations on interfaces is simply good software engineering practice, and that the presence of this requirement simplifies the implementation. I wasn't aware that this requirement is also essential for ensuring the existence of principle types. Haskell's module system of course does not allow synonym types to be exported as abstract types -- you have to use a newtype instead. However, this may be better than Mercury's approach, because abstract synonym types become second-class citizens once you add typeclasses, since (in both Haskell and Mercury) you're not allowed to have instance declarations for synonym types. -- 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?
So what does Cayenne do if you don't declare the type for `push'? Does it report an error? The basic principle in Cayenne is that you need type signatures everywhere. This is sometimes rather verbose and is relaxed in some cases, but not here. If you omit the type signature the compiler will complain. [... type signatures required for exported procedures...] I wasn't aware that this requirement is also essential for ensuring the existence of principle types. I think it depends on how you treat type synonyms. In Haskell they are true synonyms, and can always be expanded to a real type, which would be the principal type. But I really like type synonyms as abstract types, it's convenient. Haskell's module system of course does not allow synonym types to be exported as abstract types -- you have to use a newtype instead. However, this may be better than Mercury's approach, because abstract synonym types become second-class citizens once you add typeclasses, since (in both Haskell and Mercury) you're not allowed to have instance declarations for synonym types. Well, Cayenne doesn't have have type classes. :-) -- Lennart
Re: Haskell 2 -- Dependent types?
On 25-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote: Fergus Henderson [EMAIL PROTECTED] writes: Certainly a language with dependent types should define exactly what types the type checker will infer. But when generating code, the compiler ought to be able to make use of more accurate type information, if it has that information available, wouldn't you agree? I think it would be most unfortunate if simply adding more accurate type information could change a program's behaviour. I'm not sure if that last sentence refers to 1) the compiler inferring more accurate type information or 2) the user adding a more accurate type declaration. I meant it to refer to both. 1) There's a word for "optimizers" that change the meaning of a program (in ways not allowed by the language spec); that word is "buggy". Sure. But it would be a little unfortunate if compilers had to keep around two sets of type information, one being the types that the language specification required that it infer, and the other being the (potentially more accurate) set of types that it was able to infer after inlining etc. It would be nicer if compilers could just use the most precise types and be guaranteed that the extra precision wouldn't affect the semantics. However, this is a less important point than the one below. 2) Yes, I agree that the possibility that user-supplied type declarations can change the meaning of the program is a strike against the idea. -- 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?
This occurs because in the absense of type declarations, Haskell assumes that any recursion will be monomorphic, which is in general not necessarily the case. As I'm sure you know, type inference is in general impossible for polymorphic recursion, and since Haskell insists on decidable type checking this was an easy solution. Besides, Haskell had polymorphic recursion even before the rule about a type signature making it possible to make functions polymorphically recursive. It was just more tedious to write it before. Interestingly, the Mercury typechecker behaves differently for the equivalent example: it infers the more general type. Are you sure Mercury doesn't suffer from the same problem if you just complicate the example? -- Lennart
Re: Haskell 2 -- Dependent types?
The key issue in Lennart's example, I think, is monomorphic recursion. For the function f _ = let y = f 'a' in undefined Haskell incorrectly (IMHO) infers the type `f :: Char - a' instead of the more general type `f :: b - a'. This occurs because in the absense of type declarations, Haskell assumes that any recursion will be monomorphic, which is in general not necessarily the case. Interestingly, the Mercury typechecker behaves differently for the equivalent example: it infers the more general type. I consider the fact that you can construct examples like the one that Lennart showed to be a wart in Haskell, and I'm quite pleased that Mercury doesn't exhibit the same wart. On a related topic, I think there's nothing wrong with having a type system in which some expressions don't have a principle type. However, in such situations, where there is no type declaration and there is no principle type, then I think the type checker ought to complain of ambiguity rather than going ahead and inferring a type which might be too specific. If the type inference always infers the most general type, or complains of ambiguity if it can't, then it's possible to preserve the desirable property that adding type declarations won't change the program's behaviour. -- 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?
Nick Kallen [EMAIL PROTECTED] writes: You cannot do this in Cayenne, there are no operations that scrutinize types. They can only be built, and never examined or taken apart. This is a deliberate design choice. The consequence is that type cannot affect the control of a program, so they cannot really influence the result of a program, and are thus needless at runtime. ... The whole idea behind dynamic types is that run-time type information can be inspected and manipulated. You can add dependant types to Cayenne (theoretically) just by allowing the ^ dynamic? run-time type inspection that you intentionally disallowed. In my mind, you'd kill two birds with one stone. Watch out here; there may be a limit to how much run-time type inspection it is reasonable to do in the presence of dependent types. Suppose you're examining a type which happens to be the type of some sorting function: (Ord a) = (l :: [a]) - ((l' :: [a]), sorted l l') How much type inspection are you willing to allow on that? How much good will it do you? (I made up my own syntax in the above type expression; I hope it makes sense.) Carl Witty [EMAIL PROTECTED]
RE: Haskell 2 -- Dependent types?
Watch out here; there may be a limit to how much run-time type inspection it is reasonable to do in the presence of dependent types. Suppose you're examining a type which happens to be the type of some sorting function: (Ord a) = (l :: [a]) - ((l' :: [a]), sorted l l') How much type inspection are you willing to allow on that? How much good will it do you? I'm willing to allow any amount of inspection. Type inspection wrt/ dynamic types is more useful for doing OO style stuff, and things like apply (cf previous email on this topic), so I can't imagine a circumstance where one would actually want to inspect types as detailed as the example you give. But unless you provide an argument like "this makes programming in the language more complicated" or "makes implementation impossible", I'm not willing to draw some arbitrary line: "no inspection beyond `foo'."
Re: Haskell 2 -- Dependent types?
On 24-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote: Fergus Henderson [EMAIL PROTECTED] writes: What if the body of min2 were defined so that it returned something different in the two cases? Your code has no proof that the code for the two cases is equivalent. If it's not, then the behaviour would depend on whether the compiler could deduce that a particular argument had type Sorted or not. And that in turn could depend on the amount of inlining etc. that the compiler does. I would assume that any language with this feature would have a precise specification of type inference sufficient to determine which of the two cases was used. Without such a specification, portable programming with dependent types is impossible; programs would compile under one "smart" compiler (which does more inference) and fail with a type error on another. Certainly a language with dependent types should define exactly what types the type checker will infer. But when generating code, the compiler ought to be able to make use of more accurate type information, if it has that information available, wouldn't you agree? I think it would be most unfortunate if simply adding more accurate type information could change a program's behaviour. -- 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 24-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote: Fergus Henderson [EMAIL PROTECTED] writes: What if the body of min2 were defined so that it returned something different in the two cases? Your code has no proof that the code for the two cases is equivalent. If it's not, then the behaviour would depend on whether the compiler could deduce that a particular argument had type Sorted or not. And that in turn could depend on the amount of inlining etc. that the compiler does. I would assume that any language with this feature would have a precise specification of type inference sufficient to determine which of the two cases was used. Without such a specification, portable programming with dependent types is impossible; programs would compile under one "smart" compiler (which does more inference) and fail with a type error on another. Certainly a language with dependent types should define exactly what types the type checker will infer. But when generating code, the compiler ought to be able to make use of more accurate type information, if it has that information available, wouldn't you agree? I think it would be most unfortunate if simply adding more accurate type information could change a program's behaviour. See my email where I derive a type for apply. Note how by using different types, you can change the range of apply to: a, or F a * -- i.e., a, a-a, a-a-a, ... By restricting the range. So different types does equal different behavior.
RE: Haskell 2 -- Dependent types?
If this is true, then what I'm doing is horrible. But I don't see how this leads to nondeterminism or broken referential transparency. min2 returns the same value for the same list, but it's simply more efficient if we happen to know some more information about the list. In this particular case that happens to be so. But it's not true in general. What if the body of min2 were defined so that it returned something different in the two cases? Your code has no proof that the code for the two cases is equivalent. If it's not, then the behaviour would depend on whether the compiler could deduce that a particular argument had type Sorted or not. And that in turn could depend on the amount of inlining etc. that the compiler does. I'm not asking the compiler to deduce anything. I'm talking about run-time type matching; this is dynamic types! I would assume that any language with this feature would have a precise specification of type inference sufficient to determine which of the two cases was used. Without such a specification, portable programming with dependent types is impossible; programs would compile under one "smart" compiler (which does more inference) and fail with a type error on another. The issue is not determining which of two cases was used. Run time inspection is sufficient, the issue is whether I'm violating referential transparency. I've thought about this issue more and have a contrary point. I'm not violating referential transparency. Why, because it is *not* unreasonable to assume that two functions will behave differently for different types. - ad hoc polymorphism (classes) violate referential transparency by that argument, doesn't it? - for subtypes (which is what my example was), it is not unreasonable to assume that a function will have different behavior for the subtype than for the supertype. This is obvious in OO programming--overriden methods. This is further obvious in a dynamic type system where you have functions like: draw :: Dynamic - Picture draw (c :: Circle) = ... draw (s :: Square) = ... ... further: min2 :: Dynamic - Picture min2 (l :: SortedList) = hd l min2 (l :: [a]) = min l note that here SortedList is just some ADT, not something dependant. To beat this to death: min2 :: [a] - a min2 (3:ls) = 0 min2 l = min l In sum, I argue: Complete runtime type inspection on dependant (sub)types violates nothing that anything else we already have doesn't.
Re: Haskell 2 -- Dependent types?
Fergus Henderson [EMAIL PROTECTED] writes: Certainly a language with dependent types should define exactly what types the type checker will infer. But when generating code, the compiler ought to be able to make use of more accurate type information, if it has that information available, wouldn't you agree? I think it would be most unfortunate if simply adding more accurate type information could change a program's behaviour. I'm not sure if that last sentence refers to 1) the compiler inferring more accurate type information or 2) the user adding a more accurate type declaration. 1) There's a word for "optimizers" that change the meaning of a program (in ways not allowed by the language spec); that word is "buggy". 2) Yes, I agree that the possibility that user-supplied type declarations can change the meaning of the program is a strike against the idea. Carl Witty [EMAIL PROTECTED]
Re: Haskell 2 -- Dependent types?
Fergus writes: I think it's becoming clear by now that the theoretical disadvantages of undecidable type checking are often not significant in practice. Experience with C++, Gofer, ghc, Mercury, etc. all seems to confirm this. In this context, people may find the paper _C++ Templates as Partial Evaluation_ by Todd Veldhuizen (PEPM'99) interesting: it describes how it was discovered that C++ templates had accidentally introduced a compile-time Turing-complete functional/logic language into C++, and how this is now used by numeric libraries to exceedingly useful ends. URL is http://www.cs.indiana.edu/hyplan/tveldhui/papers/ --KW 8-) -- : Keith Wansbrough, MSc, BSc(Hons) (Auckland) : : PhD Student, Computer Laboratory, University of Cambridge, England. : : (and recently of the University of Glasgow, Scotland. [] ) : : Native of Antipodean Auckland, New Zealand: 174d47' E, 36d55' S.: : http://www.cl.cam.ac.uk/users/kw217/ mailto:[EMAIL PROTECTED] : :-:
RE: Haskell 2 -- Dependent types?
I don't understand. What behaviour is different here?
Certainly the type is different. But how is the behaviour different?
It behaves differently in that it accepts and returns more/less values. If
this function is part of a program, then the behavior of the program is now
different in that its domain and range are possibly different.
I would say that a program that asks a user for an integer input and echoes:
Enter number.
1
You entered 1.
behaves differently from one that does the following:
Enter number
1
error. 1 not in domain blah.
Now if "crashing vs. not crashing" isn't different behavior by your
standards, imagine the case where we have a function that does a runtime
type evaluation:
consider (f :: Int - Int) = 1
consider (f _) = 2
Changing the type of f from
f :: Int - {1} - Int
-- Int - {1} is just a set notation: all ints except 1.
to
f :: Int - Int
makes the program
consider f
behave differently.
Re: Haskell 2 -- Dependent types?
[Resend - mlist trouble; apologies if you've already received it. -moderator] Lennart Augustsson [EMAIL PROTECTED] writes: 2) Yes, I agree that the possibility that user-supplied type declarations can change the meaning of the program is a strike against the idea. I don't find that so strange. If there are no principal types (which we can't hope for), then user added signatures can have the effect of changing the meaning of a program. I've lost track of what we're talking about here. In what system can we not hope for principal types? (I believe that there are type theories with dependent types, such as the one in Thompson's _Type Theory and Functional Programming_, where each term has at most one type; so it can't just be dependent types that disallow principal types.) BTW, Haskell already has this property. There are programs that yield different results depending on if you have a type signature or not (and it's not because of the numeric defaulting). Could you give an example? I can't think how to construct a Haskell 98 program with this property (unless you count "compiling" and "failing to compile" as different results). Carl Witty [EMAIL PROTECTED]
Re: Haskell 2 -- Dependent types?
I've lost track of what we're talking about here. In what system can we not hope for principal types? (I believe that there are type theories with dependent types, such as the one in Thompson's _Type Theory and Functional Programming_, where each term has at most one type; so it can't just be dependent types that disallow principal types.) Well, maybe there are, but Cayenne doesn't have that property. Again, I think this is a feature, not a bug. I'll include a small example below. Could you give an example? I can't think how to construct a Haskell 98 program with this property (unless you count "compiling" and "failing to compile" as different results). Check the example I sent in reply to Fergus' request. -- Lennart struct abstract type Stack a = List a push :: a - Stack a - Stack a push x xs = x : xs ... This has type sig type Stack a push :: a - Stack a - Stack a ... Outside the defining struct Stack is abstract and cannot be interchanged for List. But here's another type we could give push push :: a - List a - Stack which (outside the defining struct) would look like a totally different creature.
Re: Haskell 2 -- Dependent types?
"Nick Kallen" [EMAIL PROTECTED] writes: If this is true, then what I'm doing is horrible. But I don't see how this leads to nondeterminism or broken referential transparency. min2 returns the same value for the same list, but it's simply more efficient if we happen to know some more information about the list. In this particular case that happens to be so. But it's not true in general. What if the body of min2 were defined so that it returned something different in the two cases? Your code has no proof that the code for the two cases is equivalent. If it's not, then the behaviour would depend on whether the compiler could deduce that a particular argument had type Sorted or not. And that in turn could depend on the amount of inlining etc. that the compiler does. I'm not asking the compiler to deduce anything. I'm talking about run-time type matching; this is dynamic types! Ouch. I hadn't realized this, although I should have. I think you're going to run into severe efficiency/implementation problems if you try to implement an approach like this. As far as I can tell, you need to store a potentially very large set of type information with every object (every list cell, etc.), and you need to figure out ways to efficiently create and query this type information. Sounds tough. Carl Witty [EMAIL PROTECTED]
Re: Haskell 2 -- Dependent types?
[EMAIL PROTECTED] writes: [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? I would certainly love to program in a language that let me specify that a sorting function really did sort. Also, I am confident that if done right, a dependent type system could be added on to Haskell such that all existing Haskell programs would continue to be valid. I see a couple of reasons to "enable types to express all properties you want". 1) I've been following efforts in the theorem proving/proof verification community which are based on this idea. Several type-theory based verification systems are based directly on expressing properties in types (e.g. Coq, LEGO, the Alf* family, NuPRL). Others (PVS and Ontic) gain a lot of mileage out of a very expressive type system. (My apologies for any relevant systems I've left out here.) Based on these efforts, it seems very natural to me to extend this idea to a real, usable programming language. 2) Type checking has been widely studied and is pretty well understood. It makes sense to take this base and use it to make languages even more powerful and expressive. Carl Witty [EMAIL PROTECTED]
Re: Haskell 2 -- Dependent types?
On 22-Feb-1999, Nick Kallen [EMAIL PROTECTED] wrote: min2 :: [a] - a min2 ((l:ls) :: [a] = Sorted) = l min2 l = min l What's the semantics of that supposed to be? If the list is not known to be definitely sorted, will it check sortedness at runtime? If not, then the semantics could be nondeterministic, in general, so you've broken referential transparency. If so, what's the difference between that and this? min3 :: [a] - a min3 (l:ls) | sorted (l:ls) = l min3 l = min l Here I'm just using an ordinary guard, and `sorted' is just an ordinary function. Heh. I'm not seriously advocating adding my magic operator to the language, but I am pointing out that explicitly passing around proofs is a pain in the ass. This is good evidence that Fergus is right when he says: "As a programmer, I want the two to be clearly separated." However, his clear separation would not allow min2, would it? It would allow min3, above. I'm not sure what min2 buys you over min3. If the `Sorted' type is defined in terms of `sorted', then a compiler ought to be able to optimize min3 just as well as min2, I think. -- 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: (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 -- 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.
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.
Re: Haskell 2 -- Dependent types?
Nick Kallen [EMAIL PROTECTED] wrote: apply f (p:ps) = apply (f p) ps apply f [] = f I wanted to express the type as something like: apply :: (a - a - ... - a) [a] - a No, that's not what you want. :-) You want apply :: (a - a - ... - b) [a] - b I think the distinction is important (see below). F a * = member (map (F a) [0..]) // member [a] a - Bool I mave no clue what this means. What is `member'? and applyType can be defined more succinctly: applyType a l = F a (length l) You can certainly express applyType that way in Cayenne if you wish. and since the recursion has been eliminated from applyType, you can eschew applyType altogether and type apply thusly: apply :: (F a (length l)) (l :: [a]) - a And that works in Cayenne as well (modulo the argument order). This is satisfactory, but a reasonable request is to make the *range* of apply even more general. Since apply's first parameter is a curried function, it seems to me that there's no reason why the range of apply can't also be a function. That is, I agree, that's why you should have a b as the return type of apply. The this comes for free and all the complications of apply you go through are unnecessary. arity :: (F a *) - Int arity (a - as) = 1 + (arity as) arity a = 0 You cannot do this in Cayenne, there are no operations that scrutinize types. They can only be built, and never examined or taken apart. This is a deliberate design choice. The consequence is that type cannot affect the control of a program, so they cannot really influence the result of a program, and are thus needless at runtime. Fr a min max = member (map (F a) [min..max]) so apply is now typed apply :: (f :: (Fr a [(length l)..])) (l :: [a]) - (F a ((arity f) - (length l))) Well, I'm lost again. :-) [1] What type can Cayenne infer for apply just given apply's definition? Cayenne doesn't do type inference. Well, it does a little, but it will punt on any recursive definitions. So you have to give the 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). [2] I know my last type for apply is invalid cayenne due to the order of parameters and such, but if it's massaged a little bit: can Cayenne type check it? Well, I don't really understand the definition, so I can't say. But probably not since you've used the arity function. 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. I don't think so. The type you want is (using your argument order) apply :: (F a b (length l)) - (l :: [a]) - b with F a b 0 = b F a b n = a - F a b (n-1) proving being equivalent to the program type checking. Well, actually it's not quite so simple since because Cayenne does allow general recursion, you can't actually trust the fact that your program type checks as proof it follows the specification. This is something that I would appreciate if Lennart elaborated on. To what extent is this a problem in practice? 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. -- Lennart
RE: Haskell 2 -- Dependent types?
I wanted to express the type as something like: apply :: (a - a - ... - a) [a] - a No, that's not what you want. :-) You want apply :: (a - a - ... - b) [a] - b I think the distinction is important (see below). 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. "F a *" is a predicate on types. It's a magical syntax, not valid Haskell. It checks to see if the type is in the list: [a, a - a, a - a - a, a - a - a - a, ...] and applyType can be defined more succinctly: applyType a l = F a (length l) You can certainly express applyType that way in Cayenne if you wish. and since the recursion has been eliminated from applyType, you can eschew applyType altogether and type apply thusly: apply :: (F a (length l)) (l :: [a]) - a And that works in Cayenne as well (modulo the argument order). This is satisfactory, but a reasonable request is to make the *range* of apply even more general. Since apply's first parameter is a curried function, it seems to me that there's no reason why the range of apply can't also be a function. That is, I agree, that's why you should have a b as the return type of apply. The this comes for free and all the complications of apply you go through are unnecessary. arity :: (F a *) - Int arity (a - as) = 1 + (arity as) arity a = 0 You cannot do this in Cayenne, there are no operations that scrutinize types. They can only be built, and never examined or taken apart. This is a deliberate design choice. The consequence is that type cannot affect the control of a program, so they cannot really influence the result of a program, and are thus needless at runtime. 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 ;). To add dynamic types to a language, you can make them a special feature, with some sort of "dynamic" type constructor, and pattern match like: draw :: Dynamic - Picture draw (c :: Circle) = drawCircle c draw (s :: Square) = drawSquare c ... draw (u :: _) = theEmptyPicture // What happens if you try to draw a "file"? (I'm not sure on the syntax of how existing Haskell implementations support this. The above is largely based on the Clean 2.0 syntax.) The whole idea behind dynamic types is that run-time type information can be inspected and manipulated. 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. Fr a min max = member (map (F a) [min..max]) so apply is now typed apply :: (f :: (Fr a [(length l)..])) (l :: [a]) - (F a ((arity f) - (length l))) Well, I'm lost again. :-) Well, especially since there's an error, it might lead to confusion. let me redefine Fr: Fr a l = member (map (F a) l) so Fr a [1, 4, 6] == member [a - a, a - a - a - a - a, a - a - a - a - a - a - a]. Given the same type of apply, I'll restate it in words: f is of arity = length l. The range of apply is of arity ((arity f) - (length l)). [1] What type can Cayenne infer for apply just given apply's definition? Cayenne doesn't do type inference. Well, it does a little, but it will punt on any recursive definitions. So you have to give the 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"? [2] I know my last type for apply is invalid cayenne due to the order of parameters and such, but if it's massaged a little bit: can Cayenne type check it? Well, I don't really understand the definition, so I can't say. But probably not since you've used the arity function. Right. it relies on run-time type information. 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? 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?
RE: Haskell 2 -- Dependent types?
If your language supports optional dynamic type checking, as it should, then expressing functions like apply shouldn't be too hard. Here's a dynamic apply in a pseudo Clean 2.0 syntax: apply :: Dynamic [a] - a apply (f :: a - b) (arg:args) = apply (dynamic (f arg) :: b) args apply (f :: a) [] = f apply _ _ = Error "Run Time Type Error!!" Personally, it's 6 of one, 12/2 of the other, for me. With dynamics you fill up apply's definition with noise. With dependant types apply :: (F a *) [a] - (F a *) apply f [] = a apply f [a:as] = apply (f a) as The type gets noisier. 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. That's definitely a valid argument. We have to be willing to good eschew type inference altogether (I think), to add dependant types. 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'. Indeed. But it's a question of the best tool for the job. You can basically make any function accept and return anything with dynamic types--make your program have as much static checking as a Scheme program ;). Or you can use dependant types and essentially do everything statically. Two tools that can work together, IMO. 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. I completely disagree with this argument. Your example is valid, but I think it stems from a mistaken understanding of the type system. We're not just extending HM in the case of Cayenne, we're implementing Martin Lof's constructive type system. It's a whole new ballgame. This is not a hammer; Lof's type theory is all about expressing proofs and such. I'm talking about the curry-Howard isomorphism Implication is the arrow (-) Universal quantification is a function, etc. 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 recommend you read: Type Theory and Functional Programming (International Computer Science Series) by Simon Thompson It was in my school library, and was a pleasure to read. In one of the examples, they express the properties of the quicksort (permutation, etc.), and then go on to prove that their implementation of quicksort satisfies the specification. It's not a hammer, it's a, um, pillow.
Re: Haskell 2 -- Dependent types?
OK, I'm curious. Two people replied that C++ has undecidable type checking. I was not aware of this (although I can't say I'm too surprised); do you have a reference? It's actually the template processing that can loop, but it is sort of part of the type checking. You can find an article in the POPL 99 proceeding about it. -- Lennart
Re: Haskell 2 -- Dependent types?
On 18-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
OK, I'm curious. Two people replied that C++ has undecidable type
checking. I was not aware of this (although I can't say I'm too
surprised); do you have a reference?
Not really. I believe this has been mentioned on comp.std.c++,
but I did not succeed in finding the revelant articles with the
quick DejaNews search that I did.
But basically the relevant feature is templates and template
specialization. Templates give you recursion at compile time,
and template specialization gives you the equivalent of if-then-else,
and that's about all you need. I've included below an example which
computes factorials at compile time, using successor arithmetic in the
type system. I believe it would be straight-forward, albeit tedious, to
extend this example to compute arbitrary recursive functions on natural
numbers.
The relevant part of the C++ standard is Annex B:
|-1- Because computers are finite, C++ implementations are inevitably
|limited in the size of the programs they can successfully process.
|Every implementation shall document those limitations where known.
|This documentation may cite fixed limits where they exist, say how to
|compute variable limits as a function of available resources, or say
|that fixed limits do not exist or are unknown.
|
|-2- The limits may constrain quantities that include those described
|below or others. The bracketed number following each quantity is
|recommended as the minimum for that quantity. However, these
|quantities are only guidelines and do not determine compliance.
...
| * Recursively nested template instantiations [17].
Here's the example code. Note that to compile this, you will
need a compiler that supports much more than 17 recursively
nested template instantiations.
// successor arithmetic:
struct Zero {
typedef Zero check_is_zero;
};
template class T struct Succ {
typedef T pred;
};
typedef SuccZero One;
typedef SuccOne Two;
typedef SuccTwo Three;
typedef SuccThree Four;
typedef SuccFour Five;
// some examples of recursion with if-the-else:
// addition
template class T1, class T2
struct Sum {
typedef typename Sumtypename T1::pred, SuccT2 ::t t;
};
template class T2
struct SumZero, T2 {
typedef T2 t;
};
// multiplication
template class T1, class T2
struct Prod {
typedef typename SumT2,
typename Prodtypename T1::pred,T2::t::t t;
};
template class T2
struct ProdZero, T2 {
typedef Zero t;
};
typedef ProdTwo, Five::t Ten;
typedef ProdTwo, Ten::t Twenty;
typedef ProdTen, Ten::t Hundred;
typedef ProdTen, Hundred::t Thousand;
// factorial
template class T
struct Factorial {
typedef typename ProdT,
typename Factorialtypename T::pred::t::t t;
};
template
struct FactorialZero {
typedef One t;
};
// equality
template class T1, class T2
struct ZeroIfEqual {
typedef typename ZeroIfEqualtypename T1::pred,
typename T2::pred::t t;
};
template
struct ZeroIfEqualZero, Zero {
typedef Zero t;
};
template class T1
struct ZeroIfEqualT1, Zero {
typedef One t;
};
template class T2
struct ZeroIfEqualZero, T2 {
typedef One t;
};
// now some examples where the type-correctness of the program
// depends on the results of the arithmetic
// check that 2! == 2
typedef typename ZeroIfEqualtypename FactorialTwo::t, Two::t res;
typedef typename res::check_is_zero checkme;
// check that 5! == 120
typedef typename SumHundred, Twenty::t HundredAndTwenty;
typedef typename ZeroIfEqualtypename FactorialFive::t,
HundredAndTwenty::t res2;
typedef typename res2::check_is_zero checkme2;
--
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?
Lennart Augustsson writes: OK, I'm curious. Two people replied that C++ has undecidable type checking. I was not aware of this (although I can't say I'm too surprised); do you have a reference? It's actually the template processing that can loop, but it is sort of part of the type checking. You can find an article in the POPL 99 proceeding about it. Actually, I think Lennart means PEPM '99. At least, there's an article called "C++ Templates as Partial Evaluation" by Todd Veldhuizen (from the wonderfully-named Extreme Computing Laboratory) which refers to this. He cites an example of using the templates to generate a list of prime numbers at compile time due to Erwin Unruh (apparently discovered accidentally!). Cheers, Andy
RE: Haskell 2 -- Dependent types?
I'm curious: how many people have actually written a program in Cayenne? How many people have written programs that made significant use of the dependent typing? Has anybody tried to teach a programming class using Cayenne? 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. apply f (p:ps) = apply (f p) ps apply f [] = f I wanted to express the type as something like: apply :: (a - a - ... - a) [a] - a The stated domain of apply is much larger than its actual domain. I want its domain to be: a function whose arity is the length of the second parameter (a list). It's clear that the precise domain of apply can only be expressed with a function. I would like to say that the type of the first parameter is applyType: applyType a [] = a applyType a (p:ps) = a - applyType a ps I presume the type of the applyType is then applyType :: (a :: #) - [a] - # with # being the type of all types. Thus apply is of type apply :: (applyType a l) (l :: [a]) - a Now there are a ton of problems with what I just stated. 1) The type of apply is somewhat ambiguous. The a passed to applyType is free. Assumption: free variables are universally quantified. This is consistent with Haskell's current notation for typing. 2) This isn't valid Cayenne (I'll get to this later) 3) The type of applyType can be more specific. Recall, applyType :: (a :: #) - [a] - # The final # is actually just function space. How would we express the notion of a function space? Well, lets start with the simpler problem of defining the n-function space (my vocabulary is obviously falling apart at this point). F :: (a :: #) Integer - # F a 0 = a F a n = a - (F a (n - 1)) We however want to generalize this... I'm not quite sure how to describe it, but I'll do the following: F a * = member (map (F a) [0..]) // member [a] a - Bool so applyType is then applyType :: (a :: #) - [a] - (F a *) and applyType can be defined more succinctly: applyType a l = F a (length l) and since the recursion has been eliminated from applyType, you can eschew applyType altogether and type apply thusly: apply :: (F a (length l)) (l :: [a]) - a This is satisfactory, but a reasonable request is to make the *range* of apply even more general. Since apply's first parameter is a curried function, it seems to me that there's no reason why the range of apply can't also be a function. That is, apply should return a value of type a iff the length of its second parameter equals the arity of its first. Otherwise, the length of the second must be less than the arity of the first, in which case apply should return a function whose arity is the difference of the arity first parameter and the length of the second. Example: apply (+) [1] == \x - 1 + x so one now expresses the type of apply thusly: apply :: (F a *) (l :: [a]) - (F a *). This isn't completely satisfactory, since the first parameter of apply and the range are now too general. To make them specific, I define the following: arity :: (F a *) - Int arity (a - as) = 1 + (arity as) arity a = 0 Fr a min max = member (map (F a) [min..max]) so apply is now typed apply :: (f :: (Fr a [(length l)..])) (l :: [a]) - (F a ((arity f) - (length l))) whew. Now I must warn you that I'ven't checked anything at all, so it is highly probable that there are errors. Like, I'm introducing things like pattern matching on the function type constructor (-). I'm not sure if this is valid. Some questions for Lennart (and those more knowledgeable than I): [1] What type can Cayenne infer for apply just given apply's definition? [2] I know my last type for apply is invalid cayenne due to the order of parameters and such, but if it's massaged a little bit: can Cayenne type check it? Foremost is that dependant types allow us to type more things than before. The example I've shown demonstrates that even a simple thing like apply needs them. One might infer, then, that there are possibly many simple and perhaps common things which require this sort of type system. 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. It is, however, also clear that when in using dependant types, much more type
Re: Haskell 2 -- Dependent types?
On Wed, 17 Feb 1999, George Beshers wrote: 1. If the tool can resolve the types (and I would expect this to be true most of the time) it can display the types and (if the user or style guide dictates) add the types to the source. 2. If the tool can not resolve the type of a particular construct then the programmer can add the information and the tool can verify that the supplied type is correct. 3. As D. Tweed's short STL example points out, C++ can be all but unreadable without the support of static analysis tools today (ooh... there was an implicit constructor call there!!!). I would argue that working with large software systems in any language requires support from software tools. So why not design Haskell-2 with tools in mind? For anyone who would like to see what a tool like this *might* look like I think you should look at Alfa. This tool is really a proof editor but could as well be used as a programming tool for the functional language cayenne since the proofs are formulated in cayenne and proof checking is done by typechecking the program/proof. This can be be done because cayenne is a language with dependent types which are powerful enough to express just about anything about the program. The typechecking is done incrementally which is really neat and prevents you from constructing erronious proofs/programs. Alfa has a GUI which is really nice and allows you to just use the mouse for programming/proof construction. Alfa can be found on: http://www.cs.chalmers.se/~hallgren/Alfa/ /Josef -- |Josef Svenningsson|http://www.dtek.chalmers.se/~d95josef| |Rubingatan 39 | email: [EMAIL PROTECTED] | |421 62 Göteborg | tel: 031-7090774 | -- What is a magician but a practising theorist? -- Obi-Wan Kenobi
Re: Haskell 2 -- Dependent types?
I'm not sure that anybody has "accepted" undecidable type checking. People using Gofer or C++ seem to have. -- Lennart
Re: Haskell 2 -- Dependent types?
2.in the face of the above, we need to give the compiler more guidance. Personally, I favour type declarations everywhere: all identifiers should be introduced as being of a particular specified type. Of course, whether these principles are compatible with Haskell it another question... Giving everything a type certainly is compatible with Haskell. In Haskell you can almost do it, and the syntax could be trivially extended to allow it everywhere (i.e. in lambda and case, and for type variables.) I think giving types everywhere is an excellent starting point, but I also feel that it should be relaxed a little, because sometimes it can be rather redundant. -- Lennart
RE: Haskell 2 -- Dependent types?
On Wed, 17 Feb 1999, michael abbott wrote: As a C++ user (with a background in categories) patiently waiting for something a lot better, I personally favour two principles: 1.let's go for undecidable type checking. I want the compiler to be able to do as much work as possible: ideally, everything that can be resolved at compile time should be if only we can express this correctly. 2.in the face of the above, we need to give the compiler more guidance. Personally, I favour type declarations everywhere: all identifiers should be introduced as being of a particular specified type. My personal ideals for a programming language are: (1) The compiler catches as many language inconsistencies as possible rather than resolving them in possibly incorrect ways. (2) A program should be as easily readible as reasonably possible, which strongly suggests as free for `noise' as possible. (For example, try doing simple things with the pair STL class and see how soon relatively simple expressions become incredibly opaque because of the sheer length of the identifiers make_pair, .first, .second and the fact that, to maintain portability to compilers with slightly older versions of the type-conversion algorithm, you have to write things with casts that express the desired type pairfloat,float f=g+make_pair(float(5.0),float(3.0)) and not just pairfloat,float f=g+make_pair(5.0,3.0) In practice of course the first problem can be macro'd away.) Hopefully the above digression supports my case that being explicit everywhere just to close gaps that can be automatically closed by simple (and easily human comprehensible) algorithms can make programs much harder to read, and hence harder to understand and detect algorithmic errors. I'd prefer only to have to put in type decls for identifiers only when the compiler genuinely can't use a simple algorithm to deduce the unique interpretation that fits,PROVIDING THIS ALGORITHM IS SUFFICIENTLY SIMPLE THAT YOU CAN APPLY IT IN YOUR HEAD. If not then I suppose being explicit everywhere does become a better way to go. ___cheers,_dave__ email: [EMAIL PROTECTED] "All shall be well, and all shall be www.cs.bris.ac.uk/~tweed/pi.htm well, and all manner of things work tel: (0117) 954-5253 shall be well."
RE: Haskell 2 -- Dependent types?
As a C++ user (with a background in categories) patiently waiting for something a lot better, I personally favour two principles: 1. let's go for undecidable type checking. I want the compiler to be able to do as much work as possible: ideally, everything that can be resolved at compile time should be if only we can express this correctly. 2. in the face of the above, we need to give the compiler more guidance. Personally, I favour type declarations everywhere: all identifiers should be introduced as being of a particular specified type. Of course, whether these principles are compatible with Haskell it another question... -Original Message- From: Lennart Augustsson [mailto:[EMAIL PROTECTED]] Sent: 17 February 1999 10:26 To: [EMAIL PROTECTED] Cc: [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED] Subject: Re: Haskell 2 -- Dependent types? I'm not sure that anybody has "accepted" undecidable type checking. People using Gofer or C++ seem to have. -- Lennart
Re: Haskell 2 -- Dependent types?
On 16 Feb 1999, Carl R. Witty wrote: Lars Lundgren [EMAIL PROTECTED] writes: We have already accepted undecidable type checking, so why not take a big step forward, and gain expressive power of a new magnitude, by extending the type system to allow dependent types. Wait a minute...who has accepted undecidable type checking? Are you talking about the new type class features in GHC? As far as I know, those are explicitly documented as experimental, and must be enabled by a command-line option. I'm not sure that anybody has "accepted" undecidable type checking. Yes, I was refering to various experimental features in Gofer, and recently also in GHC. I should not have used the word 'accepted' as I did. What I meant was that since those features are candidates for haskell 2, (At least, it is my impression that they are) we can also consider other extensions wich leads to undecidable type checking. Of course, this is not a desirable property, but it may not be that bad in practice. The type checker can use some default which works in in 95% of the programs, and the really complex programs can be checked by using a compiler flag which increases some limit. Decidability should not be given up to easily, but i think that dependent types has a very good price/performance ratio. /Lars L
Re: Haskell 2 -- Dependent types?
On 16-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote: I'm not sure that anybody has "accepted" undecidable type checking. I think it's becoming clear by now that the theoretical disadvantages of undecidable type checking are often not significant in practice. Experience with C++, Gofer, ghc, Mercury, etc. all seems to confirm this. So if undecidability per se is used as an argument against any particular proposal for extending the type system, I think that argument should be considerd a rather a weak one. -- 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.
XML Haskell (Was: Re: Haskell 2 -- Dependent types?)
Alexander Jacobson [EMAIL PROTECTED] writes: * facilitate better integration with other languages/systems For example, it would be nice to be able either to generate a Haskell datatype from an XML DTD or to generate a XML DTD from a Haskell datatype. Funnily enough, that's exactly what we're working on at the moment. We already have the part which converts an arbitrary Haskell datatype to an XML DTD (and values of that type to an XML document). We are part-way through the other angle, starting from an arbitrary XML DTD and deriving a Haskell datatype for it (and the functions which parse an XML document to a value of that type, and pretty-print the value back to a document.) These are written partially using DrIFT (i.e. the "derive" tool) - which has turned out to be a remarkably pleasant experience. We also have a prototype combinator library for manipulating XML documents in a generic manner (i.e. using a single generic tree structure for all documents, rather than document-specific types and values). If anyone is interested in any of these facilities, drop us an email. Regards, [EMAIL PROTECTED] [EMAIL PROTECTED]
Re: XML Haskell (Was: Re: Haskell 2 -- Dependent types?)
Alexander Jacobson [EMAIL PROTECTED] writes: * facilitate better integration with other languages/systems For example, it would be nice to be able either to generate a Haskell datatype from an XML DTD or to generate a XML DTD from a Haskell datatype. Funnily enough, that's exactly what we're working on at the moment. We already have the part which converts an arbitrary Haskell datatype to an XML DTD (and values of that type to an XML document). We are part-way through the other angle, starting from an arbitrary XML DTD and deriving a Haskell datatype for it (and the functions which parse an XML document to a value of that type, and pretty-print the value back to a document.) These are written partially using DrIFT (i.e. the "derive" tool) - which has turned out to be a remarkably pleasant experience. There's another alternative available: asdlGen http://www.cs.princeton.edu/zephyr/ASDL/ "ASDL descriptions describe the tree-like data structures such as abstract syntax trees (ASTs) and compiler intermediate representations (IRs). Tools such as asdlGen automatically produce the equivalent data structure definitions for C, C++, Java, Standard ML, and Haskell. asdlGen also produces functions for each language that read and write the data structures to and from a platform and language independent sequence of bytes. The sequence of bytes is called a pickle. " I think there's also some support for XML. I'm not sure if asdlGen can do all that Malcolm and Colin's package will do, though. In any case, I find the ability to write a pickle from C and read back from Haskell quite useful. Two relevant papers are: "Early Experience with ASDL in lcc", Software-Practice and Experience, to appear. "A Machine-Independent Debugger-Revisited", Microsoft Research TR 99-4 both available at http://www.research.microsoft.com/~drh/ If anyone is interested in any of these facilities, drop us an email. Do keep the mailing list informed of your progress! Regards, Fermin Reig
Re: Haskell 2 -- Dependent types?
I read cayenne.ps and it went somewhat over my head. I could not get a good sense of when in practice I would really want to use this. This is not an objection, just a request for explanation... As far as the type system goes, what would be more useful to me is something preprocessor functionality, like Derive or PolyP, more integrated into the language. In one feature, this would: * eliminate the obnoxiously ad-hoc deriving construct * facilitate better integration with other languages/systems For example, it would be nice to be able either to generate a Haskell datatype from an XML DTD or to generate a XML DTD from a Haskell datatype. Similarly, it would also be useful to save Haskell datatypes into SQL databases automatically (I built something like this w/ Derive). * reduce the need for separate preprocessor systems like HDirect One could write a type function that would package haskell datatypes for use by COM and Java components. i.e. one could write code in PolyP that would convert a Haskell type in to a Java type... without doing through as much of the preprocessor homework associated with HDirect. Or the flip side is that one could construct Haskell types from an IDL again without a separate system. (You just need to have a standard FFI as well). -Alex- ___ S. Alexander Jacobson Shop.Com 1-212-697-0184 voiceThe Easiest Way To Shop On Tue, 16 Feb 1999, Lars Lundgren wrote: The trend seems to be define wishes for haskell 2, so here are mine: We have already accepted undecidable type checking, so why not take a big step forward, and gain expressive power of a new magnitude, by extending the type system to allow dependent types. Cayenne, http://www.cs.chalmers.se/~augustss/cayenne, already has dependent types, but seems to be an experimental language only with a very small user base. Just a thought. /Lars L
Re: Haskell 2 -- Dependent types?
Lars Lundgren [EMAIL PROTECTED] writes: We have already accepted undecidable type checking, so why not take a big step forward, and gain expressive power of a new magnitude, by extending the type system to allow dependent types. Wait a minute...who has accepted undecidable type checking? Are you talking about the new type class features in GHC? As far as I know, those are explicitly documented as experimental, and must be enabled by a command-line option. I'm not sure that anybody has "accepted" undecidable type checking. Carl Witty [EMAIL PROTECTED]
