Hi,
The EDSL implementation (system design) I'm working on would really benefit from an implementation of fixed-sized vectors. I thought this would be a generally desired ADT but it turned out I wasn't able to find an implementation. I was thinking about using datatype algebra plus GADTs to implement a type-level parameter indicating the size of the vector. I'm a total noob with regard to GADTs and type-level algebra trickery. So my questions are: 1) Do you think it is feasible? Can you think about a better approach? 2) An implementation of type-level Naturals would really help. What has already been done? Thanks in advance, Fons _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Thu, 31 Jan 2008, Alfonso Acosta wrote: > The EDSL implementation (system design) I'm working on would really > benefit from an implementation of fixed-sized vectors. > > I thought this would be a generally desired ADT but it turned out I > wasn't able to find an implementation. > > I was thinking about using datatype algebra plus GADTs to implement > a type-level parameter indicating the size of the vector. http://www.haskell.org/haskellwiki/Linear_algebra http://www.haskell.org/haskellwiki/Libraries_and_tools/Mathematics#Linear_algebra "Frederik Eaton's library for statically checked matrix manipulation in Haskell" _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Am Donnerstag, 31. Januar 2008 12:02 schrieb Alfonso Acosta:
> Hi, > > The EDSL implementation (system design) I'm working on would really > benefit from an implementation of fixed-sized vectors. > > I thought this would be a generally desired ADT but it turned out I > wasn't able to find an implementation. > > I was thinking about using datatype algebra plus GADTs to implement > a type-level parameter indicating the size of the vector. > > I'm a total noob with regard to GADTs and type-level algebra trickery. > So my questions are: > > 1) Do you think it is feasible? Can you think about a better approach? > > 2) An implementation of type-level Naturals would really help. What > has already been done? > > Thanks in advance, > > Fons Hello Fons, interestingly, it occured to me yesterday that the graphics part of Grapefruit would benefit from fixed sized vectors. I think we should implement some small Cabal package which just provides this and upload it to the HackageDB. Are you interested in cooperating with me on this? Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Jan 31, 2008 3:03 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> Hello Fons, > > interestingly, it occured to me yesterday that the graphics part of Grapefruit > would benefit from fixed sized vectors. I think we should implement some > small Cabal package which just provides this and upload it to the HackageDB. > Are you interested in cooperating with me on this? Sure I am! Actually, thanks to the pointers provided by Henning I learned that Oleg (who else!) already has implemented them. See http://okmij.org/ftp/Haskell/number-parameterized-types.html http://www.haskell.org/tmrwiki/NumberParamTypes http://okmij.org/ftp/Haskell/number-param-vector-code.tar.gz (Oleg's multiple flavour implementations of fixed-sized vectors) I think we should base our implementation on Oleg's (for which we need his permission). Actually, I think we should create two separate libraries. One for decimal type-level arithmetic and another for the vector implementation itself. What do you think? _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Thu, 31 Jan 2008, Alfonso Acosta wrote: > On Jan 31, 2008 3:03 PM, Wolfgang Jeltsch <[hidden email]> wrote: > > Hello Fons, > > > > interestingly, it occured to me yesterday that the graphics part of Grapefruit > > would benefit from fixed sized vectors. I think we should implement some > > small Cabal package which just provides this and upload it to the HackageDB. > > Are you interested in cooperating with me on this? > > Sure I am! > > Actually, thanks to the pointers provided by Henning I learned that > Oleg (who else!) already has implemented them. See > > http://okmij.org/ftp/Haskell/number-parameterized-types.html > http://www.haskell.org/tmrwiki/NumberParamTypes > http://okmij.org/ftp/Haskell/number-param-vector-code.tar.gz (Oleg's > multiple flavour implementations of fixed-sized vectors) > > I think we should base our implementation on Oleg's (for which we need > his permission). Actually, I think we should create two separate > libraries. One for decimal type-level arithmetic I remember that type-level arithmetic is already implemented somewhere, certainly more than once, but certainly seldom in a nicely packaged form. erm, here http://www.haskell.org/haskellwiki/Type_arithmetic http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Fixed.html#t%3AFixed also here: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numbers-2007.9.25 ? _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Hello Henning,
Thursday, January 31, 2008, 5:49:23 PM, you wrote: > I remember that type-level arithmetic is already implemented somewhere, > certainly more than once, but certainly seldom in a nicely packaged form. one more: darcs get --partial --tag '0.1' http://www.eecs.tufts.edu/~rdocki01/typenats/ -- Best regards, Bulat mailto:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Henning Thielemann
> I remember that type-level arithmetic is already implemented somewhere,
> certainly more than once, but certainly seldom in a nicely packaged form. > > erm, here > http://www.haskell.org/haskellwiki/Type_arithmetic Yep, there seem to be a few implementations around (decimal, binary, peano) but Oleg's decimal one is likely to be the most friendly when it comes to compiler errors etc .. > http://www.haskell.org/ghc/docs/latest/html/libraries/base/Data-Fixed.html#t%3AFixed > > also here: > http://hackage.haskell.org/cgi-bin/hackage-scripts/package/numbers-2007.9.25 > ? I'm probably missing something, but I don't understand how these libraries could help. Thanks, Fons _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Look at
http://sneezy.cs.nott.ac.uk/fun/feb-07/jeremy-slides.pdf and http://article.gmane.org/gmane.comp.lang.haskell.cafe/27062 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bulat Ziganshin-2
On Jan 31, 2008 5:47 PM, Bulat Ziganshin <[hidden email]> wrote:
> one more: > darcs get --partial --tag '0.1' http://www.eecs.tufts.edu/~rdocki01/typenats/ Thanks for the link, I had already checked this library, but using a binary representation has the same problem as using peano numbers, error reports can be quite cryptic. I still think that using decimals is the way to go. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Alfonso Acosta <alfonso.acosta <at> gmail.com> writes:
> 2) An implementation of type-level Naturals would really help. What > has already been done? I see you have received many suggestions already and personally I don't think you can go wrong with Oleg (et al)'s implementations. For a decimal representation you probably don't have much choice anyway! For completeness let me mention that an unadvertised part of the Dimensional[1] library is an implementation of type-level unary Integers[2] (as opposed to Naturals). Addition, subtraction, multiplication and division is supported. As I side note I've spent quite some time experimenting with fixed-size vectors and matrices with heterogeneous elements. For this I've been using Oleg, Ralf and Keean's HList[3] library which also has type-level unary Naturals. -Bjorn [1] http://dimensional.googlecode.com [2] http://www.buckwalter.se/~bjorn/darcs/dimensional/Numeric/NumType.lhs [3] http://homepages.cwi.nl/~ralf/HList/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Dominic Steinitz
Am Donnerstag, 31. Januar 2008 18:30 schrieb Dominic Steinitz:
> Look at > > http://sneezy.cs.nott.ac.uk/fun/feb-07/jeremy-slides.pdf This is essentially what I had in mind. While Oleg’s implementation needs a “thrusted core”, the GADT solution doesn’t. It would be interesting to combine GADTs with decimal type-level naturals. This could look like this: > class Succ val succ | val -> succ, succ -> val where > > […] > > data List len elem where > > Nil :: List Sz elem > > Cons :: (Succ len len') => elem -> List len elem -> List len' elem Or with efficient contcatenation: > class Sum val1 val2 sum > | val1 val2 -> sum, val1 sum -> val2, val2 sum -> val1 where > > […] > > data List len elem where > > Empty :: List Sz elem > > Singleton :: List (D1 Sz) elem > > Append :: (Add len1 len2 len') => > List len1 elem -> List len2 elem -> List len' elem Note, that type families might make this code even nicer. Some words on the representation of decimal numbers as types. While the representation with types of the form D1 (D2 (D3 Sz)) has the advantage of allowing numbers of arbitrary size, it has the disadvantage of a growing number of parantheses. In my opinion, it would be nicer to have somethink like D1 :- D2 :- D9 :- () with a right-associative operator :-. We could even build the digit list the other way round—() :- D1 :- D2 :- D9—using a left-associative :-. With the latter representation, we wouldn’t need to reverse digit sequences when adding numbers. Well, the representation (D1,D2,D9) might be considered more readable. It has the disadvantage of a fixed maximum size for the numbers. Which takes me to a point I had already considered some time ago: Wouldn’t it be good if we had just a type data Pair val1 val2 = Pair val1 val2 and if then (val1,val2,…,valn) would just be syntactic sugar for this: val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…)) Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Am Donnerstag, 31. Januar 2008 15:15 schrieben Sie:
> […] > I think we should base our implementation on Oleg's (for which we need > his permission). Do you know whether Oleg has released his code under an open source license? If he had, we wouldn’t need his permission. I’m not sure whether we need his permission if we implement a library from scratch, using the concepts behind his library. Concerning the type-indexed lists, we possibly should use the GADT approach instead of the “thrusted core” approach. Concerning type-level naturals, we might want to use the representation () :- D1 :- D2 :- D9 (see my other e-mail). > Actually, I think we should create two separate libraries. One for decimal > type-level arithmetic and another for the vector implementation itself. Definitely! > […] Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Wolfgang Jeltsch-2
Wolfgang Jeltsch wrote:
> Well, the representation (D1,D2,D9) might be considered more readable. It has > the disadvantage of a fixed maximum size for the numbers. Which takes me to > a point I had already considered some time ago: Wouldn’t it be good if we had > just a type > > data Pair val1 val2 = Pair val1 val2 > > and if then (val1,val2,…,valn) would just be syntactic sugar for this: > > val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…)) I've thought of that too.. besides the asymmetry, the presence of _|_/seq makes them actually not equivalent though, unfortunately ~Isaac _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Wolfgang Jeltsch-2
On Jan 31, 2008 11:35 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> Am Donnerstag, 31. Januar 2008 18:30 schrieb Dominic Steinitz: > > Look at > > > > http://sneezy.cs.nott.ac.uk/fun/feb-07/jeremy-slides.pdf > > This is essentially what I had in mind. While Oleg's implementation needs > a "thrusted core", the GADT solution doesn't. True. However using GADTs doesn't allow to internally make use of Arrays, which (tell me if I'm wrong) are likely to be faster than the naive GADT implementation. Actually the GADT implementation you proposed fits nicely with the Vector definition already used in my EDSL (it is isomorphic actually), but efficiency could be an issue. > Some words on the representation of decimal numbers as types. While the > representation with types of the form D1 (D2 (D3 Sz)) has the advantage of > allowing numbers of arbitrary size, it has the disadvantage of a growing > number of parantheses. In my opinion, it would be nicer to have somethink > like D1 :- D2 :- D9 :- () with a right-associative operator :-. We could > even build the digit list the other way round—() :- D1 :- D2 :- D9—using a > left-associative :-. With the latter representation, we wouldn't need to > reverse digit sequences when adding numbers. Right, I agree. I think we should use the arbitrary-size implementation (actually, how arbitrary is it? what's the limit of GHC, if any?). To make it friendlier for the end user I thought about defining aliases for lets say the first 10000 numbers using Template Haskell. That could even make error reports friendlier (not sure to what point though). What do you think? So, we'll be making two separate libraries then. We should think about names. What about FixedVector for the vector library and DecTypArith (maybe too long) or DecTypes for the type-level decimal arithmetic library? I'll put my hands dirty once we agree on this. Cheers, Fons _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
> What about FixedVector for the vector library and DecTypArith (maybe
> too long) or DecTypes for the type-level decimal arithmetic library? Actually it would maybe be better to create common high-level interface that could include unary, binary and decimal arithmetic so that the library could be easily reused in other projects (people like Bjorn, seem to be using the unary implementation). I don't know if it would be feasible though. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Alfonso Acosta <alfonso.acosta <at> gmail.com> writes:
> Actually it would maybe be better to create common high-level > interface that could include unary, binary and decimal arithmetic so > that the library could be easily reused in other projects (people like > Bjorn, seem to be using the unary implementation). I don't know if it > would be feasible though. My reason for going with unary implementation was that it seemed to be the easiest and less tedious to implement. But is sure does make the error messages less friendly. It also limits the magnitude of the numbers quite severely unless one bumps up the type checker stack size. From the source code: "The practical size of the NumTypes is limited by the type checker stack. If the NumTypes grow too large (which can happen quickly with multiplication) an error message similar to the following will be emitted: Context reduction stack overflow; size = 20 Use -fcontext-stack=N to increase stack size to N This situation could concievably be mitigated significantly by using e.g. a binary representation of integers rather than Peano numbers." For my use (keeping track of physical dimensions) this hasn't been a problem. 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. Concerning whether or not there is any value in being able to change the representation of the type- level naturals in your library, my guess is that the value wouldn't be all that great. As I mentioned I use my implementation for tracking physical dimensions and HList's HNats for constraining vector dimensions but this isn't a problem since I cannot conceive of any reason why I would want to intermix the two. Of course, other usage scenarios exist where there would be a desire to intermix the vector dimensions with something else...? So sure, if you can abstract the representation away by all means do it. But I wouldn't go out of my way or impair the rest of the library to achieve this. Hope this helps, Bjorn _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
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". Again, for a proof-of-concept dimensional analysis arithmetic. No problem with the stack, but the error messages are still less than clear. -- Aaron Denney -><- _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Isaac Dupree
Am Freitag, 1. Februar 2008 05:11 schrieben Sie:
> Wolfgang Jeltsch wrote: > > Well, the representation (D1,D2,D9) might be considered more readable. > > It has the disadvantage of a fixed maximum size for the numbers. Which > > takes me to a point I had already considered some time ago: Wouldn’t it > > be good if we had just a type > > > > data Pair val1 val2 = Pair val1 val2 > > > > and if then (val1,val2,…,valn) would just be syntactic sugar for this: > > > > val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…)) > > I've thought of that too.. besides the asymmetry, the presence of > _|_/seq makes them actually not equivalent though, unfortunately > > ~Isaac With Ryan’s proposal (using strictness annotations) the new representation should be equivalent to the old one. Or am I missing something? Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Am Freitag, 1. Februar 2008 13:00 schrieb Alfonso Acosta:
> On Jan 31, 2008 11:35 PM, Wolfgang Jeltsch <[hidden email]> wrote: > > Am Donnerstag, 31. Januar 2008 18:30 schrieb Dominic Steinitz: > > > Look at > > > > > > http://sneezy.cs.nott.ac.uk/fun/feb-07/jeremy-slides.pdf > > > > This is essentially what I had in mind. While Oleg's implementation > > needs a "thrusted core", the GADT solution doesn't. > > True. However using GADTs doesn't allow to internally make use of > Arrays, which (tell me if I'm wrong) are likely to be faster than the > naive GADT implementation. It depends. My first GADT implementation is equivalent to the [] type and often [] is better than arrays. For example, if you read the contents of a file and process it with maps, filters, etc., [] is likely to give you constant space usage which arrays don’t. If you want to lookup elements by index, then arrays are better, of course. For my purpose, it would be fine to use a []-like implementation, I think. > […] > > Some words on the representation of decimal numbers as types. While the > > representation with types of the form D1 (D2 (D3 Sz)) has the advantage > > of allowing numbers of arbitrary size, it has the disadvantage of a > > growing number of parantheses. In my opinion, it would be nicer to have > > somethink like D1 :- D2 :- D9 :- () with a right-associative operator :-. > > We could even build the digit list the other way round—() :- D1 :- D2 :- > > D9—using a left-associative :-. With the latter representation, we > > wouldn't need to reverse digit sequences when adding numbers. > > Right, I agree. I think we should use the arbitrary-size implementation So let’s use the representation with the left-associative :- (or whatever operator we might choose). > (actually, how arbitrary is it? what's the limit of GHC, if any?). Arbitrary enough, I think. If we don’t need lists with billions of elements, our representations will have less than 8 digits. > To make it friendlier for the end user I thought about defining > aliases for lets say the first 10000 numbers using Template Haskell. > That could even make error reports friendlier (not sure to what point > though). What do you think? I have no clear opinion about that at the moment. Maybe it’s okay to use the representation directly. This way, we don’t introduce a dependeny on the Template Haskell language extension (which is only supported by GHC), and the actual representation will occur in error messages anyway whenever the message shows a computed number. > So, we'll be making two separate libraries then. We should think about > names. > > What about FixedVector for the vector library and DecTypArith (maybe > too long) or DecTypes for the type-level decimal arithmetic library? Alas, there is an inconsistency in naming packages already. Some prefer names which are entirely lowercase, some prefer camel case. I prefer lowercase, with hyphens separating parts of the name. And I also don’t like unusual abbreviations like “typ” (not much shorter than “type”). To mention arithmetics is not so important. So maybe something like “type-level-decimals”? Maybe it’s better to put different type-level programming things into a single package. Then we could name this package “type-level” or something similar. We could start with our decimals. Other type-level things could be added later. I already have some code about type-level booleans. It’s not very sensible to put these few lines into a separate package. It might be nice if we had a general type-level programming package where I could put this code into. As for the name of the fixed-size list package, I have to say that I don’t like the term “vector” in this context. A vector is actually something with addition and scalar multiplication defined on it. Maybe we should make also this package’s scope wider. What about something like “safe-data” or similar? > I'll put my hands dirty once we agree on this. Great!! > Cheers, > > Fons Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Am Freitag, 1. Februar 2008 13:09 schrieben Sie:
> > What about FixedVector for the vector library and DecTypArith (maybe > > too long) or DecTypes for the type-level decimal arithmetic library? > > Actually it would maybe be better to create common high-level > interface that could include unary, binary and decimal arithmetic so > that the library could be easily reused in other projects (people like > Bjorn, seem to be using the unary implementation). I don't know if it > would be feasible though. I’d say, let’s start with the decimal thing. We can extend our package later if there’s a need to do this, can’t we? Best wishes, Wolfgang _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |