Implementing fixed-sized vectors (using datatype algebra?)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
85 messages Options
12345
Reply | Threaded
Open this post in threaded view
|

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

Isaac Dupree
Wolfgang Jeltsch wrote:

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

adding the strictness annotation seems to make them equivalent, yes I
agree (I hadn't seen that post when I wrote that reply)

~Isaac
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Wolfgang Jeltsch-2
On Feb 1, 2008 10:33 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> > 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?

OK, let's do it like that.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
In reply to this post by Wolfgang Jeltsch-2
On Feb 1, 2008 10:32 PM, Wolfgang Jeltsch <[hidden email]> wrote:

> Am Freitag, 1. Februar 2008 13:00 schrieb Alfonso Acosta:
> > On Jan 31, 2008 11:35 PM, Wolfgang Jeltsch <[hidden email]>
> > > 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.

For mine it would be fine too. Let's implement our needs and then
maybe extend it if someone rants about it.

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

Well, my EDSL already makes extensive use of TH. So, being selfish, it
wouldn't be a problem for me (or any other GHC user) and I think it
would make the library much more usable.

Just compare

f :: List (() :- D1 :- D0 :- D0 :- 1000) Int -> List (() :- D1 :- D0
:- D0 :- D0) Int

with, let's say

f :: List A1000 Int -> List A1000 Int

Again, if someone complains about the TH dependency, the aliases could
be generated by TH but saved statically in a module for each release.

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

Sounds sensible. However, I would rather prefer something like
type-level-comp (from type level computations) or type-level-prog
(from type level programming). Type level by itself doesn't describe
the functionality of the package.

> 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 think safe-data is a bit too general and might lead to confusion
with other safe data packages (namely Mitchell's Safe library). Since
the main particularity of the library is that safety properties are
achieved via "emulating" dependent types I think that
light-dependent-types (from lightweight dependent types),
number-parameterized-data or simply parameterized-data (this is the
name I like best) would be more appropiate.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
On Feb 2, 2008 2:54 PM, Alfonso Acosta <[hidden email]> wrote:
> Just compare
>
> f :: List (() :- D1 :- D0 :- D0 :- 1000) Int -> List (() :- D1 :- D0
> :- D0 :- D0) Int

I meant

f :: List (() :- D1 :- D0 :- D0 :- D0) Int -> List (() :- D1 :- D0 :-
D0 :- D0) Int

sorry for the typo
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
In reply to this post by Bugzilla from alfonso.acosta@gmail.com
Am Samstag, 2. Februar 2008 14:54 schrieben Sie:
> On Feb 1, 2008 10:32 PM, Wolfgang Jeltsch wrote:
> > Am Freitag, 1. Februar 2008 13:00 schrieb Alfonso Acosta:
> […]

> > > 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.
>
> Well, my EDSL already makes extensive use of TH. So, being selfish, it
> wouldn't be a problem for me (or any other GHC user) and I think it
> would make the library much more usable.
>
> Just compare
>
> f :: List (() :- D1 :- D0 :- D0 :- 1000) Int -> List (() :- D1 :- D0 :-
> D0 :- D0) Int
>
> with, let's say
>
> f :: List A1000 Int -> List A1000 Int
>
> Again, if someone complains about the TH dependency, the aliases could
> be generated by TH but saved statically in a module for each release.

Hmm, this could be a compromise although I’m not sure whether it is sensible
to have a module with thousands of declarations.  Another solution would be
to put the Template Haskell convenience stuff into a separate package.  The
core package would probably be usable with Hugs too, while the convenience
package would be usable only with GHC.

At the moment, I’m not sure how often I’ll need to state type-level numbers
explicitely.  So currently I cannot know how important aliases for type-level
numbers are.

> > > 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.
>
> Sounds sensible. However, I would rather prefer something like
> type-level-comp (from type level computations) or type-level-prog
> (from type level programming). Type level by itself doesn't describe
> the functionality of the package.

Hmm, package names don’t have to be descriptive.  Short names tend to sound
better and be easier to remember.  My FRP GUI and graphics library is named
Grapefruit.  This name makes hardly any sense.  It refers to the previous
library Fruit and the fact that I like Grapefruits—nothing more.  But it’s a
name, people can remember more easily than FRGGLER (Functional Reactive GUI
and Graphics Library with Extensible Records). ;-)

In addition, abbreviations like “comp” typically have the problem of being
ambiguous: computation, composition, component, …

So I still prefer type-level.

> > 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 think safe-data is a bit too general and might lead to confusion
> with other safe data packages (namely Mitchell's Safe library). Since
> the main particularity of the library is that safety properties are
> achieved via "emulating" dependent types I think that
> light-dependent-types (from lightweight dependent types),
> number-parameterized-data or simply parameterized-data (this is the
> name I like best) would be more appropiate.

parametrized-data looks good.  The others seem to be too long again.

So type-level + parametrized-data is my vote.  But don’t let’s spend too much
time discussing the name. ;-)

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
On Feb 4, 2008 12:36 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> Am Samstag, 2. Februar 2008 14:54 schrieben Sie:
> > Again, if someone complains about the TH dependency, the aliases could
> > be generated by TH but saved statically in a module for each release.
>
> Hmm, this could be a compromise although I'm not sure whether it is sensible
> to have a module with thousands of declarations.

As long as the module is automatically generated I don't see why it
would be a problem.

Bear in mind that using TH would, in practice, be equivalent to code
such a module by hand anyway.

> Another solution would be
> to put the Template Haskell convenience stuff into a separate package.  The
> core package would probably be usable with Hugs too, while the convenience
> package would be usable only with GHC.


I'm not sure if it worths it to create a separate package and add
another dependency for those who would like to use it.

I don't still know how many people would be interested in using the
type-level library so, again, I think it won't hurt to include the
TH-generated aliases and then change it if some non-GHC user rants
about it.


> So type-level + parametrized-data is my vote.  But don't let's spend too much
> time discussing the name. ;-)

