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

Am Samstag, 9. Februar 2008 23:33 schrieben Sie:

On Feb 8, 2008 4:10 PM, Wolfgang Jeltsch 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