Implementing fixed-sized vectors (using datatype algebra?)

85 messages
12345
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch <[hidden email]> wrote: > Nat means "all natural numbers except zero" while Nat0 means "all natural > numbers (including zero)".  Since in computer science, natural numbers > usually cover zero, we should use Pos instead of Nat and Nat instead of Nat0. Sounds sensible, actually Nat and Nat0 is confusing. However I would rather use Pos and Nat0 to make explicit that naturals include zero . Depending on the definition of naturals they might or might not include zero.  http://en.wikipedia.org/wiki/Natural_number> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the > latter representation should probably be prefered.  With it, :+ always has a > number as its left argument and a digit as its right.  Without the () :+ we > get ugly exceptional cases. > You can see this, for example, in the instance > declarations for Compare.  With the second representation, we could reduce > the number of instances dramatically.  We would define a comparison of digits > (verbose) and than a comparison of numbers based on the digit comparison (not > verbose). Even if () would be preferred from the programmers point of view (I'm not sure how much we could reduce the number of instances though), it makes the representation less attractive on the user-side. Anyone using the library would find it annoying and would wonder why is it neccessary. Unless we find a way to use () only internally (we should use a one-character type to make it shorter to type) I think we should stick to current representation. > :+ is already used as the constructor for complex numbers.  We should probably > use some different operator. Right. I didn't think about that, thanks. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 On Feb 7, 2008 9:01 PM, Dan Weston <[hidden email]> wrote: > This may be a GHC bug, but even though in the module > Data.TypeLevel.Num.Reps has the header > > {-# LANGUAGE EmptyDataDecls, TypeOperators #-} > > I still get an error with both ghc and ghci version 6.8.2 unless I throw > in the -XTypeOperators flag. If you are using type operators in a module you have to supply the flag, independently of what flags are supplied in other modules. The same applies for other extensions which modify the _syntax_ of the language (e.g. Template Haskell etc ...) So, it's not a bug. As a side note, even if the TypeOperators flag is supplied GHC 6.8.2 fires an error with the following declaration: instance (Compare x y CEQ) => x :==: y -- GHC fires a "Malformed instance header" error whereas using an equivalent prefix definition works just fine instance (Compare x y CEQ) => (:==:) x y _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Dan Weston On Feb 7, 2008 8:38 PM, Dan Weston <[hidden email]> wrote: > I know that naming is arbitrary, but... > > Digits in types seems ugly to me. In this case, it is also redundant. > Everyone but FORTRAN programmers counts from 0, not 1. Nat and Pos seem > clear. Nat0 could even mean Nat \ {0}, the opposite of what is proposed, > so confusion is even increased with Nat0. Ok, fair enough. I changed the names of Positives and Naturals (which do include 0) for Pos and Nat. The change (together with a connective rename from :+ to :* ) is already pushed in the darcs repository. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Dan Weston On 8 Feb 2008, at 8:38 am, Dan Weston wrote: > I know that naming is arbitrary, but... > > Digits in types seems ugly to me. In this case, it is also   > redundant. Everyone but FORTRAN programmers counts from 0, not 1.   > Nat and Pos seem clear. Nat0 could even mean Nat \ {0}, the   > opposite of what is proposed, so confusion is even increased with   > Nat0. For what it's worth, the Ada names for the types      {x in Z | x >= 0} and {x in Z | x > 0} are "Natural" and "Positive" respectively.  Natural is useful for   counting stuff; Positive is useful mainly because Ada practice is to index from 1. In Z, |N is used for natural numbers, which are defined to include 0. In modern set theory, both the cardinal and the ordinal numbers start   with 0, not with 1. All things considered, I would be very upset indeed if a type called   "Nat" or "Natural" or something like that did not include 0. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Bugzilla from alfonso.acosta@gmail.com Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie: > On Feb 7, 2008 4:16 PM, Wolfgang Jeltsch <[hidden email]> wrote: > […] > > You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the > > latter representation should probably be prefered.  With it, :+ always > > has a number as its left argument and a digit as its right.  Without the > > () :+ we get ugly exceptional cases. > > You can see this, for example, in the instance > > declarations for Compare.  With the second representation, we could > > reduce the number of instances dramatically.  We would define a > > comparison of digits (verbose) and than a comparison of numbers based on > > the digit comparison (not verbose). > > Even if () would be preferred from the programmers point of view (I'm > not sure how much we could reduce the number of instances though), it > makes the representation less attractive on the user-side. Anyone > using the library would find it annoying and would wonder why is it > neccessary. I wouldn’t wonder.  Leaving out the () :* part just works because our type-level “values” are not typed, i.e., there aren’t different kinds Digit and Number but only kind *.  If :+ would be a data constructor (on the value level), it would take a number and a digit argument which would forbid using a digit as its left argument.  So I consider using a digit on the left as “unclean”.  It’s similar to using a number as the second part of a cons cell in LISP. > […] Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 On Fri, 8 Feb 2008, Wolfgang Jeltsch wrote: > Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie: > > > > Even if () would be preferred from the programmers point of view (I'm > > not sure how much we could reduce the number of instances though), it > > makes the representation less attractive on the user-side. Anyone > > using the library would find it annoying and would wonder why is it > > neccessary. > > I wouldn’t wonder.  Leaving out the () :* part just works because our > type-level “values” are not typed, i.e., there aren’t different kinds Digit > and Number but only kind *.  If :+ would be a data constructor (on the value > level), it would take a number and a digit argument which would forbid using > a digit as its left argument.  So I consider using a digit on the left > as “unclean”.  It’s similar to using a number as the second part of a cons > cell in LISP. seconded _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Wolfgang Jeltsch-2 >> > You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, the >> > latter representation should probably be prefered.  With it, :+ always >> > has a number as its left argument and a digit as its right.  Without the >> > () :+ we get ugly exceptional cases. >> > You can see this, for example, in the instance >> > declarations for Compare.  With the second representation, we could >> > reduce the number of instances dramatically.  We would define a >> > comparison of digits (verbose) and than a comparison of numbers based on >> > the digit comparison (not verbose). >> >> Even if () would be preferred from the programmers point of view (I'm >> not sure how much we could reduce the number of instances though), it >> makes the representation less attractive on the user-side. Anyone >> using the library would find it annoying and would wonder why is it >> neccessary. > I wouldn’t wonder.  Leaving out the () :* part just works because our > type-level “values” are not typed, i.e., there aren’t different kinds Digit > and Number but only kind *.  If :+ would be a data constructor (on the value > level), it would take a number and a digit argument which would forbid using > a digit as its left argument.  So I consider using a digit on the left > as “unclean”.  It’s similar to using a number as the second part of a cons > cell in LISP. How 'bout treating :+ as similar to `append' rather than similar to `cons'? Basically treat :+ as taking 2 numbers (rather than a number and a digit).         Stefan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 On Feb 8, 2008, at 11:14 , Stefan Monnier wrote: >>>> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I   >>>> think, the >>>> latter representation should probably be prefered. >>>> (...) > How 'bout treating :+ as similar to `append' rather than similar to   > `cons'? > Basically treat :+ as taking 2 numbers (rather than a number and > a digit). Dumb questions department:  why not define e.g. D'0 .. D'9 as () :*   0 .. () :* 9?  Programmers then get D'1 :* 2, but the library sees   () :* 1 :* 2. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [hidden email] system administrator [openafs,heimdal,too many hats] [hidden email] electrical and computer engineering, carnegie mellon university    KF8NH _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 On Fri, 8 Feb 2008, Brandon S. Allbery KF8NH wrote: > On Feb 8, 2008, at 11:14 , Stefan Monnier wrote: > > >>>> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I > >>>> think, the > >>>> latter representation should probably be prefered. > >>>> (...) > > How 'bout treating :+ as similar to `append' rather than similar to > > `cons'? > > Basically treat :+ as taking 2 numbers (rather than a number and > > a digit). > > Dumb questions department:  why not define e.g. D'0 .. D'9 as () :* > 0 .. () :* 9?  Programmers then get D'1 :* 2, but the library sees > () :* 1 :* 2. Do you remember that they talk about types D0, D1, and so on? _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Brandon S Allbery KF8NH Brandon S. Allbery KF8NH wrote: > > On Feb 8, 2008, at 11:14 , Stefan Monnier wrote: > >>>>> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I >>>>> think, the >>>>> latter representation should probably be prefered. >>>>> (...) >> How 'bout treating :+ as similar to `append' rather than similar to >> `cons'? >> Basically treat :+ as taking 2 numbers (rather than a number and >> a digit). > > Dumb questions department:  why not define e.g. D'0 .. D'9 as () :* 0 .. > () :* 9?  Programmers then get D'1 :* 2, but the library sees () :* 1 :* 2. > No, D'0 should be (), not () :* D0. If you allow () :* D0, then you introduce redundant types for the same number: In the first case, D'0 :* D'3 == D'3, and D'0 :* D'0 has no instance. In your example, D'3 and D'0 :* D'3 are equivalent, but no longer unify. Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 Dan Weston wrote: > Brandon S. Allbery KF8NH wrote: >> >> On Feb 8, 2008, at 11:14 , Stefan Monnier wrote: >> >>>>>> You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I >>>>>> think, the >>>>>> latter representation should probably be prefered. >>>>>> (...) >>> How 'bout treating :+ as similar to `append' rather than similar to >>> `cons'? >>> Basically treat :+ as taking 2 numbers (rather than a number and >>> a digit). >> >> Dumb questions department:  why not define e.g. D'0 .. D'9 as () :* 0 >> .. () :* 9?  Programmers then get D'1 :* 2, but the library sees () :* >> 1 :* 2. >> > > No, D'0 should be (), not () :* D0. If you allow () :* D0, then you > introduce redundant types for the same number: > > In the first case, D'0 :* D'3 == D'3, and D'0 :* D'0 has no instance. In > your example, D'3 and D'0 :* D'3 are equivalent, but no longer unify. > > Dan On second thought, how would you write D'3 :* D0 ? I think maybe using the () makes it fundamentally difficult to restrict multiple types for the same number. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Bugzilla from alfonso.acosta@gmail.com On 2008-02-05, Alfonso Acosta <[hidden email]> wrote: > On Feb 5, 2008 4:10 PM, Henning Thielemann ><[hidden email]> wrote: >> >> On Fri, 1 Feb 2008, Aaron Denney wrote: >> >> > On 2008-02-01, Bjorn Buckwalter <[hidden email]> wrote: >> > > If Naturals had been sufficient for me I wouldn't have done my own >> > > implementation (I'm unaware of any other implementation of Integers). >> > > And there is certainly a lot of value to the clearer error messages >> > > from a decimal representation. >> > >> > I did a balanced-base-three (digits are 0, and +- 1) representation to >> > get negative "decimals". >> >> Nice. In German the digit values are sometimes called "eins, keins, meins". :-) > > I'm almost done with the decimal library but it would be nice to check > some Integer implementations for future inclusion. So, Aaron, Björn, > are your implementations available somewhere? http://ofb.net/~wnoise/repos/dimensional/-- Aaron Denney -><- _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Bugzilla from alfonso.acosta@gmail.com On Feb 6, 2008 8:47 PM, Alfonso Acosta <[hidden email]> wrote: > On Feb 7, 2008 2:30 AM, Bjorn Buckwalter <[hidden email]> wrote: > > Ok. Is this what people want -- one big hold-all library with > > everything, as opposed to smaller more specialized packages? I guess I > > can see advantages (real or perceived) to both approaches. > > Apart from Dockins' typenats library there are no other user-friendly > specific type-level libraries that know, so I cannot really tell if > people would prefer a hold-all library or a couple of more granular > specialized ones. > > Right now is not hold-all at all (it is still vaporware actually :)), > so I think there's no reason to discuss that at this point. Let's see > what people think. Right, of course. I'll be taking a look at your no-longer-vaporware! ;) _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Stefan Monnier Am Freitag, 8. Februar 2008 17:14 schrieb Stefan Monnier: > >> > You seem to write 12 as 1 :+ 2 instead of () :+ 1 :+ 2.  But I think, > >> > the latter representation should probably be prefered.  With it, :+ > >> > always has a number as its left argument and a digit as its right. > >> > Without the () :+ we get ugly exceptional cases. > >> > You can see this, for example, in the instance > >> > declarations for Compare.  With the second representation, we could > >> > reduce the number of instances dramatically.  We would define a > >> > comparison of digits (verbose) and than a comparison of numbers based > >> > on the digit comparison (not verbose). > >> > >> Even if () would be preferred from the programmers point of view (I'm > >> not sure how much we could reduce the number of instances though), it > >> makes the representation less attractive on the user-side. Anyone > >> using the library would find it annoying and would wonder why is it > >> neccessary. > > > > I wouldn’t wonder.  Leaving out the () :* part just works because our > > type-level “values” are not typed, i.e., there aren’t different kinds > > Digit and Number but only kind *.  If :+ would be a data constructor (on > > the value level), it would take a number and a digit argument which would > > forbid using a digit as its left argument.  So I consider using a digit > > on the left as “unclean”.  It’s similar to using a number as the second > > part of a cons cell in LISP. > > How 'bout treating :+ as similar to `append' rather than similar to `cons'? > Basically treat :+ as taking 2 numbers (rather than a number and > a digit). So what would (D1 :* D1) :* (D2 :* D2) mean then? >         Stefan Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Wolfgang Jeltsch-2 On Feb 8, 2008 4:10 PM, Wolfgang Jeltsch <[hidden email]> wrote: > Am Donnerstag, 7. Februar 2008 16:31 schrieben Sie: > > Even if () would be preferred from the programmers point of view (I'm > > not sure how much we could reduce the number of instances though), it > > makes the representation less attractive on the user-side. Anyone > > using the library would find it annoying and would wonder why is it > > neccessary. > > I wouldn't wonder.  Leaving out the () :* part just works because our > type-level "values" are not typed, i.e., there aren't different kinds Digit > and Number but only kind *.  If :+ would be a data constructor (on the value > level), it would take a number and a digit argument which would forbid using > a digit as its left argument. Well, the fact is that :+ (or :* as it is called now) is not a value constructor but a type constructor as you said, so I don't think your example really applies here. Besides, you should be regarded :* as (,) and not as a constructor which "would take a number and a digit argument which would forbid using a digit as its left argument." Indeed, :* exists as a value-level constructor too and works exactly like that. Furthermore, you probably consider using () as natural and logical because you are still thinking from the implementation side. If you forget the implementation details and think as a user who barely wants to write type-level numerical literals, :* is simply an ugly syntactic requirement which we cannot get rid of (I would be happy to find another representation closer to a literal, but I couldn't until now). That is not the case for (), since, as shown in the initial implementation, can be avoided. So, for me, it's just a matter of usability and syntax, the closer the representation can be to literals, the better. I don't see the semantic implications of :* as a valid argument. For me, :* is just an unavoidable ugly syntactical token without meaning. Imagine that for some reason, adding () as a prefix in every numerical literal made the implementation of a compiler slightly easier/faster. I bet users would rant about it till exhaustion :) If the argument was that,  for some reason, () was proven to speed up the implementation or make a big maintainability difference (I still have my doubts) it would maybe make more sense (I still wouldn't be sure if it pays off though). Maybe it would be a good idea to create a patch and see what happens :) As a side note, I think that type-value digits actually are "typed" (metatyped maybe is a nicer term?). Class constraints take the role of types in this case. After all (sorry if the definition is imprecise), a type establishes a set of valid values. "Nat n => n" does exactly that. For example, it forces type-level naturals to be normalized (i.e. numerals with leading zeros don't satisfy the Nat constraint) > So I consider using a digit on the left > as "unclean".  It's similar to using a number as the second part of a cons > cell in LISP. Again, the comparisson is based on semantical implications of the implementation which shouldn't be visible for, or at least not taken into consideration by,  the final user. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Stefan Monnier On Feb 8, 2008 5:14 PM, Stefan Monnier <[hidden email]> wrote: > How 'bout treating :+ as similar to `append' rather than similar to `cons'? > Basically treat :+ as taking 2 numbers (rather than a number and > a digit). Interpreting it like that would certainly make make more sense. But again, I think that :* should be interpreted just as an unavoidable syntactical annoyance without meaning or interpretation. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|

Re: Re: Implementing fixed-sized vectors (using datatype algebra?)

 In reply to this post by Wolfgang Jeltsch-2 On Feb 9, 2008 4:08 PM, Wolfgang Jeltsch <[hidden email]> wrote: > So what would (D1 :* D1) :* (D2 :* D2) mean then? Nothing. That value doesn't satisfy the Nat or Post class constraints and should be taken into consideration. Why should :* be provided a meaning? it is an unavoidable syntactical connective for all that I care. The meaning is provided by class constraints and that's all that matter from the semantical point of view. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe