Re: Recursion on TypeNats
No, there's not another way to do this with built-in Nats, and there probably won't ever be. I do hope you're wrong. There are two advantages to the built-in Nats over hand-rolled ones: 1) Better syntax / error messages. 2) Built-in Nats are much more efficient than hand-rolled ones, because the hand-rolled ones are unary and take up space linear in the value of the number. If you re-hash your proposal for a Successor constructor down to the term level, it looks juts like (n+k)-patterns, which were discarded as a bad idea. (n+k) patterns are clearly a bad idea on integers, because the integers don't have the inductive structure, but they're a good idea on natural numbers, which is why they were in the language originally. The reason that the type-level numbers are natural numbers and not integers is because natural numbers have a simpler theory to solve for. I'm personally hoping for proper type-level integers at some point, and the type-checker plugins approach may make that a reality sooner than later. Type-level integers could well be useful, but they shouldn't replace type-level naturals, because they have completely different uses. At the value level, you can fudge the differences, because you can always return bottom, but at the type level you have to take correctness much more seriously if your type system is to be any use at all. The fact that Carter (and I) are forced to define hand-rolled nats on top of the built in ones demonstrates a clear need for this feature. It seems to me a valuable extension, whether the syntax uses Successor or (n+k). Why can't we combine the advantages of built-in Nats and hand-rolled ones? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
Ok, I've created a ticket https://ghc.haskell.org/trac/ghc/ticket/9731 Unfortunately I don't know enough about ghc internals to try implementing it. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Recursion on TypeNats
If you define your own type level naturals by promoting data Nat = Z | S Nat you can define data families recursively, for example data family Power :: Nat - * - * data instance Power Z a = PowerZ data instance Power (S n) a = PowerS a (Power n a) But if you use the built-in type level Nat, I can find no way to do the same thing. You can define a closed type family type family Power (n :: Nat) a where Power 0 a = () Power n a = (a, Power (n-1) a) but this isn't the same thing (and requires UndecidableInstances). Have I missed something? The user guide page is pretty sparse, and not up to date anyway. If not, are there plans to add a Successor constructor to Nat? I would have thought this was the main point of using Nat rather than Int. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
you want the following (which doesnt require undediable instances) data Nat = Z | S Nat type family U (x :: Nat) where U 0 = Z U n = S (U (n-1)) this lets you convert type lits into your own peanos or whatever Yes, you can do that, but why should you have to? Nat is already the natural numbers, so already has this structure. Why do we have to define it again, making our code that much less clear and readable? ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Recursion on TypeNats
because you haven't helped write a patch change it yet :) -Carter Would this be possible with the new type checker plugins? btw, your example gives me Nested type family application in the type family application: U (n - 1) (Use UndecidableInstances to permit this) In the equations for closed type family ‘U’ In the type family declaration for ‘U’ Failed, modules loaded: none. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker plugins
I can think of a use for a non-equality constraint: an alphabetical ordering on Symbol. This would allow experimental implementations of extensible records (without shadowing) which keep the labels sorted. An order constraint on Nat might be useful, too. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker plugins
Ok, I hadn't realised that. Looking in the user's guide, I see = and =? for Nat, but I couldn't find anything about Symbol. I must try them out! From: Carter Schonwald carter.schonw...@gmail.com the alphabetical ordering on Symbol is already exposed via TypeLits... this would be some machinery to help maintain that ordering with less user intervention? On Thu, Oct 16, 2014 at 6:59 PM, Barney Hilken b.hil...@ntlworld.com wrote: I can think of a use for a non-equality constraint: an alphabetical ordering on Symbol. This would allow experimental implementations of extensible records (without shadowing) which keep the labels sorted. An order constraint on Nat might be useful, too. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Field accessor type inference woes
The two points in AntC's message suggest a possible compromise solution. Unless I've missed something, this allows nested fields, fixed type projections, and HR fields. The only restriction is that HR fields must be fixed type, though they can still be used in multiple records. 1. Use an associated type class for Has, to solve the nesting problem: class Has (r :: *) (x :: Symbol) where type GetField r x :: * getField :: r - GetField r x (Maybe a fundep would also work, but I'm more used to thinking with associated types.) 2. Introduce a declaration for fixed type fields: field bar :: Bar is translated as: class Has_bar r where bar :: r - Bar instance Has_bar r = Has r bar where GetType r bar = Bar getField = bar 3. Undeclared fields and those declared typeless don't have their own class: field bar is translated as bar :: Has r bar = r - GetType r bar bar = getField 4. Now you can use HR fields, provided you declare them first: field bar :: forall b. b - b is translated as: class Has_bar r where bar :: r - forall b. b - b instance Has_bar r = Has r bar where GetType r bar = forall b. b - b getField = bar which doesn't look impredicative to me. Does this work, or have I missed something? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Overloaded record fields
(sorry, accidentally failed to send this to the list)
All this extra syntax, whether it's ., #, or {} seems very heavy for a problem
described as very rare.
Why not simply use a declaration
field name
whose effect is to declare
name :: r {name ::t} = r - t
name = getFld
unless name is already in scope as a field name, in which case the declaration
does nothing?
Then we could continue to use standard functional notation for projection, and
still deal with the
case of unused projections.
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Overloaded record fields
This (AntC's points 1-8) is the best plan yet. By getting rid of dot notation,
things
become more compatible with existing code. The only dodgy bit is import/export
in point 7:
7. Implement -XPolyRecordFields, not quite per Plan.
This generates a poly-record field selector function:
x :: r {x :: t} = r - t-- Has r x t = ...
x = getFld
And means that H98 syntax still works:
x e -- we must know e's type to pick which instance
But note that it must generate only one definition
for the whole module, even if x is declared in multiple data types.
(Or in both a declared and an imported.)
But not per the Plan:
Do _not_ export the generated field selector functions.
(If an importing module wants field selectors,
it must set the extension, and generate them for imported data types.
Otherwise we risk name clash on the import.
This effectively blocks H98-style modules
from using the 'new' record selectors, I fear.)
Or perhaps I mean that the importing module could choose
whether to bring in the field selector function??
Or perhaps we export/import-control the selector function
separately to the record and field name???
I don't see the problem with H98 name clash. A field declared in a
-XPolyRecordFields
module is just a polymorphic function; of course you can't use it in record
syntax in a
-XNoPolyRecordFields module, but you can still use it.
I think a -XPolyRecordFields module should automatically hide all imported H98
field names and
generate one Has instance per name on import. That way you could import two
clashing H98
modules and the clash would be resolved automatically.
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: thoughts on the record update problem
This worries me:
3. The syntax of record updates must be changed to include the class:
r {Rcls| n1 = x1, n2 = x2}
This is really the core of the proposal. If my understanding of the problem is
at all accurate, the whole reason we have trouble is that update is dependent
on the class, and the Haskel98 syntax doesn't give you enough information to
determine what the class is. You could always add an ad-hoc rule which says
something like if there is only one record class in scope which uses all the
labels in the update, assume that one but it would lead to horribly fragile
code.
And if I understand correctly this proposal is still uncertain on some
edge cases.
According to SPJ, the new version of impredicative polymorphism should allow us
to use polymorphic types in contexts, which fixes the only problem I know of.
Unfortunately, we can't yet experiment with it, since we won't know the details
until the Haskel Symposium. If you have any other edge cases, please let me
know what they are!
I think it is time to close down the records discussion on the mail
list and ask for an implementation
The implementer should use any means at their disposal, probably by
adding a new construct to the language. However, for now any new
constructs or other implementation details should be kept internal so
that we can maintain flexibility going forward.
A lot of smart people are expending a huge amount of mental effort
discussing how to shoehorn this problem into the existing Haskell
machinery and the fine details of the best way to do it even though
there is still no truly satisfactory solution. I would really like to
see this effort instead go into an implementation.
This attitude is one I can't even begin to understand. How can you implement
something before understanding it? What are you going to implement? Trying to
close down discussion when no conclusion has been reached is not the action
of a healthy community!
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: thoughts on the record update problem
Just because Haskell currently resolves its types through type-classes does not mean we are forced to stop at type-classes for every aspect of the implementation. No, we are not forced to use type classes for everything. But it makes the language much cleaner, more flexible, easier to learn and easier to implement if we use existing structures rather than creating new ones. Moreover, with our best proposal here we are left in the peculiar position of declaring victory of resolving through type-classes without annotations, but now requiring a new form of type annotation for all record updates. It would make more sense just to not go full force on the type-class resolution and instead require a normal type annotation. If you have a notation for this which actually solves the update problems, you should say what it is. I haven't seen any such suggestion which really works. The semantics that will be exposed to users have already been largely decide upon. Please tell us what this agreed semantics is, so that we know what we have agreed to! If we like, we can continue to debate the fine details of the semantics we would like to expose. The problem is that we have been mixing the semantics with the implementation details and using it as an excuse to hold up any implementation. What? I have seen no discussion of implementation details at all. The translations I gave in my proposal could be used as the basis for an implementation, but the point of them was to give an unambiguous semantics for the new language features. I read the translations given by others in the same way: as semantics, not implementation. I assume that implementers would use some equivalent but more efficient method depending on the internals of ghc. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
thoughts on the record update problem
There are actually four problems with overloaded record update, not three as
mentioned on the SORF page. This is an attempt to solve them.
The SORF update mechanism.
--
SORF suggests adding a member set to the class Has which does the actual
updating just as get does the selecting. So
set :: Has r f t = t - r - r
and r {n1 = x1, n2 = x2} is translated as
set @ n2 x2 (set @ n1 x1)
The Problems.
-
1. It's not clear how to define set for virtual record selectors. For example,
we might define
data Complex = Complex {re :: Float, im :: Float}
instance Has Complex arg Float where
get r = atan2 r.im r.re
but if we want to set arg, what should be kept constant? The obvious answer
is mod, but we haven't even defined it, and there are plenty of cases where
there is no obvious answer.
2. If the data type has one or more parameters, updates can change the type of
the record. Set can never do this, because of its type. What is more, if
several fields depend on the parameter, for example
data Twice a = Twice {first :: a, second :: a}
any update of first which changes the type must also update second at the
same time to keep the type correct. No hacked version of set can do this.
3. The Haskel implementation of impredicative polymorphism (from the Boxy Types
paper) isn't strong enough to cope with higher rank field types in instances of
set.
4. The translation of multiple updates into multiple applications of set is not
the same as the definition of updates in the Haskel report, where updates are
simultaneous not sequential. This would be less efficient, and in the case of
virtual record selectors, it wouldn't be equal, and is arguably incorrect.
Point 3 could possibly be fixed by improving the strength of the type system,
but SPJ says this is a hard problem, and no-one else seems ready to tackle it.
Points 1, 2 4 suggest that any solution must deal not with individual fields
but with sets of fields that can sensibly be updated together.
The Proposed Solution.
--
This is an extension to SORF. I don't know if the same approach could be
applied to other label systems.
1. Introduce a new form of class declaration:
class Rcls r where
r {n1 :: t1, n2 :: t2}
is translated as
class (Has r n1 t1, Has r n2 t2) = Rcls r where
setRcls :: t1 - t2 - r - r
setRcls is used internally but hidden from the user.
2. Instances of record classes can use a special form of default. So
data Rec = Rec {n1 :: t1, n2 :: t2}
instance Rcls Rec
is translated as
instance Rcls Rec where
setRcls x1 y1 (Rec _ _) = Rec x1 y1
provided all the fields in the class occur in the data type with the correct
types. In general, the definition of the update function is the same as the
Haskel98 translation of update, solving problem 4.
3. The syntax of record updates must be changed to include the class:
r {Rcls| n1 = x1, n2 = x2}
is translated as
setRcls x1 x2 r
Updating a subset of the fields is allowed, so
r {Rcls| n1 = x1}
is translated as
setRcls x1 (r.n2) r
4. Non default instances use the syntax:
instance Rcls Rec where
r {Rcls| n1 = x1, n2 = x2} = ...x1..x2..
which is translated as
instance Rcls Rec where
setRcls x1 y1 r = ...x1..x2..
in order to allow virtual selectors. This solves problem 1, because updates are
grouped together in a meaningful way. An extended example is given below.
5. Record classes can have parameters, so
class TwiceClass r where
r a {first :: a, second :: a}
data Twice a = Twice {first :: a, second :: a}
instance TwiceClass Twice
translates as
class TwiceClass r where
setTwiceClass :: a - a - r b - r a
data Twice a = Twice {first :: a, second :: a}
instance TwiceClass Twice where
setTwiceClass x y (Twice _ _) = Twice x y
which allows updates to change the type correctly. This solves problem 2.
6. Problem 3 *almost* works. The translation of
class HRClass r where
r {rev :: forall a. [a] - [a]}
is
class Has r rev (forall a. [a] - [a]) = HRClass r where
setHRClass :: (forall a.[a] - [a]) - r - r
which is fine as far as updating is concerned, but the context is not
(currently) allowed by ghc. I have no idea whether allowing polymorphic types
in contexts would be a hard problem for ghc or not. None of my attempted
work-rounds have been entirely satisfactory, but I might have missed something.
Comments
-
1. This makes the special syntax for Has pretty useless. When you have a set
of labels you want to use together, you usually want to use update as well as
selection, so it's
[Haskell] Higher types in contexts
Is there any deep reason why I can't write a polymorphic type in a context? I think the record update problem can be (sort of) solved if you could write: class Has r Rev (forall a. [a] - [a]) = HRClass r where setHRClass :: (forall a.[a] - [a]) - r - r but polymorphic types are not allowed in contexts. Is this one of the problems SPJ considers Hard or is it a feasible extension? Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: Records in Haskell
I'm not sure it's a good proposal, but it seems like the only way to handle this issue is to (1) introduce a new kind for semantically-oriented field names, and (2) make the Has class use that kind rather than a type-level string. The second half of my message showed exactly how to handle the problem, using nothing more than existing Haskel features (and SORF for the record fields). The point is that the extra complexity of DORF is completely unnecessary. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
Please remember SPJ's request on the Records wiki to stick to the namespace issue. We're trying to make something better that H98's name clash. We are not trying to build some ideal polymorphic record system. I must admit that this attitude really gets my hackles up. You are effectively saying that, so long as the one narrow problem you have come across is solved, it doesn't matter how bad the design is in other ways. This is the attitude that gave us the H98 records system with all its problems, and the opposite of the attitude which gave us type classes and all the valuable work that has flowed from them. Haskel is supposed to be a theoretically sound, cleanly designed language, and if we lose sight of this we might as well use C++. Whatever new records system gets chosen for Haskel, we are almost certain to be stuck with it for a long time, so it is important to get it right. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
After more pondering, I finally think I understand what the DORFistas want. Here is an example: You want to define records which describe people, and include (among other things) a field called name. There might be several different record types with a name field, depending on whether the record refers to a customer, an employee, a business contact etc., but in each case name is the name of the person to which the record refers. You then write various functions which assume this, such as spam :: Has r name String = r - String spam r = Dear ++ r.name ++ \nHave you heard... Now I want to define records which describe products, and I also use a field name in the same way, except that it is the brand name of the product. I also define functions such as offer :: Has r name String = r - String offer r = Reduced! ++ r.name ++ 50% off! It doesn't make any sense to apply your functions to my records or vice-versa, but because we both chose the same label, the compiler allows it. Putting the code in separate modules makes no difference, since labels are global. Here is a simple solution, using SORF: The real problem is that the polymorphism of spam and offer is too general. We should each define new classes class Has r name String = HasPersonalName r class Has r name String = HasBrandName r and make each of our record types an instance of this class instance HasPersonalName EmployeeRecord instance HasPersonalName CustomerRecord instance HasBrandName FoodRecord then we can define functions with a more specific polymorphism spam :: HasPersonalName r = r - String spam r = Dear ++ r.name ++ \nHave you heard... offer :: HasBrandName r = r - String offer r = Reduced! ++ r.name ++ 50% off! Now there is no danger of confusing the two uses of name, because my records are not instances of HasPersonalName, they are instances of HasBrandName. You only use the class Has if you really want things to be polymorphic over all records, otherwise you use the more specific class. This seems to me a much simpler approach than building the mechanism in to the language as DORF does, and it's also more general, because it isn't hard linked to the module system. Does it have any disadvantages? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
My objection is that I'm not sure if there is ever a case where you really want things to be polymorphic over all records. Well, I don't have a simple, really convincing example, but there are certainly things I want to play with. More importantly, DORF automatically attaches one class to each label, but this is often not what you want. For example, if you have two fields firstname and lastname the associated classes are less useful: what you really want is class (Has r firstname String, Has r lastname String) = HasPersonalName r so that you can define fullname :: HasPersonalName r = r - String fullname r = r.firstname ++ ++ r.lastname You may also want to define subclasses to express more specific conditions. In general, the compiler cannot automatically deduce what is semantically important: you need to define it yourself. The Has class is the base on which you can build. It doesn't seem like the Haskell way to have the less safe thing as the one that's default and convenient, and to allow the programmer to layer a more-safe thing on top of it if he or she wants to. It seems more like the Haskell way to have the safer thing be the default and to require extra work if you want to do something less safe*. I think you are using the word safe in a slightly misleading way. None of this is mathematically unsafe, because projections are natural (truly polymorphic). The safety that is broken here is nothing to do with the semantics of the language, it is to do with the semantics of the system being implemented, and that is something the compiler cannot infer. As my example above shows, it doesn't always correspond one to one with the labels. The Haskel way is to make things as polymorphic as is mathematically safe, even when this goes beyond the programmers original intention. You can then restrict this polymorphism by giving explicit less general types in the same way as in my examples. I think my approach is more Haskel like. Another important Haskel design consideration is to reuse parts of the language where possible, rather than introduce new structures. Type classes were originally introduced to deal with equality and numeric functions, but were reused for many things including monads. My approach achieves the same as DORF (and more), but using existing language features instead of introducing new ones. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
This should be used to generate internal constraints and not be exposed to the end user and not automatically abstract over fields. Every one of your messages about records stresses your dislike for polymorphic projections, and your insistence that the Has class should be hidden from the user. I've read all of your explanations, but I'm still totally unconvinced. All your arguments about the semantics of labels are based on the way you want to use them, not on what they are. They are projection functions! Semantically, the only difference between them is the types. Polymorphism makes perfect sense and is completely natural. There is nothing untyped about it. I feel you are pushing a narrow personal agenda here. I think the Has class would be useful to programmers and no harder to understand than other Haskel classes. It should not be hidden. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
I'm sorry Greg, I didn't mean to be offensive. I just feel that all your arguments in favour of this restriction are based on one particular application of records, rather than a general notion of what records are. Obviously this application is what motivates you to do all the valuable work you have done, and I appreciate that. But people are going to use records in many different ways, and I don't think that a restriction which makes perfect sense in your application should be allowed to restrict the ways other people want to write programs. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
I share Greg's concerns about polymorphic projections. For example, given a function sort :: Ord a = ... we don't allow any 'a' that happens to export a operator that's spelled = to be passed to 'sort'. We have the user explicitly create an instance and thereby defining that their = is e.g. a strict weak ordering and thus make sense when used with 'sort'. This explicitness is useful, it communicates the contract of the function to the reader and lets us catch mistakes in a way that automatically polymorphic projections don't. But the difference is that = is (potentially) an arbitrary function, so we need to be careful that the instances make sense. A formally correct system would insist that all instances are (at least) reflexive and transitive. But in the case of records, we know what the instances are: they are projection functions. Every single (automatically generated) instance does exactly the same thing: it projects out one component of a record. This isn't like OO polymorphism, where messages are actually arbitrary functions which could do anything, the polymorphism is exactly the same as that of fst and snd. At the very least use two different LANGUAGE pragmas so users can have one without the other. This I can agree with. It was the way that Greg mentioned it in every single email which was starting to worry me. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
The problem with this approach is that different labels do not have different representations at the value level. I think this is an advantage, because it means you don't have to carry this stuff about at runtime. This allows me to pattern match records, since I can construct record patterns that contain fixed labels: X : MyName1 := myValue1 : MyName2 := myValue2 I cannot see how this could be done using kind String. Do you see a solution for this? A similar problem arises when you want to define a selector function. You could implement a function get that receives a record and a label as arguments. However, you could not say something like the following then: get myRecord MyName1 Instead, you would have to write something like this: get myRecord (Label :: MyName1) Just define a constant myName1 = Label :: MyName1 for each label you actually use, and you can use it in both get and pattern matching Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] Records in Haskell
(sorry, I meant to send this to the list, but only sent it to Wolfgang) Here is my understanding of the current state of the argument: Instead of Labels, there will be a new kind String, which is not a subkind of *, so its elements are not types. The elements of String are strings at the type level, written just like normal strings. If you want labels, you can define them yourself, either empty: data Label (a :: String) or inhabited data Label (a :: String) = Label these definitions give you a family of types of the form Label name, in the first case empty (except for undefined), in the second case inhabited by a single element (Label :: Label name) There are several similar proposals for extensible records defined using labels, all of which (as far as I can see) could be defined just as easily using the kind String. There is also a proposal for nonextensible records, using the same techniques, which has (almost) converged with Simon's latest version of TDNR records. The problem with all of these is dealing with higher-rank field types: the current implementation of impredicative polymorphism isn't general enough to allow update of polymorphic fields. It seems to me that, if we could solve the (hard) impredicativity problem, we would be very close to a design which would 1. be compatible with existing code 2. allow field names to be polymorphic 3. make the future addition of extensible records possible The question is, should we wait till someone solves the impredicativity problem, or go ahead with a cludgy design now? Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
deep record update
All this talk about records got me thinking. I don't really like the current
syntax for record update (because it looks too much like function application)
but here is an extension to it which might be useful.
If you use nested records, many languages allow you to update the inner records
directly, for example rect.bottomLeft.xCoord += 3. We could allow a similar
thing in Haskell by extending the syntax like this:
fbind - qvar = exp
| qvar { fbind1 , ... , fbindn }
then
rec { l1 { l2 = x }}
would mean
rec { l1 = (l1 rec) { l2 = x }}
The advantage (apart from convenience) is that we don't have to repeat rec,
which could be a complex expression.
Is this any use?
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
I have added my proposal to the wiki.The only downsides to it that I can see are: 1. If the types can be resolved at compile time, the compiler needs to optimise away the dictionaries, otherwise there will be a performance cost. Since this is always the case for type classes, I assume this is a well-studied problem. 2. The olegites are going to use the Label mechanism for other things, and ask for extra features. What features would be worth implementing? Do we want a member function to return the name as a string? How about a lexicographic ordering type function so we can implement extensible records? Where do we stop? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
As formulated on the wiki page, the narrow issue is a problem without a good solution. The reason the community rejected TDNR is because it's basically polymorphism done wrong. Since we already have polymorphism done right, why would we want it? The right way to deal with records is first to agree a mechanism for writing a context which means a is a datatype with a field named n of type b then give the selector n the type a is a datatype with a field named n of type b = n :: a - b There is no reason why this shouldn't be used with the current syntax (although it might clash with more advanced features like first-class labels). Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
Here is a simple concrete proposal:
Nonextensible records with polymorphic selectors.
=
1. Introduce a built-in class Label, whose members are strings at the type
level. We need a notation for them; I will use double single quotes, so
''string'' is automatically an instance of Label, and you can't define other
instances.
2. Define a class (in a library somewhere)
class Label n = Contains r n where
type field r n :: *
select :: r - n - field r n
update :: r - n - field r n - r
3. Declarations with field labels such as
data C = F {l1 :: t1, l2 :: t2} | G {l2 :: t2}
are syntactic sugar for
data C = F t1 t2 | G t2
instance Contains C ''l1'' where
field C ''l1'' = t1
select (F x y) _ = x
update (F x y) _ x' = F x' y
instance Contains C ''l2'' where
field C ''l2'' = t2
select (F x y) _ = y
select (G y) _ = y
update (F x y) _ y' = F x y'
update (G y) _ y' = G y'
4. Selector functions only need to be defined once, however many types they are
used in
l1 :: Contains r ''l1'' = r - field r ''l1''
l1 = select r (undef ::''l1'')
l2 :: Contains r ''l2'' = r - field r ''l2''
l2 = select r (undef ::''l2'')
5. Constructors are exactly as before
6. Updates such as
r {l1 = x}
are syntactic sugar for
update r (undef::''l1'') x
=
This has the advantage that the extension to Haskell is fairly small, and it's
compatible with existing user code, but if we later decide we want extensible
records, we need only add a type function to order Label lexicographically.
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Records in Haskell
Typos in my last message: the identifier field should be Field throughout,
and undef should be undefined. Here is the corrected version:
Nonextensible records with polymorphic selectors.
=
1. Introduce a built-in class Label, whose members are strings at the type
level. We need a notation for them; I will use double single quotes, so
''string'' is automatically an instance of Label, and you can't define other
instances.
2. Define a class (in a library somewhere)
class Label n = Contains r n where
type Field r n :: *
select :: r - n - Field r n
update :: r - n - Field r n - r
3. Declarations with field labels such as
data C = F {l1 :: t1, l2 :: t2} | G {l2 :: t2}
are syntactic sugar for
data C = F t1 t2 | G t2
instance Contains C ''l1'' where
Field C ''l1'' = t1
select (F x y) _ = x
update (F x y) _ x' = F x' y
instance Contains C ''l2'' where
Field C ''l2'' = t2
select (F x y) _ = y
select (G y) _ = y
update (F x y) _ y' = F x y'
update (G y) _ y' = G y'
4. Selector functions only need to be defined once, however many types they are
used in
l1 :: Contains r ''l1'' = r - Field r ''l1''
l1 = select r (undefined ::''l1'')
l2 :: Contains r ''l2'' = r - Field r ''l2''
l2 = select r (undefined ::''l2'')
5. Constructors are exactly as before
6. Updates such as
r {l1 = x}
are syntactic sugar for
update r (undefined::''l1'') x
=
Sorry about that.
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] Re: Re: RE: Extensible records: Static duck typing
While I agree with your general argument, I wonder if you realize that functional dependencies have a strong, general, and elegant mathematical foundation that long predates their use in Haskell? If you want even a brief glimpse, there's s short article at http://en.wikipedia.org/wiki/Functional_dependencies that might give you some ideas. The mathematics of functional dependencies plays an important role in the theory of relational databases. I don't know what you consider as the mathematical foundations for associated types, nor do I know why you consider that to be either more general or more mathematical (whatever that means) but I hope you'll enjoy the material on functional dependencies. I admit I was being unfair on fundeps in calling them less mathematical. Nonetheless, something about their addition to Haskell grates on my mathematical sensitivities. They feel bolted on in a way that associated types don't. Probably this is because of my own bias which leads me to see Haskell as a subset of dependent type theory, and ATs as some kind of sigma type (though I've never tried to make this precise). Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Re: RE: Extensible records: Static duck typing
My rationale for these criteria goes like this: efficient access is necessary if we want to compete with the much simpler record systems in mainstream languages. If records are not as light-weight (syntactically as well as wrt run-time performance) as 'normal' Haskell data types, then people will be reluctant to use them, especially in library APIs. Finally, having to wait for highly experimental additional extensions to be available, tried, and tested, would only help to indefinitely post- pone the introduction of a usable record system. I totally disagree. The great strength of Haskell is that, whenever important design decisions have been made, the primary consideration has not been practicality, but generality and mathematical foundation. When the Haskell committee first started work, many people said lazy evaluation was an academic curiosity: mathematically right, but far too inefficient for real programs. When Haskell adopted type classes, people said they were far too heavy a machinery to solve the relatively simple problems of equality, show and numbers. In each case the more general, abstract approach has shown enormous advantages in the long term. I'm sure the same will be true of associated types, which are a lot more complex than functional dependencies, but also more general, and more mathematical. My criteria for choosing a record system would be: continue with the philosophy which has served Haskell so well up to now. In other words, choose the system which is most general and most mathematically sound; get some kind of implementation working so that we can get some experience with using it; then worry about efficiency later. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: RE: Extensible records: Static duck typing
Begin forwarded message: From: Ben Franksen [EMAIL PROTECTED] Date: 18 February 2008 21:32:29 GMT To: haskell@haskell.org Could you be more specific? Which proposals exactly do you mean and where can I read more about them? Hlist is one of the ones | was thinking of. Two more are poor man's records a.k.a. Data.Record.hs, whose author certainly believes it should be the basis for the new system, and my own system, downloadable from http://homepage.ntlworld.com/b.hilken/files/Records.hs There is a discussion of the various possibilities on the wiki http://hackage.haskell.org/trac/ghc/wiki/ExtensibleRecords which you are encouraged to contribute to! Sorry about the lack of response on cafe, but I only read that when people say they are moving their discussion there. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] RE: Extensible records: Static duck typing
What about just implementing the cheapest solution that still gets us most of the way? (3) If it is as cheap (to implement) as advertised then there is no great risk involved. If it turns out the missing features are a great show-stopper for some people (which I don't believe) then let them present their case afterwards, with good examples at hand. We can still decide to aim for a higher goal in the long term. If in doubt, chose the solution that is easier to implement. Since this paper, there have been several proposals which can be 90% implemented as libraries, using either functional dependencies or associated types. These all have much more expressive type systems than the SPJ paper, yet need very little compiler support. The question is, which one (if any) should get this small but necessary support? Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Extensible records: Static duck typing
2. List the possible features that “records” might mean. For example:
· Anonymous records as a type. So {x::Int, y::Bool} is a
type. (In Haskell as it stands, records are always associated with
a named data type.
· Polymorphic field access. r.x accesses a field in any
record with field x, not just one record type.
· Polymorphic extension
· Record concatenation
· Are labels first-class?
· etc
Give examples of why each is useful. Simply writing down these
features in a clear way would be a useful exercise. Probably some
are “must have” for some people, but others might be optional.
This is what I was trying to do with the wiki page. I stopped because
the only other contributor decided he could no longer contribute, and
I felt I was talking to myself. If we want to be rational about the
design, we need real examples to demonstrate what is genuinely useful,
and I don't have that many of them.
Barney.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Extensible records: Static duck typing
Everyone wants to add extensible records to Haskell. The problem is
that, in a formally defined language like Haskell, we need to agree
how they should behave, and there are too many conflicting ideas.
I was involved recently in an attempt to try to sort out some of the
alternatives (recorded here: http://hackage.haskell.org/trac/ghc/wiki/ExtensibleRecords)
which collapsed because of argument over a fundamental question:
Should {label := Hi, color := blue} and {color := blue, label :=
Hi} have the same type?
One of the main contributors felt that the answer was no (because it
allows more different records to be represented, and makes
implementation simpler), and that we should say so. I felt that most
people would consider that the answer was yes, and that we shouldn't
make such a fundamental design decision without some evidence about
what is best in practice.
The result was that our attempt to sort things out stopped.
This sort of disagreement means that nothing gets done. After my
experience with the wiki page, I don't believe anything will get done
until one of the core ghc developers makes some arbitrary decisions
and implements whatever they want to, which will then eventually
become part of the standard by default.
Barney.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Extensible records: Static duck typing
The scoped labels paper has an interesting feature in this regard: labels with different names can be swapped at will, but labels having the same name (which is allowed) maintain their order. - Cale Yes, I know. The problem is that there are TOO MANY proposals, and they are all fundamentally incompatible. The scoped labels idea is interesting, but is it useful? No-one has written enough code with ANY of the proposals to say what their strengths and weaknesses are. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Extensible records: Static duck typing
new record (x = 3,y = 4)
subtraction \r - ( x = 3 | r - x)
replacement \r - (x := 3 | r) (equivalent to the above)
type (x::Int,y::Char)
degenerate cases:
empty record (|)
subtracting a label (| r - x)
a record can always be determined by the presence of a '|' within
parenthesis.
One of the advantages of the systems with richer polymorphism and more
predicates is that they need less syntax. It is possible (once you
have solved the permutation/scoping problem) to use constructors as
labels, and define all the basic operators on records as standard
Haskell functions. With this approach you can even treat labels as
first-class citizens and write polymorphic record zip:
labelZip :: ({n :: a} `Disjoint` {m :: b}) = n - m - [a] - [b] -
[{n :: a, m :: b}]
labelZip n m = zipWith (\x y - {n := x, m := y})
But no-one knows whether this extra expressive power has an
unacceptable cost in terms of extra complexity, because no-one has
implemented and used these systems seriously.
Barney.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Re: Extensible Records
I've tried to summarise the important differences between the various proposals on the wiki page, but it still needs lots of illustrative examples. Anyone who is interested, please contribute! Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Extensible Records
I think this would be a BIG mistake. Whatever system GHC settles on
is almost certain to become part of the Haskell standard, and this
particular system has some deep limitations which could not be got
round without ripping it all out and starting again.
The problem with this (and other Flex-like) systems is that they
take record extension as the basic operation of record building,
rather than record merging. This means that you can only ever add or
update statically determined fields of a given record.
An important application which is made impossible by this approach is
functions with optional arguments. For example, if you look at the
definition of R (the statistics system) every function has a small
number of mandatory positional arguments, and a very large number of
optional named arguments, which take sensible default values. I want
to be able to write:
f opts x = let vals = {Opt1 =: default1, ... } |: opts in
... vals ... x ...
where '{Opt1 =: default1, ... }' is some fixed record of default
values, and '|:' is record overwrite. The type of f should be
f :: (a `Subrecord` {Opt1 :=: t1, ...}) = a - b - c
where '{Opt1 :=: t1, ...}' is the (fixed) type of '{Opt1 =:
default1, ... }' (and x::b, and c is the type of the result).
The condition 'a `Subrecord` {Opt1 :=: t1, ...}' in the context of
this type means that every field of 'opts :: a' must be a field of
'{Opt1 :=: t1, ...}', but opts can have as few fields as you like.
This is exactly what you want for optional arguments.
This could never be defined in any Flex-like system, because these
systems depend on the fact that their record types can be reduced to
a type variable extended by a fixed set of labels. This is a major
restriction to what you can do with them: you can never define
operations like '|:' or '+:' where the second argument does not have
a constant set of fields.
This restriction does not hold for more flexible systems like that
defined by Oleg co using functional dependencies, or the one I
proposed on this list using type families. Although these systems are
much more flexible than the scoped labels system, they would take
LESS work to add to GHC because they have less built-in syntax, and
are almost entirely defined in a library.
I second the call for a records system, but please don't limit us to
something like scoped labels!
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Extensible Records
Hugs.Trex :t let f opts x = (opt1=default|opts) in f
let {...} in f :: a\opt1 = Rec a - b - Rec (opt1 :: [Char] | a)
This completely loses the aim of optional arguments: with this type,
the argument 'opts' cannot have a field 'opt1' (as shown by the
context 'a\opt1'). The type we want should say that 'opts' cannot
have any fields except 'opt1' (though that is optional). Flex cannot
express this type.
(btw, what is Flex-like?)
What I meant by Flex-like systems is that they can only extend
record types by fixed fields. As well as the usual extraction and
deletion of fields, I want first-class operators:
(+:) :: r `Disjoint` s = r - s - r :+: s
x +: y is the concatenation of two records x and y, under the
condition that they have no fields in common
r :+: s is the type of x +: y, assuming x::r and y::s
(|:) :: r `Subrecord` s = s - r - s
x |: y is the update of x by y, under the condition that every field
of y is a field of x of the same type
the type of x |: y is the same as the type of x
The conditions on the types of these operators are important, as they
catch common errors. For example, if a function 'f' has optional
arguments 'opt1::x1, ... optn::xn' you want 'f {optt1 = val}' to give
a type error because you've misspelled 'opt1', not simply to ignore
it. In other words, you need a condition that the fields of the
record argument of f are a subset of {opt1, .., optn}.
These operators can be defined using type families: download the code
from
http://homepage.ntlworld.com/b.hilken/files/Records.hs
This code would only need minimal extensions to GHC to make it
completely useable.
some time ago (was that really 2 years? trac claims it was), i
suggested that any record system with first-class labels needs
language support for type sharing: if i import modules A and B,
each of which introduces a record-label X, i need some way of
telling the type system that A.X ~ B.X (Trex solved that problem
by not requiring label declarations at all, but Trex labels weren't
first-class objects, either).
I believe this issue is completely independent of records. Exactly
the same problem would arise if the same datatype with the same
constructors was defined in two different modules. To solve this we
need a mechanism whereby identically defined types in different
modules can be identified.
i propose to start Records project by composing list of
requirements/applications to fulfill; we can keep it on Wiki page.
this will create base for language theorists to investigate various
solutions. i think they will be more motivated seeing our large
interest in this extension
I am happy to contribute to this, but I am strongly biased in favour
of my own records system!
Barney.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] Re: [Haskell-cafe] PROPOSAL: Rename haskell@ to haskell-announce@
From: Isaac Dupree I haven't been able to see how it makes sense to subscribe to haskell@ but not haskell-cafe -- because if a discussion interested you, and went in-depth, you might want to be able to read the whole thread! (It is possible to read the archives, but that doesn't help if you're inspired to _reply_ to the thread...) This is exactly what I do. I subscribe to haskell so as not to miss anything important, and when something I'm interested in moves to haskell-cafe, I use gmane. I think most of the people complaining about this issue do the same. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: unique id for data types
Ok, I'm stuck. The Oleg stuff is great, and it looks like he did everything I've done long ago, without needing type functions or associated types. But I can't use the TTypeable stuff directly because you can't convert the relational style of Oleg's work (using functional dependencies) to the functional style I'm using (using type families). Rewriting all the basics in my style is no problem (especially as I only need a limited part of it) EXCEPT Derive depends on (at least the types of) Template Haskell, and TH can't define type family or associated type instances. So I'm back where I started. Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
unique id for data types
In order to make my records system practically useable, I need a type family type family NameCmp n m which totally orders datatypes. More precisely, it should return one of the following types: data NameLT = NameLT data NameEQ = NameEQ data NameGT = NameGT for each pair of datatypes n m, according to whether n m, n = m, or n m in some global ordering. This ordering needs to be independent of the context, so it can't be affected by whatever imports there are in the current module. What I want to know is: does GHC give datatypes any global id I could use to generate such an ordering? Would fully qualified names work? Secondly (assuming it's possible) how easy would it be for me to write a patch to add NameCmp to GHC? Where in the source should I start looking? Thanks, Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: unique id for data types
Hi Simon, thanks for the response. In fact I really only need NameCmp to be defined for datatypes of the form data T = T but it's still a lot, so I was expecting to need an extension. Lexical comparison of fully qualified names is what I had in mind, but I wanted some confirmation that such things exist! I could post a GHC feature request, but unless I get someone else interested in this, it would probably just sit in Trac indefinitely. Where should I look in the ghc source if I want to add it myself? Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: unique id for data types
Hi Stefan, That's great! Where can I get hold of your TTypable? It's not in Hackage and Google didn't find it. I don't know where else to look... Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: unique id for data types
Ah! your link lead me to the HList paper, where all questions are answered... Thanks, Barney. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] unique id for data types
In order to make my records system practically useable, I need a type family type family NameCmp n m which totally orders datatypes. More precisely, it should return one of the following types: data NameLT = NameLT data NameEQ = NameEQ data NameGT = NameGT for each pair of datatypes n m, according to whether n m, n = m, or n m in some global ordering. This ordering needs to be independent of the context, so it can't be affected by whatever imports there are in the current module. What I want to know is: does GHC give datatypes any global id I could use to generate such an ordering? Would fully qualified names work? Secondly (assuming it's possible) how easy would it be for me to write a patch to add NameCmp to GHC? Where in the source should I start looking? Thanks, Barney. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] unique id for data types
Hi Neil, thanks for the response. The problem is this: It is in the IO monad because the actual value of the key may vary from run to run of the program (taken from the web page). Since I'm relying on the order, not just equality, this will seriously screw things up, because my records are done at compile time. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Records: Examples
{-# LANGUAGE TypeFamilies #-}
Hi Justin, thanks for your interest. Hope this helps!
module Examples where
import Records
To get started, you need to define your labels. They are just
singleton datatypes:
data FirstName = FirstName deriving (Show, Eq, Ord)
data Surname = Surname deriving (Show, Eq, Ord)
data Address = Address deriving (Show, Eq, Ord)
data PhoneNo = PhoneNo deriving (Show, Eq, Ord)
you can define as many as you like. Next you have to define the order
on fields. At
the moment you have to do this by hand, but I hope to get ghc to do
this automatically:
type instance NameCmp FirstName FirstName = NameEQ
type instance NameCmp FirstName Surname = NameLT
type instance NameCmp FirstName Address = NameLT
type instance NameCmp FirstName PhoneNo = NameLT
type instance NameCmp Surname FirstName = NameGT
type instance NameCmp Surname Surname = NameEQ
type instance NameCmp Surname Address = NameLT
type instance NameCmp Surname PhoneNo = NameLT
type instance NameCmp Address FirstName = NameGT
type instance NameCmp Address Surname = NameGT
type instance NameCmp Address Address = NameEQ
type instance NameCmp Address PhoneNo = NameLT
type instance NameCmp PhoneNo FirstName = NameGT
type instance NameCmp PhoneNo Surname = NameGT
type instance NameCmp PhoneNo Address = NameGT
type instance NameCmp PhoneNo PhoneNo = NameEQ
Now we are ready to play!
To define records, use (=:) and (+:)
barney = FirstName =: Barney +: Surname =: Hilken +:
Address =: Horwich +: PhoneNo =: 697223
You can use as many or as few of the fields as you like, and you can
write them in any order,
but trying to use a field twice in the same record will give you a
(rather incomprehensible)
type error.
justin = Surname =: Bailey +: FirstName =: Justin +: Address
=: Somewhere
To extract the value at a field use (.:)
myPhone = barney.:PhoneNo
To delete part of a record, use (-:)
noCallers = barney -: Address
To update existing fields in a record, use (|:)
barney' = barney |: Address =: ((barney .: Address) ++ , UK)
The power of the records system is that these five operators, =:
+: .: -: |: are Haskell
polymorphic functions. So you can define functions like
livesWith p q = p |: Address =: (q .: Address)
which returns p, but with its Address field changed to that of q.
Note that this function
works on any records p and q with Address fields, whatever other
fields they may have.
You can even define functions parametrised by field names:
labelZip n m = zipWith (\x y - n =: x +: m =: y)
then 'labelZip FirstName Surname' is a function which takes two lists
and returns a list of records:
names = labelZip FirstName Surname [Barney, Justin] [Hilken,
Bailey]
of course, labelZip isn't restricted to the four labels we defined
earlier, it works on anything.
The system is strongly typed, so record errors (such as missing or
duplicated fields) are caught
at compile time. There are type operators (:=:), (:+:), (:-:), (:.:)
corresponding to the record
operators, and classes `Contains`, `Disjoint`, `Subrecord` which
allow you to express conditions
on types. Unfortunately, the type system sometimes decides that a
function has a different type
from the one you expect, and won't accept the header you want to give
it. More experience with the
system is needed before we can say whether this is a problem.
Barney.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell] Records
Now that I have a version of ghc with type classes, I have had a go at implementing records based on the ideas I mentioned on this list a few months ago. The code of my first attempt is available at http:// homepage.ntlworld.com/b.hilken/files/Records.hs I am releasing this to get feedback. I think Haskell needs a records system of this kind of generality, and this code at least allows you to play around. From the comment section of the file: --- Record construction: EmptyRecis the empty record. N =: x is the record with one field labelled N carrying data x. t +: u is the union of records t and u. Any overlap of labels gives a static error. Record destruction: t .: N is the value of field N in record t. A lack of field N gives a static error. t -: N is record t with field N deleted. A lack of field N gives a static error. Record update: t |: u is the record with fields from u where it has them, t otherwise. If u has any fields not in t, or of different types from t, there is a static error. Note that the result has the same type as t. All these records have types: EmptyRecis the type of the empty record. N :=: a is the type of a record with one field labelled N carrying data of type a. r :+: s is the union of record types r and s. Any overlap of labels gives a static error. r :.: N is the type of field N in a record of type r. A lack of field N gives a static error. r :-: N is record type r with field N deleted. A lack of field N gives a static error. Finally some classes to govern the polymorphism: r `Contains` N means that r is a record type with a field labelled N. r `Disjoint` s means that r and s are record types with no fields in common. r `Subrecord` s means that r and s are record types, and every field of r also occurs in s (with the same type). The types of the basic operators are as follows: (=:) :: n - a - n :=: a (+:) :: r `Disjoint` s = r - s - r :+: s (.:) :: r `Contains` n = r - n - r :.: n (-:) :: r `Contains` n = r - n - r :-: n (|:) :: r `Subrecord` s = s - r - s -- Note that these records are a lot more expressive than the Hugs system, as you can not only extend records by adding fields, but also take unions of arbitrary (disjoint) records. Record update is designed for functions with lots of named optional arguments. If you define f opts = ... options.:Optj ... where options = (Opt1 =: val1 +: ... +: Optn =: valn) |: opts then the user can write (for example): f (Optk =: u +: Optl =: v) to set just two of the options, leaving the rest as default. This also cannot be done in the Hugs system. The main disadvantage of the current implementation is that you have to tell the compiler in which order to store the fields, by defining one of the following: type instance NameCmp N M = NameLT type instance NameCmp N N = NameEQ type instance NameCmp N M = NameGT for each pair of labels N M in such a way as to give a linear order on labels. You need n^2 definitions, where n is the number of labels. I would do this in Template Haskell, but it won't yet allow you to declare type instances. Maybe some compiler support? Error messages tend to be cryptic. They mostly complain of missing instances, and can run to several pages. There is really no way to improve this without building it all in to the compiler! All comments gratefully received, including suggestions on syntax, choice of operators, implementation, explanation, etc. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] View patterns in GHC: Request for feedback
I think you should add the form: (function - pattern) @ pattern as well. The reason you don't need general 'pattern @ pattern' with normal patterns is that, if anything is going to match, the two patterns must have the same outermost constructor, so you can push the @ inside. This doesn't hold for view patterns, and you might well want to match against several views. Of course you can do this with 'both', but the readability is terrible, especially if you want to match against more than two patterns. Nested 'both' gets extremely long, or do you want to define 'allThree', 'allFour', ... The reason I think this might be important is that you could use view patterns for records: (label1 - x)@(label2 - y)@(label3 - z) ... gives a reasonable syntax for a record pattern, and it would be compatible with any form of extensible records. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
Sorry if people are really bored with this thread, but I thought of another advantage of this approach. Trex (and similar systems) have a limitation that stops you using them to define functions with default values. In systems like R (the stats package) most functions have a huge number of named parameters which usually take default values, but can be changed if necessary. In order to define such functions, what you want is an operation 'update r s' which takes the value of the record 's' (the non-default values) for each field which 's' has, and the value of 'r' (the default values) for all other fields. The type of 's' should be such that it can only have fields which 'r' has, and each such field must have the same type, but it doesn't need all the fields of 'r'. The type of the result is the same as the type of 'r'. This can't be typed in Hugs because you can only update particular fields, but we can easily add it to (at least the quadratic version of) AT-records. Introduce a class 'subRecord r s' which means that every field of 's' is a field of 'r' with the same type: class subRecord r s where update :: r - s - r The type 'Empty' is a subRecord of everything, and updating by it changes nothing: instance subRecord r Empty where update t Empty = t For each label 'N' define: instance subRecord r s = subRecord (N a r) (N a s) where update (N x t) (N y u) = N y (update t u) For each previous label 'M' define: instance subRecord r (M b s) = subRecord (N a r) (M b s) where update (N x t) (M y u) = N x (update t (M y u)) There are probably other useful additions to the records system which could be coded up in a similar way. In fact, the class 'Disjoint' of my original proposal already goes beyond hugs. Until it is clear what is useful and what is not, a system like this which requires little compiler support has the great advantage that it is easy to change. Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
Manuel M T Chakravarty: This is problematic as the instance heads are distinguished only by the context; ie, both instances are for `Lacks m (N a r)'. Haskell's instance selection mechanism (with or without associated types) selects instances purely by looking at the arguments of the class; hence, you cannot use instance context as a kind of guard to guide instance selection. A pity. Would resolving instance declarations as Horn clauses be useful to deal with any other examples of overlapping instances? If you don't mind the code for each new label being linear in the number of previous labels (so the total code is quadratic in the global number of labels) the idea can be rescued. Get rid of (::), and keep the same definitions of Constructor, Contains, Lacks, Disjoint and Empty, and the same instances of 'Lacks n Empty' and 'Disjoint Empty r'. For each label 'N', define: data N a r = N a r instance Contains N (N a r) where type Project N (N a r) = a type Delete N (N a r) = r project N (N x t) = x delete N (N x t) = t instance Disjoint r s, Lacks N (Union r s) = Disjoint (N a r) s where type Union (N a r) s = Extend N a (Union r s) union (N x t) u = extend N x (union t u) and for each previous label 'M', define: instance Contains M r = Contains M (N a r) where type Project M (N a r) = Project M r type Delete M (N a r) = N a (Delete M r) project M (N x t) = project M t delete M (N x t) = N x (delete M t) instance Lacks M r = Lacks M (N a r) where type Extend M b (N a r) = N a (Extend M b r) extend M y (N x t) = N x (extend M y t) instance Lacks N (M a r) where type Extend N b (M a r) = N b (M a r) extend N y (M x t) = N y (M x t) This saves the bother of fiddling with (::) but means that every time you import a module which declares labels you would have to generate code for the interactions between each new label and each existing one. At least it's not exponential! Barney. ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] extensible records using associated types
The implementation of records using types data N a r = N a r might
well be inefficient, and I don't know enough about the workings of
the compiler to see whether it could be improved by unboxing and
strictness. But the real point of my post was the classes Contains,
Lacks and Disjoint which give you extensibility. To give another
example, if Haskell had non-extensible records {N1 = x1, ..., Nn =
xn} of type {N1 :: a1, ..., Nn :: an} we could use the same technique
to make them extensible.
Assume we can represent the field names N somehow as values (N ::
Constructor N). Then we can define instances of the form
instance Contains Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} where
type Project Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} = aj
type Delete Nj {N1 :: a1, ..., Nj :: aj, ..., Nn :: an} = {N1 ::
a1, ..., Nn :: an}
project Nj {N1 = x1, ..., Nj = xj, ..., Nn = xn} = xj
delete Nj {N1 = x1, ..., Nj = xj, ..., Nn = xn} = {N1 = x1, ..., Nn
= xn}
instance Lacks M {N1 :: a1, ..., Nn :: an} where
type Extend M a {N1 :: a1, ..., Nn :: an} = {M :: a, N1 :: a1, ...,
Nn :: an}
type extend M x {N1 = x1, ..., Nn = xn} = {M = x, N1 = x1, ..., Nn
= xn}
instance Disjoint {N1 :: a1, ..., Nn :: an} {M1 :: b1, ..., Mm ::
bm} where
type Union {N1 :: a1, ..., Nn :: an} {M1 :: b1, ..., Mm :: bm}
= {N1 :: a1, ..., Nn :: an, M1 :: b1, ..., Mm :: bm}
union {N1 = x1, ..., Nn = xn} {M1 = y1, ..., Mm = ym}
= {N1 = x1, ..., Nn = xn, M1 = y1, ..., Mm = ym}
Of course, there are a lot of these (exponential in the number of
field names!) so you don't really want to generate them all. But
exactly the same classes (modulo the definition of Constructor, which
should be hidden anyway) give you extensibility, so any code you
write will work with either implementation.
Barney.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
[Haskell] extensible records using associated types
I'm sorry if this example has already been posted, but I couldn't
find it by searching the archives. If it's new (and works properly),
it provides more evidence that ATs are a good thing.
You can use associated type synonyms to implement polymorphic
extensible records.
-
We will represent records as values of the form
N1 x1 (N2 x2 ... (Nn xn Empty)...)
with corresponding type
N1 a1 (N2 a2 ... (Nn an Empty)...)
where the field name N is defined by the declaration
data N a r = N a r
For convenience, we define the type of field name constructors:
type Constructor n = forall a. forall r. a - r - n a r
so that N :: Constructor N for each field name N.
Next we define a class (::) whose purpose is to tell the compiler in
which order to store fields:
class (m :: * - * - *) :: (n :: * - * - *)
The idea is that if N and M are distinct field names which might
appear the same record, then there must be an instance of exactly one
of N :: M and M :: N.
The class Contains n r asserts that r is a record type with a field
labelled n:
class Contains n r where
type Project n r
type Delete n r
project :: Constructor n - r - Project n r
delete :: Constructor n - r - Delete n r
There are two associated types: Project n r is the type of the n
field, and Delete n r is the type of the rest of the record. The
functions project and delete give the corresponding values.
The class Lacks n r asserts that r is a record type without a field
labelled n:
class Lacks n r where
type Extend n a r
extend :: Constructor n - a - r - Extend n a r
There is one associated type: Extend n a r is the type of the record
obtained by adding a field of type a labelled n. Note that according
to the AT paper, the parameter a should come last, but this order is
much more convenient. The function extend adds the new field to the
record.
The class Disjoint r s asserts that r and s are record types with no
fields in common:
class Disjoint r s where
type Union r s
union :: r - s - Union r s
There is one associated type: Union r s is the type of the merged
record, and union is the merge function.
Next we define the empty record:
data Empty = Empty
It has no fields, so has no instances of Contains, but lots of
instances of Lacks:
instance Lacks n Empty where
type Extend n a Empty = n a Empty
extend nn x Empty = nn x Empty
It is also disjoint from everything:
instance Disjoint Empty r where
type Union Empty r = r
union Empty t = t
Each field name must be defined as a data type together with
instances of the classes Contains, Lacks and Disjoint as follows:
data N a r = N a r
The type N a r certainly contains a field named N:
instance Contains N (N a r) where
type Project N (N a r) = a
type Delete N (N a r) = r
project N (N x t) = x
delete N (N x t) = t
It also Contains all the fields of r, though you only need to check
names which are below N:
instance m :: N, Contains m r = Contains m (N a r) where
type Project m (N a r) = Project m r
type Delete m (N a r) = N a (Delete m r)
project mm (N x t) = project mm t
delete mm (N x t) = N x (delete mm t)
Similarly, it Lacks all the fields which r Lacks, except for N
itself. This is where we really need the ordering :: to ensure that
m is not equal to N. There are two cases, m :: N:
instance m :: N, Lacks m r = Lacks m (N a r) where
type Extend m b (N a r) = N a (Extend m b r)
extend mm y (N x t) = N x (extend mm y t)
and N :: m:
instance N :: m = Lacks m (N a r) where
type Extend m b (N a r) = m b (N a r)
extend mm y (N x t) = mm y (N x t)
To ensure that N a r is disjoint from s, it is enough that r is
disjoint from s and N is not in their union:
instance Disjoint r s, Lacks N (Union r s) = Disjoint (N a r) s
where
type Union (N a r) s = Extend N a (Union r s)
union (N x t) u = extend N x (union t u)
Finally, we must maintain the ordering ::. It has to be a global
linear order, so if we know the last field name was M, we can define:
instance M :: N
instance m :: M = m :: N
Usage.
--
The record {N1 = x1, ... Nn = xn} should be
Re: [Haskell] extensible records using associated types
Of course, under Usage, I should have written:
The record {N1 = x1, ... Nn = xn} should be constructed as (extend N1
x1 $ ... $ extend Nn xn $ Empty).
Sorry about any confusion!
Barney.
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
Records
Extensible records for Haskell -- A proposal for extensible records which is compatible with type classes and constructor classes, and has a type inference algorithm. Based on ideas of Sean Bechhofer and implemented within Mark Jones' 'Qualified Types'. Barney Hilken and Giuliano Procida This is a proposal for an expressive record language. Records are first class values and can be manipulated by the extraction, addition and deletion of named fields. Polymorphism is allowed over the types of fields and over all fields not explicitly mentioned. This record system is not based on subtyping. Instead, the necessary constraints on polymorphism are expressed as predicates on types. This means that Mark Jones' type inference algorithm extends to record types. In what follows we present one possible syntax for the record values, types and predicates. The importance of our proposal is not the particular syntax, but the logical structure of the type system, and the way it integrates with type classes. -- Labels -- Records are collections of named fields. Because of the limits of namespace, it is necessary to declare which identifiers are to be considered field names. The declaration label A1, ..., An introduces field names or `labels' A1, ..., An. This also helps in finding common errors such as typos. -- Fixed records -- Fixed records are just ML records; their types include complete information about the types of the fields. The expression (A1 is v1, ..., An is vn) denotes a record with fields labelled A1, ..., An containing values v1, ..., vn respectively. The order of fields is not significant. This expression has type (A1 is t1, ..., An is tn) where v1 :: t1, ..., vn :: tn, following the Haskell convention that types have the same form as their values. The same expression can be used as a pattern: f (A1 is x1, ..., an is xn) = rhs where rhs can refer to variables x1, ..., xn. -- Predicates -- Extensible records use the `predicates' of the type class mechanism to allow record polymorphism. For each collection of labels A1, ..., An there is a predicate Lacks A1, ..., An r which says that r is a record type with no `Ai' fields (r must be a constructor variable of kind *). It satisfies Lacks A1, ..., An r = Lacks B1, ...,Bm r for any the subset Bi of the Ai. Note that Lacks A1 r ... Lacks An r = Lacks A1, ..., An r also holds. For aesthetic reasons, the abbreviation Rec r is used when n=0. It says simply that r is a record type. -- Indeterminate record types -- For each label A there are type constructors ()::: * add A ::: * - * - * del A ::: * - * satisfying Lacks A () Lacks A r = Rec (add A t r) Rec r = Rec (del A r) Given a type t and a record type r with no A field, add A t r constructs the type of records with all the fields of r, and additionally, an A field of type t. When applied to an appropriate fixed record type: add A1 t1 (A2 is t2, ..., An is tn) = (A1 is t1, A2 is t2, ..., An is tn) In this way fixed record types may be considered as successive applications of add constructors to the null record type. Given any record type r, del A r constructs the type of records which do not have an A field, but are otherwise like r. If r does not have an A field, then del A r = r. If r is an indeterminate record type (possibly a simple type variable) then add A t r is also an indeterminate record type, likewise del A r. There may be many different ways of expressing the same record type. -- Polymorphic record operations -- For each label A there are three functions A :: Lacks A r = add A t r - t add A :: Lacks A r = t - r - add A t r del A :: Rec r = r - del A r of extraction, extension and deletion: Aj (A1 is v1, ..., An is vn) = vj add A1 v1 (A2 is v2, ..., An is vn) = (A1 is v1, A2 is v2, ..., An is vn) del A1 (A1 is v1, ..., An is vn) = (A2 is v2, ..., An is vn) del B (A1 is v1, ..., An is vn) = (A1 is v1, ..., An is vn) The type system protects against failure and name-clash by insisting that a field exists before it is extracted, and is absent before it is added. Deletion does not require the existence of the field as this is more expressive. Partial pattern matching is also possible: f (A1 is x1, ..., An is xn | y) = rhs If xj has type tj, y has type u and rhs has type v then f :: Lacks A1, ..., An u = add A1 t1 (... add An tn u) - v -- Copatterns -- Pattern matching can be duallized in a useful way for record definition. The equations A1 x = rhs1 . . . An x = rhsn (where rhsj has type tj) define record x :: (A1 is t1, ..., An is tn) with field Aj given by rhsj. This can be generalised to function definition and nested copatterns. -- Implementation -- We have implemented almost all
