[Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)

[Alfonso Acosta]

On Feb 1, 2008 10:32 PM, Wolfgang Jeltsch <g9ks157k at acme.softbase.org> wrote:
> Am Freitag, 1. Februar 2008 13:00 schrieb Alfonso Acosta:
> > On Jan 31, 2008 11:35 PM, Wolfgang Jeltsch <g9ks157k at acme.softbase.org>
> > > 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.