Re[4]: ADT views Re: [Haskell] Views in Haskell
Hello J., Thursday, February 1, 2007, 1:36:33 AM, you wrote: Yes - you've reiterated Wadler's original design, with an automatic problems with equational reasoning raised by this approach. ok, i can live without it. i mean reasoning :) i guess that anything more complex than Turing machine makes reasoning harder. 18 years ago Haskell fathers chosen to simpilfy language in order to make reasoning easier. may be now we can change this decision? that i've proposed is made on basis of my 15 years of software development experience and i'm sure that abstraction of data representation is very important issue (and much more important than reasoning for practical programming) -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Global variables
The trick of controlling allocation of external resources by using NOINLINE, unsafePerfromIO, and IORef to create global variables has become an indispensable technique in Haskell. It seems to work well enough with most current compilers. However, it is well known that the semantics of NOINLINE are not sufficient to guarantee that this is safe. In principle, the runtime is permitted to GC and reinstantiate these things at any time. Also, it would be nice if we could have a guarantee that global constants are not instantiated until first use. That would allow us to skip the IORef in some cases. I think this issue needs to be addressed in Haskell'. (If it has already, please accept my apologies.) Since NOINLINE has more general use, perhaps there should be a new pragma for this purpose. Thanks, Yitz ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ADT views
Bulat Ziganshin wrote: ok, i can live without it. i mean reasoning :) i guess that anything more complex than Turing machine makes reasoning harder. 18 years ago Haskell fathers chosen to simpilfy language in order to make reasoning easier. may be now we can change this decision? that i've proposed is made on basis of my 15 years of software development experience and i'm sure that abstraction of data representation is very important issue (and much more important than reasoning for practical programming) No. Abstractions should (and mostly do) make reasoning easier, not harder, by having clear semantics, suited to the problem domain. The ability to reason about your program is vital in about every part of the programming cycle, and is one of the things that make Haskell work. Another of those things is abstraction of data representation, you're right about that. But I think there is no conflict between those goals. In fact, all the views proposal does is to give the natural meaning to the equation f (v x) = h x , by letting the programmer specify a partial inverse for 'v'. Greetings, Arie ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
A view of views -- something classy? Re: [Haskell] Views in Haskell
Bulat Ziganshin [EMAIL PROTECTED] writes: Yes - you've reiterated Wadler's original design, with an automatic problems with equational reasoning raised by this approach. ok, i can live without it. i mean reasoning :) That's probably not good, but I don't follow that problem yet. I'm afraid I've not had the stamina to follow this thread properly, and I doubt if I'll get any more stamina soon, so let me make a proposal not too disimilar to Bulat's and just hope that people find it appealing enough to flesh it out. The idea I'm presenting is simple enough: allow data constructors as members of classes. (Sure, David, this does have the problem of hiding potentially expensive operations as straightforward pattern matches, but that's abstraction for you). So class Sequence s where (some other stuff) Cons:: a - s a - s a Nil:: s a Here Cons and Nil both stand for two things: a constructor and a deconstructor. The question is how to specify the values of the two parts when giving an instance. The easiest way is just to give it in terms of something that already has the two aspects: instance Sequence [] where ... Cons = (::) Nil = [] And so a definition like f Nil = ... f (Cons a l) = ... gets a type like Sequence s = s a - ... But we also want it to work for cases where the type we are viewing doesn't already have a constructor that does what we want, such as giving a list instance for another member of Sequence: class Sequence s where Snoc:: s a - a - s a (some other stuff) The idea here would be to announce that all data constructors really do have two parts and they are accessed via qualified names. So the Snoc part of the list instance would look like this: ... Snoc.construct l x = l ++ [x] Snoc.deconstruct f g [] = g Snoc.deconstruct f g l = f (init l) (last l) (We can of course argue about the precise type used for deconstructors and there is endless bikeshed painting to be done for the names construct and deconstruct, but I hope this gives the general idea). I think this proposal is simpler than the earlier ones presented -- enough that someone in better shape than me could work out the details and implement it. There's no exciting new syntax, just an extension of some current syntax to a new area, and functions declared using a view are automatically overloaded for everything that shares the view. As far as equational reasoning goes, I think the approach would be to specify what laws Foo.construct and Foo.deconstruct have to follow to preserve it, and leave them up to the programmer to respect (in the same way that the monad laws aren't tested by the compiler). -- Jón Fairbairn [EMAIL PROTECTED] ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: help from the community?
Taral wrote:
On 1/31/07, Conor McBride [EMAIL PROTECTED] wrote:
So, as far as Haskell' is concerned, I'd favour forbidding non-empty
cases, but only because I favour having some more explicit syntax for
empty cases, further down the line.
I see nothing wrong with case x of {}, with required braces. The
layout rule never generates empty braces.
main = do
a - do
b - something
case b of
return a
Doesn't the layout rule convert the above to:
main = do { a - do { b - something; case b of {}}; return a}
^^
empty braces
In any case I thought the layout rule was supposed to be regarded as just a
convenience rather than making a distinction between explicit braces and
braces added by the rule?
Also, can anyone explain why empty case constructs are needed? Why not just
write undefined?
Brian.
--
http://www.metamilk.com
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Global variables
Hi Bulat, You wrote: there is common proposal that i support. example of its use: i :: IORef Int i - newIORef 1 with a semantics equivalent to current use of usafePerformIO+INLINE in GHC Are the details of this posted anywhere? Is there a ticket for this? I assume you mean that this will work for anything in the IO monad, not just newIORef. I really like this approach - it is much cleaner than a pragma with unsafePerformIO. Regards, Yitz ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Global variables
On 01/02/07, Bulat Ziganshin [EMAIL PROTECTED] wrote:
there is common proposal that i support. example of its use:
i :: IORef Int
i - newIORef 1
with a semantics equivalent to current use of usafePerformIO+INLINE in GHC
I think that's too safe-looking. Anything that translates to something
involving unsafe* should be tagged with 'unsafe' somewhere as well.
Also, as unsafe* is still compiler specific, I think a pragma is
probably most appropriate:
{-# GLOBAL-MUTVAR #-}
i :: IORef Int
i = unsafePerformIO (newIORef 1)
--
-David House, [EMAIL PROTECTED]
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Global variables
On Thu, 1 Feb 2007, David House wrote:
I think that's too safe-looking. Anything that translates to something
involving unsafe* should be tagged with 'unsafe' somewhere as well.
Also, as unsafe* is still compiler specific, I think a pragma is
probably most appropriate:
{-# GLOBAL-MUTVAR #-}
i :: IORef Int
i = unsafePerformIO (newIORef 1)
There might be a more sensible way to handle it while retaining the meat
of Bulat's proposal, but I don't think it can really be done without
making significant changes to the module system - it amounts to having
initialiser actions, and once you've got those there're all sorts of
things that rapidly become desirable. I've had a couple of occasions where
being able to treat an entire module as being within a monad or an arrow
could've been used to good effect though.
--
[EMAIL PROTECTED]
The reason for this is simple yet profound. Equations of the form
x = x are completely useless. All interesting equations are of the
form x = y. -- John C. Baez
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ADT views Re: [Haskell] Views in Haskell
On Wed, Jan 31, 2007 at 09:28:30PM +0300, Bulat Ziganshin wrote: Wednesday, January 31, 2007, 7:12:05 PM, you wrote: data Coord = Coord Float Float view of Coord = Polar Float Float where Polar r d= Coord (r*d) (r+d)-- construction Coord x y | x/=0 || y/=0 = Polar (x*y) (x+y)-- matching This is somewhat pretty, but in spite of your desire to avoid creating new syntax, you have just done so, and in the process made views more limited. Pattern matching sytax remains the same, but a new declaration syntax has been added. And now in order to pattern match on a function it needs to explicitely be declared as a view. yes. among the possible uses for views i clearly prefers the following: definition of abstract data views that may differ from actual type representation. moreover, i think that this facility should be syntactically indistinguishable from ordinary data constructor patterns in order to simplify learning and using of language. *defining* view is a rare operation, using it - very common so my first point is that views should be used in just the same way as ordinary constructors, both on left and right side: f (Polar r a) = Polar (r*2) a I guess your assumption that views will rarely be defined is rather in conflict with the proposal of Simon, which was to create considerably more powerful views, I presume. Next, i don't think that ability to use any functions in view buy something important. pattern guards can be used for arbitrary functions, or such function can be used in view definition. view, imho, is not a function - it's a two-way conversion between abstract and real data representation which has one or more alternative variants - just like Algebraic Data Types. so, when defining a view, i want to have ability to define exactly all variants alternative to each other. for another representation, another view should be created. so But you *are* using functions in views, that's what they are. And the two-way conversion, while pretty, is likely to be a fiction. It'll be too easy (and useful) for someone to define view RegexpMatch String of String where string | matchesRegexp regexp string = RegexpMatch regexp RegexpMatch regexp = undefined f (RegexpMatch foo.+bar) = It has foo bar in it f s@(RegexpMatch baz.+bar) = s ++ has baz bar in it You can pretend that noone will do this, but it's a nice syntax for pattern guards, which allows us to stick the guard right next to the data being guarded, which is often handy. So I guess you can see this as a promise to subvert your two-way conversion views immediately after they're created. It's worth considering whether one should try to make the syntax friendlier to such uses. One option which is sort of in between would be something like: view regexpMatch String of String where string | matchesRegexp regexp string = regexpMatch regexp f (regexpMatch foo.+bar) = It has foo bar in it f s@(regexpMatch baz.+bar) = s ++ has baz bar in it where the lowercaseness of regexpMatch indicates that this is a one-way matching function. I believe this would work just fine, and then we'd have a bit of new syntax for function-like views, and your constructor-like syntax for constructor-like views. And noone would be tempted to subvert your constructor-like views. And good programmers would have a policy that constructor-like views would really be invertible, for some definition of invertible, analogous to the monad laws, which aren't enforced, but reasonable programmers obey. view Polar Float Float of Coord where constructor (Polar r a) means (Coord (r*sin a) (r*cos a)) match pattern (Polar (sqrt(x*x+y*y)) (atan(y/x))) for (Coord x y) where x/=0 (Polar y (pi/2))for (Coord x y) where y0 (Polar (-y) (-pi/2))for (Coord x y) where y0 of course, my syntax is cumbersome. that is important is that view definition should be explicit (no arbitrary functions), it should mention all possible alternatives and provide a way to use the same constructor name both for construction of new values and matching existing ones. this all together should allow to transparently use ADT views instead of plain ADTs I definitely agree that being able to transparently switch a library between views and exported constructors would be handy, but don't think it's necesary, provided the view syntax is sufficiently elegant (which I'm not convinced Simon's proposed syntax is). If views have a distinct--but pretty--syntax, people can just move to always using views, and that's that. And unless you are planning to allow one-way views (you don't give any examples of that), view functions must be invertible, which greatly weakens their power. If you choose to allow one-way views (non-invertible functions), then I'd vote for not allowing two-way views, as it adds complexity without adding any appreciable
Re: Global variables
On 2007 Feb 1, at 11:51 AM, David House indited:
On 01/02/07, Bulat Ziganshin [EMAIL PROTECTED] wrote:
there is common proposal that i support. example of its use:
i :: IORef Int
i - newIORef 1
with a semantics equivalent to current use of usafePerformIO
+INLINE in GHC
I think that's too safe-looking. Anything that translates to something
involving unsafe* should be tagged with 'unsafe' somewhere as well.
Also, as unsafe* is still compiler specific, I think a pragma is
probably most appropriate:
{-# GLOBAL-MUTVAR #-}
i :: IORef Int
i = unsafePerformIO (newIORef 1)
Hear hear!
As a Haskell newbie things are hard enough to keep straight without
that kind of magical unsafe stuff going on.
Just sayin'
--D'gou
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: ADT views Re: [Haskell] Views in Haskell
On Thu, Feb 01, 2007 at 09:12:02AM -0800, David Roundy wrote: On Wed, Jan 31, 2007 at 09:28:30PM +0300, Bulat Ziganshin wrote: Next, i don't think that ability to use any functions in view buy something important. pattern guards can be used for arbitrary functions, or such function can be used in view definition. view, imho, is not a function - it's a two-way conversion between abstract and real data representation which has one or more alternative variants - just like Algebraic Data Types. so, when defining a view, i want to have ability to define exactly all variants alternative to each other. for another representation, another view should be created. so But you *are* using functions in views, that's what they are. And the two-way conversion, while pretty, is likely to be a fiction. It'll be too easy (and useful) for someone to define view RegexpMatch String of String where string | matchesRegexp regexp string = RegexpMatch regexp RegexpMatch regexp = undefined Never mind. I see that this won't work, and it's not so easy to usefully get around your restrictions. But I must admit that this power was one of the nicest things in Simon's proposal. You'd still be in danger of me subverting your proposal with something like view Odd of Int where i | isOdd i = Odd Odd = undefined but I'll admit that this isn't particularly powerful. It's allowing arguments to the match (e.g. the regexp I was trying to sneak through) that gives Simon's views their power. It's also what forces the syntactic complexity of the - in the matches, since you need a way to distinguish the arguments from the patterns in something like f (foomatch x y z) -- David Roundy Department of Physics Oregon State University ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: help from the community?
Here are some of my comments to Iavor's proposals: Notation for Schemes PROPOSAL: be liberal: allow empty quantifier lists allow variables that are not mentioned in the body of a type (but warn) allow predicates that do not mention quantified variables (but warn?) For the reasons that others have expressed, I prefer that we not be liberal here. I think we should reject the first two cases. I'm ambivalent about the last one. I don't think we want to allow types like: forall . Int or forall a b. Int These types are mostly bugs. Furthermore, rejecting them doesn't limit expressiveness: they should both be equivalent to Int, so user could just write Int. I can't really think how allowing these types extends the expressiveness of the language, nor can I imagine a situation where someone would prefer seeing one of these types instead of Int. And in fact, given restrictions on higher-rank and impredicativity, Int would be a much better type to use. (This issue is *slightly* related to the one below. Perhaps different answers for that question may interact with this one.) On the other hand, perhaps there is uses for types like C a = a - a where a is bound in some external context? The last issue doesn't seem very straightforward to me. Equivalence for type schemes PROPOSAL: Use syntactic equivalence modulo alpha renaming order/repetition of predicates (i.e. compare predicates as sets) This proposal doesn't go as far as entailment---which would equate the types forall . Int and Int. And also types that are not alpha-equivalent but differ only in the order of quantification: i.e. forall a b. (a,b) - a =/= forall b a. (a,b) - a are *not* alpha equivalent, but it would be nice if they were semantically equivalent. I guess at this point we need to hear from implementors about how difficult it would be to implement semantic entailment? Is there another point in the space between syntactic equivalence and full entailment? (i.e. normalize types in some way and then compare them?) Higher-rank types and data constructors I'll chime in and say that I'm in favor of rank-n over rank-2 types, and I would like to allow subexpressions to have higher-rank types as well. As a user (not an implementer) I find this to be the easiest to think about, as I only have to worry about the difference between monotypes and polytypes where type inference is concerned. If my program doesn't typecheck, I need only add more annotations. I don't need to rewrite the code. About this example: data T = C1 Int (forall a. (Eq a, Show a) = a - a) | C2 (forall a. (Show a, Eq a) = a - a) h :: a - a - Int h _ _ = 1 test= h (C1 1) C2 Note that even if partial applications (of constructors and other higher-rank functions) are allowed, in this example would still be rejected because it requires impredicative polymorphism. However, -- type abbreviation for convenience type U = forall a. (Eq a, Show a) = a - a h :: U - U - Int h _ _ = 1 test = h (C1 1) C2 should be accepted if we chose the proposal for type scheme equivalence above. ---Stephanie On Jan 25, 2007, at 5:39 PM, isaac jones wrote: On Sun, 2007-01-21 at 14:25 -0800, Iavor Diatchki wrote: Hello, I have written some notes about changes to Haskell 98 that are required to add the polymorphic components extension. The purpose of the notes is to enumerate all the details that need to be specified in the Haskell report. I don't have access to the haskell-prime wiki so I attached the notes to the ticke for polymorphic components: http://hackage.haskell.org/trac/haskell-prime/ticket/57 When there are different ways to do things I have tried to enumerate the alternatives and the PROPOSAL paragraph marks the choice that I favor. Does anyone have any feedback on this work? The critical path for Haskell', at this point, is writing these bits of the report and having them validated by the community. But no one has read and commented on these topics: - Plans for changes to the report relating to Polymorphic Components - Draft changes to the report for pattern guards I understand that taking the time to pour over the report is a bit hard, but we desperately need people who are willing to do so if we're going to make progress. I think Iavor and I will start to make these changes tomorrow; does anyone have feedback before then? peace, isaac ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Global variables
(CCing the list as this is of general concern.) On 01/02/07, Yitzchak Gale [EMAIL PROTECTED] wrote: Why is this unsafe? What could go wrong? It could segfault due to the type safety properties that unsafePerformIO breaks: import System.IO.Unsafe import Data.IORef ref :: IORef [a] ref - newIORef [] main = do writeIORef ref [42] val - readIORef ref print (val :: [Char]) If you use the pragma you're forced to import unsafePerformIO and hopefully check the haddock docs [1] where this issue is listed. [1]: http://haskell.org/ghc/docs/latest/html/libraries/base/System-IO-Unsafe.html -- -David House, [EMAIL PROTECTED] ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: help from the community?
On 1 Feb 2007, at 21:31, Jacques Carette wrote: Stephanie Weirich wrote: I don't think we want to allow types like: forall . Int or forall a b. Int These types are mostly bugs. Furthermore, rejecting them doesn't limit expressiveness: If you restrict yourself to programs entirely written by humans, I agree completely. But if you consider programs written by programs (say Template Haskell to be specific, but it could be via many other means), such degenerate types occur rather often. I find the program-generated code argument rather weak. In that past it was used to justify all kinds of minor horrors like excess commas in lists and so on. But if one can write a program to generate syntactically valid but ugly code, one can easily spend a little extra effort on making the result beautiful too. After all, which is the more difficult task - devising the auto-coding schema, or pretty-printing? There is no reason to accept ugly coding practices just because it makes the auto-coder's job slightly simpler. That only encourages humans to use sloppy practices in hand- written code as well. Regards, Malcolm ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: help from the community?
Malcolm Wallace wrote: I find the program-generated code argument rather weak. One might satisfy both camps by having a compiler flag to allow auto-generated ugliness. -- Ashley Yakeley ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: help from the community?
Malcolm Wallace wrote: If you restrict yourself to programs entirely written by humans, I agree completely. But if you consider programs written by programs (say Template Haskell to be specific, but it could be via many other means), such degenerate types occur rather often. I find the program-generated code argument rather weak. In that past it was used to justify all kinds of minor horrors like excess commas in lists and so on. But if one can write a program to generate syntactically valid but ugly code, one can easily spend a little extra effort on making the result beautiful too. I used to think so too - but some very hard-won experience [1] has changed my mind. Generating good code is very hard. And if you are doing it in a typeful way (see [1] again), you may not be able to spend a little extra effort to make the results beautiful, because typeful code does not let you do introspection very easily. I will agree with you on one aspect: if the program-generated code done by untyped manipulations, then writing a small type-simplifier is pretty easy, and my argument is weak. But this is Haskell we're talking about, and one should really hope that TH will eventually be typed, no? After all, which is the more difficult task - devising the auto-coding schema, or pretty-printing? If pretty-printing was all there was to it, I would not have made this comment. Pretty-printing is indeed easy. Typeful type-level programming is quite hard. Jacques [1] http://www.cas.mcmaster.ca/~carette/metamonads/ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Global variables
On Thu, Feb 01, 2007 at 04:51:39PM +, David House wrote: I think that's too safe-looking. Anything that translates to something involving unsafe* should be tagged with 'unsafe' somewhere as well. Also, as unsafe* is still compiler specific, I think a pragma is probably most appropriate: then pretty much everything will have to be 'unsafe' :) look inside of how the libraries are implemented and they all involve unsafe operations at some point, 'unsafe' does not mean unsafe always, it means it is up to the user to provide proofs of certain properties rather than the compiler. when such a proof is provided and abstracted by an API, then it is safe. As to this particular extension, depending on the exact details it can be safe or unsafe and make different demands on the implementation. luckily, pretty much all of this was worked out in a discussion a while ago, the trick was to create a new type 'ACIO' which contained only 'good' top level operations. There will be an 'unsafeIOToACIO' of course, I mean, ACIO functions have to be implemented somehow. :) John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: help from the community?
On 2007 Feb 1, at 4:53 PM, Malcolm Wallace indited: I find the program-generated code argument rather weak. In that past it was used to justify all kinds of minor horrors like excess commas in lists and so on. ... That only encourages humans to use sloppy practices in hand-written code as well. Oh, you mean something like: x = ( asdf, qwer, -- ... foobar, ) Cause I really want to have to fark around with that stoopid ass last comma when I rearrange the order of the itmes in my tuple (or list). Gah, gratuitous syntax pain for what actual benefit? Pisses off users so that some domineering compiler writer can feel smug 'bout 'mself. Feh. Feh^2. It isn't sloppy, it is REGULAR. It is easy to use that trivial human eye/brain pattern matching to see that it _is_ correct. But maybe this is off topic. Sorry, I don't know if that is troll bait or not... --D'gou ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Polymorphic components, so far
Hello, Thanks to everyone who took time to comment on my notes. My Isaac's previous post spawned a few separate discussions so I though I'd send a separate message to summarize the status of what has happened so far with regard to polymorphic components. * Rank-2 vs Rank-n types. I think that this is the most important issue that we need to resolve which is why I am placing it first :-) Here are our options: - option 1: Hugs style rank-2 types (what I described, very briefly) - option 2: GHC 6.4 style rank-2 types. As far as I understand, these are the details: * Based on Putting Type Annotations to Work. * Predicative (type variables range only over simple (mono) types) We do not need to compare schemes for equality but, rather, we compare them for generality, using a kind of sub-typing. There * Notation for polymorphic types with explicit quantifiers. The main issue is if we should allow some corner case notational issues, such as empty quantifier lists, and quantified variables that are not mentioned in the type. - option 1: disallow these cases because they are likely to be accidental mistakes. - option 2: allow them because they make automatic program generation simpler. My initial proposal was suggesting 2 but I think that, having heard the arguments, I am leaning towards option 1. * Equality of schemes for labeled fields in different constructors. My suggestion did not seem to be too controversial. Stephanie is leaning towards a more semantic comparison of schemes. Indeed, just using alpha equivalence might be a bit too weak in some cases. Another, still fairly syntactic option, would be to pick a fixed order for the variables in quantifiers (e.g., alphabetic) for the purposes of comparison. * Pattern matching on polymorphic fields. This does not appear to be too controversial, although Atze had some reservations about this design choice. This is all that I recall, apologies if I missed something (if I did and someone notices, please post a replay so that we can keep track of what is going on). -Iavor ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Polymorphic components, so far
Hello, (Apologies for the two emails, I accidentally hit the send button on my client before I had finished the first e-mail...) * Rank-2 vs Rank-n types. I think that this is the most important issue that we need to resolve which is why I am placing it first :-) Our options (please feel free to suggest others) - option 1: Hugs style rank-2 types (what I described , very briefly, on the ticket) * Based on From Hindley Milner Types to First-Class Structures * Predicative * Requires function with rank-2 types to be applied to all their polymorphic arguments. - option 2: GHC 6.4 style rank-N types. As far as I understand, these are the details: * Based on Putting Type Annotations to Work. * Predicative * We do not compare schemes for equality but, rather, for generality, using a kind of sub-typing. * Function type constructors are special (there are two of them) because of co/contra variance issues. - option 3: GHC 6.6 style rank-N types. This one I am less familiar with but here is my understanding: * Based on Boxy types: type inference for higher-rank types and impredicativity * Impredicative (type variables may be bound to schemes) * Sometimes we compare schemes for equality (this is demonstrated by the example on ticket 57) and we also use the sub-typing by generality on schemes * Again, function types are special So far, Andres and Stephanie prefer a system based on rank-N types (which flavor?), and I prefer the rank-2 design. Atze would like a more expressive system that accepts the example presented on the ticket. I think this is all. -Iavor ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
