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
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
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: 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: 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