Fair enough. type-level + parameterized-data it is then (unless
someone else has a better suggestion). I'm going to begin coding now.

I'll host the project in community.haskell.org, do you have an account there?

PS: BTW, I asked Oleg for permission and, as expected, agreed to
create the library under a BS-D license.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
Am Montag, 4. Februar 2008 13:22 schrieben Sie:
> On Feb 4, 2008 12:36 PM, Wolfgang Jeltsch wrote:
>[…]

> I don't still know how many people would be interested in using the
> type-level library so, again, I think it won't hurt to include the
> TH-generated aliases and then change it if some non-GHC user rants
> about it.

Okay, let’s do so for now.

> > So type-level + parametrized-data is my vote.  But don't let's spend too
> > much time discussing the name. ;-)
>
> Fair enough. type-level + parameterized-data it is then (unless
> someone else has a better suggestion). I'm going to begin coding now.

Yes, go ahead. :-)  Thanks a lot.

> I'll host the project in community.haskell.org, do you have an account
> there?

Now, I haven’t. :-(

> PS: BTW, I asked Oleg for permission and, as expected, agreed to
> create the library under a BS-D license.

Great.  So the packages you create now will be released under BSD3, right?

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
On Feb 4, 2008 8:27 PM, Wolfgang Jeltsch <[hidden email]> wrote:
> Am Montag, 4. Februar 2008 13:22 schrieben Sie:
> > I don't still know how many people would be interested in using the
> > type-level library so, again, I think it won't hurt to include the
> > TH-generated aliases and then change it if some non-GHC user rants
> > about it.
>
> Okay, let's do so for now.

Actually, I was considering to conditionally include the TH code or
not depending on the compiler (using Cabal configurations).

I thought "that should make everyone happy". Then, I realized we
agreed to make use of infix type constructors anyway (which seems to
be a GHC-only extension, tell me if I'm wrong), so the TH dependency
is not that important anymore (unless we decide to avoid infix type
constructors)

> > I'll host the project in community.haskell.org, do you have an account
> > there?
>
> Now, I haven't. :-(

Well, you can request one at
http://community.haskell.org/admin/account_request.html if you want

Otherwise I'll take the maintainer role.

> > PS: BTW, I asked Oleg for permission and, as expected, agreed to
> > create the library under a BS-D license.
>
> Great.  So the packages you create now will be released under BSD3, right?

Yes, that's the intention.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
Am Montag, 4. Februar 2008 20:44 schrieben Sie:
> > > I'll host the project in community.haskell.org, do you have an account
> > > there?
> >
> > Now, I haven't. :-(
>
> Well, you can request one at
> http://community.haskell.org/admin/account_request.html if you want
>
> Otherwise I'll take the maintainer role.

I’m fine with you having the maintainer role as long as you accept a patch
from me from time to time. :-)


Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Henning Thielemann
In reply to this post by Aaron Denney

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". :-)
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
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?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bjorn Buckwalter-2
On Feb 5, 2008 2:16 PM, 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?

As noted elsewhere in the thread my implementation is available at:

http://www.buckwalter.se/~bjorn/darcs/dimensional/Numeric/NumType.lhs

It is my intent to extract this (self-contained) module to its own
package and put on hackage. It's been a low priority for me but I'm
rather incentivized by this thread.

Thanks,
Bjorn
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
On Feb 5, 2008 8:29 PM, Bjorn Buckwalter <[hidden email]> wrote:

>
> On Feb 5, 2008 2:16 PM, 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?
>
> As noted elsewhere in the thread my implementation is available at:
>
> http://www.buckwalter.se/~bjorn/darcs/dimensional/Numeric/NumType.lhs

Thanks!

> It is my intent to extract this (self-contained) module to its own
> package and put on hackage. It's been a low priority for me but I'm
> rather incentivized by this thread.

Great!

How about joining efforts? As I said I almost have a preliminary
version of the decimal library which I'll realease for reviewing
purpouses soon (It won't include Integer computations though)
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bjorn Buckwalter-2
> > > 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?
> >
> > As noted elsewhere in the thread my implementation is available at:
> >
> > http://www.buckwalter.se/~bjorn/darcs/dimensional/Numeric/NumType.lhs
>
> Thanks!
>
> > It is my intent to extract this (self-contained) module to its own
> > package and put on hackage. It's been a low priority for me but I'm
> > rather incentivized by this thread.
>
> Great!
>
> How about joining efforts? As I said I almost have a preliminary
> version of the decimal library which I'll realease for reviewing
> purpouses soon (It won't include Integer computations though)

Well, could you elaborate a little on joining efforts? The effort I
was planning to invest in my package consists mainly of creating a
.cabal file plus some logistics to get tarballs to where they have to
be.

I understand that you (and Wolfgang) are creating a library of type
level decimals for the purpose of constraining vector (list?) lengths.
After that I haven't been paying attention fully to the thread. Is the
goal to create a general-purpose library for type-level programming
and my module would fit into that grander scheme?

Or did you have something else in mind with joining efforts? E.g. help
reviewing your code or writing new code?
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
On Feb 6, 2008 4:32 AM, Bjorn Buckwalter <[hidden email]> wrote:

> Well, could you elaborate a little on joining efforts? The effort I
> was planning to invest in my package consists mainly of creating a
> .cabal file plus some logistics to get tarballs to where they have to
> be.
>
> I understand that you (and Wolfgang) are creating a library of type
> level decimals for the purpose of constraining vector (list?) lengths.
> After that I haven't been paying attention fully to the thread. Is the
> goal to create a general-purpose library for type-level programming
> and my module would fit into that grander scheme?

Yes,the idea is to create a Cabal-ready wide-scope type-level
programming library, joining the operations implemented in the
different type-level libraries which are around. The goal (or at least
mine) is to provide a common reusable type-level library which saves
constantly reinventing the wheel.

I'll provide an initial implementation (just including naturals in
decimal representation) soon. Wolfgang suggested adding booleans at a
later point too if I recall properly.

Any useful type-level operation should have a place in the library.

> Or did you have something else in mind with joining efforts? E.g. help
> reviewing your code or writing new code?
>

This would certainly help too.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bjorn Buckwalter-2
On Feb 6, 2008 1:03 PM, Alfonso Acosta <[hidden email]> wrote:

> On Feb 6, 2008 4:32 AM, Bjorn Buckwalter <[hidden email]> wrote:
> > I understand that you (and Wolfgang) are creating a library of type
> > level decimals for the purpose of constraining vector (list?) lengths.
> > After that I haven't been paying attention fully to the thread. Is the
> > goal to create a general-purpose library for type-level programming
> > and my module would fit into that grander scheme?
>
> Yes,the idea is to create a Cabal-ready wide-scope type-level
> programming library, joining the operations implemented in the
> different type-level libraries which are around. The goal (or at least
> mine) is to provide a common reusable type-level library which saves
> constantly reinventing the wheel.

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.

The other library I use for type-level programming is HList. It has
type-level booleans already so you might what to take a look at it if
you're not already familiar with it. In fact, if you are serious about
creating the de facto(?) type-level programming library trying to get
Oleg involved would be very beneficial both in terms of innovation and
credibility.


> > Or did you have something else in mind with joining efforts? E.g. help
> > reviewing your code or writing new code?
> >
>
> This would certainly help too.

I'm sure it would. ;)  I didn't mean to imply that I have plenty of
spare time to invest in this but I'll certainly be paying attention
when you start releasing code.

Thanks,
Bjorn
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
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.

> The other library I use for type-level programming is HList. It has
> type-level booleans already so you might what to take a look at it if
> you're not already familiar with it.

Thanks I'll have a look at it.

>  In fact, if you are serious about
> creating the de facto(?) type-level programming library trying to get
> Oleg involved would be very beneficial both in terms of innovation and
> credibility.

Sure. I've actually been exchanging mail with Oleg. He has given me
some useful suggestions and contributed with some code. He didn't
mention to what point he wanted to get involved though, but I'm sure
he will try to help.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
Am Donnerstag, 7. Februar 2008 02:47 schrieb Alfonso Acosta:
> > The other library I use for type-level programming is HList. It has
> > type-level booleans already so you might what to take a look at it if
> > you're not already familiar with it.
>
> Thanks I'll have a look at it.

I have to admit that I don’t like the names HBool, HTrue and HFalse.  What do
they mean?  Heterogenous booleans?  Heterogenous truth?  Why it’s “Bool”
instead of “Boolean” and therefore not conforming to the Prelude convention?

Heterogenous lists are not directly about type level computation.  A HList
type is usually inhabited.  On the other hand, types which denote type level
naturals or type-level booleans are empty data types.  So type level booleans
should go into some type level programming library like the one Alfonso and I
want to create.  HList should then use these booleans.  This is at least my
opinion.

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Bugzilla from alfonso.acosta@gmail.com
Don't expect anything astonishing yet, but an initial version of the
library can be found at

http:/code.haskell.org/type-level

To make reviewing easier I have put the haddock-generated documentation at

http://code.haskell.org/~fons/type-level/doc/

Some remarks:

* Only Positive and Natural numerals in decimal representation are
supported. It would be cool to add support for Integers though.

* The code is based on Oleg's implimentation of type-level binaries
http://okmij.org/ftp/Computation/resource-aware-prog/BinaryNumber.hs

* exponentiation/log and GCD is not implemented yet

* multiplication is not relational and thus division is broken. I
tried porting Oleg's multiplication algorithm without success.

* Aliases (in binary, octal decimal and hexadecimal form) for
type-level values and their value-level reflection functions are
generated with TH.
  That implies:
    * Long compilation time depending on your system
    * Although errors will always be reported in decimal form, the end
user can input values using other bases (only for values in the range
of generated aliases of course)

* It would be cool to have "real" support for other bases apart from decimals
  * It would imply having unlimited size of input for other bases
(right now if we want to input a value out of the alises limit,
decimal reprentation is mandatory)
  * However, is it feasible? How could it be done without needing to
implement the operations for each base? WOuld it be possible to
"overload" the type-level operators so that they worked with different
representations and mixed representation arguments?

* Booleans are not implemented (Wolfgang?)

I would be happy to hear any suggestions, get code reviews and/or contributions.

Cheers,

Fons








On Feb 7, 2008 11:17 AM, Wolfgang Jeltsch <[hidden email]> wrote:

> Am Donnerstag, 7. Februar 2008 02:47 schrieb Alfonso Acosta:
> > > The other library I use for type-level programming is HList. It has
> > > type-level booleans already so you might what to take a look at it if
> > > you're not already familiar with it.
> >
> > Thanks I'll have a look at it.
>
> I have to admit that I don't like the names HBool, HTrue and HFalse.  What do
> they mean?  Heterogenous booleans?  Heterogenous truth?  Why it's "Bool"
> instead of "Boolean" and therefore not conforming to the Prelude convention?
>
> Heterogenous lists are not directly about type level computation.  A HList
> type is usually inhabited.  On the other hand, types which denote type level
> naturals or type-level booleans are empty data types.  So type level booleans
> should go into some type level programming library like the one Alfonso and I
> want to create.  HList should then use these booleans.  This is at least my
> opinion.
>
> Best wishes,
> Wolfgang
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Wolfgang Jeltsch-2
Am Donnerstag, 7. Februar 2008 15:56 schrieben Sie:
> Don't expect anything astonishing yet, but an initial version of the
> library can be found at
>
> http:/code.haskell.org/type-level
>
> To make reviewing easier I have put the haddock-generated documentation at
>
> http://code.haskell.org/~fons/type-level/doc/

Thanks for your effort.  From a quick look at the Haddock documentation, some
questions/remarks arised.

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.

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).

:+ is already used as the constructor for complex numbers.  We should probably
use some different operator.

Again, thanks for your work.

> […]

Best wishes,
Wolfgang
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12345