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

[Alfonso Acosta]

On Feb 8, 2008 4:10 PM, Wolfgang Jeltsch <g9ks157k at acme.softbase.org> 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.