Could somebody show an example which requires fundeps and cannot be expressed using a simpler model explained below - a model that I can even understand? Is the model self-consistent at all? Each class is associated with a set of subsets of type variables in its head. Let's call it the set of keys. The intuitive meaning of a key is that types corresponding to these variables are sufficient to determine which instance to choose. They correspond to lhss of some fundeps. Plain classes without explicitly written keys correspond to having a single key consisting of all type variables. Keys influence the typechecking thus: - A type is unambiguous if for every class constraint in it there exists its key such that types in the constraint corresponding to type variables from the key contain no type variables which are absent in the type itself. - All class methods must have unambiguous types, i.e. for each method there must be a key whose all type variables are present in the method's type. - For each key, there must be no pair of instances whose heads projected to the class parameters from the key overlap. - For each class constraint of an unambiguous type an each its key there must be an instance found basing on this key, or the type is incorrect because of missing instances. Moreover, instances found basing on all keys must be identical. - Perhaps something must be said about class contexts and instance contexts. I'm not sure what yet. Examples: class Collection c e | c where empty :: c insert :: c -> e -> c class Monad m => MonadState s m | m where get :: m s put :: s -> m () newtype State s a = State {runState :: s -> (a,s)} instance Monad (State s) instance MonadState s (State s) test1:: Int -> Int test1 x = snd (runState get x) -- Not ambiguous. class IOvsST io st | io, st where -- Two single-element keys. ioToST :: io -> st stToIO :: st -> io instance IOvsST (IORef a) (STRef s a) where ioToST = unsafeCoerce# stToIO = unsafeCoerce# test2:: IORef a -> IORef a test2 = ioToST . stToIO -- Not ambiguous. class Foo a b | a instance Foo Int [a] -- This is rejected by Hugs (with fundep a->b) but I would definitely -- accept it. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Alternatively, I wonder whether the current system of type classes is the right model at all. Although I prefer the Haskell system, I think it is instructive to compare it with the Standard ML (SML) system of structures and functors. My point is that both Haskell and SML impose one of two possible extremes on the user, and suffer for it. With SML, it is as if all instances are explicitly named. SML does not permit user-defined overloading, and so SML is not capable of understanding something such as a "type class of things we can compare", and has a horrible set of kludges to cope with implementing the equality operator. With Haskell, on the other hand, there is no way of referring to a particular instance when you want to. We see a particular consequence of that here, in that (unlike SML), it is not possible to associate an internal type with a given instance. Another problem is that no-one has any control over what instances get exported, because since instances are anonymous there is no way of referring to them. Hence the current procedure is to expose everything to the importer, which is surely a mistake. So if you agree with me up to here, perhaps you are agreed that it is worth while trying to find a middle way, in which we try to combine both approaches. Well I'm not an expert language designer, and I'm doing this off the top of my head late on Thursday evening, so please don't nitpick about syntax; I'm aware that parsing will probably be difficult in all sorts of ways with exactly what I'm writing, but that shouldn't be too hard to tweak. In particular I have followed SML in using "." to express qualification by something, even though Haskell already used "." for something else, because I can't be bothered right now to dig up a better symbol. On the other hand if my whole approach is a pile of elephant dung I apologise for wasting your time, and wish you a happy Christmas/holidays, but do try to find a better way of combining the best of SML functors and Haskell classes. Anyway here is my proposal. (1) We extend type classes to allow them to introduce types. Thus for example I would replace Marcin's first example by class Collectible e where type c -- or we could just omit the "type" keyword, trading clarity -- for conciseness. -- note also that we need a way of expressing a context for -- "c", EG that it's an instance of Eq. empty :: c insert :: c -> e -> c As usual, you can refer to "empty" and "insert" right away, but you can't refer to "c" without extra syntax. We need a way of referring to the particular instance of Collectible. So I suggest something like: singleton :: (method | Collectible e) => e -> method.c singleton el = insert empty el (2) We extend instance declarations in two ways. Firstly and obviously, we need a way of declaring the type c in the instance second declaration. The second thing is to introduce named instance declarations, like this: instance IntList | Collectible Int where type c = [Int] empty = [] insert = (flip(:)) To actually _refer_ to a specific instance, you would qualify with IntList. So you could refer to IntList.c, IntList.empty, IntList.insert, just like you would with SML. But as with Haskell, "empty" and "insert" would continue to be available implicitly. A more complicated example arises when you have instances depending on other instances. EG instance SetCollection | Ord el => Collectible el where type c = Set el empty = emptySet insert = addToSet -- new function, thank Simon Marlow Then, in this case, you would refer to SetCollection.c when you wanted to refer to the type c. However note that in this case we are implicitly using an anonymous use of Ord. Supposing you had previously defined (ignoring questions about overlapping instances for now . . .) instance EccentricOrd | Ord Int where ... and you wanted to define Sets in terms of EccentricOrd. Then I suggest that you use instead SetCollection(EccentricOrd).c and likewise SetCollection(EccentricOrd).empty and Sets(EccentricOrd).insert, though I hope that such monstrous constructions will not often be necessary. When they are, maybe it would be a good idea to allow the user to abbreviate, as in instance EccentricSet | Collectible Int = SetCollection(EccentricOrd) just as you can do in SML. (3) Finally it would be nice to extend the module syntax to allow named instances to be selectively exported and imported, just like variables. If I could ignore all pre-existing Haskell code I would specify that whenever a module has a specific import list, no instances are imported unless specified. However this is politically impossible, so instead I suggest that all anonymous instances continue to be implicitly imported, as now, but that named instances are only imported when named in the import list. EG "import File(instance SetCollection)". Also, I think it would be nice to have something similar to the "qualified" operator, by which class membership is NOT automatically inherited, and would have to be explicitly specified by referring to "SetCollection.insert" or indeed "SetCollection.singleton"; in particular this would provide a clean way of handling overlapping classes. OK, so I realise this is probably not the final answer, but wouldn't it be nice if something along these lines could be got to work?
Thu, 21 Dec 2000 21:20:46 +0100, George Russell <ger@tzi.de> pisze:
So if you agree with me up to here, perhaps you are agreed that it is worth while trying to find a middle way, in which we try to combine both approaches.
I am thinking about a yet different approach. Leave classes and SML structures as they are, and make *records* more flexible, to be used instead of classes if instances are to be manipulated explicitly, and instead of structures if we are using Haskell rather than SML or OCaml, and instead of objects if we are using Haskell rather than some OO language, and as a general way of expressing things behaving like fixed dictionaries of values. I have yet to play more with it. I already have some thoughts and a working preprocessor which translates my extensions to Haskell (with multi-parameter classes and fundeps). -------- GOALS -------- * Replace the current record mechanism with a better one. * Don't require sets of fields of different record types disjoint. It's not only to avoid inventing unique field names, but also to have functions polymorphic over all records containing specific fields of specific types. * Provide a way to specialize existing record types to new types that behave similarly except of small changes. I.e. kind of inheritance. * Since Haskell does not have subtyping, have coercions up the inheritance tree. Overloading functions on record types is not always enough, e.g. to put records in a heterogeneous collection they must be coerced to a common type. * Don't constrain the implementation of field access for different record types. As long as it behaves like a record, it is a record. * Don't constrain the implementation of methods even for the same record type. Since Haskell does not have subtyping, records which would have different types in other languages can have the same type in Haskell, as long as the same interface suffices. * Express keyword parameters of functions. A function might use many parameters refining its behavior which usually have some default values. Old code using that function must not break when more parameters are added. * A piece of code should be understandable locally, independently of definitions and instances present elsewhere. * Have a nice syntax. * Keep it simple and easily translatable to the core language. Fields and methods are really the same thing. Moreover, inheritance is really delegation and coercions are the same things as field accesses as well. Record types are not anonymous, unlike TREX. Field names are born implicitly and live in a separate namespace. Each field name is associated with a class of record types having that field. Instances of these classes are defined implicitly for types defined as records, but can also be given explicitly for any type. -------- FIELD SELECTION -------- A field selection expression of the form expr.label is equivalent to (.label) expr where (.label) :: (r.label :: a) => r -> a is an overloaded selector function. (rec.label:: a) is a syntax for Has_label rec a, where Has_label is the implicitly defined class for this label. Such class would look like this if it were defined as normal classes: class Has_label r a | r -> a where (.label) :: r -> a set_label :: r -> a -> r except that there are no real names Has_label nor set_label. -------- DEFINITION OF RECORD TYPES -------- The definition of a record type: data Monoid e = record zero :: e plus :: e -> e -> e defines the appropriate single-constructor algebraic type and obvious instances: instance (Monoid e).zero :: e where ... instance (Monoid e).plus :: e -> e -> e where ... We can construct values of this type thus: numAddMonoid :: Num e => Monoid e numAddMonoid = record zero = 0 plus = (+) The meaning of such overloaded record creation expressions will be specified later. -------- INHERITANCE -------- Here is another example of a record type definition: data Group e = record monoid :: Monoid e minus :: e -> e -> e neg :: e -> e monoid (zero, plus) x `minus` y = x `plus` neg y neg y = zero `minus` y This record type has three direct members: monoid, minus, and neg. monoid holds its zero and plus. We want to be able to extract zero and plus of a group directly, instead of going through the underlying monoid. We could define appropriate instances: instance (Group e).zero :: e where ... instance (Group e).plus :: e -> e -> e where ... and this is what the inheritance declaration monoid (zero, plus) does automatically for us. So groups too have zero and plus, which are deleagated to the monoid. Seen from outside, these fields are indistinguishable from proper Group's fields. -------- DEFAULT DEFINITIONS -------- minus and neg in Group have default definitions expressed in terms of each other. When making a Group we can provide the definition of either one or both, otherwise both will diverge. We could provide default definitions of inherited methods too. If they had default definition in the supertype, they would be overridden. This is how the system expresses OO methods belonging to a type: by default definitions. They can be overridden in subtypes or at object creation time. How is it done that the default definition of minus refers to the definition of neg which will be supplied later? It is not known yet which fields will be specified at creation time. OTOH at the creation time it is not known which fields have default definitions, because the creation expression is polymorphic over record types containing specific fields and will be instantiated based on the context. There is a standard class defined as follows: class Record r where bless :: r -> r A record creation expression, say: record zero = 0 plus = (+) is a syntactic sugar for a recursively defined object: let this = bless this `set_zero` 0 `set_plus` (+) in this The bless function, named after Perl's mechanism used in a similar context, returns a record with all fields initialized using their default definitions, or bottoms for fields with no defaults. Default definitions refer to other fields through the parameter of bless. As seen above, bless is applied to the record to be constructed, and then fields with values specified at creation time are overridden. That way all field definitions can find right versions of other fields, no matter which were defined together with the type and which were supplied at the creation time. The type of the above record creation expression is (Record r, Num a, Num b, r.zero :: a, r.plus :: b -> b -> b) => r -------- DEFINITION OF BLESS -------- Definition of a record type automatically makes it an instance of the class Record. A field from which some other fields are inherited is initialized to blessed value of the same field taken from the parameter of bless, modified by setting those fields which have default defintions. It sounds complicated but this is what yields right bindings of all definitions. If a type behaves like a record, it is a record. You can make Record instances of arbitrary types, making them constructible using the record syntax. bless should be lazy. Field setters can be strict. -------- UPDATING FIELDS -------- If fields represent state changing over time, they can be mutable references. Fields can also be updated in a functional style, but this is really construction of new objects basing on old ones. Field update syntax is as follows: expr.record label1 = value1 label2 = value2 It is equivalent to simple nested set_label applications. Fields initialized with default definitions will not switch to refer to updated values of other fields! All magic already happened at record creation time. This can be changed in at least two ways. First, you can define instances of appropriate Has_label classes yourself and associate arbitrary magic with field updates. Second, you can make such instance for the field that you want to be a function of other fields instead of putting the field in the record directly. Definitions of two methods of Has_label classes have special syntax: instance (a,b).fst :: a where (a,_).fst = a (_,b).record {fst = a} = (a,b) instance (a,b).snd :: b where (_,b).snd = b (a,_).record {snd = b} = (a,b) I.e. pattern.label is equivalent to (.label) pattern and defines the getter function, and pattern1.record {label = pattern2} defines the setter when applied to the record matching pattern1 and field value matching pattern2. Braces can be omitted, but they make the syntax more clear. -------- SYNTAX DETAILS -------- The record keyword triggers the layout rules. Value definitions after the record keyword look like let bindings. They can be defined by cases with argument patterns on the left of the equal sign. In record type definitions, record creations and record updates definitions of fields can refer to all fields mentioned in those constructs in an unqualified form. They can also refer to a special variable called this, which holds the whole record after construction or update. -------- EXAMPLE -------- This example introduces a feature of renaming fields while inheriting.
data Monoid e = record zero :: e plus :: e -> e -> e
numAddMonoid :: Num e => Monoid e numAddMonoid = record zero = 0 plus = (+)
numMulMonoid :: Num e => Monoid e numMulMonoid = record zero = 1 plus = (*)
data Group e = record monoid :: Monoid e minus :: e -> e -> e neg :: e -> e monoid (zero, plus) x `minus` y = x `plus` neg y neg y = zero `minus` y
numAddGroup :: Num e => Group e numAddGroup = record monoid = numAddMonoid minus = (-) neg = negate
numMulGroup :: Fractional e => Group e numMulGroup = record monoid = numMulMonoid minus = (/) neg = recip
data Ring e = record addGroup :: Group e mulMonoid :: Monoid e addGroup (monoid as addMonoid, zero, plus, minus, neg) mulMonoid (zero as one, plus as times)
numRing :: Num e => Ring e numRing = record addGroup = numAddGroup mulMonoid = numMulMonoid
data Field e = record addGroup :: Group e mulGroup :: Group e addGroup (monoid as addMonoid, zero, plus, minus, neg) mulGroup (monoid as mulMonoid, zero as one, plus as times, minus as div, neg as recip)
instance (Field e).ring :: Ring e where f.ring = record addGroup = f.addGroup mulMonoid = f.mulMonoid f.record {ring = r} = f.record addGroup = r.addGroup mulMonoid = r.mulMonoid
-- Alternatively a Field could consist of a Ring and div + recip. -- The difference is an implementation detail not visible outside. -- The following definition will work with either variant:
numField :: Fractional e => Field e numField = record addGroup = numAddGroup mulGroup = numMulGroup
-------- PROBLEMS -------- If those records are to simulate classes, they should be able to have polymorphic fields. Unfortunately it does not work to have overloaded setters in this case. I don't know a good solution. Similarly we would want to have records with existentially quantified types. Again it does not work to have overloaded getters and setters. Listing all inherited fields can be annoying. It would not really work otherwise, as arbitrary instances for sypertypes can be added at any time. It is not necessary to list all fields: other fields are available through the field we inherit from anyway. It would be desirable to selectively export instances. -------- PROTOTYPE IMPLEMENTATION -------- I have an implementation of this in the form of a preprocessor, based on hssource from ghc-4.11's hslibs. I will polish it and put for downloading to let people play with my records. I hope to have more interesting examples. The difference between this implementation and the above proposal is that types of inherited fields must be given explicitly. This is because delegation instances would otherwise have to have types which are not accepted by ghc, and they would require -fallow-undecidable-instances if they were legal (which is not a surprise because cyclic inheritance makes it impossible to determine the type of the field). I reported the problem under the subject "Problem with functional dependencies" on December 17th. I believe that both problems can be fixed, especially if handling those constructs were inside the compiler. -------- THE REST OF MY REPLY TO GEORGE RUSSELL --------
(1) We extend type classes to allow them to introduce types.
If your classes were expressed as my records, it would roughly correspond to existential quantification. But there are big problems with typechecking in this approach. I hope somebody will invent a solution. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
I also like the approach of generalizing the record system, although I have not evaluated your particular proposal. Speaking of record improvements why is http://www.cse.ogi.edu/~mpj/pubs/lightrec.html not listed on the future of haskell page? has it already been determined to not be in the future of haskell or has no one gotten around to it? Does anyone else read this proposal and drool? Speaking of this proposal does anyone else see parallels between the lightweight modules proposal and the implicit parameters proposal http://www.cse.ogi.edu/~jlewis/implicit.ps.gz as implemented in ghc. in particular implicit parameters seem like they would be able to be implemented as syntatic sugar on the lightweight module system, one could rewrite implicit parameters as every function taking a record which we can call 'imp' now '?foo' can be rewritten as 'imp.foo' and the 'with ?foo = 1' construct can be rewritten as nimp = {imp | foo := 1} and then passing nimp to all called functions. I have not thought this too far thorough so I could be missing something obvious but I think it shows potential at least for the unification of two popular extensions. and I am pretty sure this was too obvious to mention in the lightweight records paper but the section of (.foo) being equivalent to (\{_|foo=v} -> v) seems appropriate. John -- -------------------------------------------------------------- John Meacham http://www.ugcs.caltech.edu/~john/ California Institute of Technology, Alum. john@foo.net --------------------------------------------------------------
Fri, 29 Dec 2000 00:37:45 -0800, John Meacham <john@foo.net> pisze:
I've read it and posted some comments in February 2000. There was no answer AFAIR. Here are they again, slightly edited and extended: I don't understand why to separate kinds of rows and record types, instead of having "a type which is known to be a record type", at least on the level visible for the programmer. So instead of type Point r = (r | x::Int, y::Int) type Colored r = (r | c::Color) type ColoredPoint r = Point (Colored r) p :: {ColoredPoint()} -- Point, Colored, ColoredPoint :: row -> row it would be type Point r = {r | x::Int, y::Int} type Colored r = {r | c::Color} type ColoredPoint r = Point (Colored r) p :: ColoredPoint() -- Point, Colored, ColoredPoint :: recordType -> recordType -- where recordType is something like a subkind of *. -------- It is bad to require the programmers to think in advance that a type is going to be subtyped, and write elaborated type Point r = (r | x::Int, y::Int) ... {Point()} ... instead of simpler type Point = {x::Int, y::Int} ... Point ... which is not extensible. -------- I got used to () as a unit type. It would be a pity to lose it. -------- A minor problem. If tuples are records, field names should be such that alphabetic order gives the sequential order of fields, or have a special rule of field ordering for names of tuple fields... -------- In general I don't quite like the fact that records are getting more anonymous. Magical instances of basic classes? How inelegant. If I want the record type to have an identity, it will have to be wrapped in a newtype, so I must think at the beginning if I will ever want to write specialized insances for it and then all the code will depend on the decision. Currently a datatype with named fields has both an identity and convenient syntax of field access. (And why newtype is not mentioned in section 5.1?) I like name equivalence where it increases type safety. Extensible records promote structural equivalence. Unfortunately the proposal seems to increase the number of irregularities and inelegant rules... If expr.Constructor for a multiparameter constructor yields a tuple, then for an unary constructor it should give a 1-tuple, no? I know it would be extremely inconvenient, especially as newtypes are more used, so I don't propose it, but it is getting less regular. What about nullary constructors - empty tuple? :-) I don't say that I don't like the proposal at all, or that I never wanted to have several types with the same field names. But it is not clean for me, it's a compromise between usability and elegance, and from the elegance point of view I like current records more. Maybe it would be helpful to show how to translate a program with extensible records to a program without them (I guess it's possible in a quite natural way, but requires global transformation of the whole program). -------- Extensible records makes a syntactic difference between field access and function call. So if one wants to export a type abstractly or simply to provide functions operating on it without fixing the fact that they are physically fields, he ends in writing functions like size:: MyRecord -> Int size x = x.MyRecord.size which are unnecessary now, even if size is simply a field. It reminds me of C++ which wants us to provide methods for accessing data fields (for allowing them to be later redefined as methods, and for allowing everything to be uniformly used with "()" after the feature name). Ugh. -------- My new record scheme proposal does not provide such lightweight extensibility, but fields can be added and deleted in a controlled way if the right types and instances are made. The distinction between having a field and having a supertype is blurred. Similarly between having itself a field called foo and having a supertype which has a field called foo. Similarly between creating a record by adding fields to another record and creating a record by putting another record as one of fields. Similarly between casting to a supertype by removing some fields and extracting the supertype represented by a field. An advantage is that the interface of records does not constrain the representation in any way. It's up to how instances are defined, with the provision of natural definitions for records implemented physically as product types. For example supplying a color for a colorless point and the reverse operation can be written thus: addColor :: (Record cp, cp.point :: p, cp.color :: Color) => p -> Color -> cp addColor p c = record point = p; color = c removeColor :: (cp.point :: p) => cp -> p removeColor = (.point) When the following definitions are present: data Point = record x, y :: Int data ColoredPoint = record point :: Point point (x, y) color :: Color these functions can be used as of types addColor :: Point -> Color -> ColoredPoint removeColor :: ColoredPoint -> Point A colored point can be constructed either as in addColor, from a point and a color, or thus: record x = ... y = ... color = ... If ColoredPoint were defined directly as data ColoredPoint = record x, y :: Int color :: Color the previous interface could be *retroactively* reconstructed thus: instance (ColoredPoint).point :: Point where cp.point = record x = cp.x; y = cp.y cp.record {point = p} = cp.record x = p.x; y = p.y Multiple inheritance can be modelled as well. And field renaming during inheritance. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Hello, All this talk about Haskell classes, ML modules and improved record types reminds me of the rumours of a "First Class Modules" system for Haskell, but the only documentation I found was a fairly brief document that looked like an application for a research grant. So... Could somebody explain what a first class module is? How does it differ from a record? What could I do with a first class module (if Haskell provided them)? Thanks -- Adrian Hey
Marcin 'Qrczak' Kowalczyk writes: [...]
My new record scheme proposal does not provide such lightweight extensibility, but fields can be added and deleted in a controlled way if the right types and instances are made.
Johan Nordlander must be on holiday or something, so I'll deputise for him. :-) O'Haskell also has add-a-field subtyping. Here's the coloured point example (from http://www.cs.chalmers.se/~nordland/ohaskell/survey.html): struct Point = x,y :: Float struct CPoint < Point = color :: Color Regards, Tom
On 21-Dec-2000, George Russell <ger@tzi.de> wrote:
(3) Finally it would be nice to extend the module syntax to allow named instances to be selectively exported and imported, just like variables.
Mercury's module system allows instance declarations (which, as in Haskell 98, are unnamed) to be selectively exported. :- module foo. :- interface. :- import_module enum. :- type t. :- instance enum(t). :- implementation. :- instance enum(t) where [ ... ]. Mercury doesn't directly support selective import -- you can only import a whole module, not part of it. But if you really want that you can achieve it by putting each instance declaration in its own nested module. :- module foo. :- interface. :- import_module enum. :- type t. :- module enum_t. :- interface. :- instance enum(t). :- end_module enum_t. :- implementation. :- module enum_t. :- implementation. :- instance enum(t) where [ ... ]. :- end_module enum_t. -- Fergus Henderson <fjh@cs.mu.oz.au> | "I have always known that the pursuit | of excellence is a lethal habit" WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.
Tue, 26 Dec 2000 12:10:55 +1100, Fergus Henderson <fjh@cs.mu.oz.au> pisze:
Mercury's module system allows instance declarations (which, as in Haskell 98, are unnamed) to be selectively exported.
If they could be selectively exported in Haskell, how to make it compatible with the current assumption that they are exported by default? Selective hiding would be weird. Perhaps there should be a separate section for exporting instances. If not present, then everything is exported (as with plain module contents). I hope selective export would help with resolving conflicting instances. There might be a confusion if a function does indeed get a sorted list of objects of type T but it expected a different ordering, but the danger of inability of linking two independent libraries due to an innocent overlapping instance might be worse. As we are at it, it would be nice to be able to specify signatures and other interface details where they belong - in the export list. With a different syntax of the export list; there would be an ambiguity if ..., var1, var2 :: Type, ... gives Type to both variables or only one, and items should be separated by layoutable semicolons. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
A syntax to choose the active instances may be useful, too. E.g.: use EccenticOrd, SetCollection in exp then in exp the instances EccenticOrd, SetCollection are known (or preferred). This is similiar to the open syntax in Cayenne. -- Stefan Karrmann
Marcin 'Qrczak' Kowalczyk writes:
Could somebody show an example which requires fundeps and cannot be expressed using a simpler model explained below - a model that I can even understand? Is the model self-consistent at all?
[a model which uses key constraints instead of functional dependencies] Hi. Try this: class C a b c | b -> c instance C t () t Hugs rejects it. If we try to express C with keys instead of fundeps, the key must contain both a and b, which is equivalent to this: class C a b c | a b -> c instance C t () t Hugs accepts this, but only because the constraint has been weakened to something which can be expressed with keys. It's quite a contrived example, and I'm not sure how it relates to your later statement:
Having types with type variables which are never instantiated nor constrained should be equivalent to having ground types!
Do you have any examples of such a type variable in an instance decl? I'm having trouble imagining it, because I keep running into unnecessary class parameters and overlapping instances. Regards, Tom
Mon, 8 Jan 2001 17:53:35 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
Having types with type variables which are never instantiated nor constrained should be equivalent to having ground types!
Do you have any examples of such a type variable in an instance decl?
Not quite. When the type variable is never instantiated, like in ST (ghc's and hbc's state threads), I don't see fundeps. -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Mon, 8 Jan 2001 17:53:35 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
Having types with type variables which are never instantiated nor constrained should be equivalent to having ground types!
Do you have any examples of such a type variable in an instance decl?
Now I have a practical example where fundeps don't work and keys would work - but the type variable is later instantiated. Let's take Parsec from ghc's libraries which includes the following (this is cut down): data TokenParser = TokenParser { identifier :: Parser String, reserved :: String -> Parser (), operator :: Parser String, reservedOp :: String -> Parser (), parens :: forall a. Parser a -> Parser a} makeTokenParser:: LanguageDef -> TokenParser I would like to express this "first-class module" in my records proposal, to make it extensible (there can be different types similar to TokenParser with similar fields and used polymorphically together with TokenParser). Each record field in my proposal induces a class: class Has_field r a | r -> a where get_field :: r -> a The fundep, or something which allows to find the instance from the type of the record only, is required to make this practical. A type which includes Has_field r a in its context, and includes r but not a in its body, is legal. For non-polymorphic fields it works great. But parens cause trouble: instance Has_parens TokenParser (Parser a -> Parser a) This instance is illegal because of the fundep. What it should mean is: instance Has_parens TokenParser (forall a. Parser a -> Parser a) but this is not possible either. With keys instead of fundeps it works! The first instance is OK. The record type is specified to be a key in all Has_field classes, meaning that the record type alone is sufficient to determine which instance of a field getter to use. It is not always sufficient to determine the exact type of the field, but this is not needed. For example here many types are good because the instance is polymorphic wrt. a type variable used in the field's type. I want keys instead of fundeps! :-) -- __("< Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/ \__/ ^^ SYGNATURA ZASTÊPCZA QRCZAK
Marcin 'Qrczak' Kowalczyk writes:
Mon, 8 Jan 2001 17:53:35 +1300, Tom Pledger <Tom.Pledger@peace.com> pisze:
Having types with type variables which are never instantiated nor constrained should be equivalent to having ground types!
Do you have any examples of such a type variable in an instance decl?
Now I have a practical example where fundeps don't work and keys would work - but the type variable is later instantiated.
Let's take Parsec from ghc's libraries which includes the following (this is cut down):
data TokenParser = TokenParser { identifier :: Parser String, reserved :: String -> Parser (), operator :: Parser String, reservedOp :: String -> Parser (), parens :: forall a. Parser a -> Parser a}
makeTokenParser:: LanguageDef -> TokenParser
I would like to express this "first-class module" in my records proposal, to make it extensible (there can be different types similar to TokenParser with similar fields and used polymorphically together with TokenParser).
Each record field in my proposal induces a class: class Has_field r a | r -> a where get_field :: r -> a
The fundep, or something which allows to find the instance from the type of the record only, is required to make this practical. A type which includes Has_field r a in its context, and includes r but not a in its body, is legal.
For non-polymorphic fields it works great. But parens cause trouble: instance Has_parens TokenParser (Parser a -> Parser a) This instance is illegal because of the fundep. What it should mean is: instance Has_parens TokenParser (forall a. Parser a -> Parser a) but this is not possible either. [...]
Hallo again. The second instance decl expresses the situation better, because it's faithful to the rank-2 polymorphism in TokenParser, i.e. the requirement that the TokenParser constructor's 5th argument have a type at *least* as general as forall a. Parser a -> Parser a. The first instance decl Should we be able to put a local forall in an instance decl? I suspect that we shouldn't in general, because it would cause leaks in the rank-2 polymorphism restrictions. For example: module MA where class C a where f :: () -> a -> () module MB where import MA f' :: C a => a -> () f' = f () module MC where import MA instance C (forall a. a -> a) where f z g = if g True then g () else z If any other module imports both MB and MC, the partial application of f in MB will break the "maximal function application subexpressions must include arguments for all rank-2 polymorphic parameters" restriction. (I don't actually know the purpose of this restriction and its friends, but I'm sure there's a good reason for them.) Trex avoids the question of field types in contexts, by using a Lacks context which only mentions the row type and the label. Is the combination of Trex and newtype worth another look? This sort of thing: newtype T1 a = T1 {unT1 :: Rec (foo :: a)} newtype T2 a = T2 {unT2 :: Rec (foo :: a, bar :: a)} Regards, Tom
| Now I have a practical example where fundeps don't work and keys | would work - but the type variable is later instantiated. | ... | Each record field in my proposal induces a class: | class Has_field r a | r -> a where | get_field :: r -> a | | The fundep, or something which allows to find the instance from the | type of the record only, is required to make this practical. A type | which includes Has_field r a in its context, and includes r but not a | in its body, is legal. | | For non-polymorphic fields it works great. But parens cause trouble: | instance Has_parens TokenParser (Parser a -> Parser a) | This instance is illegal because of the fundep. What it should mean is: | instance Has_parens TokenParser (forall a. Parser a -> Parser a) | but this is not possible either. Let's explore the design space a little more carefully. There's a wide spectrum of options, and it's not yet entirely clear which one Marcin is referring to by "keys". Perhaps it will be one of the entries on the following list: 0) "Standard multiple parameter classes": A class constraint Has_parens r a does not imply any connection between the different parameters, and a type like Has_parens r a => r is ambiguous. This kind of class has its uses, but also tends to lead to ambiguity problems. It doesn't address Marcin's needs. 1) "A weaker notion of ambiguity" (title of Section 5.8.3 in my dissertation, which is where I think the following idea originated): We can modify the definition of ambiguity for certain kinds of class constraint by considering (for example) only certain subsets of parameters. In this setting, a type P => t is ambiguous if and only if there is a variable in AV(P) that is not in t. The AV function returns the set of potentially ambiguous variables in the predicates P. It is defined so that AV(Eq t) = TV(t), but also can accommodate things like AV(Has_field r a) = TV(r). A semantic justification for the definition of AV(...) is needed in cases where only some parameters are used; this is straightforward in the case of Has_field-like classes. Note that, in this setting, the only thing that changes is the definition of an ambiguous type. A similar weakening of the notion of ambiguity is permitted by each of the following points in the design space. 2) "Partial dependencies": At this point in the spectrum, we allow the values of one or more class parameters to specify something about the shape of the values of the other parameters, without uniquely determining them. This is perhaps closest to what Marcin is asking for in the text included above. For his example, a partial dependency might ensure that the type t in any constraint of the form Has_parens TokenParser t is of the form Parser a -> Parser a for *some* a, which may be chosen in different ways at each use. My old work on improvement provides a theoretical foundation for this. And, in fact, an unimplemented proposal for supporting this kind of extension is included in the source code for Hugs (subst.c), predating functional dependencies by several years. With the syntax used there, the improvement would be specified as follows: instance Has_parens TokenParser (Parser a -> Parser a) improves Has_parens TokenParser b where ... The idea here is to use improvement at the level of individual instances, whereas functional dependencies use improvement at the level of whole classes. Given a declaration instance P => p where ... we expect the instance to be used for any constraint that matches p. If an improves clause is specified, possibly with multiple predicates, as in: instance P => p improves p1, ..., pn where ... then we expect p to be a substitution instance of each of p1, ..., pn, and we expect the instance to apply to any constraint that matches one (or more) of p1, ..., pn, with an appropriate improving substitution applied to bring it into line with p. 3) "Underspecified/Inferred Functional Dependencies": Here, we insist that the values of certain parameters in a constraint are *uniquely* determined by the values of other parameters ... but we allow the values of the determined types to be inferred rather than declared explicitly. For example, one might write: instance C Int b where ... and then leave type inference to figure out that the value for b in this particular instance must actually be Bool (say). I don't know whether anyone has seriously explored this point in the design space, in particular to determine conditions under which we can be sure that missing parameters can be inferred, or to come up with a good, clean syntax. The whole idea may seem a bit odd, but it is in line with proposals circulating a couple of weeks ago by folks who want to allow declared types like forall b. C Int b => b -> Bool in situations where they knew that the only possible instantiation for b was some fixed type like Int (say). 4) "Functional Dependencies": As described in my ESOP 00 paper (the Hugs manual, and the HTML note on my web page, don't tell the whole story). This allows a programmer to indicate that, like (3), some of the parameters in a constraint will be *uniquely* determined by other parameters. Unlike (3), the assumption in the ESOP paper, and in current implementations, is that these uniquely determined types will be mentioned explicitly in each instance declaration. With functional dependencies, inferred constraint sets can be improved in ways that are (a) important in practice, and (b) not possible in any of the options mentioned previously. For example, given class Collects c e | c -> e, we can simplify (Collects c e, Collects c f) => e -> f -> c -> c to (Collects c e) => e -> e -> c -> c. [Aside: Marcin's specific problem with Has_parens could be dealt with in this framework also, but that would probably require the introduction of a newtype like: newtype PP = forall a. PP (Parser a -> Parser a) instance Has_parens TokenParser PP where ... This, of course, would require extra games with the PP constructor (and an appropriately defined inverse) in expressions, which would probably be too messy and awkward in practice; a record system designed to support polymorphic fields from the outset would be a better solution here.] 5) And so on. There are other alternatives ... | I want keys instead of fundeps! :-) I've found it hard to assess or make sense of your descriptions of keys in previous postings; at different times it has seemed as though keys could be any of options 1, 2, 3, 4, or 5 in the above. But I hope that my analysis of the design space above is helping us to reach a better shared understanding of exactly what you are proposing. In terms of what I've written above, my current guess at interpreting your proposal goes something like this: - You want to allow each class declaration to be annotated with zero or more subsets of the parameters, each of which you refer to as a "key" for the class. - When a user writes an instance declaration: instance P => C t1 ... tn where ... you treat it, in the notation of (2) above, as if they'd written: instance P => C t1 ... tn improves C t11 ... t1n, ..., C tm1 ... tmn where ... Here, m is the number of keys, and: tij = ti, if parameter i is in key j = ai, otherwise where a1, ..., an are distinct new variables. If this is correct, then it seems to me that: - Keys will provide a more concise, but less expressive notation than (2). The notation of (2) is considerably more expressive because it isn't limited to the form used in the translation above, and because it can be used on an instance by instance basis rather than a specification that applies uniformly to all instances of a class. It's hard to know what the tradeoffs will be in practice, but I'm inclined to believe that keys are too limited, and the more general mechanism will not be too cumbersome in many practical cases. - Keys will not give you the full functionality of functional dependencies, and that missing functionality is important in some cases. All the best, Mark PS. If we're going to continue this discussion any further, let's take it over into the haskell-cafe ...
participants (8)
-
Adrian Hey -
Fergus Henderson -
George Russell -
John Meacham -
Mark P Jones -
qrczak＠knm.org.pl -
Stefan Karrmann -
Tom Pledger