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

[Wolfgang Jeltsch]

Am Samstag, 9. Februar 2008 23:33 schrieben Sie:
> 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.

My arguments were not so much about implementation, I think.  I’d see a 
type-level number as a list of digits, and a list has the form

    x1 : (x2 : (… : (xn : [])…))

or

    ((…([] `Snoc` x1) `Snoc` …) `Snoc` x(n-1)) `Snoc` xn.

From this point of view, it’s reasonable to have the extra () :*.

On the other hand, it might be sensible to give the user the illusion that :* 
is part of a special syntax while it’s actually an operator.  I’m not really 
sure what the better approach is.

Best wishes,
Wolfgang